]> 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.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.LOL.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 -- ** Type 'Expr_From'
33 type Expr_From ast ex hs ret
34 = Proxy ex
35 -- ^ Select the 'Expr_from' instance.
36 -> ast
37 -- ^ The input data to parse.
38 -> Context (Lambda_Var (Type_Root_of_Expr ex)) hs
39 -- ^ The bound variables in scope and their types:
40 -- held in the heterogeneous list @hs@,
41 -- from the closest including lambda abstraction to the farest.
42 -> ( forall h
43 . Type_Root_of_Expr ex h
44 -> Forall_Repr_with_Context ex hs h
45 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
46 -- ^ The accumulating continuation.
47 -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
48
49 -- | Parse a literal.
50 lit_from
51 :: forall ty lit ex ast hs ret.
52 ( ty ~ Type_Root_of_Expr ex
53 , Read lit
54 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
55 (Error_of_Expr ast (Root_of_Expr ex))
56 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
57 -> ty lit -> Lambda_Var_Name
58 -> Expr_From ast ex hs ret
59 lit_from lit ty_lit toread ex ast _ctx k =
60 case read_safe toread of
61 Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
62 Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
63
64 -- | Parse a unary operator.
65 op1_from
66 :: forall root ty lit ex ast hs ret.
67 ( ty ~ Type_Root_of_Expr ex
68 , root ~ Root_of_Expr ex
69 , Type_Eq (Type_Root_of_Expr root)
70 , Expr_from ast root
71 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
72 (Error_of_Expr ast root)
73 , Root_of_Expr root ~ root
74 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
75 -> ty lit -> ast
76 -> Expr_From ast ex hs ret
77 op1_from op ty_lit ast_x ex ast ctx k =
78 expr_from (Proxy::Proxy root) ast_x ctx $
79 \ty_x (Forall_Repr_with_Context x) ->
80 when_type_eq ex ast ty_lit ty_x $ \Refl ->
81 k ty_x $ Forall_Repr_with_Context (op . x)
82
83 -- | Parse a binary operator.
84 op2_from
85 :: forall root ty lit ex ast hs ret.
86 ( ty ~ Type_Root_of_Expr ex
87 , root ~ Root_of_Expr ex
88 , Type_Eq (Type_Root_of_Expr root)
89 , Expr_from ast root
90 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
91 (Error_of_Expr ast root)
92 , Root_of_Expr root ~ root
93 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
94 -> ty lit -> ast -> ast
95 -> Expr_From ast ex hs ret
96 op2_from op ty_lit ast_x ast_y ex ast ctx k =
97 expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
98 expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
99 when_type_eq ex ast ty_lit ty_x $ \Refl ->
100 when_type_eq ex ast ty_lit ty_y $ \Refl ->
101 k ty_x $ Forall_Repr_with_Context $
102 \c -> x c `op` y c
103
104 -- ** Type 'Context'
105
106 -- | GADT for a typing context,
107 -- accumulating an @item@ at each lambda;
108 -- used to accumulate object-types of lambda variables in 'Expr_from'
109 -- or host-terms of lambda variables in 'Repr_Host'.
110 data Context :: (* -> *) -> [*] -> * where
111 Context_Empty :: Context item '[]
112 Context_Next :: item h -> Context item hs -> Context item (h ': hs)
113 infixr 5 `Context_Next`
114
115 -- ** Type 'Lambda_Var'
116 -- | Join a name and a type.
117 --
118 -- This data type is used to handle lambda variables by name
119 -- (instead of DeBruijn indices for instance).
120 data Lambda_Var ty h
121 = Lambda_Var Lambda_Var_Name (ty h)
122 type Lambda_Var_Name = Text
123
124 -- ** Type 'Forall_Repr_with_Context'
125 -- | A data type embedding a universal quantification
126 -- over an interpreter @repr@
127 -- and qualified by the symantics of an expression.
128 --
129 -- Moreover the expression is abstracted by a 'Context'
130 -- built at parsing time to build a /Higher-Order Abstract Syntax/ (HOAS)
131 -- for lambda abstractions.
132 --
133 -- This data type is used to keep a parsed expression polymorphic enough
134 -- to stay interpretable by different interpreters.
135 --
136 -- NOTE: 'Sym_of_Expr'@ ex repr@
137 -- is needed to be able to use symantic methods of the parsed expression
138 -- into a 'Forall_Repr_with_Context'@ ex@.
139 --
140 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
141 -- is needed to be able to use an expression
142 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
143 -- into a 'Forall_Repr_with_Context'@ ex@,
144 -- which happens when a symantic method includes a polymorphic type
145 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
146 data Forall_Repr_with_Context ex hs h
147 = Forall_Repr_with_Context
148 ( forall repr. ( Sym_of_Expr ex repr
149 , Sym_of_Expr (Root_of_Expr ex) repr
150 ) => Context repr hs -> repr h )
151
152 -- ** Type 'Forall_Repr'
153 data Forall_Repr ex h
154 = Forall_Repr
155 { unForall_Repr :: forall repr
156 . Sym_of_Expr ex repr
157 => repr h }
158
159 -- ** Type family 'Root_of_Expr'
160 -- | The root expression of an expression.
161 type family Root_of_Expr (ex:: *) :: *
162
163 -- ** Type family 'Sym_of_Expr'
164 -- | The symantic of an expression.
165 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
166
167 -- ** Type family 'Error_of_Expr'
168 -- | The error(s) of an expression.
169 type family Error_of_Expr (ast:: *) (ex:: *) :: *
170
171 -- ** Type family 'Type_of_Expr'
172 -- | The type of an expression, parameterized by a root type.
173 type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *
174
175 -- ** Type 'Type_Root_of_Expr'
176 -- | Convenient alias.
177 --
178 -- NOTE: include 'Type_Var' only to use it
179 -- within 'Error_Expr_Type_mismatch' so far.
180 type Type_Root_of_Expr (ex:: *)
181 = Type_Root (Type_Alt Type_Var (Type_of_Expr (Root_of_Expr ex)))
182
183 -- * Type 'Expr_Root'
184 -- | The root expression, passing itself as parameter to the given expression.
185 newtype Expr_Root (ex:: * -> *)
186 = Expr_Root (ex (Expr_Root ex))
187 type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
188 type instance Type_of_Expr (Expr_Root ex)
189 = Type_of_Expr (ex (Expr_Root ex))
190 type instance Error_of_Expr ast (Expr_Root ex)
191 = Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
192 (Type_Root_of_Expr (ex (Expr_Root ex)))
193 ast)
194 (Error_of_Expr ast (ex (Expr_Root ex)))
195 type instance Sym_of_Expr (Expr_Root ex) repr
196 = Sym_of_Expr (ex (Expr_Root ex)) repr
197 instance -- Expr_from
198 ( Expr_from ast (ex (Expr_Root ex))
199 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
200 ) => Expr_from ast (Expr_Root ex) where
201 expr_from _ex ctx ast k =
202 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
203 ctx ast $ \ty (Forall_Repr_with_Context repr) ->
204 k ty (Forall_Repr_with_Context repr)
205
206 {- NOTE: useless code so far.
207 -- ** Class 'Expr_Root_Lift'
208 -- | Lift a given expression to a given root expression.
209 class Expr_Root_Lift ex root where
210 expr_root_lift :: ex root -> root
211 instance
212 Expr_Lift ex root =>
213 Expr_Root_Lift ex (Expr_Root root) where
214 expr_root_lift = Expr_Root . expr_lift
215 -}
216
217 -- * Type 'Expr_Alt'
218 -- | Expression making an alternative between two expressions.
219 data Expr_Alt curr next (root:: *)
220 = Expr_Alt_Curr (curr root)
221 | Expr_Alt_Next (next root)
222 type instance Root_of_Expr (Expr_Alt curr next root) = root
223 type instance Sym_of_Expr (Expr_Alt curr next root) repr
224 = ( Sym_of_Expr (curr root) repr
225 , Sym_of_Expr (next root) repr
226 )
227 type instance Type_of_Expr (Expr_Alt curr next root)
228 = Type_of_Expr_Alt
229 (Type_of_Expr (curr root))
230 (Type_of_Expr (next root))
231 curr next root
232 -- ** Type family 'Type_of_Expr_Alt'
233 -- | Remove 'No_Type' type when building 'Type_of_Expr'.
234 type family Type_of_Expr_Alt
235 (type_curr:: (* -> *) -> * -> *)
236 (type_next:: (* -> *) -> * -> *)
237 curr next root where
238 Type_of_Expr_Alt No_Type type_next curr next root = Type_of_Expr (next root)
239 Type_of_Expr_Alt type_curr No_Type curr next root = Type_of_Expr (curr root)
240 Type_of_Expr_Alt type_curr type_next curr next root
241 = Type_Alt (Type_of_Expr (curr root))
242 (Type_of_Expr (next root))
243
244 type instance Error_of_Expr ast (Expr_Alt curr next root)
245 = Error_of_Expr_Alt ast (curr root) (next root)
246 -- ** Type family 'Error_of_Expr_Alt'
247 -- | Remove 'No_Error_Expr' type when building the error of an expression.
248 type family Error_of_Expr_Alt ast curr next where
249 Error_of_Expr_Alt ast No_Error_Expr next = Error_of_Expr ast next
250 Error_of_Expr_Alt ast curr No_Error_Expr = Error_of_Expr ast curr
251 Error_of_Expr_Alt ast curr next
252 = Error_Expr_Alt (Error_of_Expr ast curr)
253 (Error_of_Expr ast next)
254 -- ** Type 'No_Error_Expr'
255 -- | A discarded error.
256 data No_Error_Expr
257 = No_Error_Expr
258 deriving (Eq, Show)
259
260 instance -- Expr_from
261 ( Expr_from ast (curr root)
262 , Expr_from ast (next root)
263 , Root_of_Expr (curr root) ~ root
264 , Root_of_Expr (next root) ~ root
265 , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
266 (Type_Root_of_Expr root) ast)
267 (Error_of_Expr ast root)
268 ) => Expr_from ast (Expr_Alt curr next root) where
269 expr_from _ex ctx ast k =
270 case expr_from (Proxy::Proxy (curr root)) ctx ast $
271 \ty (Forall_Repr_with_Context repr) ->
272 Right $ k ty (Forall_Repr_with_Context repr) of
273 Right ret -> ret
274 Left err ->
275 case error_expr_unlift err of
276 Just (Error_Expr_Unsupported_here _
277 :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
278 (Type_Root_of_Expr root) ast) ->
279 expr_from (Proxy::Proxy (next root)) ctx ast $
280 \ty (Forall_Repr_with_Context repr) ->
281 k ty (Forall_Repr_with_Context repr)
282 _ -> Left err
283
284 {- NOTE: useless code so far.
285 -- ** Type 'Expr_Lift'
286 -- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
287 type Expr_Lift ex exs
288 = Expr_LiftN (Peano_of_Expr ex exs) ex exs
289
290 -- | Convenient wrapper around 'expr_liftN',
291 -- passing it the 'Peano' number from 'Peano_of_Expr'.
292 expr_lift
293 :: forall ex exs (root:: *).
294 Expr_Lift ex exs =>
295 ex root -> exs root
296 expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))
297
298 -- *** Type family 'Peano_of_Expr'
299 -- | Return a 'Peano' number derived from the location
300 -- of a given expression within a given expression stack,
301 -- which is used to avoid @OverlappingInstances@.
302 type family Peano_of_Expr
303 (ex:: * -> *)
304 (exs:: * -> *) :: * where
305 Peano_of_Expr ex ex = Zero
306 Peano_of_Expr ex (Expr_Alt ex next) = Zero
307 Peano_of_Expr other (Expr_Alt curr next) = Succ (Peano_of_Expr other next)
308
309 -- *** Class 'Expr_LiftN'
310 -- | Lift a given expression to the top of a given expression stack including it,
311 -- by constructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
312 class Expr_LiftN (p:: *) ex exs where
313 expr_liftN :: forall (root:: *). Proxy p -> ex root -> exs root
314 instance Expr_LiftN Zero curr curr where
315 expr_liftN _ = id
316 instance Expr_LiftN Zero curr (Expr_Alt curr next) where
317 expr_liftN _ = Expr_Alt_Curr
318 instance
319 Expr_LiftN p other next =>
320 Expr_LiftN (Succ p) other (Expr_Alt curr next) where
321 expr_liftN _ = Expr_Alt_Next . expr_liftN (Proxy::Proxy p)
322
323 -- ** Type 'Expr_Unlift'
324 -- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
325 type Expr_Unlift ex exs
326 = Expr_UnliftN (Peano_of_Expr ex exs) ex exs
327
328 -- | Convenient wrapper around 'expr_unliftN',
329 -- passing it the 'Peano' number from 'Peano_of_Expr'.
330 expr_unlift
331 :: forall ex exs (root:: *).
332 Expr_Unlift ex exs =>
333 exs root -> Maybe (ex root)
334 expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))
335
336 -- *** Class 'Expr_UnliftN'
337 -- | Try to unlift a given expression out of a given expression stack including it,
338 -- by deconstructing the appropriate sequence of 'Expr_Alt_Curr' and 'Expr_Alt_Next'.
339 class Expr_UnliftN (p:: *) ex exs where
340 expr_unliftN :: forall (root:: *). Proxy p -> exs root -> Maybe (ex root)
341 instance Expr_UnliftN Zero curr curr where
342 expr_unliftN _ = Just
343 instance Expr_UnliftN Zero curr (Expr_Alt curr next) where
344 expr_unliftN _ (Expr_Alt_Curr x) = Just x
345 expr_unliftN _ (Expr_Alt_Next _) = Nothing
346 instance
347 Expr_UnliftN p other next =>
348 Expr_UnliftN (Succ p) other (Expr_Alt curr next) where
349 expr_unliftN _ (Expr_Alt_Next x) = expr_unliftN (Proxy::Proxy p) x
350 expr_unliftN _ (Expr_Alt_Curr _) = Nothing
351 -}
352
353 -- ** Type family 'Is_Last_Expr'
354 -- | Return whether a given expression is the last one in a given expression stack.
355 --
356 -- NOTE: each expression parser uses this type family
357 -- when it encounters unsupported syntax:
358 -- to know if it is the last expression parser component that will be tried
359 -- (and thus return 'Error_Expr_Unsupported')
360 -- or if some other expression parser component shall be tried
361 -- (and thus return 'Error_Expr_Unsupported_here',
362 -- which is then handled accordingly by the 'Expr_from' instance of 'Expr_Alt').
363 type family Is_Last_Expr (ex:: *) (exs:: *) :: Bool where
364 Is_Last_Expr ex ex = 'True
365 Is_Last_Expr ex (Expr_Root exs) = Is_Last_Expr ex (exs (Expr_Root exs))
366 Is_Last_Expr (ex root) (Expr_Alt ex next root) = 'False
367 Is_Last_Expr other (Expr_Alt curr next root) = Is_Last_Expr other (next root)
368
369 -- * Type 'Error_Expr_Alt'
370 -- | Error expression making an alternative between two error expressions.
371 data Error_Expr_Alt curr next
372 = Error_Expr_Alt_Curr curr
373 | Error_Expr_Alt_Next next
374 deriving (Eq, Show)
375
376 -- ** Type 'Error_Expr_Lift'
377 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftN'.
378 type Error_Expr_Lift err errs
379 = Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
380
381 -- | Convenient wrapper around 'error_expr_liftN',
382 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
383 error_expr_lift
384 :: forall err errs.
385 Error_Expr_Lift err errs => err -> errs
386 error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))
387
388 -- *** Type family 'Peano_of_Error_Expr'
389 -- | Return a 'Peano' number derived from the location
390 -- of a given error expression within a given error expression stack,
391 -- which is used to avoid @OverlappingInstances@.
392 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
393 Peano_of_Error_Expr err err = Zero
394 Peano_of_Error_Expr err (Error_Expr_Alt err next) = Zero
395 Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)
396
397 -- *** Class 'Error_Expr_LiftN'
398 -- | Lift a given expression to the top of a given expression stack including it,
399 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
400 class Error_Expr_LiftN (p:: *) err errs where
401 error_expr_liftN :: Proxy p -> err -> errs
402 instance Error_Expr_LiftN Zero curr curr where
403 error_expr_liftN _ = id
404 instance Error_Expr_LiftN Zero curr (Error_Expr_Alt curr next) where
405 error_expr_liftN _ = Error_Expr_Alt_Curr
406 instance
407 Error_Expr_LiftN p other next =>
408 Error_Expr_LiftN (Succ p) other (Error_Expr_Alt curr next) where
409 error_expr_liftN _ = Error_Expr_Alt_Next . error_expr_liftN (Proxy::Proxy p)
410
411 -- ** Type 'Error_Expr_Unlift'
412 -- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftN'.
413 type Error_Expr_Unlift ex exs
414 = Error_Expr_UnliftN (Peano_of_Error_Expr ex exs) ex exs
415
416 -- | Convenient wrapper around 'error_expr_unliftN',
417 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
418 error_expr_unlift
419 :: forall ex exs.
420 Error_Expr_Unlift ex exs => exs -> Maybe ex
421 error_expr_unlift = error_expr_unliftN (Proxy::Proxy (Peano_of_Error_Expr ex exs))
422
423 -- *** Class 'Error_Expr_UnliftN'
424 -- | Try to unlift a given expression error out of a given expression error stack including it,
425 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
426 class Error_Expr_UnliftN (p:: *) ex exs where
427 error_expr_unliftN :: Proxy p -> exs -> Maybe ex
428 instance Error_Expr_UnliftN Zero curr curr where
429 error_expr_unliftN _ = Just
430 instance Error_Expr_UnliftN Zero curr (Error_Expr_Alt curr next) where
431 error_expr_unliftN _ (Error_Expr_Alt_Curr x) = Just x
432 error_expr_unliftN _ (Error_Expr_Alt_Next _) = Nothing
433 instance
434 Error_Expr_UnliftN p other next =>
435 Error_Expr_UnliftN (Succ p) other (Error_Expr_Alt curr next) where
436 error_expr_unliftN _ (Error_Expr_Alt_Next x) = error_expr_unliftN (Proxy::Proxy p) x
437 error_expr_unliftN _ (Error_Expr_Alt_Curr _) = Nothing
438
439 -- * Type 'Error_Expr_Read'
440 -- | Common expression errors.
441 data Error_Expr err_ty ty ast
442 = Error_Expr_Wrong_number_of_arguments ast Int
443 -- ^ Wrong number of arguments applied to a term,
444 -- the integer is the number of arguments expected.
445 | Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
446 -- ^ Mismatch between respectively expected and actual type.
447 | Error_Expr_Read Error_Read ast
448 -- ^ Error when reading a literal.
449 | Error_Expr_Type err_ty ast
450 -- ^ Error when parsing a type.
451 | Error_Expr_Unsupported ast
452 -- ^ Given syntax is supported by none
453 -- of the expression parser components
454 -- of the expression stack.
455 | Error_Expr_Unsupported_here ast
456 -- ^ Given syntax not supported by
457 -- the current expression parser component.
458 deriving (Eq, Show)
459
460 -- | Convenient wrapper around 'error_expr_lift',
461 -- passing the type family boilerplate.
462 error_expr
463 :: forall ast ex ty.
464 (ty ~ Type_Root_of_Expr ex)
465 => Error_Expr_Lift
466 (Error_Expr (Error_of_Type ast ty) ty ast)
467 (Error_of_Expr ast (Root_of_Expr ex))
468 => Proxy ex
469 -> Error_Expr (Error_of_Type ast ty) ty ast
470 -> Error_of_Expr ast (Root_of_Expr ex)
471 error_expr _ = error_expr_lift
472
473 -- | Utility to return 'Error_Expr_Unsupported'
474 -- or 'Error_Expr_Unsupported_here'
475 -- according to the given expression.
476 error_expr_unsupported
477 :: forall ast ex ty root.
478 ( root ~ Root_of_Expr ex
479 , ty ~ Type_Root_of_Expr ex
480 , Implicit_HBool (Is_Last_Expr ex root)
481 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
482 (Error_of_Expr ast root)
483 ) => Proxy ex -> ast
484 -> Error_of_Expr ast (Root_of_Expr ex)
485 error_expr_unsupported ex ast =
486 case hbool :: HBool (Is_Last_Expr ex root) of
487 HTrue -> error_expr ex $ Error_Expr_Unsupported ast
488 HFalse -> error_expr ex $ Error_Expr_Unsupported_here ast
489
490 -- | Utility to check that two types are equal
491 -- or raise 'Error_Expr_Type_mismatch'.
492 when_type_eq
493 :: forall ast ex root ty x y ret.
494 ( root ~ Root_of_Expr ex
495 , ty ~ Type_Root_of_Expr ex
496 , Type_Eq ty
497 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
498 (Error_of_Expr ast root)
499 )
500 => Proxy ex -> ast -> ty x -> ty y
501 -> (forall. x :~: y -> Either (Error_of_Expr ast root) ret)
502 -> Either (Error_of_Expr ast root) ret
503 when_type_eq ex ast x y k =
504 case x `type_eq` y of
505 Nothing -> Left $ error_expr ex $
506 Error_Expr_Type_mismatch ast
507 (Exists_Type x)
508 (Exists_Type y)
509 Just Refl -> k Refl
510
511 -- * Type 'Error_Read'
512 -- | Error parsing a host-term.
513 data Error_Read
514 = Error_Read Text
515 deriving (Eq, Show)
516
517 -- | Parse a host-term.
518 read_safe :: Read h => Text -> Either Error_Read h
519 read_safe t =
520 case reads $ Text.unpack t of
521 [(x, "")] -> Right x
522 _ -> Left $ Error_Read t