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