author | haftmann |
Fri, 19 Jun 2009 17:23:21 +0200 | |
changeset 31723 | f5cafe803b55 |
parent 31597 | 9a59cf39ee78 |
child 35743 | c506c029a082 |
permissions | -rw-r--r-- |
19459 | 1 |
(* Title: HOL/Tools/typedef_codegen.ML |
31597 | 2 |
Author: Stefan Berghofer, TU Muenchen |
19459 | 3 |
|
4 |
Code generators for trivial typedefs. |
|
5 |
*) |
|
6 |
||
7 |
signature TYPEDEF_CODEGEN = |
|
8 |
sig |
|
20428 | 9 |
val setup: theory -> theory |
19459 | 10 |
end; |
11 |
||
12 |
structure TypedefCodegen: TYPEDEF_CODEGEN = |
|
13 |
struct |
|
14 |
||
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
15 |
fun typedef_codegen thy defs dep module brack t gr = |
19459 | 16 |
let |
17 |
fun get_name (Type (tname, _)) = tname |
|
18 |
| get_name _ = ""; |
|
19 |
fun mk_fun s T ts = |
|
20 |
let |
|
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
21 |
val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr; |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
22 |
val (ps, gr'') = |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
23 |
fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr'; |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
24 |
val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s) |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
25 |
in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end; |
19459 | 26 |
fun lookup f T = |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31597
diff
changeset
|
27 |
(case Typedef.get_info thy (get_name T) of |
19459 | 28 |
NONE => "" |
19704 | 29 |
| SOME info => f info); |
19459 | 30 |
in |
31 |
(case strip_comb t of |
|
32 |
(Const (s, Type ("fun", [T, U])), ts) => |
|
19704 | 33 |
if lookup #Rep_name T = s andalso |
19459 | 34 |
is_none (Codegen.get_assoc_type thy (get_name T)) |
35 |
then mk_fun s T ts |
|
19704 | 36 |
else if lookup #Abs_name U = s andalso |
19459 | 37 |
is_none (Codegen.get_assoc_type thy (get_name U)) |
38 |
then mk_fun s U ts |
|
39 |
else NONE |
|
40 |
| _ => NONE) |
|
41 |
end; |
|
42 |
||
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
43 |
fun mk_tyexpr [] s = Codegen.str s |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
44 |
| mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)] |
19459 | 45 |
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
46 |
||
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
47 |
fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr = |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31597
diff
changeset
|
48 |
(case Typedef.get_info thy s of |
19459 | 49 |
NONE => NONE |
19704 | 50 |
| SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} => |
19459 | 51 |
if is_some (Codegen.get_assoc_type thy tname) then NONE else |
52 |
let |
|
53 |
val module' = Codegen.if_library |
|
27398
768da1da59d6
simplified retrieval of theory names of consts and types
haftmann
parents:
26975
diff
changeset
|
54 |
(Codegen.thyname_of_type thy tname) module; |
19459 | 55 |
val node_id = tname ^ " (type)"; |
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
56 |
val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map |
19459 | 57 |
(Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) |
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
58 |
Ts ||>> |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
59 |
Codegen.mk_const_id module' Abs_name ||>> |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
60 |
Codegen.mk_const_id module' Rep_name ||>> |
19459 | 61 |
Codegen.mk_type_id module' s; |
62 |
val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id) |
|
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
63 |
in SOME (tyexpr, case try (Codegen.get_node gr') node_id of |
19459 | 64 |
NONE => |
65 |
let |
|
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
66 |
val (p :: ps, gr'') = fold_map |
19459 | 67 |
(Codegen.invoke_tycodegen thy defs node_id module' false) |
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
68 |
(oldT :: Us) (Codegen.add_edge (node_id, dep) |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
69 |
(Codegen.new_node (node_id, (NONE, "", "")) gr')); |
19459 | 70 |
val s = |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
71 |
Codegen.string_of (Pretty.block [Codegen.str "datatype ", |
19459 | 72 |
mk_tyexpr ps (snd ty_id), |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
73 |
Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"), |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
74 |
Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^ |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
75 |
Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
76 |
Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
77 |
Codegen.str "x) = x;"]) ^ "\n\n" ^ |
19459 | 78 |
(if "term_of" mem !Codegen.mode then |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
79 |
Codegen.string_of (Pretty.block [Codegen.str "fun ", |
19459 | 80 |
Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
81 |
Codegen.str ("(" ^ Abs_id), Pretty.brk 1, |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
82 |
Codegen.str "x) =", Pretty.brk 1, |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
83 |
Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","), |
19459 | 84 |
Pretty.brk 1, Codegen.mk_type false (oldT --> newT), |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
85 |
Codegen.str ")"], Codegen.str " $", Pretty.brk 1, |
19459 | 86 |
Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
87 |
Codegen.str "x;"]) ^ "\n\n" |
19459 | 88 |
else "") ^ |
89 |
(if "test" mem !Codegen.mode then |
|
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
90 |
Codegen.string_of (Pretty.block [Codegen.str "fun ", |
19459 | 91 |
Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
92 |
Codegen.str "i =", Pretty.brk 1, |
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
93 |
Pretty.block [Codegen.str (Abs_id ^ " ("), |
19459 | 94 |
Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1, |
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset
|
95 |
Codegen.str "i);"]]) ^ "\n\n" |
19459 | 96 |
else "") |
97 |
in Codegen.map_node node_id (K (NONE, module', s)) gr'' end |
|
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
98 |
| SOME _ => Codegen.add_edge (node_id, dep) gr') |
19459 | 99 |
end) |
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset
|
100 |
| typedef_tycodegen thy defs dep module brack _ gr = NONE; |
19459 | 101 |
|
102 |
val setup = |
|
103 |
Codegen.add_codegen "typedef" typedef_codegen |
|
104 |
#> Codegen.add_tycodegen "typedef" typedef_tycodegen |
|
105 |
||
106 |
end; |