{-# LANGUAGE RankNTypes #-}

module Symantic.Parser where

import Control.Applicative (Applicative (..))
import Control.Monad (Monad (..))
import Control.Monad.Trans.Except qualified as MT
import Control.Monad.Trans.Reader qualified as MT
import Control.Monad.Trans.State qualified as MT
import Data.Bool (otherwise)
import Data.Either (Either (..))
import Data.Eq (Eq (..))
import Data.Function (id, ($), (.))
import Data.Functor (Functor (..), (<$>))
import Data.Functor.Constant (Constant (..))
import Data.Int (Int)
import Data.Kind (Constraint, Type)
import Data.Maybe (Maybe (..), isJust)
import Data.Proxy (Proxy (..))
import Data.Semigroup (Semigroup (..))
import Data.String (String)
import Data.Void (Void)
import GHC.Types
import Text.Read (Read (..), reads)
import Text.Show (Show (..))
import Unsafe.Coerce (unsafeCoerce)
import Prelude (error)
import Prelude qualified

import Symantic.Compiler
import Symantic.Typer

-- * Type 'Parser'
data Parser syn meta = Parser
  { unParser ::
      ( -- MT.State (TokenTerm meta a)
        forall vs.
        CtxTy meta vs Void ->
        Either ErrMsg (TermVT syn meta vs)
      )
  }
type ErrMsg = String

data TermVT syn meta vs = forall a vs'.
  TermVT
  { termVTType :: Ty meta vs' a
  , unTermVT :: OTerm syn vs a
  }

-- * Type 'BinTree'

-- | /Binary Tree/.
data BinTree a
  = BinTree0 a
  | BinTree2 (BinTree a) (BinTree a)
  deriving (Eq, Show)

type TermAST meta = BinTree (TokenTerm meta)
data TokenTerm meta
  = TokenTermAtom String
  | TokenTermVar Name
  | TokenTermAbst String (TyT meta '[]) (TermAST meta)
  deriving (Show)

safeRead :: Read a => String -> Either ErrMsg a
safeRead s = case reads s of
  [(x, "")] -> Right x
  _ -> Left $ "Read error: " <> s

{-
instance ( forall sem. syn sem => Functor sem
         ) => Functor (Parser syn) where
  fmap f (Parser esa) = Parser $
    case esa of
      Left e -> Left e
      Right (ForallSem sem) -> Right (ForallSem (f <$> sem))
  a <$ Parser esa = Parser $
    case esa of
      Left e -> Left e
      Right (ForallSem sem) -> Right (ForallSem (a <$ sem))
instance ( forall sem. syn sem => Applicative sem
         , Applicative (ForallSem syn)
         , forall err. syn (Either err)
         , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
         ) => Applicative (Parser syn) where
  pure a = Parser (Right (ForallSem (pure a)))
  liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
  (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
  (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
  (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
instance ( forall sem. syn sem => Monad sem
         , forall err. syn (Either err)
         , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
         ) => Monad (Parser syn) where
  (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSem sa) -> sa >>= unParser . f)
-}

-- * Type 'CtxTy'

-- | /Typing context/
-- accumulating at each /lambda abstraction/
-- the 'Type' of the introduced variable.
-- It is built top-down from the closest
-- including /lambda abstraction/ to the farest.
-- It determines the 'Type's of 'CtxTe'.
data CtxTy meta (as :: [Type]) void where
  CtxTyZ :: CtxTy meta '[] Void
  CtxTyS :: NameTe -> Ty meta '[] a -> CtxTy meta as Void -> CtxTy meta (a ': as) Void

infixr 5 `CtxTyS`

instance LenVar CtxTy where
  lenVar CtxTyZ = LenZ
  lenVar (CtxTyS _n _ty x) = LenS (lenVar x)

type NameTe = String