]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Term.hs
Move libraries in Lib.
[haskell/symantic.git] / 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 is
65 = forall (h::Kind.Type). ETerm
66 (Type (Consts_of_Ifaces is) h)
67 (Term is h)
68
69 -- * Type 'Compile'
70 -- | Convenient type synonym wrapping 'CompileR' to initiate its recursion.
71 class Compile is where
72 compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
73 instance CompileR is '[] is => Compile is where
74 compileO (EToken tok) = compileR tok
75
76 -- | Like 'compileO' minus for a term with an empty /lambda context/.
77 compile
78 :: Compile is
79 => EToken meta is
80 -> Either (Error_Term meta is) (ETerm 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 is ls rs
88 = LamCtx_Type is Term_Name 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 (Consts_of_Ifaces is) (h::Kind.Type)
94 -> TermO ctx h is ls rs
95 -> Either (Error_Term meta is) ret )
96 -- ^ The accumulating continuation called bottom-up.
97 -> Either (Error_Term meta 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 (is::[*]) (ls::[*]) (rs::[*]) where
107 compileR :: TokenR meta is rs i -> CompileT meta ctx ret 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 is i
114 , CompileR is (i ': ls) (r ': rs)
115 ) => CompileR 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 is i =>
125 CompileR 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 (is::[*]) (i:: *) where
132 compileI :: TokenT meta is i -> CompileT meta ctx ret 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 'Consts_of_Ifaces'
143 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
144
145 -- ** Type family 'Consts_of_IfaceR'
146 type family Consts_of_IfaceR (is::[*]) where
147 Consts_of_IfaceR '[] = '[]
148 Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
149
150 -- ** Type family 'Consts_of_Iface'
151 type family Consts_of_Iface (i:: *) :: [*]
152 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
153
154 -- * Type 'LamCtx_Type'
155 -- | GADT for a typing context,
156 -- accumulating an @item@ at each lambda;
157 -- used to accumulate object-types (in 'Expr_From')
158 -- or host-terms (in 'HostI')
159 -- associated with the 'LamVar's in scope.
160 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
161 LamCtx_TypeZ :: LamCtx_Type is name '[]
162 LamCtx_TypeS :: name
163 -> Type (Consts_of_Ifaces is) (h::Kind.Type)
164 -> LamCtx_Type is name hs
165 -> LamCtx_Type is name (h ': hs)
166 infixr 5 `LamCtx_TypeS`
167
168 -- * Type 'LamCtx_Term'
169 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
170 LamCtx_TermZ :: LamCtx_Term term '[]
171 LamCtx_TermS :: term h
172 -> LamCtx_Term term hs
173 -> LamCtx_Term term (h ': hs)
174 infixr 5 `LamCtx_TermS`
175
176 -- * Type 'Error_Term'
177 data Error_Term meta (is::[*])
178 = Error_Term_unbound Term_Name
179 | Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
180 | Error_Term_Constraint_Type
181 (Either
182 (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
183 (Constraint_Type meta is (Consts_of_Ifaces is)))
184 | Error_Term_Constraint_Kind (Constraint_Kind meta is)
185 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
186 deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)
187
188 -- * Type 'Constraint_Type'
189 data Constraint_Type meta ts cs
190 = Constraint_Type_Eq (Either (At meta '[Proxy Token_Type] (EType cs))
191 (At meta ts (EType cs)))
192 (At meta ts (EType cs))
193 | Constraint_Type_App (At meta ts (EType cs))
194 | Constraint_Type_Con (At meta ts (KType cs Constraint))
195 | Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
196 deriving instance
197 ( Eq meta
198 , Eq_Token meta ts
199 ) => Eq (Constraint_Type meta ts cs)
200 deriving instance
201 ( Show meta
202 , Show_Token meta ts
203 , Show_Const cs
204 ) => Show (Constraint_Type meta ts cs)
205
206 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
207 olift = Error_Term_Typing . olift
208 instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
209 olift = Prelude.id
210 instance
211 cs ~ Consts_of_Ifaces is =>
212 MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
213 olift = Error_Term_Constraint_Type . Right
214 instance
215 cs ~ Consts_of_Ifaces is =>
216 MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
217 olift = Error_Term_Constraint_Type . Left
218 instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
219 olift = Error_Term_Typing . Error_Type_Constraint_Kind
220 instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
221 olift = Error_Term_Constraint_Kind
222
223 -- ** Checks
224 check_type
225 :: MonoLift (Constraint_Type meta ts cs) err
226 => At meta ts (Type cs x)
227 -> At meta ts (Type cs y)
228 -> ((x :~: y) -> Either err ret) -> Either err ret
229 check_type x y k =
230 case unAt x `eq_type` unAt y of
231 Just Refl -> k Refl
232 Nothing -> Left $ olift $
233 Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)
234
235 check_type_is
236 :: MonoLift (Constraint_Type meta ts cs) err
237 => At meta '[Proxy Token_Type] (Type cs x)
238 -> At meta ts (Type cs y)
239 -> ((x :~: y) -> Either err ret) -> Either err ret
240 check_type_is x y k =
241 case unAt x `eq_type` unAt y of
242 Just Refl -> k Refl
243 Nothing -> Left $ olift $
244 Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)
245
246 check_type_app
247 :: MonoLift (Constraint_Type meta ts cs) err
248 => At meta ts (Type cs (fa::kfa))
249 -> (forall ka f a. (fa :~: f a)
250 -> Type cs (f::ka -> kfa)
251 -> Type cs (a::ka)
252 -> Either err ret)
253 -> Either err ret
254 check_type_app typ k =
255 case unAt typ of
256 a :$ b -> k Refl a b
257 _ -> Left $ olift $
258 Constraint_Type_App (EType <$> typ)
259
260 check_type1
261 :: ( MonoLift (Constraint_Type meta ts cs) err
262 , MonoLift (Constraint_Kind meta ts) err )
263 => Type cs (f:: * -> *)
264 -> At meta ts (Type cs fa)
265 -> (forall a. (fa :~: f a)
266 -> Type cs a
267 -> Either err ret)
268 -> Either err ret
269 check_type1 typ ty_fa k =
270 check_type_app ty_fa $ \Refl ty_f ty_a ->
271 check_kind
272 (At Nothing $ SKiType `SKiArrow` SKiType)
273 (kind_of ty_f <$ ty_fa) $ \Refl ->
274 check_type
275 (At Nothing typ)
276 (ty_f <$ ty_fa) $ \Refl ->
277 k Refl ty_a
278
279 check_type2
280 :: ( MonoLift (Constraint_Type meta ts cs) err
281 , MonoLift (Constraint_Kind meta ts) err )
282 => Type cs (f:: * -> * -> *)
283 -> At meta ts (Type cs fab)
284 -> (forall a b. (fab :~: f a b)
285 -> Type cs a
286 -> Type cs b
287 -> Either err ret)
288 -> Either err ret
289 check_type2 typ ty_fab k =
290 check_type_app ty_fab $ \Refl ty_fa ty_b ->
291 check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f ty_a ->
292 check_kind
293 (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
294 (kind_of ty_f <$ ty_fab) $ \Refl ->
295 check_type
296 (At Nothing typ)
297 (ty_f <$ ty_fab) $ \Refl ->
298 k Refl ty_a ty_b
299
300 check_con
301 :: ( Proj_Con cs
302 , MonoLift (Constraint_Type meta ts cs) err )
303 => At meta ts (Type cs (q::Constraint))
304 -> (Con q -> Either err ret)
305 -> Either err ret
306 check_con typ k =
307 case proj_con $ unAt typ of
308 Just Con -> k Con
309 Nothing -> Left $ olift $
310 Constraint_Type_Con (KType <$> typ)
311
312 check_con1
313 :: ( Proj_Con cs
314 , MonoLift (Constraint_Type meta ts cs) err
315 , MonoLift (Constraint_Kind meta ts) err )
316 => Type cs con
317 -> At meta ts (Type cs (fa:: *))
318 -> (forall f a. (fa :~: f a)
319 -> Con (con f)
320 -> Type cs (f:: * -> *)
321 -> Type cs (a:: *)
322 -> Either err ret)
323 -> Either err ret
324 check_con1 con ty_fa k =
325 check_type_app ty_fa $ \Refl ty_f ty_a ->
326 check_kind
327 (At Nothing (SKiType `SKiArrow` SKiType))
328 (kind_of ty_f <$ ty_fa) $ \Refl ->
329 check_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
330 k Refl Con ty_f ty_a
331
332 check_fam
333 :: ( MonoLift (Constraint_Type meta ts cs) err
334 , Proj_Fam cs fam
335 , Show fam )
336 => At meta ts fam
337 -> Types cs hs
338 -> (Type cs (Fam fam hs) -> Either err ret)
339 -> Either err ret
340 check_fam fam tys k =
341 case proj_fam (unAt fam) tys of
342 Just t -> k t
343 Nothing -> Left $ olift $
344 Constraint_Type_Fam
345 (Text.pack . show <$> fam)
346 (etypes tys)