19459
|
1 |
(* Title: HOL/Tools/typedef_codegen.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer and Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Code generators for trivial typedefs.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature TYPEDEF_CODEGEN =
|
|
9 |
sig
|
20428
|
10 |
val setup: theory -> theory
|
19459
|
11 |
end;
|
|
12 |
|
|
13 |
structure TypedefCodegen: TYPEDEF_CODEGEN =
|
|
14 |
struct
|
|
15 |
|
|
16 |
fun typedef_codegen thy defs gr dep module brack t =
|
|
17 |
let
|
|
18 |
fun get_name (Type (tname, _)) = tname
|
|
19 |
| get_name _ = "";
|
|
20 |
fun mk_fun s T ts =
|
|
21 |
let
|
|
22 |
val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
|
|
23 |
val (gr'', ps) =
|
|
24 |
foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
|
|
25 |
val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
|
|
26 |
in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
|
|
27 |
fun lookup f T =
|
19704
|
28 |
(case TypedefPackage.get_info thy (get_name T) of
|
19459
|
29 |
NONE => ""
|
19704
|
30 |
| SOME info => f info);
|
19459
|
31 |
in
|
|
32 |
(case strip_comb t of
|
|
33 |
(Const (s, Type ("fun", [T, U])), ts) =>
|
19704
|
34 |
if lookup #Rep_name T = s andalso
|
19459
|
35 |
is_none (Codegen.get_assoc_type thy (get_name T))
|
|
36 |
then mk_fun s T ts
|
19704
|
37 |
else if lookup #Abs_name U = s andalso
|
19459
|
38 |
is_none (Codegen.get_assoc_type thy (get_name U))
|
|
39 |
then mk_fun s U ts
|
|
40 |
else NONE
|
|
41 |
| _ => NONE)
|
|
42 |
end;
|
|
43 |
|
|
44 |
fun mk_tyexpr [] s = Pretty.str s
|
|
45 |
| mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
|
|
46 |
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
|
|
47 |
|
|
48 |
fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
|
19704
|
49 |
(case TypedefPackage.get_info thy s of
|
19459
|
50 |
NONE => NONE
|
19704
|
51 |
| SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
|
19459
|
52 |
if is_some (Codegen.get_assoc_type thy tname) then NONE else
|
|
53 |
let
|
|
54 |
val module' = Codegen.if_library
|
|
55 |
(Codegen.thyname_of_type tname thy) module;
|
|
56 |
val node_id = tname ^ " (type)";
|
|
57 |
val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
|
|
58 |
(Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
|
|
59 |
(gr, Ts) |>>>
|
|
60 |
Codegen.mk_const_id module' Abs_name |>>>
|
|
61 |
Codegen.mk_const_id module' Rep_name |>>>
|
|
62 |
Codegen.mk_type_id module' s;
|
|
63 |
val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
|
|
64 |
in SOME (case try (Codegen.get_node gr') node_id of
|
|
65 |
NONE =>
|
|
66 |
let
|
|
67 |
val (gr'', p :: ps) = foldl_map
|
|
68 |
(Codegen.invoke_tycodegen thy defs node_id module' false)
|
|
69 |
(Codegen.add_edge (node_id, dep)
|
|
70 |
(Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
|
|
71 |
val s =
|
|
72 |
Pretty.string_of (Pretty.block [Pretty.str "datatype ",
|
|
73 |
mk_tyexpr ps (snd ty_id),
|
|
74 |
Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
|
|
75 |
Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
|
|
76 |
Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
|
|
77 |
Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
|
|
78 |
Pretty.str "x) = x;"]) ^ "\n\n" ^
|
|
79 |
(if "term_of" mem !Codegen.mode then
|
|
80 |
Pretty.string_of (Pretty.block [Pretty.str "fun ",
|
|
81 |
Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
|
|
82 |
Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
|
|
83 |
Pretty.str "x) =", Pretty.brk 1,
|
|
84 |
Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
|
|
85 |
Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
|
|
86 |
Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
|
|
87 |
Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
|
|
88 |
Pretty.str "x;"]) ^ "\n\n"
|
|
89 |
else "") ^
|
|
90 |
(if "test" mem !Codegen.mode then
|
|
91 |
Pretty.string_of (Pretty.block [Pretty.str "fun ",
|
|
92 |
Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
|
|
93 |
Pretty.str "i =", Pretty.brk 1,
|
|
94 |
Pretty.block [Pretty.str (Abs_id ^ " ("),
|
|
95 |
Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
|
|
96 |
Pretty.str "i);"]]) ^ "\n\n"
|
|
97 |
else "")
|
|
98 |
in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
|
|
99 |
| SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
|
|
100 |
end)
|
|
101 |
| typedef_tycodegen thy defs gr dep module brack _ = NONE;
|
|
102 |
|
|
103 |
val setup =
|
|
104 |
Codegen.add_codegen "typedef" typedef_codegen
|
|
105 |
#> Codegen.add_tycodegen "typedef" typedef_tycodegen
|
|
106 |
|
|
107 |
end;
|