1 local open Ast; |
1 local open Ast; |
2 fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] = |
2 fun Gbigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] = |
3 fold_ast_p "κλ" (unfold_ast "_asms" asms, concl) |
3 fold_ast_p "κλ" (unfold_ast "_asms" asms, concl) |
4 | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; |
4 | Gbigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; |
5 fun impl_ast_tr' (*"κλ"*) asts = |
5 fun Glam_ast_tr (*"Glam"*) [idts, body] = |
|
6 fold_ast_p "_abs" (unfold_ast "_idts" idts, body) |
|
7 | Glam_ast_tr (*"Glam"*) asts = raise_ast "lambda_ast_tr" asts; |
|
8 |
|
9 fun Gimpl_ast_tr' (*"Gbigimpl"*) asts = |
6 (case unfold_ast_p "κλ" (Appl (Constant "κλ" :: asts)) of |
10 (case unfold_ast_p "κλ" (Appl (Constant "κλ" :: asts)) of |
7 (asms as _ :: _ :: _, concl) |
11 (asms as _ :: _ :: _, concl) |
8 => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl] |
12 => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl] |
9 | _ => raise Match); |
13 | _ => raise Match); |
10 |
|
11 in |
14 in |
12 val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr):: |
15 val parse_ast_translation = ("Gbigimpl", Gbigimpl_ast_tr):: |
13 ("Glam", fn asts => Appl (Constant "_abs" :: asts)):: |
16 ("Glam", Glam_ast_tr):: |
14 parse_ast_translation; |
17 parse_ast_translation; |
15 |
18 |
16 val print_ast_translation = ("κλ", impl_ast_tr'):: |
19 val print_ast_translation = ("κλ", Gimpl_ast_tr'):: |
17 ("_lambda", fn asts => Appl (Constant "Glam" :: asts)) :: |
20 ("_lambda", fn asts => |
|
21 Appl (Constant "Glam" :: asts)) :: |
18 print_ast_translation; |
22 print_ast_translation; |
19 |
23 |
20 end; |
24 end; |
21 |
25 |
22 local open Syntax in |
26 local open Syntax in |