]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Compiling/Term.hs
Rename Term_Name -> TeName
[haskell/symantic.git] / symantic / Language / Symantic / Compiling / Term.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 {-# OPTIONS_GHC -fno-warn-orphans #-}
6 module Language.Symantic.Compiling.Term
7 ( module Language.Symantic.Compiling.Term
8 , module Language.Symantic.Compiling.Term.Grammar
9 ) where
10
11 import qualified Data.Kind as Kind
12 import Data.Proxy (Proxy(..))
13 import qualified Data.Text as Text
14 import Data.Type.Equality ((:~:)(..))
15 import GHC.Exts (Constraint)
16
17 import Language.Symantic.Helper.Data.Type.List
18 import Language.Symantic.Parsing
19 import Language.Symantic.Typing
20
21 import Language.Symantic.Compiling.Term.Grammar
22
23 -- * Type 'Term'
24 -- | Closed 'TermO'.
25 data Term is h
26 = Term
27 (forall term. ( Sym_of_Ifaces is term
28 , Sym_of_Iface (Proxy (->)) term
29 ) => term h)
30
31 -- ** Type 'TermO'
32 -- | An open term (i.e. with a /lambda context/).
33 -- The data type wraps a universal quantification
34 -- over an interpreter @term@
35 -- qualified by the symantics of a term.
36 --
37 -- Moreover the term is abstracted by a 'LamCtx_Term'
38 -- built top-down by 'compileO',
39 -- to enable a /Higher-Order Abstract Syntax/ (HOAS)
40 -- for /lambda abstractions/ ('lam').
41 --
42 -- This data type is used to keep a parsed term polymorphic enough
43 -- to stay interpretable by different interpreters.
44 --
45 -- * @(@'Sym_of_Ifaces'@ is term)@
46 -- is needed when a symantic method includes a polymorphic type
47 -- and thus calls: 'compileO'.
48 --
49 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
50 -- make a zipper needed to be able to write the recursing 'CompileR' instance.
51 --
52 -- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
53 -- is needed to handle partially applied functions.
54 data TermO ctx h is ls rs
55 = TermO
56 (forall term. ( Sym_of_Ifaces is term
57 , Sym_of_Ifaces ls term
58 , Sym_of_Ifaces rs term
59 , Sym_of_Iface (Proxy (->)) term
60 ) => LamCtx_Term term ctx -> term h)
61
62 -- * Type 'ETerm'
63 -- | Existential 'Term', with its 'Type'.
64 data ETerm cs is
65 = forall (h::Kind.Type). ETerm
66 (Type cs h)
67 (Term is h)
68
69 -- * Type 'Compile'
70 -- | Convenient class wrapping 'CompileR' to initiate its recursion.
71 class CompileR cs is '[] is => Compile cs is where
72 compileO :: EToken meta is -> CompileT meta ctx ret cs is '[] is
73 instance CompileR cs is '[] is => Compile cs is where
74 compileO (EToken tok) = compileR tok
75
76 -- | Like 'compileO' but for a term with an empty /lambda context/.
77 compile
78 :: Compile cs is
79 => EToken meta is
80 -> Either (Error_Term meta cs is) (ETerm cs is)
81 compile tok =
82 compileO tok LamCtx_TypeZ $ \typ (TermO te) ->
83 Right $ ETerm typ $ Term $ te LamCtx_TermZ
84
85 -- ** Type 'CompileT'
86 -- | Convenient type synonym defining a term parser.
87 type CompileT meta ctx ret cs is ls rs
88 = LamCtx_Type cs is TeName ctx
89 -- ^ The bound variables in scope and their types:
90 -- built top-down in the heterogeneous list @ctx@,
91 -- from the closest including /lambda abstraction/ to the farest.
92 -> ( forall h.
93 Type cs (h::Kind.Type)
94 -> TermO ctx h is ls rs
95 -> Either (Error_Term meta cs is) ret )
96 -- ^ The accumulating continuation called bottom-up.
97 -> Either (Error_Term meta cs is) ret
98
99 -- ** Class 'CompileR'
100 -- | Intermediate type class to construct an instance of 'Compile'
101 -- from many instances of 'CompileI', one for each item of @is@.
102 --
103 -- * @is@: starting list of /term constants/.
104 -- * @ls@: done list of /term constants/.
105 -- * @rs@: remaining list of /term constants/.
106 class CompileR (cs::[*]) (is::[*]) (ls::[*]) (rs::[*]) where
107 compileR :: TokenR meta is rs i -> CompileT meta ctx ret cs is ls rs
108
109 -- | Recurse into into the given 'TokenR'
110 -- to call the 'compileI' instance associated
111 -- to the 'TokenT' it contains.
112 instance
113 ( CompileI cs is i
114 , CompileR cs is (i ': ls) (r ': rs)
115 ) => CompileR cs is ls (i ': r ': rs) where
116 compileR tok ctx k =
117 case tok of
118 TokenZ _m t -> compileI t ctx k
119 TokenS t ->
120 compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
121 k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
122 -- | End the recursion.
123 instance
124 CompileI cs is i =>
125 CompileR cs is ls (i ': '[]) where
126 compileR (TokenZ _m t) ctx k = compileI t ctx k
127 compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."
128
129 -- ** Class 'CompileI'
130 -- | Handle the work of 'Compile' for a given /interface/ @i@.
131 class CompileI (cs::[*]) (is::[*]) (i:: *) where
132 compileI :: TokenT meta is i -> CompileT meta ctx ret cs is ls (i ': rs)
133
134 -- * Type family 'Sym_of_Ifaces'
135 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
136 Sym_of_Ifaces '[] term = ()
137 Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
138
139 -- ** Type family 'Sym_of_Iface'
140 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
141
142 -- * Type 'TyConsts_of_Ifaces'
143 type TyConsts_of_Ifaces is = Nub (TyConsts_of_IfaceR is)
144
145 -- ** Type family 'TyConsts_of_IfaceR'
146 type family TyConsts_of_IfaceR (is::[*]) where
147 TyConsts_of_IfaceR '[] = '[]
148 TyConsts_of_IfaceR (i ': is) = TyConsts_of_Iface i ++ TyConsts_of_IfaceR is
149
150 -- ** Type family 'TyConsts_of_Iface'
151 type family TyConsts_of_Iface (i:: *) :: [*]
152
153 -- * Type 'LamCtx_Type'
154 -- | GADT for a typing context,
155 -- accumulating an @item@ at each lambda;
156 -- used to accumulate object-types (in 'Expr_From')
157 -- or host-terms (in 'HostI')
158 -- associated with the 'LamVar's in scope.
159 data LamCtx_Type (cs::[*]) (is::[*]) (name:: *) (ctx::[*]) where
160 LamCtx_TypeZ :: LamCtx_Type cs is name '[]
161 LamCtx_TypeS :: name
162 -> Type cs (h::Kind.Type)
163 -> LamCtx_Type cs is name hs
164 -> LamCtx_Type cs is name (h ': hs)
165 infixr 5 `LamCtx_TypeS`
166
167 -- * Type 'LamCtx_Term'
168 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
169 LamCtx_TermZ :: LamCtx_Term term '[]
170 LamCtx_TermS :: term h
171 -> LamCtx_Term term hs
172 -> LamCtx_Term term (h ': hs)
173 infixr 5 `LamCtx_TermS`
174
175 -- * Type 'Error_Term'
176 data Error_Term meta (cs::[*]) (is::[*])
177 = Error_Term_unbound TeName
178 | Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
179 | Error_Term_Con_Type
180 (Either
181 (Con_Type meta cs '[Proxy Token_Type])
182 (Con_Type meta cs is))
183 | Error_Term_Con_Kind (Con_Kind meta is)
184 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta cs is)
185 deriving instance (Show meta, Show_Token meta is, Show_TyConst cs) => Show (Error_Term meta cs is)
186
187 -- * Type 'Con_Type'
188 data Con_Type meta cs ts
189 = Con_TyEq (Either (At meta '[Proxy Token_Type] (EType cs))
190 (At meta ts (EType cs)))
191 (At meta ts (EType cs))
192 | Con_TyApp (At meta ts (EType cs))
193 | Con_TyCon (At meta ts (KType cs Constraint))
194 | Con_TyFam (At meta ts TyFamName) [EType cs]
195 deriving instance
196 ( Eq meta
197 , Eq_Token meta ts
198 ) => Eq (Con_Type meta cs ts)
199 deriving instance
200 ( Show meta
201 , Show_Token meta ts
202 , Show_TyConst cs
203 ) => Show (Con_Type meta cs ts)
204
205 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta cs ts) where
206 olift = Error_Term_Typing . olift
207 instance MonoLift (Error_Term meta cs ts) (Error_Term meta cs ts) where
208 olift = id
209 instance
210 MonoLift (Con_Type meta cs is) (Error_Term meta cs is) where
211 olift = Error_Term_Con_Type . Right
212 instance
213 MonoLift (Con_Type meta cs '[Proxy Token_Type]) (Error_Term meta cs is) where
214 olift = Error_Term_Con_Type . Left
215 instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta cs is) where
216 olift = Error_Term_Typing . Error_Type_Con_Kind
217 instance MonoLift (Con_Kind meta is) (Error_Term meta cs is) where
218 olift = Error_Term_Con_Kind
219
220 -- ** Checks
221 check_TyEq
222 :: MonoLift (Con_Type meta cs ts) err
223 => At meta ts (Type cs x)
224 -> At meta ts (Type cs y)
225 -> ((x :~: y) -> Either err ret) -> Either err ret
226 check_TyEq x y k =
227 case unAt x `eq_Type` unAt y of
228 Just Refl -> k Refl
229 Nothing -> Left $ olift $
230 Con_TyEq (Right $ EType <$> x) (EType <$> y)
231
232 check_Type_is
233 :: MonoLift (Con_Type meta cs ts) err
234 => At meta '[Proxy Token_Type] (Type cs x)
235 -> At meta ts (Type cs y)
236 -> ((x :~: y) -> Either err ret) -> Either err ret
237 check_Type_is x y k =
238 case unAt x `eq_Type` unAt y of
239 Just Refl -> k Refl
240 Nothing -> Left $ olift $
241 Con_TyEq (Left $ EType <$> x) (EType <$> y)
242
243 check_TyApp
244 :: MonoLift (Con_Type meta cs ts) err
245 => At meta ts (Type cs (fa::kfa))
246 -> (forall ka f a. (fa :~: f a)
247 -> Type cs (f::ka -> kfa)
248 -> Type cs (a::ka)
249 -> Either err ret)
250 -> Either err ret
251 check_TyApp typ k =
252 case unAt typ of
253 a :$ b -> k Refl a b
254 _ -> Left $ olift $
255 Con_TyApp (EType <$> typ)
256
257 check_TyEq1
258 :: ( MonoLift (Con_Type meta cs ts) err
259 , MonoLift (Con_Kind meta ts) err )
260 => Type cs (f:: * -> *)
261 -> At meta ts (Type cs fa)
262 -> (forall a. (fa :~: f a)
263 -> Type cs a
264 -> Either err ret)
265 -> Either err ret
266 check_TyEq1 typ ty_fa k =
267 check_TyApp ty_fa $ \Refl ty_f ty_a ->
268 check_Kind
269 (At Nothing $ SKiType `SKiArrow` SKiType)
270 (kind_of ty_f <$ ty_fa) $ \Refl ->
271 check_TyEq
272 (At Nothing typ)
273 (ty_f <$ ty_fa) $ \Refl ->
274 k Refl ty_a
275
276 check_TyEq2
277 :: ( MonoLift (Con_Type meta cs ts) err
278 , MonoLift (Con_Kind meta ts) err )
279 => Type cs (f:: * -> * -> *)
280 -> At meta ts (Type cs fab)
281 -> (forall a b. (fab :~: f a b)
282 -> Type cs a
283 -> Type cs b
284 -> Either err ret)
285 -> Either err ret
286 check_TyEq2 typ ty_fab k =
287 check_TyApp ty_fab $ \Refl ty_fa ty_b ->
288 check_TyApp (ty_fa <$ ty_fab) $ \Refl ty_f ty_a ->
289 check_Kind
290 (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
291 (kind_of ty_f <$ ty_fab) $ \Refl ->
292 check_TyEq
293 (At Nothing typ)
294 (ty_f <$ ty_fab) $ \Refl ->
295 k Refl ty_a ty_b
296
297 check_TyCon
298 :: ( Proj_TyCon cs
299 , MonoLift (Con_Type meta cs ts) err )
300 => At meta ts (Type cs (q::Constraint))
301 -> (TyCon q -> Either err ret)
302 -> Either err ret
303 check_TyCon typ k =
304 case proj_TyCon $ unAt typ of
305 Just TyCon -> k TyCon
306 Nothing -> Left $ olift $
307 Con_TyCon (KType <$> typ)
308
309 check_TyCon1
310 :: ( Proj_TyCon cs
311 , MonoLift (Con_Type meta cs ts) err
312 , MonoLift (Con_Kind meta ts) err )
313 => Type cs con
314 -> At meta ts (Type cs (fa:: *))
315 -> (forall f a. (fa :~: f a)
316 -> TyCon (con f)
317 -> Type cs (f:: * -> *)
318 -> Type cs (a:: *)
319 -> Either err ret)
320 -> Either err ret
321 check_TyCon1 con ty_fa k =
322 check_TyApp ty_fa $ \Refl ty_f ty_a ->
323 check_Kind
324 (At Nothing (SKiType `SKiArrow` SKiType))
325 (kind_of ty_f <$ ty_fa) $ \Refl ->
326 check_TyCon ((con :$ ty_f) <$ ty_fa) $ \TyCon ->
327 k Refl TyCon ty_f ty_a
328
329 check_TyFam
330 :: ( MonoLift (Con_Type meta cs ts) err
331 , Proj_TyFam cs fam
332 , Show fam )
333 => At meta ts fam
334 -> Types cs hs
335 -> (Type cs (TyFam fam hs) -> Either err ret)
336 -> Either err ret
337 check_TyFam fam tys k =
338 case proj_TyFam (unAt fam) tys of
339 Just t -> k t
340 Nothing -> Left $ olift $
341 Con_TyFam
342 (Text.pack . show <$> fam)
343 (eTypes tys)