]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/Common.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / Common.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE GADTs #-}
6 {-# LANGUAGE KindSignatures #-}
7 {-# LANGUAGE MultiParamTypeClasses #-}
8 {-# LANGUAGE Rank2Types #-}
9 {-# LANGUAGE ScopedTypeVariables #-}
10 {-# LANGUAGE TypeFamilies #-}
11 {-# LANGUAGE TypeOperators #-}
12 {-# LANGUAGE UndecidableInstances #-}
13 module Language.LOL.Symantic.Expr.Common where
14
15 import Data.Peano
16 import Data.Proxy (Proxy(..))
17 import Data.Text (Text)
18 import Data.Type.Equality ((:~:)(Refl))
19 import GHC.Prim (Constraint)
20
21 import Language.LOL.Symantic.AST
22 import Language.LOL.Symantic.Type
23
24 -- * Class 'Expr_from'
25
26 class Expr_from ast (ex:: *) where
27 expr_from
28 :: forall hs ret
29 . Proxy ex
30 -- ^ Select the 'Expr_from' instance for the expression @ex@.
31 -> Context (Var (Type_Root_of_Expr ex)) hs
32 -- ^ The bound variables in scope and their types:
33 -- held in the heterogeneous list @hs@,
34 -- from the closest including lambda abstraction to the farest.
35 -> ast
36 -- ^ The input data to parse.
37 -> ( forall h
38 . Type_Root_of_Expr ex h
39 -> Forall_Repr_with_Context ex hs h
40 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
41 -- ^ The accumulating continuation.
42 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
43
44 -- ** Type 'Context'
45
46 -- | GADT for a typing context,
47 -- accumulating an @item@ at each lambda;
48 -- used to accumulate object-types of lambda variables in 'Expr_from'
49 -- or host-terms of lambda variables in 'Repr_Host'.
50 data Context :: (* -> *) -> [*] -> * where
51 Context_Empty :: Context item '[]
52 Context_Next :: item h -> Context item hs -> Context item (h ': hs)
53 infixr 5 `Context_Next`
54
55 -- ** Type 'Var'
56 -- | Join a name and a type.
57 --
58 -- This data type is used to handle lambda variables by name
59 -- (instead of DeBruijn indices for instance).
60 data Var ty h
61 = Var Var_Name (ty h)
62 type Var_Name = Text
63
64 -- ** Type 'Forall_Repr_with_Context'
65 -- | A data type embedding a universal quantification
66 -- over an interpreter @repr@
67 -- and qualified by the symantics of an expression.
68 --
69 -- Moreover the expression is abstracted by a 'Context'
70 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
71 -- for lambda abstractions.
72 --
73 -- This data type is used to keep a parsed expression polymorphic enough
74 -- to stay interpretable by different interpreters.
75 --
76 -- NOTE: 'Sym_of_Expr'@ ex repr@
77 -- is needed to be able to use symantic methods of the parsed expression
78 -- into a 'Forall_Repr_with_Context' @ex@.
79 --
80 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
81 -- is needed to be able to use an expression
82 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
83 -- into a 'Forall_Repr_with_Context'@ ex@,
84 -- which happens when a symantic method includes a polymorphic type
85 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
86 data Forall_Repr_with_Context ex hs h
87 = Forall_Repr_with_Context
88 ( forall repr. ( Sym_of_Expr ex repr
89 , Sym_of_Expr (Root_of_Expr ex) repr
90 ) => Context repr hs -> repr h )
91
92 -- ** Type 'Forall_Repr'
93 data Forall_Repr ex h
94 = Forall_Repr
95 { unForall_Repr :: forall repr
96 . Sym_of_Expr ex repr
97 => repr h }
98
99 -- ** Type family 'Root_of_Expr'
100 -- | The root expression of an expression.
101 type family Root_of_Expr (ex:: *) :: *
102
103 -- ** Type family 'Sym_of_Expr'
104 -- | The symantic of an expression.
105 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
106
107 -- ** Type family 'Error_of_Expr'
108 -- | The error(s) of an expression.
109 type family Error_of_Expr (ast:: *) (ex:: *) :: *
110
111 -- ** Type family 'Type_of_Expr'
112 -- | The type of an expression, parameterized by a root type.
113 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
114
115 -- ** Type 'Type_Root_of_Expr'
116 -- | Convenient alias.
117 type Type_Root_of_Expr ex
118 = Type_Root (Type_of_Expr (Root_of_Expr ex))
119
120 -- * Type 'Expr_Root'
121 -- | The root expression, passing itself as parameter to the given expression.
122 newtype Expr_Root (ex:: * -> *)
123 = Expr_Root (ex (Expr_Root ex))
124 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
125 type instance Type_of_Expr (Expr_Root ex)
126 = Type_of_Expr (ex (Expr_Root ex))
127 type instance Error_of_Expr ast (Expr_Root ex)
128 = Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
129 (Type_Root_of_Expr (ex (Expr_Root ex)))
130 ast)
131 (Error_of_Expr ast (ex (Expr_Root ex)))
132 type instance Sym_of_Expr (Expr_Root ex) repr
133 = Sym_of_Expr (ex (Expr_Root ex)) repr
134 instance -- Expr_from
135 ( Expr_from ast (ex (Expr_Root ex))
136 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
137 ) => Expr_from ast (Expr_Root ex) where
138 expr_from _px_ex ctx ast k =
139 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
140 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
141 k ty (Forall_Repr_with_Context repr)
142
143 {- NOTE: useless code so far.
144 -- ** Class 'Expr_Root_Lift'
145 -- | Lift a given expression to a given root expression.
146 class Expr_Root_Lift ex root where
147 expr_root_lift :: ex root -> root
148 instance
149 Expr_Lift ex root =>
150 Expr_Root_Lift ex (Expr_Root root) where
151 expr_root_lift = Expr_Root . expr_lift
152 -}
153
154 -- * Type 'Expr_Alt'
155 -- | Expression making an alternative between two expressions.
156 data Expr_Alt curr next (root:: *)
157 = Expr_Alt_Curr (curr root)
158 | Expr_Alt_Next (next root)
159 type instance Root_of_Expr (Expr_Alt curr next root) = root
160 type instance Type_of_Expr (Expr_Alt curr next root)
161 = Type_Alt (Type_of_Expr (curr root))
162 (Type_of_Expr (next root))
163 type instance Error_of_Expr ast (Expr_Alt curr next root)
164 = Error_Expr_Alt (Error_of_Expr ast (curr root))
165 (Error_of_Expr ast (next root))
166 type instance Sym_of_Expr (Expr_Alt curr next root) repr
167 = ( Sym_of_Expr (curr root) repr
168 , Sym_of_Expr (next root) repr
169 )
170 instance -- Expr_from
171 ( Expr_from ast (curr root)
172 , Expr_from ast (next root)
173 , Root_of_Expr (curr root) ~ root
174 , Root_of_Expr (next root) ~ root
175 , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
176 (Type_Root_of_Expr root) ast)
177 (Error_of_Expr ast root)
178 ) => Expr_from ast (Expr_Alt curr next root) where
179 expr_from _px_ex ctx ast k =
180 case expr_from (Proxy::Proxy (curr root)) ctx ast $
181 \ty (Forall_Repr_with_Context repr) ->
182 Right $ k ty (Forall_Repr_with_Context repr) of
183 Right ret -> ret
184 Left err ->
185 case error_expr_unlift err of
186 Just (Error_Expr_Unsupported_here _
187 :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
188 (Type_Root_of_Expr root) ast) ->
189 expr_from (Proxy::Proxy (next root)) ctx ast $
190 \ty (Forall_Repr_with_Context repr) ->
191 k ty (Forall_Repr_with_Context repr)
192 _ -> Left err
193
194 {- NOTE: useless code so far.
195 -- ** Type 'Expr_Lift'
196 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
197 type Expr_Lift ex exs
198 = Expr_LiftN (Peano_of_Expr ex exs) ex exs
199
200 -- | Convenient wrapper around 'expr_liftN',
201 -- passing it the 'Peano' number from 'Peano_of_Expr'.
202 expr_lift
203 :: forall ex exs (root:: *).
204 Expr_Lift ex exs =>
205 ex root -> exs root
206 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
207
208 -- *** Type family 'Peano_of_Expr'
209 -- | Return a 'Peano' number derived from the location
210 -- of a given expression within a given expression stack,
211 -- which is used to avoid @OverlappingInstances@.
212 type family Peano_of_Expr
213 (ex:: * -> *)
214 (exs:: * -> *) :: Peano where
215 Peano_of_Expr ex ex = 'Zero
216 Peano_of_Expr ex (Expr_Alt ex next) = 'Zero
217 Peano_of_Expr other (Expr_Alt curr next) = 'Succ (Peano_of_Expr other next)
218
219 -- *** Class 'Expr_LiftN'
220 -- | Lift a given expression to the top of a given expression stack including it,
221 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
222 class Expr_LiftN (n::Peano) ex exs where
223 expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
224 instance Expr_LiftN 'Zero curr curr where
225 expr_liftN _ = id
226 instance Expr_LiftN 'Zero curr (Expr_Alt curr next) where
227 expr_liftN _ = Expr_Alt_Curr
228 instance
229 Expr_LiftN n other next =>
230 Expr_LiftN ('Succ n) other (Expr_Alt curr next) where
231 expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy n)
232 -}
233
234 {- NOTE: useless code so far.
235 -- ** Type 'Expr_Unlift'
236 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
237 type Expr_Unlift ex exs
238 = Expr_UnliftN (Peano_of_Expr ex exs) ex exs
239
240 -- | Convenient wrapper around 'expr_unliftN',
241 -- passing it the 'Peano' number from 'Peano_of_Expr'.
242 expr_unlift
243 :: forall ex exs (root:: *).
244 Expr_Unlift ex exs =>
245 exs root -> Maybe (ex root)
246 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
247
248 -- *** Class 'Expr_UnliftN'
249 -- | Try to unlift a given expression out of a given expression stack including it,
250 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
251 class Expr_UnliftN (n::Peano) ex exs where
252 expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
253 instance Expr_UnliftN 'Zero curr curr where
254 expr_unliftN _ = Just
255 instance Expr_UnliftN 'Zero curr (Expr_Alt curr next) where
256 expr_unliftN _ (Expr_Alt_Curr x) = Just x
257 expr_unliftN _ (Expr_Alt_Next _) = Nothing
258 instance
259 Expr_UnliftN n other next =>
260 Expr_UnliftN ('Succ n) other (Expr_Alt curr next) where
261 expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy n) x
262 expr_unliftN _ (Expr_Alt_Curr _) = Nothing
263 -}
264
265 -- ** Type family 'Is_Last_Expr'
266 -- | Return whether a given expression is the last one in a given expression stack.
267 --
268 -- NOTE: each expression parser uses this type family
269 -- when it encounters unsupported syntax:
270 -- to know if it is the last expression parser component that will be tried
271 -- (and thus return 'Error_Expr_Unsupported')
272 -- or if some other expression parser component shall be tried
273 -- (and thus return 'Error_Expr_Unsupported_here',
274 -- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
275 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
276 Is_Last_Expr ex ex = 'True
277 Is_Last_Expr ex (Expr_Root exs) = Is_Last_Expr ex (exs (Expr_Root exs))
278 Is_Last_Expr (ex root) (Expr_Alt ex next root) = 'False
279 Is_Last_Expr other (Expr_Alt curr next root) = Is_Last_Expr other (next root)
280
281 -- * Type 'Error_Expr_Alt'
282 -- | Error expression making an alternative between two error expressions.
283 data Error_Expr_Alt curr next
284 = Error_Expr_Alt_Curr curr
285 | Error_Expr_Alt_Next next
286 deriving (Eq, Show)
287
288 -- ** Type 'Error_Expr_Lift'
289 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
290 type Error_Expr_Lift err errs
291 = Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
292
293 -- | Convenient wrapper around 'error_expr_liftN',
294 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
295 error_expr_lift
296 :: forall err errs.
297 Error_Expr_Lift err errs => err -> errs
298 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
299
300 -- *** Type family 'Peano_of_Error_Expr'
301 -- | Return a 'Peano' number derived from the location
302 -- of a given error expression within a given error expression stack,
303 -- which is used to avoid @OverlappingInstances@.
304 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
305 Peano_of_Error_Expr err err = 'Zero
306 Peano_of_Error_Expr err (Error_Expr_Alt err next) = 'Zero
307 Peano_of_Error_Expr other (Error_Expr_Alt curr next) = 'Succ (Peano_of_Error_Expr other next)
308
309 -- *** Class 'Error_Expr_LiftN'
310 -- | Lift a given expression to the top of a given expression stack including it,
311 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
312 class Error_Expr_LiftN (n::Peano) err errs where
313 error_expr_liftN :: Proxy n -> err -> errs
314 instance Error_Expr_LiftN 'Zero curr curr where
315 error_expr_liftN _ = id
316 instance Error_Expr_LiftN 'Zero curr (Error_Expr_Alt curr next) where
317 error_expr_liftN _ = Error_Expr_Alt_Curr
318 instance
319 Error_Expr_LiftN n other next =>
320 Error_Expr_LiftN ('Succ n) other (Error_Expr_Alt curr next) where
321 error_expr_liftN _ = Error_Expr_Alt_Next . error_expr_liftN (Proxy::Proxy n)
322
323 -- ** Type 'Error_Expr_Unlift'
324 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
325 type Error_Expr_Unlift ex exs
326 = Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
327
328 -- | Convenient wrapper around 'error_expr_unliftN',
329 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
330 error_expr_unlift
331 :: forall ex exs.
332 Error_Expr_Unlift ex exs => exs -> Maybe ex
333 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
334
335 -- *** Class 'Error_Expr_UnliftN'
336 -- | Try to unlift a given expression error out of a given expression error stack including it,
337 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
338 class Error_Expr_UnliftN (n::Peano) ex exs where
339 error_expr_unliftN :: Proxy n -> exs -> Maybe ex
340 instance Error_Expr_UnliftN 'Zero curr curr where
341 error_expr_unliftN _ = Just
342 instance Error_Expr_UnliftN 'Zero curr (Error_Expr_Alt curr next) where
343 error_expr_unliftN _ (Error_Expr_Alt_Curr x) = Just x
344 error_expr_unliftN _ (Error_Expr_Alt_Next _) = Nothing
345 instance
346 Error_Expr_UnliftN n other next =>
347 Error_Expr_UnliftN ('Succ n) other (Error_Expr_Alt curr next) where
348 error_expr_unliftN _ (Error_Expr_Alt_Next x) = error_expr_unliftN (Proxy::Proxy n) x
349 error_expr_unliftN _ (Error_Expr_Alt_Curr _) = Nothing
350
351 -- ** Type 'Error_Expr_Read'
352 -- | Common expression errors.
353 data Error_Expr err_ty ty ast
354 = Error_Expr_Wrong_number_of_arguments Int ast
355 -- ^ Wrong number of arguments applied to a term,
356 -- the integer is the number of arguments expected.
357 | Error_Expr_Type_mismatch (Exists_Type ty) (Exists_Type ty) ast
358 -- ^ Mismatch between respectively expected and actual type when applying a function.
359 | Error_Expr_Read Error_Read ast
360 -- ^ Error when reading a literal.
361 | Error_Expr_Type err_ty ast
362 -- ^ Error when parsing a type.
363 | Error_Expr_Unsupported ast
364 -- ^ Given syntax is supported by none
365 -- of the expression parser components
366 -- of the expression stack.
367 | Error_Expr_Unsupported_here ast
368 -- ^ Given syntax not supported by the current expression parser component.
369 deriving (Eq, Show)
370
371 -- | Convenient wrapper around 'error_expr_lift',
372 -- passing the type family boilerplate.
373 error_expr
374 :: Error_Expr_Lift
375 (Error_Expr (Error_of_Type ast (Type_Root_of_Expr ex)) (Type_Root_of_Expr ex) ast)
376 (Error_of_Expr ast (Root_of_Expr ex))
377 => Proxy ex
378 -> Error_Expr (Error_of_Type ast (Type_Root_of_Expr ex)) (Type_Root_of_Expr ex) ast
379 -> Error_of_Expr ast (Root_of_Expr ex)
380 error_expr _ = error_expr_lift
381
382 -- | Utility to check that two types are equal
383 -- or raise 'Error_Expr_Type_mismatch'.
384 when_type_eq
385 :: forall ast ex root ty x y ret.
386 ( root ~ Root_of_Expr ex
387 , ty ~ Type_Root (Type_of_Expr root)
388 , Type_Eq ty
389 , Error_Expr_Lift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr ex))
390 ( Type_Root_of_Expr ex)
391 ast)
392 (Error_of_Expr ast root)
393 )
394 => Proxy ex -> ast -> ty x -> ty y
395 -> (forall. x :~: y -> Either (Error_of_Expr ast root) ret)
396 -> Either (Error_of_Expr ast root) ret
397 when_type_eq px_ex ast x y k =
398 case x `type_eq` y of
399 Nothing -> Left $ error_expr px_ex $
400 Error_Expr_Type_mismatch
401 (Exists_Type x)
402 (Exists_Type y) ast
403 Just Refl -> k Refl