16 parse_ast_translation {* |
16 parse_ast_translation {* |
17 let |
17 let |
18 fun alpha_ast_tr [] = Syntax.Variable "'a" |
18 fun alpha_ast_tr [] = Syntax.Variable "'a" |
19 | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
19 | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
20 fun alpha_ofsort_ast_tr [ast] = |
20 fun alpha_ofsort_ast_tr [ast] = |
21 Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast] |
21 Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast] |
22 | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
22 | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
23 fun beta_ast_tr [] = Syntax.Variable "'b" |
23 fun beta_ast_tr [] = Syntax.Variable "'b" |
24 | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
24 | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
25 fun beta_ofsort_ast_tr [ast] = |
25 fun beta_ofsort_ast_tr [ast] = |
26 Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast] |
26 Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast] |
27 | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
27 | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
28 in [ |
28 in |
29 ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr), |
29 [(@{syntax_const "_alpha"}, alpha_ast_tr), |
30 ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr) |
30 (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr), |
31 ] end |
31 (@{syntax_const "_beta"}, beta_ast_tr), |
|
32 (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)] |
|
33 end |
32 *} |
34 *} |
33 |
35 |
34 end |
36 end |