]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/AST/Test.hs
init
[haskell/symantic.git] / Language / Symantic / AST / Test.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE GADTs #-}
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.
12 module AST.Test where
13
14 import Test.Tasty
15 -- import Test.Tasty.HUnit
16
17 import qualified Data.List as List
18 import Data.Proxy (Proxy(..))
19 import Data.Text (Text)
20 import qualified Data.Text as Text
21
22 import Language.Symantic.Lib.Data.Bool
23 import Language.Symantic.Type
24 import Language.Symantic.Expr as Expr
25
26 tests :: TestTree
27 tests = testGroup "AST" $
28 [
29 ]
30
31 -- * Type 'AST'
32 data AST
33 = AST Text [AST]
34 deriving (Eq)
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
40 case ast of
41 AST _ [] -> showString n
42 AST "->" [a] ->
43 showParen (p >= prec_arrow) $
44 showString ("("++n++") ") .
45 showsPrec prec_arrow a
46 AST "->" [a, b] ->
47 showParen (p >= prec_arrow) $
48 showsPrec prec_arrow a .
49 showString (" "++n++" ") .
50 showsPrec prec_arrow b
51 _ ->
52 showString n .
53 showString "(" .
54 showString (List.intercalate ", " $ show Prelude.<$> args) .
55 showString ")"
56 where prec_arrow = 1
57
58 -- ** Parsing utilities
59 from_ast0
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))
64 ) => [ast]
65 -> Expr_From ast ex hs ret
66 -> Expr_From ast ex hs ret
67 from_ast0 asts k' ex ast ctx k =
68 case asts of
69 [] -> k' ex ast ctx k
70 _ -> Left $ error_expr ex $
71 Error_Expr_Wrong_number_of_arguments ast 0
72
73 from_ast1
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 =
81 case asts of
82 [ast_0] -> k' ast_0 ex ast ctx k
83 _ -> Left $ error_expr ex $
84 Error_Expr_Wrong_number_of_arguments ast 1
85
86 from_ast2
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 =
94 case asts of
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
98
99 from_ast3
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 =
107 case asts of
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
111
112 lit_from_AST
113 :: forall root ty lit ex ast hs ret.
114 ( ty ~ Type_Root_of_Expr ex
115 , root ~ Root_of_Expr ex
116 , ast ~ AST
117 , Read lit
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)
121 -> ty lit -> [ast]
122 -> Expr_From ast ex hs ret
123 lit_from_AST op ty_lit asts ex ast ctx k =
124 case asts of
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
128
129 op1_from_AST
130 :: forall root ty lit ex ast hs ret.
131 ( ty ~ Type_Root_of_Expr ex
132 , root ~ Root_of_Expr ex
133 , ast ~ AST
134 , Eq_Type (Type_Root_of_Expr root)
135 , Expr_from ast 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)
140 -> ty lit -> [ast]
141 -> Expr_From ast ex hs ret
142 op1_from_AST op ty_lit asts ex ast ctx k =
143 case asts of
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
147
148 op2_from_AST
149 :: forall root ty lit ex ast hs ret.
150 ( ty ~ Type_Root_of_Expr ex
151 , root ~ Root_of_Expr ex
152 , ast ~ AST
153 , Eq_Type (Type_Root_of_Expr root)
154 , Expr_from ast 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)
159 -> ty lit -> [ast]
160 -> Expr_From ast ex hs ret
161 op2_from_AST op ty_lit asts ex ast ctx k =
162 case asts of
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
166
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
186 type_from ty ast k =
187 case ast of
188 AST "()" asts ->
189 case asts of
190 [] -> k type_unit
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
199 type_from ty ast k =
200 case ast of
201 AST "Bool" asts ->
202 case asts of
203 [] -> k type_bool
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
212 type_from ty ast k =
213 case ast of
214 AST "Int" asts ->
215 case asts of
216 [] -> k type_int
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
225 type_from ty ast k =
226 case ast of
227 AST "Ordering" asts ->
228 case asts of
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
234 ( Eq_Type root
235 , Type_from AST root
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
242 type_from ty ast k =
243 case ast of
244 AST "->" asts ->
245 case asts of
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
251 ( Eq_Type root
252 , Type_from AST root
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
259 type_from ty ast k =
260 case ast of
261 AST "Maybe" asts ->
262 case asts of
263 [ast_a] ->
264 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
265 k (type_maybe 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
270 ( Eq_Type root
271 , Type_from AST root
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
278 type_from ty ast k =
279 case ast of
280 AST "[]" asts ->
281 case asts of
282 [ast_a] ->
283 type_from (Proxy::Proxy root) ast_a $ \ty_a ->
284 k (type_list 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
289 ( Eq_Type root
290 , Type_from AST root
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
298 type_from ty ast k =
299 case ast of
300 AST "Map" asts ->
301 case asts of
302 [ast_k, ast_a] ->
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
311 ( Eq_Type root
312 , Type_from AST root
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
319 type_from ty ast k =
320 case ast of
321 AST "(,)" asts ->
322 case asts of
323 [ast_a, ast_b] ->
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
331 ( Eq_Type root
332 , Type_from AST root
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
339 type_from ty ast k =
340 case ast of
341 AST "Either" asts ->
342 case asts of
343 [ast_l, ast_r] ->
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
350
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
376 ( Type_from AST root
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 =
384 case ast of
385 AST "Maybe" asts ->
386 case asts of
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
392 ( Eq_Type root
393 , Type_from AST root
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 =
401 case ast of
402 AST "[]" asts ->
403 case asts of
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
409 ( Eq_Type root
410 , Type_from AST root
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 =
418 case ast of
419 AST "->" asts ->
420 case asts of
421 [ast_arg] ->
422 type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
423 k (Proxy::Proxy (Lambda lam h_arg)) $
424 type_fun ty_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
429 ( Eq_Type root
430 , Type_from AST root
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 =
438 case ast of
439 AST "Either" asts ->
440 case asts of
441 [ast_l] ->
442 type_from (Proxy::Proxy root) ast_l $ \(ty_l::root h_l) ->
443 k (Proxy::Proxy (Either h_l)) $
444 type_either ty_l
445 _ -> Left $ lift_error_type $
446 Error_Type_Wrong_number_of_arguments ast 1
447 _ -> Left $ error_type_unsupported ty ast
448
449 instance -- Expr_from AST Expr_Bool
450 ( Eq_Type (Type_Root_of_Expr root)
451 , Expr_from AST 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
458 expr_from ex ast =
459 case ast of
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)
468 , Expr_from AST 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 =
475 case ast of
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)
480 , Expr_from AST 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 =
488 case ast of
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)
493 , Expr_from AST 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
500 expr_from ex ast =
501 case ast of
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)
513 , Expr_from AST 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 =
522 case ast of
523 AST "var" asts ->
524 case asts of
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)
533 , Expr_from AST 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 =
542 case ast of
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
546 where
547 go_lam asts
548 (lam::forall repr arg res. Sym_Lambda_Inline lam repr
549 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
550 case asts of
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
555 go_let asts
556 (let_::forall repr var res. Sym_Lambda_Inline lam repr
557 => repr var -> (repr var -> repr res) -> repr res) =
558 case asts of
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)
566 , Expr_from AST 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 =
575 case ast of
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
579 where
580 go_lam asts
581 (lam::forall repr arg res. Sym_Lambda_Val lam repr
582 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
583 case asts of
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
588 go_let asts
589 (let_::forall repr var res. Sym_Lambda_Val lam repr
590 => repr var -> (repr var -> repr res) -> repr res) =
591 case asts of
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)
599 , Expr_from AST 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 =
608 case ast of
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
612 where
613 go_lam asts
614 (lam::forall repr arg res. Sym_Lambda_Lazy lam repr
615 => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
616 case asts of
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
621 go_let asts
622 (let_::forall repr var res. Sym_Lambda_Lazy lam repr
623 => repr var -> (repr var -> repr res) -> repr res) =
624 case asts of
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)
632 , Expr_from AST 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 =
642 case ast of
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)
651 , Expr_from AST 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 =
657 case ast of
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)
664 , Expr_from AST 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 =
670 case ast of
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)
676 , Expr_from AST 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 =
687 case ast of
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
691 AST "list" asts ->
692 case asts of
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)
699 , Expr_from AST 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 =
714 case ast of
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)
720 , Expr_from AST 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 =
730 case ast of
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)
737 , Expr_from AST 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 =
748 case ast of
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)
755 , Expr_from AST 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 =
767 case ast of
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)
773 , Expr_from AST 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 =
784 case ast of
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)
792 , Expr_from AST 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 =
802 case ast of
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