]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Common.hs
init
[haskell/symantic.git] / Language / 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.Symantic.Expr.Common where
14
15 import Data.Proxy (Proxy(..))
16 import Data.Text (Text)
17 import qualified Data.Text as Text
18 import Data.Type.Equality ((:~:)(Refl))
19 import GHC.Prim (Constraint)
20
21 import Language.Symantic.Type
22
23 -- * Class 'Expr_from'
24
25 -- | Parse given @ast@ into
26 -- a 'Type_Root_of_Expr' and
27 -- a 'Forall_Repr_with_Context',
28 -- or return an 'Error_of_Expr'.
29 class Expr_from ast (ex:: *) where
30 expr_from :: Expr_From ast ex hs ret
31
32 -- | Like 'expr_from' but for a root expression.
33 root_expr_from
34 :: forall lam ast root.
35 ( Expr_from ast root
36 , Root_of_Expr root ~ root )
37 => Proxy root -> Proxy lam -> ast
38 -> Either (Error_of_Expr ast root)
39 (Exists_Type_and_Repr (Type_Root_of_Expr root)
40 (Forall_Repr root))
41 root_expr_from _ex _lam ast =
42 expr_from (Proxy::Proxy root) ast
43 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
44 Right $ Exists_Type_and_Repr ty $
45 Forall_Repr $ repr Context_Empty
46
47 -- ** Type 'Expr_From'
48 type Expr_From ast ex hs ret
49 = Proxy ex
50 -- ^ Select the 'Expr_from' instance.
51 -> ast
52 -- ^ The input data to parse.
53 -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
54 -- ^ The bound variables in scope and their types:
55 -- held in the heterogeneous list @hs@,
56 -- from the closest including lambda abstraction to the farest.
57 -> ( forall h
58 . Type_Root_of_Expr ex h
59 -> Forall_Repr_with_Context ex hs h
60 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
61 -- ^ The accumulating continuation.
62 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
63
64 -- | Parse a literal.
65 lit_from
66 :: forall ty lit ex ast hs ret.
67 ( ty ~ Type_Root_of_Expr ex
68 , Read lit
69 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
70 (Error_of_Expr ast (Root_of_Expr ex))
71 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
72 -> ty lit -> Lambda_Var_Name
73 -> Expr_From ast ex hs ret
74 lit_from lit ty_lit toread ex ast _ctx k =
75 case read_safe toread of
76 Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
77 Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
78
79 -- | Parse a unary operator.
80 op1_from
81 :: forall root ty lit ex ast hs ret.
82 ( ty ~ Type_Root_of_Expr ex
83 , root ~ Root_of_Expr ex
84 , Eq_Type (Type_Root_of_Expr root)
85 , Expr_from ast root
86 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
87 (Error_of_Expr ast root)
88 , Root_of_Expr root ~ root
89 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
90 -> ty lit -> ast
91 -> Expr_From ast ex hs ret
92 op1_from op ty_lit ast_x ex ast ctx k =
93 expr_from (Proxy::Proxy root) ast_x ctx $
94 \ty_x (Forall_Repr_with_Context x) ->
95 check_eq_type ex ast ty_lit ty_x $ \Refl ->
96 k ty_x $ Forall_Repr_with_Context (op . x)
97
98 -- | Parse a binary operator.
99 op2_from
100 :: forall root ty lit ex ast hs ret.
101 ( ty ~ Type_Root_of_Expr ex
102 , root ~ Root_of_Expr ex
103 , Eq_Type (Type_Root_of_Expr root)
104 , Expr_from ast root
105 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
106 (Error_of_Expr ast root)
107 , Root_of_Expr root ~ root
108 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
109 -> ty lit -> ast -> ast
110 -> Expr_From ast ex hs ret
111 op2_from op ty_lit ast_x ast_y ex ast ctx k =
112 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
113 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
114 check_eq_type ex ast ty_lit ty_x $ \Refl ->
115 check_eq_type ex ast ty_lit ty_y $ \Refl ->
116 k ty_x $ Forall_Repr_with_Context $
117 \c -> x c `op` y c
118
119 -- ** Type 'Context'
120
121 -- | GADT for a typing context,
122 -- accumulating an @item@ at each lambda;
123 -- used to accumulate object-types (in 'Expr_from')
124 -- or host-terms (in 'Repr_Host')
125 -- associated with the 'Lambda_Var's in scope.
126 data Context :: (* -> *) -> [*] -> * where
127 Context_Empty :: Context item '[]
128 Context_Next :: item h -> Context item hs -> Context item (h ': hs)
129 infixr 5 `Context_Next`
130
131 -- ** Type 'Lambda_Var'
132 -- | Join a name and a type.
133 --
134 -- This data type is used to handle lambda variables by name
135 -- (instead of DeBruijn indices for instance).
136 data Lambda_Var ty h
137 = Lambda_Var Lambda_Var_Name (ty h)
138 type Lambda_Var_Name = Text
139
140 -- ** Type 'Forall_Repr_with_Context'
141 -- | A data type embedding a universal quantification
142 -- over an interpreter @repr@
143 -- and qualified by the symantics of an expression.
144 --
145 -- Moreover the expression is abstracted by a 'Context'
146 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
147 -- for lambda abstractions.
148 --
149 -- This data type is used to keep a parsed expression polymorphic enough
150 -- to stay interpretable by different interpreters.
151 --
152 -- NOTE: 'Sym_of_Expr'@ ex repr@
153 -- is needed to be able to use symantic methods of the parsed expression
154 -- into a 'Forall_Repr_with_Context'@ ex@.
155 --
156 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
157 -- is needed to be able to use an expression
158 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
159 -- into a 'Forall_Repr_with_Context'@ ex@,
160 -- which happens when a symantic method includes a polymorphic type
161 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
162 data Forall_Repr_with_Context ex hs h
163 = Forall_Repr_with_Context
164 ( forall repr. ( Sym_of_Expr ex repr
165 , Sym_of_Expr (Root_of_Expr ex) repr
166 ) => Context repr hs -> repr h )
167
168 -- ** Type 'Forall_Repr'
169 data Forall_Repr ex h
170 = Forall_Repr
171 { unForall_Repr :: forall repr
172 . ( Sym_of_Expr ex repr
173 , Sym_of_Expr (Root_of_Expr ex) repr )
174 => repr h }
175
176 -- ** Type family 'Root_of_Expr'
177 -- | The root expression of an expression.
178 type family Root_of_Expr (ex:: *) :: *
179
180 -- ** Type family 'Sym_of_Expr'
181 -- | The symantic of an expression.
182 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
183
184 -- ** Type family 'Error_of_Expr'
185 -- | The error(s) of an expression.
186 type family Error_of_Expr (ast:: *) (ex:: *) :: *
187
188 -- ** Type family 'Type_of_Expr'
189 -- | The type of an expression, parameterized by a root type.
190 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
191
192 -- ** Type 'Type_Root_of_Expr'
193 -- | Convenient alias.
194 --
195 -- NOTE: include 'Type_Var' only to use it
196 -- within 'Error_Expr_Type_mismatch' so far.
197 type Type_Root_of_Expr (ex:: *)
198 = Type_Root (Type_Var :|: Type_of_Expr (Root_of_Expr ex))
199
200 -- * Type 'Expr_Root'
201 -- | The root expression, passing itself as parameter to the given expression.
202 newtype Expr_Root (ex:: * -> *)
203 = Expr_Root (ex (Expr_Root ex))
204 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
205 type instance Type_of_Expr (Expr_Root ex)
206 = Type_of_Expr (ex (Expr_Root ex))
207 type instance Error_of_Expr ast (Expr_Root ex)
208 = Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
209 (Type_Root_of_Expr (ex (Expr_Root ex)))
210 ast)
211 (Error_of_Expr ast (ex (Expr_Root ex)))
212 type instance Sym_of_Expr (Expr_Root ex) repr
213 = Sym_of_Expr (ex (Expr_Root ex)) repr
214 instance -- Expr_from
215 ( Expr_from ast (ex (Expr_Root ex))
216 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
217 ) => Expr_from ast (Expr_Root ex) where
218 expr_from _ex ctx ast k =
219 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
220 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
221 k ty (Forall_Repr_with_Context repr)
222
223 {- NOTE: useless code so far.
224 -- ** Class 'Expr_Root_Lift'
225 -- | Lift a given expression to a given root expression.
226 class Expr_Root_Lift ex root where
227 expr_root_lift :: ex root -> root
228 instance
229 Lift_Expr ex root =>
230 Expr_Root_Lift ex (Expr_Root root) where
231 expr_root_lift = Expr_Root . lift_expr
232 -}
233
234 -- * Type 'Expr_Alt'
235 -- | Expression making an alternative between two expressions.
236 data Expr_Alt curr next (root:: *)
237 = Expr_Alt_Curr (curr root)
238 | Expr_Alt_Next (next root)
239 -- | Convenient alias. Requires @TypeOperators@.
240 --
241 -- TODO: see if using a type-level list is better.
242 type (.|.) = Expr_Alt
243 infixr 5 .|.
244 type instance Root_of_Expr (Expr_Alt curr next root) = root
245 type instance Sym_of_Expr (Expr_Alt curr next root) repr
246 = ( Sym_of_Expr (curr root) repr
247 , Sym_of_Expr (next root) repr
248 )
249 type instance Type_of_Expr (Expr_Alt curr next root)
250 = Type_of_Expr_Alt (Type_of_Expr (curr root))
251 (Type_of_Expr (next root))
252 -- ** Type family 'Type_of_Expr_Alt'
253 -- | Remove 'No_Type' type when building 'Type_of_Expr'.
254 type family Type_of_Expr_Alt
255 (type_curr:: (* -> *) -> * -> *)
256 (type_next:: (* -> *) -> * -> *)
257 where
258 Type_of_Expr_Alt No_Type next = next
259 Type_of_Expr_Alt curr No_Type = curr
260 Type_of_Expr_Alt curr next = Type_Alt curr next
261
262 type instance Error_of_Expr ast (Expr_Alt curr next root)
263 = Error_of_Expr_Alt ast (Error_of_Expr ast (curr root))
264 (Error_of_Expr ast (next root))
265 -- ** Type family 'Error_of_Expr_Alt'
266 -- | Remove 'No_Error_Expr' type when building the error of an expression.
267 type family Error_of_Expr_Alt ast curr next where
268 Error_of_Expr_Alt ast No_Error_Expr next = next
269 Error_of_Expr_Alt ast curr No_Error_Expr = curr
270 Error_of_Expr_Alt ast curr next = Error_Expr_Alt curr next
271
272 -- ** Type 'No_Error_Expr'
273 -- | A discarded error.
274 data No_Error_Expr
275 = No_Error_Expr
276 deriving (Eq, Show)
277
278 instance -- Expr_from
279 ( Expr_from ast (curr root)
280 , Expr_from ast (next root)
281 , Root_of_Expr (curr root) ~ root
282 , Root_of_Expr (next root) ~ root
283 , Unlift_Error_Expr (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
284 (Type_Root_of_Expr root) ast)
285 (Error_of_Expr ast root)
286 ) => Expr_from ast (Expr_Alt curr next root) where
287 expr_from _ex ctx ast k =
288 case expr_from (Proxy::Proxy (curr root)) ctx ast $
289 \ty (Forall_Repr_with_Context repr) ->
290 Right $ k ty (Forall_Repr_with_Context repr) of
291 Right ret -> ret
292 Left err ->
293 case unlift_error_expr err of
294 Just (Error_Expr_Unsupported_here _
295 :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
296 (Type_Root_of_Expr root) ast) ->
297 expr_from (Proxy::Proxy (next root)) ctx ast $
298 \ty (Forall_Repr_with_Context repr) ->
299 k ty (Forall_Repr_with_Context repr)
300 _ -> Left err
301
302 {- NOTE: useless code so far.
303 -- ** Type 'Lift_Expr'
304 -- | Apply 'Peano_of_Expr' on 'Lift_ExprP'.
305 type Lift_Expr ex exs
306 = Lift_ExprP (Peano_of_Expr ex exs) ex exs
307
308 -- | Convenient wrapper around 'expr_liftN',
309 -- passing it the 'Peano' number from 'Peano_of_Expr'.
310 lift_expr
311 :: forall ex exs (root:: *).
312 Lift_Expr ex exs =>
313 ex root -> exs root
314 lift_expr = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
315
316 -- *** Type family 'Peano_of_Expr'
317 -- | Return a 'Peano' number derived from the location
318 -- of a given expression within a given expression stack,
319 -- which is used to avoid @OverlappingInstances@.
320 type family Peano_of_Expr
321 (ex:: * -> *)
322 (exs:: * -> *) :: * where
323 Peano_of_Expr ex ex = Zero
324 Peano_of_Expr ex (Expr_Alt ex next) = Zero
325 Peano_of_Expr other (Expr_Alt curr next) = Succ (Peano_of_Expr other next)
326
327 -- *** Class 'Lift_ExprP'
328 -- | Lift a given expression to the top of a given expression stack including it,
329 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
330 class Lift_ExprP (p:: *) ex exs where
331 expr_liftN :: forall (root:: *). Proxy p -> ex root -> exs root
332 instance Lift_ExprP Zero curr curr where
333 expr_liftN _ = id
334 instance Lift_ExprP Zero curr (Expr_Alt curr next) where
335 expr_liftN _ = Expr_Alt_Curr
336 instance
337 Lift_ExprP p other next =>
338 Lift_ExprP (Succ p) other (Expr_Alt curr next) where
339 expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy p)
340
341 -- ** Type 'Unlift_Expr'
342 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
343 type Unlift_Expr ex exs
344 = Expr_UnliftN (Peano_of_Expr ex exs) ex exs
345
346 -- | Convenient wrapper around 'expr_unliftN',
347 -- passing it the 'Peano' number from 'Peano_of_Expr'.
348 expr_unlift
349 :: forall ex exs (root:: *).
350 Unlift_Expr ex exs =>
351 exs root -> Maybe (ex root)
352 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
353
354 -- *** Class 'Expr_UnliftN'
355 -- | Try to unlift a given expression out of a given expression stack including it,
356 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
357 class Expr_UnliftN (p:: *) ex exs where
358 expr_unliftN :: forall (root:: *). Proxy p -> exs root -> Maybe (ex root)
359 instance Expr_UnliftN Zero curr curr where
360 expr_unliftN _ = Just
361 instance Expr_UnliftN Zero curr (Expr_Alt curr next) where
362 expr_unliftN _ (Expr_Alt_Curr x) = Just x
363 expr_unliftN _ (Expr_Alt_Next _) = Nothing
364 instance
365 Expr_UnliftN p other next =>
366 Expr_UnliftN (Succ p) other (Expr_Alt curr next) where
367 expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy p) x
368 expr_unliftN _ (Expr_Alt_Curr _) = Nothing
369 -}
370
371 -- ** Type family 'Is_Last_Expr'
372 -- | Return whether a given expression is the last one in a given expression stack.
373 --
374 -- NOTE: each expression parser uses this type family
375 -- when it encounters unsupported syntax:
376 -- to know if it is the last expression parser component that will be tried
377 -- (and thus return 'Error_Expr_Unsupported')
378 -- or if some other expression parser component shall be tried
379 -- (and thus return 'Error_Expr_Unsupported_here',
380 -- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
381 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
382 Is_Last_Expr ex ex = 'True
383 Is_Last_Expr ex (Expr_Root exs) = Is_Last_Expr ex (exs (Expr_Root exs))
384 Is_Last_Expr (ex root) (Expr_Alt ex next root) = 'False
385 Is_Last_Expr other (Expr_Alt curr next root) = Is_Last_Expr other (next root)
386
387 -- * Type 'Error_Expr_Alt'
388 -- | Error expression making an alternative between two error expressions.
389 data Error_Expr_Alt curr next
390 = Error_Expr_Alt_Curr curr
391 | Error_Expr_Alt_Next next
392 deriving (Eq, Show)
393
394 -- ** Type 'Lift_Error_Expr'
395 -- | Apply 'Peano_of_Error_Expr' on 'Lift_Error_ExprP'.
396 type Lift_Error_Expr err errs
397 = Lift_Error_ExprP (Peano_of_Error_Expr err errs) err errs
398
399 -- | Convenient wrapper around 'lift_error_exprP',
400 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
401 lift_error_expr
402 :: forall err errs.
403 Lift_Error_Expr err errs => err -> errs
404 lift_error_expr = lift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr err errs))
405
406 -- *** Type family 'Peano_of_Error_Expr'
407 -- | Return a 'Peano' number derived from the location
408 -- of a given error expression within a given error expression stack,
409 -- which is used to avoid @OverlappingInstances@.
410 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
411 Peano_of_Error_Expr err err = Zero
412 Peano_of_Error_Expr err (Error_Expr_Alt err next) = Zero
413 Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)
414
415 -- *** Class 'Lift_Error_ExprP'
416 -- | Lift a given expression to the top of a given expression stack including it,
417 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
418 class Lift_Error_ExprP (p:: *) err errs where
419 lift_error_exprP :: Proxy p -> err -> errs
420 instance Lift_Error_ExprP Zero curr curr where
421 lift_error_exprP _ = id
422 instance Lift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
423 lift_error_exprP _ = Error_Expr_Alt_Curr
424 instance
425 Lift_Error_ExprP p other next =>
426 Lift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
427 lift_error_exprP _ = Error_Expr_Alt_Next . lift_error_exprP (Proxy::Proxy p)
428
429 -- ** Type 'Unlift_Error_Expr'
430 -- | Apply 'Peano_of_Error_Expr' on 'Unlift_Error_ExprP'.
431 type Unlift_Error_Expr ex exs
432 = Unlift_Error_ExprP (Peano_of_Error_Expr ex exs) ex exs
433
434 -- | Convenient wrapper around 'unlift_error_exprP',
435 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
436 unlift_error_expr
437 :: forall ex exs.
438 Unlift_Error_Expr ex exs => exs -> Maybe ex
439 unlift_error_expr = unlift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr ex exs))
440
441 -- *** Class 'Unlift_Error_ExprP'
442 -- | Try to unlift a given expression error out of a given expression error stack including it,
443 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
444 class Unlift_Error_ExprP (p:: *) ex exs where
445 unlift_error_exprP :: Proxy p -> exs -> Maybe ex
446 instance Unlift_Error_ExprP Zero curr curr where
447 unlift_error_exprP _ = Just
448 instance Unlift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
449 unlift_error_exprP _ (Error_Expr_Alt_Curr x) = Just x
450 unlift_error_exprP _ (Error_Expr_Alt_Next _) = Nothing
451 instance
452 Unlift_Error_ExprP p other next =>
453 Unlift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
454 unlift_error_exprP _ (Error_Expr_Alt_Next x) = unlift_error_exprP (Proxy::Proxy p) x
455 unlift_error_exprP _ (Error_Expr_Alt_Curr _) = Nothing
456
457 -- * Type 'Error_Expr_Read'
458 -- | Common expression errors.
459 data Error_Expr err_ty ty ast
460 = Error_Expr_Wrong_number_of_arguments ast Int
461 -- ^ Wrong number of arguments applied to a term,
462 -- the integer is the number of arguments expected.
463 | Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
464 -- ^ Mismatch between respectively expected and actual type.
465 | Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type ty)
466 -- ^ A 'Constraint' is missing.
467 | Error_Expr_Read Error_Read ast
468 -- ^ Error when reading a literal.
469 | Error_Expr_Type err_ty ast
470 -- ^ Error when parsing a type.
471 | Error_Expr_Unsupported ast
472 -- ^ Given syntax is supported by none
473 -- of the expression parser components
474 -- of the expression stack.
475 | Error_Expr_Unsupported_here ast
476 -- ^ Given syntax not supported by
477 -- the current expression parser component.
478 deriving (Eq, Show)
479
480 -- | Convenient type alias.
481 type Error_Expr_of_Root ast root
482 = Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
483 (Type_Root_of_Expr root)
484 ast
485
486 -- | Convenient wrapper around 'lift_error_expr',
487 -- passing the type family boilerplate.
488 error_expr
489 :: forall ast ex ty.
490 (ty ~ Type_Root_of_Expr ex)
491 => Lift_Error_Expr
492 (Error_Expr (Error_of_Type ast ty) ty ast)
493 (Error_of_Expr ast (Root_of_Expr ex))
494 => Proxy ex
495 -> Error_Expr (Error_of_Type ast ty) ty ast
496 -> Error_of_Expr ast (Root_of_Expr ex)
497 error_expr _ = lift_error_expr
498
499 -- | Parsing utility to return 'Error_Expr_Unsupported'
500 -- or 'Error_Expr_Unsupported_here'
501 -- according to the given expression.
502 error_expr_unsupported
503 :: forall ast ex ty root.
504 ( root ~ Root_of_Expr ex
505 , ty ~ Type_Root_of_Expr ex
506 , Implicit_HBool (Is_Last_Expr ex root)
507 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
508 (Error_of_Expr ast root)
509 ) => Proxy ex -> ast
510 -> Error_of_Expr ast (Root_of_Expr ex)
511 error_expr_unsupported ex ast =
512 case hbool :: HBool (Is_Last_Expr ex root) of
513 HTrue -> error_expr ex $ Error_Expr_Unsupported ast
514 HFalse -> error_expr ex $ Error_Expr_Unsupported_here ast
515
516 -- | Parsing utility to check that two types are equal,
517 -- or raise 'Error_Expr_Type_mismatch'.
518 check_eq_type
519 :: forall ast ex root ty x y ret.
520 ( root ~ Root_of_Expr ex
521 , ty ~ Type_Root_of_Expr ex
522 , Eq_Type ty
523 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
524 (Error_of_Expr ast root)
525 )
526 => Proxy ex -> ast -> ty x -> ty y
527 -> (x :~: y -> Either (Error_of_Expr ast root) ret)
528 -> Either (Error_of_Expr ast root) ret
529 check_eq_type ex ast x y k =
530 case x `eq_type` y of
531 Just Refl -> k Refl
532 Nothing -> Left $ error_expr ex $
533 Error_Expr_Type_mismatch ast
534 (Exists_Type x)
535 (Exists_Type y)
536 check_eq_type1
537 :: forall ast ex root ty h1 h2 a1 a2 ret.
538 ( root ~ Root_of_Expr ex
539 , ty ~ Type_Root_of_Expr ex
540 , Eq_Type1 ty
541 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
542 (Error_of_Expr ast root)
543 )
544 => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
545 -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
546 -> Either (Error_of_Expr ast root) ret
547 check_eq_type1 ex ast h1 h2 k =
548 case h1 `eq_type1` h2 of
549 Just Refl -> k Refl
550 Nothing -> Left $ error_expr ex $
551 Error_Expr_Type_mismatch ast
552 (Exists_Type h1)
553 (Exists_Type h2)
554
555 -- | Parsing utility to check that a type is has instance of a given 'Constraint',
556 -- or raise 'Error_Expr_Constraint_missing'.
557 check_constraint_type
558 :: forall ast ex c root ty h ret.
559 ( root ~ Root_of_Expr ex
560 , ty ~ Type_Root_of_Expr ex
561 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
562 (Error_of_Expr ast root)
563 , Constraint_Type c ty
564 )
565 => Proxy ex -> Proxy c -> ast -> ty h
566 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
567 -> Either (Error_of_Expr ast root) ret
568 check_constraint_type ex c ast ty k =
569 case constraint_type c ty of
570 Just Dict -> k Dict
571 Nothing -> Left $ error_expr ex $
572 Error_Expr_Constraint_missing ast
573 {-(Exists_Dict c)-}
574 -- FIXME: not easy to report the constraint
575 -- and still support 'Eq' and 'Show' deriving.
576 (Exists_Type ty)
577
578 -- | Parsing utility to check that a type is has instance of a given 'Constraint'1,
579 -- or raise 'Error_Expr_Constraint_missing'.
580 check_constraint1_type
581 :: forall ast ex c root ty h a ret.
582 ( root ~ Root_of_Expr ex
583 , ty ~ Type_Root_of_Expr ex
584 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
585 (Error_of_Expr ast root)
586 , Constraint_Type1 c ty
587 )
588 => Proxy ex -> Proxy c -> ast -> ty (h a)
589 -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
590 -> Either (Error_of_Expr ast root) ret
591 check_constraint1_type ex c ast ty k =
592 case constraint_type1 c ty of
593 Just Dict -> k Dict
594 Nothing -> Left $ error_expr ex $
595 Error_Expr_Constraint_missing ast
596 (Exists_Type ty)
597
598 -- | Parsing utility to check that the given type is a 'Type_Maybe'
599 -- or raise 'Error_Expr_Type_mismatch'.
600 check_type1
601 :: forall ast ex root ty h ret.
602 ( root ~ Root_of_Expr ex
603 , ty ~ Type_Root_of_Expr ex
604 , Unlift_Type1 (Type_of_Expr root)
605 , String_from_Type ty
606 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
607 (Error_of_Expr ast root)
608 )
609 => Proxy ex -> ast -> ty h
610 -> (forall (f:: * -> *).
611 ( Type_Type1 f ty h
612 , Lift_Type1 f (Type_Var :|: Type_of_Expr root)
613 ) -> Either (Error_of_Expr ast root) ret)
614 -> Either (Error_of_Expr ast root) ret
615 check_type1 ex ast ty k =
616 case unlift_type1 (unType_Root ty) $ Just . k of
617 Just x -> x
618 Nothing -> undefined
619 {-
620 Just x -> k x
621 Nothing ->
622 error ("check_type1: " ++ show ty)
623 Left $
624 error_expr ex $
625 Error_Expr_Type_mismatch ast
626 (Exists_Type (lift_type_root (Type_Type1 $ type_var SZero) -- $ type_var SZero
627 :: Type_Root_of_Expr ex (Zero1 Zero)))
628 (Exists_Type ty)
629 -}
630 data Zero1 a
631
632 -- * Type 'Error_Read'
633 -- | Error parsing a host-term.
634 data Error_Read
635 = Error_Read Text
636 deriving (Eq, Show)
637
638 -- | Parse a host-term.
639 read_safe :: Read h => Text -> Either Error_Read h
640 read_safe t =
641 case reads $ Text.unpack t of
642 [(x, "")] -> Right x
643 _ -> Left $ Error_Read t