author | wenzelm |
Wed, 29 Dec 2010 17:34:41 +0100 | |
changeset 41413 | 64cd30d6b0b8 |
parent 38321 | 7edf0ab9d5cb |
child 42224 | 578a51fae383 |
permissions | -rw-r--r-- |
28565 | 1 |
theory Setup |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
38321
diff
changeset
|
2 |
imports Main "~~/src/HOL/Library/Code_Integer" |
28565 | 3 |
uses |
38321 | 4 |
"../../antiquote_setup.ML" |
5 |
"../../more_antiquote.ML" |
|
28565 | 6 |
begin |
7 |
||
34071 | 8 |
setup {* Code_Target.set_default_code_width 74 *} |
28565 | 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] = |
|
35113 | 21 |
Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast] |
28565 | 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] = |
|
35113 | 26 |
Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast] |
28565 | 27 |
| beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
35113 | 28 |
in |
29 |
[(@{syntax_const "_alpha"}, alpha_ast_tr), |
|
30 |
(@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr), |
|
31 |
(@{syntax_const "_beta"}, beta_ast_tr), |
|
32 |
(@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)] |
|
33 |
end |
|
28565 | 34 |
*} |
35 |
||
36 |
end |