{-# 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 Symantic.Syntaxes.Classes (Syntax)
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'
type TermAST prov = BinTree (TokenTerm prov)

-- * Type 'TokenTerm'
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