{-# LANGUAGE RankNTypes #-}

module Symantic.Parser where

import Data.Either (Either (..))
import Data.Eq (Eq (..))
import Data.Function (($))
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 Symantic.Compiler
import Symantic.Typer

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

data TermVT syns meta vs = forall a vs'.
  TermVT
  { termVTType :: Ty meta vs' a
  , unTermVT :: OpenTerm syns 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
  = TokenTermAbst String (TyT meta '[]) (TermAST meta)
  | TokenTermVar Name
  | TokenTermAtom String
  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. syns sem => Functor sem
         ) => Functor (Parser syns) where
  fmap f (Parser esa) = Parser $
    case esa of
      Left e -> Left e
      Right (ForallSemantic sem) -> Right (ForallSemantic (f <$> sem))
  a <$ Parser esa = Parser $
    case esa of
      Left e -> Left e
      Right (ForallSemantic sem) -> Right (ForallSemantic (a <$ sem))
instance ( forall sem. syns sem => Applicative sem
         , Applicative (ForallSemantic syns)
         , forall err. syns (Either err)
         , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
         ) => Applicative (Parser syns) where
  pure a = Parser (Right (ForallSemantic (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. syns sem => Monad sem
         , forall err. syns (Either err)
         , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
         ) => Monad (Parser syns) where
  (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSemantic 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