|
28565
|
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 |