1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE Rank2Types #-}
7 {-# LANGUAGE ScopedTypeVariables #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE TypeOperators #-}
10 {-# LANGUAGE UndecidableInstances #-}
11 -- | Abstract Syntax Tree.
15 -- import Test.Tasty.HUnit
17 import qualified Data.List as List
18 import Data.Proxy (Proxy(..))
19 import Data.Text (Text)
20 import qualified Data.Text as Text
22 import Language.Symantic.Lib.Data.Bool
23 import Language.Symantic.Type
24 import Language.Symantic.Expr as Expr
27 tests = testGroup "AST" $
35 -- | Custom 'Show' instance a little bit more readable
36 -- than the automatically derived one.
37 instance Show AST where
38 showsPrec p ast@(AST f args) =
39 let n = Text.unpack f in
41 AST _ [] -> showString n
43 showParen (p >= prec_arrow) $
44 showString ("("++n++") ") .
45 showsPrec prec_arrow a
47 showParen (p >= prec_arrow) $
48 showsPrec prec_arrow a .
49 showString (" "++n++" ") .
50 showsPrec prec_arrow b
54 showString (List.intercalate ", " $ show Prelude.<$> args) .
58 -- ** Parsing utilities
60 :: forall ty ast ex hs ret.
61 ( ty ~ Type_Root_of_Expr ex
62 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
63 (Error_of_Expr ast (Root_of_Expr ex))
65 -> Expr_From ast ex hs ret
66 -> Expr_From ast ex hs ret
67 from_ast0 asts k' ex ast ctx k =
70 _ -> Left $ error_expr ex $
71 Error_Expr_Wrong_number_of_arguments ast 0
74 :: forall ty ast ex hs ret.
75 ( ty ~ Type_Root_of_Expr ex
76 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
77 (Error_of_Expr ast (Root_of_Expr ex))
78 ) => [ast] -> (ast -> Expr_From ast ex hs ret)
79 -> Expr_From ast ex hs ret
80 from_ast1 asts k' ex ast ctx k =
82 [ast_0] -> k' ast_0 ex ast ctx k
83 _ -> Left $ error_expr ex $
84 Error_Expr_Wrong_number_of_arguments ast 1
87 :: forall ty ast ex hs ret.
88 ( ty ~ Type_Root_of_Expr ex
89 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
90 (Error_of_Expr ast (Root_of_Expr ex))
91 ) => [ast] -> (ast -> ast -> Expr_From ast ex hs ret)
92 -> Expr_From ast ex hs ret
93 from_ast2 asts k' ex ast ctx k =
95 [ast_0, ast_1] -> k' ast_0 ast_1 ex ast ctx k
96 _ -> Left $ error_expr ex $
97 Error_Expr_Wrong_number_of_arguments ast 2
100 :: forall ty ast ex hs ret.
101 ( ty ~ Type_Root_of_Expr ex
102 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
103 (Error_of_Expr ast (Root_of_Expr ex))
104 ) => [ast] -> (ast -> ast -> ast -> Expr_From ast ex hs ret)
105 -> Expr_From ast ex hs ret
106 from_ast3 asts k' ex ast ctx k =
108 [ast_0, ast_1, ast_2] -> k' ast_0 ast_1 ast_2 ex ast ctx k
109 _ -> Left $ error_expr ex $
110 Error_Expr_Wrong_number_of_arguments ast 3
113 :: forall root ty lit ex ast hs ret.
114 ( ty ~ Type_Root_of_Expr ex
115 , root ~ Root_of_Expr ex
118 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
119 (Error_of_Expr ast root)
120 ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
122 -> Expr_From ast ex hs ret
123 lit_from_AST op ty_lit asts ex ast ctx k =
125 [AST lit []] -> lit_from op ty_lit lit ex ast ctx k
126 _ -> Left $ error_expr ex $
127 Error_Expr_Wrong_number_of_arguments ast 1
130 :: forall root ty lit ex ast hs ret.
131 ( ty ~ Type_Root_of_Expr ex
132 , root ~ Root_of_Expr ex
134 , Eq_Type (Type_Root_of_Expr root)
136 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
137 (Error_of_Expr ast root)
138 , Root_of_Expr root ~ root
139 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
141 -> Expr_From ast ex hs ret
142 op1_from_AST op ty_lit asts ex ast ctx k =
144 [ast_x] -> op1_from op ty_lit ast_x ex ast ctx k
145 _ -> Left $ error_expr ex $
146 Error_Expr_Wrong_number_of_arguments ast 1
149 :: forall root ty lit ex ast hs ret.
150 ( ty ~ Type_Root_of_Expr ex
151 , root ~ Root_of_Expr ex
153 , Eq_Type (Type_Root_of_Expr root)
155 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
156 (Error_of_Expr ast root)
157 , Root_of_Expr root ~ root
158 ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
160 -> Expr_From ast ex hs ret
161 op2_from_AST op ty_lit asts ex ast ctx k =
163 [ast_x, ast_y] -> op2_from op ty_lit ast_x ast_y ex ast ctx k
164 _ -> Left $ error_expr ex $
165 Error_Expr_Wrong_number_of_arguments ast 2
167 instance -- Type_from AST Type_Var0
168 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
169 , IBool (Is_Last_Type (Type_Var0 root) root)
170 ) => Type_from AST (Type_Var0 root) where
171 type_from ty ast _k =
172 Left $ error_type_unsupported ty ast
173 -- NOTE: no support so far.
174 instance -- Type_from AST Type_Var1
175 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
176 , IBool (Is_Last_Type (Type_Var1 root) root)
177 ) => Type_from AST (Type_Var1 root) where
178 type_from ty ast _k =
179 Left $ error_type_unsupported ty ast
180 -- NOTE: no support so far.
181 instance -- Type_from AST Type_Unit
182 ( Lift_Type_Root Type_Unit root
183 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
184 , IBool (Is_Last_Type (Type_Unit root) root)
185 ) => Type_from AST (Type_Unit root) where
191 _ -> Left $ lift_error_type $
192 Error_Type_Wrong_number_of_arguments ast 0
193 _ -> Left $ error_type_unsupported ty ast
194 instance -- Type_from AST Type_Bool
195 ( Lift_Type_Root Type_Bool root
196 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
197 , IBool (Is_Last_Type (Type_Bool root) root)
198 ) => Type_from AST (Type_Bool root) where
204 _ -> Left $ lift_error_type $
205 Error_Type_Wrong_number_of_arguments ast 0
206 _ -> Left $ error_type_unsupported ty ast
207 instance -- Type_from AST Type_Int
208 ( Lift_Type_Root Type_Int root
209 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
210 , IBool (Is_Last_Type (Type_Int root) root)
211 ) => Type_from AST (Type_Int root) where
217 _ -> Left $ lift_error_type $
218 Error_Type_Wrong_number_of_arguments ast 0
219 _ -> Left $ error_type_unsupported ty ast
220 instance -- Type_from AST Type_Ordering
221 ( Lift_Type_Root Type_Ordering root
222 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
223 , IBool (Is_Last_Type (Type_Ordering root) root)
224 ) => Type_from AST (Type_Ordering root) where
227 AST "Ordering" asts ->
229 [] -> k type_ordering
230 _ -> Left $ lift_error_type $
231 Error_Type_Wrong_number_of_arguments ast 0
232 _ -> Left $ error_type_unsupported ty ast
233 instance -- Type_from AST Type_Fun
236 , Lift_Type_Root (Type_Fun lam) root
237 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
238 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
239 , Root_of_Type root ~ root
240 , IBool (Is_Last_Type (Type_Fun lam root) root)
241 ) => Type_from AST (Type_Fun lam root) where
246 [ast_arg, ast_res] -> type_fun_from ty ast_arg ast_res k
247 _ -> Left $ lift_error_type $
248 Error_Type_Wrong_number_of_arguments ast 2
249 _ -> Left $ error_type_unsupported ty ast
250 instance -- Type_from AST Type_Maybe
253 , Lift_Type_Root Type_Maybe root
254 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
255 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
256 , Root_of_Type root ~ root
257 , IBool (Is_Last_Type (Type_Maybe root) root)
258 ) => Type_from AST (Type_Maybe root) where
264 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
266 _ -> Left $ lift_error_type $
267 Error_Type_Wrong_number_of_arguments ast 1
268 _ -> Left $ error_type_unsupported ty ast
269 instance -- Type_from AST Type_List
272 , Lift_Type_Root Type_List root
273 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
274 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
275 , Root_of_Type root ~ root
276 , IBool (Is_Last_Type (Type_List root) root)
277 ) => Type_from AST (Type_List root) where
283 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
285 _ -> Left $ lift_error_type $
286 Error_Type_Wrong_number_of_arguments ast 1
287 _ -> Left $ error_type_unsupported ty ast
288 instance -- Type_from AST Type_Map
291 , Lift_Type_Root Type_Map root
292 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
293 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
294 , Constraint_Type Ord root
295 , Root_of_Type root ~ root
296 , IBool (Is_Last_Type (Type_Map root) root)
297 ) => Type_from AST (Type_Map root) where
303 type_from (Proxy::Proxy root) ast_k $ \ty_k ->
304 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
305 check_type_constraint (Proxy::Proxy Ord) ast_k ty_k $ \Dict ->
306 k (type_map ty_k ty_a)
307 _ -> Left $ lift_error_type $
308 Error_Type_Wrong_number_of_arguments ast 2
309 _ -> Left $ error_type_unsupported ty ast
310 instance -- Type_from AST Type_Tuple2
313 , Lift_Type_Root Type_Tuple2 root
314 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
315 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
316 , Root_of_Type root ~ root
317 , IBool (Is_Last_Type (Type_Tuple2 root) root)
318 ) => Type_from AST (Type_Tuple2 root) where
324 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
325 type_from (Proxy::Proxy root) ast_b $ \ty_b ->
326 k (type_tuple2 ty_a ty_b)
327 _ -> Left $ lift_error_type $
328 Error_Type_Wrong_number_of_arguments ast 2
329 _ -> Left $ error_type_unsupported ty ast
330 instance -- Type_from AST Type_Either
333 , Lift_Type_Root Type_Either root
334 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
335 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
336 , Root_of_Type root ~ root
337 , IBool (Is_Last_Type (Type_Either root) root)
338 ) => Type_from AST (Type_Either root) where
344 type_from (Proxy::Proxy root) ast_l $ \ty_l ->
345 type_from (Proxy::Proxy root) ast_r $ \ty_r ->
346 k (type_either ty_l ty_r)
347 _ -> Left $ lift_error_type $
348 Error_Type_Wrong_number_of_arguments ast 2
349 _ -> Left $ error_type_unsupported ty ast
351 instance -- Type1_from AST Type_Bool
352 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
353 , IBool (Is_Last_Type (Type_Bool root) root)
354 ) => Type1_from AST (Type_Bool root)
355 instance -- Type1_from AST Type_Int
356 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
357 , IBool (Is_Last_Type (Type_Int root) root)
358 ) => Type1_from AST (Type_Int root)
359 instance -- Type1_from AST Type_Unit
360 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
361 , IBool (Is_Last_Type (Type_Unit root) root)
362 ) => Type1_from AST (Type_Unit root)
363 instance -- Type1_from AST Type_Ordering
364 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
365 , IBool (Is_Last_Type (Type_Ordering root) root)
366 ) => Type1_from AST (Type_Ordering root)
367 instance -- Type1_from AST Type_Var0
368 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
369 , IBool (Is_Last_Type (Type_Var0 root) root)
370 ) => Type1_from AST (Type_Var0 root)
371 instance -- Type1_from AST Type_Var1
372 ( Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
373 , IBool (Is_Last_Type (Type_Var1 root) root)
374 ) => Type1_from AST (Type_Var1 root)
375 instance -- Type1_from AST Type_Maybe
377 , Lift_Type_Root Type_Maybe root
378 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
379 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
380 , Root_of_Type root ~ root
381 , IBool (Is_Last_Type (Type_Maybe root) root)
382 ) => Type1_from AST (Type_Maybe root) where
383 type1_from ty ast k =
387 [] -> k (Proxy::Proxy Maybe) type_maybe
388 _ -> Left $ lift_error_type $
389 Error_Type_Wrong_number_of_arguments ast 0
390 _ -> Left $ error_type_unsupported ty ast
391 instance -- Type1_from AST Type_List
394 , Lift_Type_Root Type_List root
395 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
396 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
397 , Root_of_Type root ~ root
398 , IBool (Is_Last_Type (Type_List root) root)
399 ) => Type1_from AST (Type_List root) where
400 type1_from ty ast k =
404 [] -> k (Proxy::Proxy []) type_list
405 _ -> Left $ lift_error_type $
406 Error_Type_Wrong_number_of_arguments ast 0
407 _ -> Left $ error_type_unsupported ty ast
408 instance -- Type1_from AST Type_Fun
411 , Lift_Type_Root (Type_Fun lam) root
412 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
413 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
414 , Root_of_Type root ~ root
415 , IBool (Is_Last_Type (Type_Fun lam root) root)
416 ) => Type1_from AST (Type_Fun lam root) where
417 type1_from ty ast k =
422 type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
423 k (Proxy::Proxy (Lambda lam h_arg)) $
425 _ -> Left $ lift_error_type $
426 Error_Type_Wrong_number_of_arguments ast 1
427 _ -> Left $ error_type_unsupported ty ast
428 instance -- Type1_from AST Type_Either
431 , Lift_Type_Root Type_Either root
432 , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
433 , Unlift_Error_Type (Error_Type AST) (Error_of_Type AST root)
434 , Root_of_Type root ~ root
435 , IBool (Is_Last_Type (Type_Either root) root)
436 ) => Type1_from AST (Type_Either root) where
437 type1_from ty ast k =
442 type_from (Proxy::Proxy root) ast_l $ \(ty_l::root h_l) ->
443 k (Proxy::Proxy (Either h_l)) $
445 _ -> Left $ lift_error_type $
446 Error_Type_Wrong_number_of_arguments ast 1
447 _ -> Left $ error_type_unsupported ty ast
449 instance -- Expr_from AST Expr_Bool
450 ( Eq_Type (Type_Root_of_Expr root)
452 , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
453 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
454 , Unlift_Type Type_Bool (Type_of_Expr root)
455 , Root_of_Expr root ~ root
456 , IBool (Is_Last_Expr (Expr_Bool root) root)
457 ) => Expr_from AST (Expr_Bool root) where
460 AST "bool" asts -> lit_from_AST bool type_bool asts ex ast
461 AST "not" asts -> op1_from_AST Expr.not type_bool asts ex ast
462 AST "&&" asts -> op2_from_AST (Expr.&&) type_bool asts ex ast
463 AST "||" asts -> op2_from_AST (Expr.||) type_bool asts ex ast
464 AST "xor" asts -> op2_from_AST Expr.xor type_bool asts ex ast
465 _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
466 instance -- Expr_from AST Expr_If
467 ( Eq_Type (Type_Root_of_Expr root)
469 , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
470 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
471 , Root_of_Expr root ~ root
472 , IBool (Is_Last_Expr (Expr_If root) root)
473 ) => Expr_from AST (Expr_If root) where
474 expr_from ex ast ctx k =
476 AST "if" asts -> from_ast3 asts if_from ex ast ctx k
477 _ -> Left $ error_expr_unsupported ex ast
478 instance -- Expr_from AST Expr_When
479 ( Eq_Type (Type_Root_of_Expr root)
481 , Lift_Type_Root Type_Bool (Type_Root_of_Expr root)
482 , Lift_Type_Root Type_Unit (Type_Root_of_Expr root)
483 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
484 , Root_of_Expr root ~ root
485 , IBool (Is_Last_Expr (Expr_When root) root)
486 ) => Expr_from AST (Expr_When root) where
487 expr_from ex ast ctx k =
489 AST "when" asts -> from_ast2 asts when_from ex ast ctx k
490 _ -> Left $ error_expr_unsupported ex ast
491 instance -- Expr_from AST Expr_Int
492 ( Eq_Type (Type_Root_of_Expr root)
494 , Lift_Type_Root Type_Int (Type_Root_of_Expr root)
495 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
496 , Unlift_Type Type_Int (Type_of_Expr root)
497 , Root_of_Expr root ~ root
498 , IBool (Is_Last_Expr (Expr_Int root) root)
499 ) => Expr_from AST (Expr_Int root) where
502 AST "int" asts -> lit_from_AST int type_int asts ex ast
503 AST "abs" asts -> op1_from_AST Expr.abs type_int asts ex ast
504 AST "negate" asts -> op1_from_AST Expr.negate type_int asts ex ast
505 AST "+" asts -> op2_from_AST (Expr.+) type_int asts ex ast
506 AST "-" asts -> op2_from_AST (Expr.-) type_int asts ex ast
507 AST "*" asts -> op2_from_AST (Expr.*) type_int asts ex ast
508 AST "mod" asts -> op2_from_AST Expr.mod type_int asts ex ast
509 _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
510 instance -- Expr_from AST Expr_Lambda
511 ( Eq_Type (Type_Root_of_Expr root)
512 , Type_from AST (Type_Root_of_Expr root)
514 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
515 , Lift_Error_Expr (Error_Expr_Lambda AST) (Error_of_Expr AST root)
516 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
517 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
518 , Root_of_Expr root ~ root
519 , IBool (Is_Last_Expr (Expr_Lambda_App lam root) root)
520 ) => Expr_from AST (Expr_Lambda_App lam root) where
521 expr_from ex ast ctx k =
525 [AST name []] -> var_from name ex ast ctx k
526 _ -> Left $ error_expr ex $
527 Error_Expr_Wrong_number_of_arguments ast 1
528 AST "app" asts -> from_ast2 asts app_from ex ast ctx k
529 _ -> Left $ error_expr_unsupported ex ast
530 instance -- Expr_from AST Expr_Lambda_Inline
531 ( Eq_Type (Type_Root_of_Expr root)
532 , Type_from AST (Type_Root_of_Expr root)
534 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
535 , Lift_Error_Expr (Error_Expr_Lambda AST) (Error_of_Expr AST root)
536 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
537 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
538 , Root_of_Expr root ~ root
539 , IBool (Is_Last_Expr (Expr_Lambda_Inline lam root) root)
540 ) => Expr_from AST (Expr_Lambda_Inline lam root) where
541 expr_from ex ast ctx k =
543 AST "inline" asts -> go_lam asts inline
544 AST "let_inline" asts -> go_let asts let_inline
545 _ -> Left $ error_expr_unsupported ex ast
548 (lam::forall repr arg res. Sym_Lambda_Inline lam repr
549 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
551 [AST name [], ast_ty_arg, ast_body] ->
552 lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
553 _ -> Left $ error_expr ex $
554 Error_Expr_Wrong_number_of_arguments ast 3
556 (let_::forall repr var res. Sym_Lambda_Inline lam repr
557 => repr var -> (repr var -> repr res) -> repr res) =
559 [AST name [], ast_var, ast_body] ->
560 let_from let_ name ast_var ast_body ex ast ctx k
561 _ -> Left $ error_expr ex $
562 Error_Expr_Wrong_number_of_arguments ast 3
563 instance -- Expr_from AST Expr_Lambda_Val
564 ( Eq_Type (Type_Root_of_Expr root)
565 , Type_from AST (Type_Root_of_Expr root)
567 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
568 , Lift_Error_Expr (Error_Expr_Lambda AST) (Error_of_Expr AST root)
569 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
570 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
571 , Root_of_Expr root ~ root
572 , IBool (Is_Last_Expr (Expr_Lambda_Val lam root) root)
573 ) => Expr_from AST (Expr_Lambda_Val lam root) where
574 expr_from ex ast ctx k =
576 AST "val" asts -> go_lam asts val
577 AST "let_val" asts -> go_let asts let_val
578 _ -> Left $ error_expr_unsupported ex ast
581 (lam::forall repr arg res. Sym_Lambda_Val lam repr
582 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
584 [AST name [], ast_ty_arg, ast_body] ->
585 lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
586 _ -> Left $ error_expr ex $
587 Error_Expr_Wrong_number_of_arguments ast 3
589 (let_::forall repr var res. Sym_Lambda_Val lam repr
590 => repr var -> (repr var -> repr res) -> repr res) =
592 [AST name [], ast_var, ast_body] ->
593 let_from let_ name ast_var ast_body ex ast ctx k
594 _ -> Left $ error_expr ex $
595 Error_Expr_Wrong_number_of_arguments ast 3
596 instance -- Expr_from AST Expr_Lambda_Lazy
597 ( Eq_Type (Type_Root_of_Expr root)
598 , Type_from AST (Type_Root_of_Expr root)
600 , Lift_Type_Root (Type_Fun lam) (Type_Root_of_Expr root)
601 , Lift_Error_Expr (Error_Expr_Lambda AST) (Error_of_Expr AST root)
602 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
603 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
604 , Root_of_Expr root ~ root
605 , IBool (Is_Last_Expr (Expr_Lambda_Lazy lam root) root)
606 ) => Expr_from AST (Expr_Lambda_Lazy lam root) where
607 expr_from ex ast ctx k =
609 AST "lazy" asts -> go_lam asts lazy
610 AST "let_lazy" asts -> go_let asts let_lazy
611 _ -> Left $ error_expr_unsupported ex ast
614 (lam::forall repr arg res. Sym_Lambda_Lazy lam repr
615 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
617 [AST name [], ast_ty_arg, ast_body] ->
618 lam_from (Proxy::Proxy lam) lam name ast_ty_arg ast_body ex ast ctx k
619 _ -> Left $ error_expr ex $
620 Error_Expr_Wrong_number_of_arguments ast 3
622 (let_::forall repr var res. Sym_Lambda_Lazy lam repr
623 => repr var -> (repr var -> repr res) -> repr res) =
625 [AST name [], ast_var, ast_body] ->
626 let_from let_ name ast_var ast_body ex ast ctx k
627 _ -> Left $ error_expr ex $
628 Error_Expr_Wrong_number_of_arguments ast 3
629 instance -- Expr_from AST Expr_Maybe
630 ( Eq_Type (Type_Root_of_Expr root)
631 , Type_from AST (Type_Root_of_Expr root)
633 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
634 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
635 , Lift_Type Type_Maybe (Type_of_Expr root)
636 , Unlift_Type Type_Maybe (Type_of_Expr root)
637 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
638 , Root_of_Expr root ~ root
639 , IBool (Is_Last_Expr (Expr_Maybe lam root) root)
640 ) => Expr_from AST (Expr_Maybe lam root) where
641 expr_from ex ast ctx k =
643 AST "maybe" asts -> from_ast3 asts maybe_from ex ast ctx k
644 AST "nothing" asts -> from_ast1 asts nothing_from ex ast ctx k
645 AST "just" asts -> from_ast1 asts just_from ex ast ctx k
646 _ -> Left $ error_expr_unsupported ex ast
647 instance -- Expr_from AST Expr_Eq
648 ( Eq_Type (Type_Root_of_Expr root)
649 , Lift_Type Type_Bool (Type_of_Expr root)
650 , Constraint_Type Eq (Type_Root_of_Expr root)
652 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
653 , Root_of_Expr root ~ root
654 , IBool (Is_Last_Expr (Expr_Eq root) root)
655 ) => Expr_from AST (Expr_Eq root) where
656 expr_from ex ast ctx k =
658 AST "==" asts -> from_ast2 asts eq_from ex ast ctx k
659 _ -> Left $ error_expr_unsupported ex ast
660 instance -- Expr_from AST Expr_Ord
661 ( Eq_Type (Type_Root_of_Expr root)
662 , Lift_Type Type_Ordering (Type_of_Expr root)
663 , Constraint_Type Ord (Type_Root_of_Expr root)
665 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
666 , Root_of_Expr root ~ root
667 , IBool (Is_Last_Expr (Expr_Ord root) root)
668 ) => Expr_from AST (Expr_Ord root) where
669 expr_from ex ast ctx k =
671 AST "compare" asts -> from_ast2 asts compare_from ex ast ctx k
672 _ -> Left $ error_expr_unsupported ex ast
673 instance -- Expr_from AST Expr_List
674 ( Eq_Type (Type_Root_of_Expr root)
675 , Type_from AST (Type_Root_of_Expr root)
677 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
678 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
679 , Lift_Type Type_List (Type_of_Expr root)
680 , Unlift_Type Type_List (Type_of_Expr root)
681 , Lift_Type Type_Bool (Type_of_Expr root)
682 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
683 , Root_of_Expr root ~ root
684 , IBool (Is_Last_Expr (Expr_List lam root) root)
685 ) => Expr_from AST (Expr_List lam root) where
686 expr_from ex ast ctx k =
688 AST "[]" asts -> from_ast1 asts list_empty_from ex ast ctx k
689 AST ":" asts -> from_ast2 asts list_cons_from ex ast ctx k
690 AST "list_filter" asts -> from_ast2 asts list_filter_from ex ast ctx k
693 ast_ty_a:asts' -> list_from ast_ty_a asts' ex ast ctx k
694 _ -> Left $ error_expr ex $
695 Error_Expr_Wrong_number_of_arguments ast 1
696 _ -> Left $ error_expr_unsupported ex ast
697 instance -- Expr_from AST Expr_Map
698 ( Eq_Type (Type_Root_of_Expr root)
700 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
701 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
702 , Lift_Type Type_Map (Type_of_Expr root)
703 , Unlift_Type Type_Map (Type_of_Expr root)
704 , Lift_Type Type_List (Type_of_Expr root)
705 , Unlift_Type Type_List (Type_of_Expr root)
706 , Lift_Type Type_Tuple2 (Type_of_Expr root)
707 , Unlift_Type Type_Tuple2 (Type_of_Expr root)
708 , Constraint_Type Ord (Type_Root_of_Expr root)
709 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
710 , Root_of_Expr root ~ root
711 , IBool (Is_Last_Expr (Expr_Map lam root) root)
712 ) => Expr_from AST (Expr_Map lam root) where
713 expr_from ex ast ctx k =
715 AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
716 AST "map_map" asts -> from_ast2 asts map_map_from ex ast ctx k
717 _ -> Left $ error_expr_unsupported ex ast
718 instance -- Expr_from AST Expr_Functor
719 ( Eq_Type (Type_Root_of_Expr root)
721 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
722 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
723 , Unlift_Type1 (Type_of_Expr root)
724 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
725 , Constraint_Type1 Functor (Type_Root_of_Expr root)
726 , Root_of_Expr root ~ root
727 , IBool (Is_Last_Expr (Expr_Functor lam root) root)
728 ) => Expr_from AST (Expr_Functor lam root) where
729 expr_from ex ast ctx k =
731 AST "fmap" asts -> from_ast2 asts fmap_from ex ast ctx k
732 AST "<$>" asts -> from_ast2 asts fmap_from ex ast ctx k
733 _ -> Left $ error_expr_unsupported ex ast
734 instance -- Expr_from AST Expr_Applicative
735 ( Eq_Type (Type_Root_of_Expr root)
736 , Type1_from AST (Type_Root_of_Expr root)
738 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
739 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
740 , Eq_Type1 (Type_Root_of_Expr root)
741 , Unlift_Type1 (Type_of_Expr root)
742 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
743 , Constraint_Type1 Applicative (Type_Root_of_Expr root)
744 , Root_of_Expr root ~ root
745 , IBool (Is_Last_Expr (Expr_Applicative lam root) root)
746 ) => Expr_from AST (Expr_Applicative lam root) where
747 expr_from ex ast ctx k =
749 AST "pure" asts -> from_ast2 asts pure_from ex ast ctx k
750 AST "<*>" asts -> from_ast2 asts ltstargt_from ex ast ctx k
751 _ -> Left $ error_expr_unsupported ex ast
752 instance -- Expr_from AST Expr_Traversable
753 ( Eq_Type (Type_Root_of_Expr root)
754 , Type1_from AST (Type_Root_of_Expr root)
756 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
757 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
758 , Eq_Type1 (Type_Root_of_Expr root)
759 , Unlift_Type1 (Type_of_Expr root)
760 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
761 , Constraint_Type1 Applicative (Type_Root_of_Expr root)
762 , Constraint_Type1 Traversable (Type_Root_of_Expr root)
763 , Root_of_Expr root ~ root
764 , IBool (Is_Last_Expr (Expr_Traversable lam root) root)
765 ) => Expr_from AST (Expr_Traversable lam root) where
766 expr_from ex ast ctx k =
768 AST "traverse" asts -> from_ast2 asts traverse_from ex ast ctx k
769 _ -> Left $ error_expr_unsupported ex ast
770 instance -- Expr_from AST Expr_Monad
771 ( Eq_Type (Type_Root_of_Expr root)
772 , Type1_from AST (Type_Root_of_Expr root)
774 , Lift_Type (Type_Fun lam) (Type_of_Expr root)
775 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
776 , Eq_Type1 (Type_Root_of_Expr root)
777 , Unlift_Type1 (Type_of_Expr root)
778 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
779 , Constraint_Type1 Monad (Type_Root_of_Expr root)
780 , Root_of_Expr root ~ root
781 , IBool (Is_Last_Expr (Expr_Monad lam root) root)
782 ) => Expr_from AST (Expr_Monad lam root) where
783 expr_from ex ast ctx k =
785 AST "return" asts -> from_ast2 asts return_from ex ast ctx k
786 AST ">>=" asts -> from_ast2 asts bind_from ex ast ctx k
787 _ -> Left $ error_expr_unsupported ex ast
788 instance -- Expr_from AST Expr_Either
789 ( Eq_Type (Type_Root_of_Expr root)
790 , Type_from AST (Type_Root_of_Expr root)
791 , Type1_from AST (Type_Root_of_Expr root)
793 , Eq_Type1 (Type_Root_of_Expr root)
794 , Unlift_Type1 (Type_of_Expr root)
795 , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
796 , Root_of_Expr root ~ root
797 , Lift_Type Type_Either (Type_of_Expr root)
798 , Unlift_Type Type_Either (Type_of_Expr root)
799 , IBool (Is_Last_Expr (Expr_Either root) root)
800 ) => Expr_from AST (Expr_Either root) where
801 expr_from ex ast ctx k =
803 AST "left" asts -> from_ast2 asts left_from ex ast ctx k
804 AST "right" asts -> from_ast2 asts right_from ex ast ctx k
805 _ -> Left $ error_expr_unsupported ex ast