src/Symantic/Parser.hs

   1 {-# LANGUAGE RankNTypes #-}
   2 {-# OPTIONS_GHC -Wno-partial-fields #-}
   3
   4 module Symantic.Parser where
   5
   6 import Data.Either (Either (..))
   7 import Data.Eq (Eq (..))
   8 import Data.Function (($))
   9 import Data.Semigroup (Semigroup (..))
  10 import Data.String (String)
  11 import Data.Void (Void)
  12 import GHC.Types
  13 import Symantic.Syntaxes.Classes (Syntax)
  14 import Text.Read (Read (..), reads)
  15 import Text.Show (Show (..))
  16
  17 import Symantic.Compiler
  18 import Symantic.Semantics (PerSyntax)
  19 import Symantic.Typer
  20
  21 -- * Type 'Parser'
  22 data Parser syns prov = Parser
  23   { unParser ::
  24       ( -- MT.State (TokenTerm prov a)
  25         forall vs.
  26         CtxTy prov vs Void ->
  27         Either (PerSyntax syns (ErrorParser prov)) (TermVT syns prov vs)
  28       )
  29   }
  30 type ErrMsg = String
  31
  32 -- * Data family 'ErrorParser'
  33 data family ErrorParser prov (syn :: Syntax)
  34
  35 ---- * Type 'SomeParsingError'
  36 -- data SomeParsingError
  37 --  = forall syn.
  38 --    (
  39 --    -- Derivable (SomeParsingError syn sem),
  40 --    Typeable syn
  41 --    ) =>
  42 --    SomeParsingError (SomeParsingError syn)
  43 --
  44 ----type instance Derived (SomeParsingError sem) = sem
  45 ----instance Derivable (SomeParsingError sem) where
  46 ----  derive (SomeParsingError x) = derive x
  47 --
  48 ---- ** Type 'SomeParsingError'
  49 --
  50 ---- TODO: neither data families nor data instances
  51 ---- can have phantom roles with GHC-9's RoleAnnotations,
  52 ---- hence 'SomeParsingError.Coerce.coerce' cannot be used on them for now.
  53 ---- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
  54 ---- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
  55 -- data family SomeParsingError (syn :: Syntax) :: Semantic -> Semantic
  56 ----type instance Derived (SomeParsingError syn sem) = sem
  57 --
  58 ---- | Convenient utility to pattern-match a 'SomeParsingError'.
  59 ----pattern SomeParsingError :: Typeable syn => SomeParsingError syn sem a -> SomeParsingError sem a
  60 ----pattern SomeParsingError x <- (unSomeParsingError -> Maybe.Just x)
  61 --
  62 ---- | @(unSomeParsingError sd :: 'Maybe' ('SomeParsingError' syn sem a))@
  63 ---- extract the data-constructor from the given 'SomeParsingError' @(sd)@
  64 ---- iif. it belongs to the @('SomeParsingError' syn sem a)@ data-instance.
  65 -- unSomeParsingError ::
  66 --  forall syn sem a.
  67 --  Typeable syn =>
  68 --  SomeParsingError sem a ->
  69 --  Maybe (SomeParsingError syn sem a)
  70 -- unSomeParsingError (SomeParsingError (constr :: SomeParsingError actualSyn sem a)) =
  71 --  case typeRep @syn `eqTypeRep` typeRep @actualSyn of
  72 --    Maybe.Just HRefl -> Maybe.Just constr
  73 --    Maybe.Nothing -> Maybe.Nothing
  74
  75 data TermVT syns prov vs = forall a vs'.
  76   TermVT
  77   { termVTType :: Ty prov vs' a
  78   , unTermVT :: OpenTerm syns vs a
  79   }
  80
  81 -- * Type 'BinTree'
  82
  83 -- | /Binary Tree/.
  84 data BinTree a
  85   = BinTree0 a
  86   | BinTree2 (BinTree a) (BinTree a)
  87   deriving (Eq, Show)
  88
  89 -- * Type 'TermAST'
  90 type TermAST prov = BinTree (TokenTerm prov)
  91
  92 -- * Type 'TokenTerm'
  93 data TokenTerm prov
  94   = TokenTermAbst String (TyT prov '[]) (TermAST prov)
  95   | TokenTermVar Name
  96   | TokenTermAtom String
  97   deriving (Show)
  98
  99 safeRead :: Read a => String -> Either ErrMsg a
 100 safeRead s = case reads s of
 101   [(x, "")] -> Right x
 102   _ -> Left $ "Read error: " <> s
 103
 104 {-
 105 instance ( forall sem. syns sem => Functor sem
 106          ) => Functor (Parser syns) where
 107   fmap f (Parser esa) = Parser $
 108     case esa of
 109       Left e -> Left e
 110       Right (Sem sem) -> Right (Sem (f <$> sem))
 111   a <$ Parser esa = Parser $
 112     case esa of
 113       Left e -> Left e
 114       Right (Sem sem) -> Right (Sem (a <$ sem))
 115 instance ( forall sem. syns sem => Applicative sem
 116          , Applicative (Sem syns)
 117          , forall err. syns (Either err)
 118          , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
 119          ) => Applicative (Parser syns) where
 120   pure a = Parser (Right (Sem (pure a)))
 121   liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
 122   (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
 123   (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
 124   (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
 125 instance ( forall sem. syns sem => Monad sem
 126          , forall err. syns (Either err)
 127          , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
 128          ) => Monad (Parser syns) where
 129   (>>=) (Parser efsa) f = Parser (efsa >>= \(Sem sa) -> sa >>= unParser . f)
 130 -}
 131
 132 -- * Type 'CtxTy'
 133
 134 -- | /Typing context/
 135 -- accumulating at each /lambda abstraction/
 136 -- the 'Type' of the introduced variable.
 137 -- It is built top-down from the closest
 138 -- including /lambda abstraction/ to the farest.
 139 -- It determines the 'Type's of 'CtxTe'.
 140 data CtxTy prov (as :: [Type]) void where
 141   CtxTyZ :: CtxTy prov '[] Void
 142   CtxTyS :: NameTe -> Ty prov '[] a -> CtxTy prov as Void -> CtxTy prov (a ': as) Void
 143
 144 infixr 5 `CtxTyS`
 145
 146 instance LenVar CtxTy where
 147   lenVar CtxTyZ = LenZ
 148   lenVar (CtxTyS _n _ty x) = LenS (lenVar x)
 149
 150 type NameTe = String