1 {-# LANGUAGE RankNTypes #-}
2 {-# OPTIONS_GHC -Wno-partial-fields #-}
4 module Symantic.Parser where
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)
13 import Text.Read (Read (..), reads)
14 import Text.Show (Show (..))
16 import Symantic.Compiler
17 import Symantic.Semantics (PerSyntax)
21 data Parser syns prov = Parser
23 ( -- MT.State (TokenTerm prov a)
26 Either (PerSyntax syns (ErrorParser prov)) (TermVT syns prov vs)
31 -- * Data family 'ErrorParser'
32 data family ErrorParser prov (syn :: Syntax)
34 ---- * Type 'SomeParsingError'
35 -- data SomeParsingError
38 -- -- Derivable (SomeParsingError syn sem),
41 -- SomeParsingError (SomeParsingError syn)
43 ----type instance Derived (SomeParsingError sem) = sem
44 ----instance Derivable (SomeParsingError sem) where
45 ---- derive (SomeParsingError x) = derive x
47 ---- ** Type 'SomeParsingError'
49 ---- TODO: neither data families nor data instances
50 ---- can have phantom roles with GHC-9's RoleAnnotations,
51 ---- hence 'SomeParsingError.Coerce.coerce' cannot be used on them for now.
52 ---- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
53 ---- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
54 -- data family SomeParsingError (syn :: Syntax) :: Semantic -> Semantic
55 ----type instance Derived (SomeParsingError syn sem) = sem
57 ---- | Convenient utility to pattern-match a 'SomeParsingError'.
58 ----pattern SomeParsingError :: Typeable syn => SomeParsingError syn sem a -> SomeParsingError sem a
59 ----pattern SomeParsingError x <- (unSomeParsingError -> Maybe.Just x)
61 ---- | @(unSomeParsingError sd :: 'Maybe' ('SomeParsingError' syn sem a))@
62 ---- extract the data-constructor from the given 'SomeParsingError' @(sd)@
63 ---- iif. it belongs to the @('SomeParsingError' syn sem a)@ data-instance.
64 -- unSomeParsingError ::
67 -- SomeParsingError sem a ->
68 -- Maybe (SomeParsingError syn sem a)
69 -- unSomeParsingError (SomeParsingError (constr :: SomeParsingError actualSyn sem a)) =
70 -- case typeRep @syn `eqTypeRep` typeRep @actualSyn of
71 -- Maybe.Just HRefl -> Maybe.Just constr
72 -- Maybe.Nothing -> Maybe.Nothing
74 data TermVT syns prov vs = forall a vs'.
76 { termVTType :: Ty prov vs' a
77 , unTermVT :: OpenTerm syns vs a
85 | BinTree2 (BinTree a) (BinTree a)
89 type TermAST prov = BinTree (TokenTerm prov)
93 = TokenTermAbst String (TyT prov '[]) (TermAST prov)
95 | TokenTermAtom String
98 safeRead :: Read a => String -> Either ErrMsg a
99 safeRead s = case reads s of
101 _ -> Left $ "Read error: " <> s
104 instance ( forall sem. syns sem => Functor sem
105 ) => Functor (Parser syns) where
106 fmap f (Parser esa) = Parser $
109 Right (Sem sem) -> Right (Sem (f <$> sem))
110 a <$ Parser esa = Parser $
113 Right (Sem sem) -> Right (Sem (a <$ sem))
114 instance ( forall sem. syns sem => Applicative sem
115 , Applicative (Sem syns)
116 , forall err. syns (Either err)
117 , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
118 ) => Applicative (Parser syns) where
119 pure a = Parser (Right (Sem (pure a)))
120 liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
121 (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
122 (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
123 (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
124 instance ( forall sem. syns sem => Monad sem
125 , forall err. syns (Either err)
126 , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
127 ) => Monad (Parser syns) where
128 (>>=) (Parser efsa) f = Parser (efsa >>= \(Sem sa) -> sa >>= unParser . f)
133 -- | /Typing context/
134 -- accumulating at each /lambda abstraction/
135 -- the 'Type' of the introduced variable.
136 -- It is built top-down from the closest
137 -- including /lambda abstraction/ to the farest.
138 -- It determines the 'Type's of 'CtxTe'.
139 data CtxTy prov (as :: [Type]) void where
140 CtxTyZ :: CtxTy prov '[] Void
141 CtxTyS :: NameTe -> Ty prov '[] a -> CtxTy prov as Void -> CtxTy prov (a ': as) Void
145 instance LenVar CtxTy where
147 lenVar (CtxTyS _n _ty x) = LenS (lenVar x)