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 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 = Parser
  { unParser ::
      ( -- MT.State (TokenTerm a)
        Either ErrMsg (TermVT syn)
      )
  }
type ErrMsg = String
-- * Type 'BinTree'

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

type TermAST = BinTree TokenTerm
data TokenTerm
  = TokenTermAtom String
  | TokenTermAbst String (TyVT ()) TermAST
  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)
-}