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
20 data Parser syns meta = Parser
22 ( -- MT.State (TokenTerm meta a)
25 Either (PerSyntax syns (ErrorParser meta)) (TermVT syns meta vs)
30 -- * Data family 'ErrorParser'
31 data family ErrorParser meta (syn :: Syntax)
33 ---- * Type 'SomeParsingError'
34 -- data SomeParsingError
37 -- -- Derivable (SomeParsingError syn sem),
40 -- SomeParsingError (SomeParsingError syn)
42 ----type instance Derived (SomeParsingError sem) = sem
43 ----instance Derivable (SomeParsingError sem) where
44 ---- derive (SomeParsingError x) = derive x
46 ---- ** Type 'SomeParsingError'
48 ---- TODO: neither data families nor data instances
49 ---- can have phantom roles with GHC-9's RoleAnnotations,
50 ---- hence 'SomeParsingError.Coerce.coerce' cannot be used on them for now.
51 ---- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
52 ---- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
53 -- data family SomeParsingError (syn :: Syntax) :: Semantic -> Semantic
54 ----type instance Derived (SomeParsingError syn sem) = sem
56 ---- | Convenient utility to pattern-match a 'SomeParsingError'.
57 ----pattern SomeParsingError :: Typeable syn => SomeParsingError syn sem a -> SomeParsingError sem a
58 ----pattern SomeParsingError x <- (unSomeParsingError -> Maybe.Just x)
60 ---- | @(unSomeParsingError sd :: 'Maybe' ('SomeParsingError' syn sem a))@
61 ---- extract the data-constructor from the given 'SomeParsingError' @(sd)@
62 ---- iif. it belongs to the @('SomeParsingError' syn sem a)@ data-instance.
63 -- unSomeParsingError ::
66 -- SomeParsingError sem a ->
67 -- Maybe (SomeParsingError syn sem a)
68 -- unSomeParsingError (SomeParsingError (constr :: SomeParsingError actualSyn sem a)) =
69 -- case typeRep @syn `eqTypeRep` typeRep @actualSyn of
70 -- Maybe.Just HRefl -> Maybe.Just constr
71 -- Maybe.Nothing -> Maybe.Nothing
73 data TermVT syns meta vs = forall a vs'.
75 { termVTType :: Ty meta vs' a
76 , unTermVT :: OpenTerm syns vs a
84 | BinTree2 (BinTree a) (BinTree a)
87 type TermAST meta = BinTree (TokenTerm meta)
89 = TokenTermAbst String (TyT meta '[]) (TermAST meta)
91 | TokenTermAtom String
94 safeRead :: Read a => String -> Either ErrMsg a
95 safeRead s = case reads s of
97 _ -> Left $ "Read error: " <> s
100 instance ( forall sem. syns sem => Functor sem
101 ) => Functor (Parser syns) where
102 fmap f (Parser esa) = Parser $
105 Right (Sem sem) -> Right (Sem (f <$> sem))
106 a <$ Parser esa = Parser $
109 Right (Sem sem) -> Right (Sem (a <$ sem))
110 instance ( forall sem. syns sem => Applicative sem
111 , Applicative (Sem syns)
112 , forall err. syns (Either err)
113 , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
114 ) => Applicative (Parser syns) where
115 pure a = Parser (Right (Sem (pure a)))
116 liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
117 (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
118 (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
119 (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
120 instance ( forall sem. syns sem => Monad sem
121 , forall err. syns (Either err)
122 , syns (Parser syns) -- FIXME: what constraint is still missing to still require that?
123 ) => Monad (Parser syns) where
124 (>>=) (Parser efsa) f = Parser (efsa >>= \(Sem sa) -> sa >>= unParser . f)
129 -- | /Typing context/
130 -- accumulating at each /lambda abstraction/
131 -- the 'Type' of the introduced variable.
132 -- It is built top-down from the closest
133 -- including /lambda abstraction/ to the farest.
134 -- It determines the 'Type's of 'CtxTe'.
135 data CtxTy meta (as :: [Type]) void where
136 CtxTyZ :: CtxTy meta '[] Void
137 CtxTyS :: NameTe -> Ty meta '[] a -> CtxTy meta as Void -> CtxTy meta (a ': as) Void
141 instance LenVar CtxTy where
143 lenVar (CtxTyS _n _ty x) = LenS (lenVar x)