author | wenzelm |
Tue, 05 Apr 2011 14:25:18 +0200 | |
changeset 42224 | 578a51fae383 |
parent 41413 | 64cd30d6b0b8 |
child 43564 | 9864182c6bad |
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 |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
18 |
fun alpha_ast_tr [] = Ast.Variable "'a" |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
19 |
| alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts); |
28565 | 20 |
fun alpha_ofsort_ast_tr [ast] = |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
21 |
Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast] |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
22 |
| alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts); |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
23 |
fun beta_ast_tr [] = Ast.Variable "'b" |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
24 |
| beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts); |
28565 | 25 |
fun beta_ofsort_ast_tr [ast] = |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
26 |
Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast] |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
41413
diff
changeset
|
27 |
| beta_ofsort_ast_tr asts = raise Ast.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 |