{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wno-partial-fields #-}

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.Semantics (PerSyntax)
import Symantic.Typer

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

-- * Data family 'ErrorParser'
data family ErrorParser prov (syn :: Syntax)

---- * Type 'SomeParsingError'
-- data SomeParsingError
--  = forall syn.
--    (
--    -- Derivable (SomeParsingError syn sem),
--    Typeable syn
--    ) =>
--    SomeParsingError (SomeParsingError syn)
--
----type instance Derived (SomeParsingError sem) = sem
----instance Derivable (SomeParsingError sem) where
----  derive (SomeParsingError x) = derive x
--
---- ** Type 'SomeParsingError'
--
---- TODO: neither data families nor data instances
---- can have phantom roles with GHC-9's RoleAnnotations,
---- hence 'SomeParsingError.Coerce.coerce' cannot be used on them for now.
---- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
---- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
-- data family SomeParsingError (syn :: Syntax) :: Semantic -> Semantic
----type instance Derived (SomeParsingError syn sem) = sem
--
---- | Convenient utility to pattern-match a 'SomeParsingError'.
----pattern SomeParsingError :: Typeable syn => SomeParsingError syn sem a -> SomeParsingError sem a
----pattern SomeParsingError x <- (unSomeParsingError -> Maybe.Just x)
--
---- | @(unSomeParsingError sd :: 'Maybe' ('SomeParsingError' syn sem a))@
---- extract the data-constructor from the given 'SomeParsingError' @(sd)@
---- iif. it belongs to the @('SomeParsingError' syn sem a)@ data-instance.
-- unSomeParsingError ::
--  forall syn sem a.
--  Typeable syn =>
--  SomeParsingError sem a ->
--  Maybe (SomeParsingError syn sem a)
-- unSomeParsingError (SomeParsingError (constr :: SomeParsingError actualSyn sem a)) =
--  case typeRep @syn `eqTypeRep` typeRep @actualSyn of
--    Maybe.Just HRefl -> Maybe.Just constr
--    Maybe.Nothing -> Maybe.Nothing

data TermVT syns prov vs = forall a vs'.
  TermVT
  { termVTType :: Ty prov 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 prov = BinTree (TokenTerm prov)
data TokenTerm prov
  = TokenTermAbst String (TyT prov '[]) (TermAST prov)
  | 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 (Sem sem) -> Right (Sem (f <$> sem))
  a <$ Parser esa = Parser $
    case esa of
      Left e -> Left e
      Right (Sem sem) -> Right (Sem (a <$ sem))
instance ( forall sem. syns sem => Applicative sem
         , Applicative (Sem 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 (Sem (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 >>= \(Sem 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 prov (as :: [Type]) void where
  CtxTyZ :: CtxTy prov '[] Void
  CtxTyS :: NameTe -> Ty prov '[] a -> CtxTy prov as Void -> CtxTy prov (a ': as) Void

infixr 5 `CtxTyS`

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

type NameTe = String