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