1 theory Setup |
|
2 imports Main Code_Integer |
|
3 uses |
|
4 "../../../antiquote_setup" |
|
5 "../../../more_antiquote" |
|
6 begin |
|
7 |
|
8 ML {* Code_Target.code_width := 74 *} |
|
9 |
|
10 syntax |
|
11 "_alpha" :: "type" ("\<alpha>") |
|
12 "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000) |
|
13 "_beta" :: "type" ("\<beta>") |
|
14 "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000) |
|
15 |
|
16 parse_ast_translation {* |
|
17 let |
|
18 fun alpha_ast_tr [] = Syntax.Variable "'a" |
|
19 | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
|
20 fun alpha_ofsort_ast_tr [ast] = |
|
21 Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast] |
|
22 | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
|
23 fun beta_ast_tr [] = Syntax.Variable "'b" |
|
24 | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
|
25 fun beta_ofsort_ast_tr [ast] = |
|
26 Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast] |
|
27 | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
|
28 in [ |
|
29 ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr), |
|
30 ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr) |
|
31 ] end |
|
32 *} |
|
33 |
|
34 end |
|