author | haftmann |
Wed, 28 Dec 2005 21:14:23 +0100 | |
changeset 18516 | 4424e2bce9af |
parent 18515 | 1cad5c2b2a0b |
child 18517 | 788fa99aba33 |
permissions | -rw-r--r-- |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
1 |
(* Title: Pure/Tools/codegen_package.ML |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
2 |
ID: $Id$ |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
4 |
|
18217 | 5 |
Code generator from Isabelle theories to |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
6 |
intermediate language ("Thin-gol"). |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
7 |
*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
8 |
|
18282 | 9 |
(*NOTE: for simplifying developement, this package contains |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
10 |
some stuff which will finally be moved upwards to HOL*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
11 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
12 |
signature CODEGEN_PACKAGE = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
13 |
sig |
18454 | 14 |
type auxtab; |
18335 | 15 |
type appgen; |
18217 | 16 |
type defgen; |
18516 | 17 |
val add_appconst: string * ((int * int) * appgen) -> theory -> theory; |
18 |
val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory; |
|
18335 | 19 |
val add_appgen: string * appgen -> theory -> theory; |
18217 | 20 |
val add_defgen: string * defgen -> theory -> theory; |
21 |
val add_lookup_tyco: string * string -> theory -> theory; |
|
22 |
val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory; |
|
18516 | 23 |
val add_syntax_tyco: string -> (xstring * string * CodegenSerializer.fixity) |
18217 | 24 |
* (string option * (string * string list)) option |
25 |
-> theory -> theory; |
|
18516 | 26 |
val add_syntax_tyco_i: string -> (string * CodegenThingol.itype Codegen.mixfix list * CodegenSerializer.fixity) |
18217 | 27 |
* (string * (string * string list)) option |
28 |
-> theory -> theory; |
|
18516 | 29 |
val add_syntax_const: string -> ((xstring * string option) * string * CodegenSerializer.fixity) |
18217 | 30 |
* (string option * (string * string list)) option |
31 |
-> theory -> theory; |
|
18516 | 32 |
val add_syntax_const_i: string -> ((string * typ) * CodegenThingol.iexpr Codegen.mixfix list * CodegenSerializer.fixity) |
18217 | 33 |
* (string * (string * string list)) option |
34 |
-> theory -> theory; |
|
18516 | 35 |
val add_prim_class: xstring -> (string * string) -> string list |
36 |
-> theory -> theory; |
|
37 |
val add_prim_tyco: xstring -> (string * string) -> string list |
|
38 |
-> theory -> theory; |
|
39 |
val add_prim_const: xstring * string -> (string * string) -> string list |
|
40 |
-> theory -> theory; |
|
41 |
val add_prim_i: string -> (string * Pretty.T) -> string list |
|
42 |
-> theory -> theory; |
|
18217 | 43 |
val add_alias: string * string -> theory -> theory; |
44 |
val set_is_datatype: (theory -> string -> bool) -> theory -> theory; |
|
18455 | 45 |
val set_get_all_datatype_cons : (theory -> (string * string) list) |
18454 | 46 |
-> theory -> theory; |
18217 | 47 |
|
18516 | 48 |
val exprgen_type: theory -> auxtab |
18217 | 49 |
-> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact; |
18516 | 50 |
val exprgen_term: theory -> auxtab |
18217 | 51 |
-> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; |
18454 | 52 |
val ensure_def_tyco: theory -> auxtab |
18217 | 53 |
-> string -> CodegenThingol.transact -> string * CodegenThingol.transact; |
18454 | 54 |
val ensure_def_const: theory -> auxtab |
55 |
-> string * typ -> CodegenThingol.transact -> string * CodegenThingol.transact; |
|
18217 | 56 |
|
18335 | 57 |
val appgen_let: (int -> term -> term list * term) |
58 |
-> appgen; |
|
59 |
val appgen_split: (int -> term -> term list * term) |
|
60 |
-> appgen; |
|
61 |
val appgen_number_of: (term -> IntInf.int) -> (term -> term) |
|
62 |
-> appgen; |
|
63 |
val appgen_case: (theory -> string -> (string * int) list option) |
|
64 |
-> appgen; |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
65 |
val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option) |
18335 | 66 |
-> (theory -> string * string -> typ list option) |
18217 | 67 |
-> defgen; |
68 |
val defgen_datacons: (theory -> string * string -> typ list option) |
|
69 |
-> defgen; |
|
70 |
val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ) |
|
71 |
-> defgen; |
|
72 |
||
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
73 |
val print_codegen_generated: theory -> unit; |
18454 | 74 |
val rename_inconsistent: theory -> theory; |
18515 | 75 |
|
76 |
(*debugging purpose only*) |
|
18454 | 77 |
structure InstNameMangler: NAME_MANGLER; |
78 |
structure ConstNameMangler: NAME_MANGLER; |
|
79 |
structure DatatypeconsNameMangler: NAME_MANGLER; |
|
18231 | 80 |
structure CodegenData: THEORY_DATA; |
18454 | 81 |
val mk_tabs: theory -> auxtab; |
82 |
val alias_get: theory -> string -> string; |
|
18515 | 83 |
val idf_of_name: theory -> string -> string -> string; |
84 |
val idf_of_const: theory -> auxtab -> string * typ -> string; |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
85 |
end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
86 |
|
18217 | 87 |
structure CodegenPackage : CODEGEN_PACKAGE = |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
88 |
struct |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
89 |
|
18385 | 90 |
open CodegenThingolOp; |
91 |
infix 8 `%%; |
|
92 |
infixr 6 `->; |
|
93 |
infixr 6 `-->; |
|
94 |
infix 4 `$; |
|
95 |
infix 4 `$$; |
|
96 |
infixr 5 `|->; |
|
97 |
infixr 5 `|-->; |
|
18217 | 98 |
|
99 |
(* auxiliary *) |
|
100 |
||
18454 | 101 |
fun devarify_type ty = (fst o Type.freeze_thaw_type) ty; |
18335 | 102 |
fun devarify_term t = (fst o Type.freeze_thaw) t; |
18454 | 103 |
|
104 |
val is_number = is_some o Int.fromString; |
|
18217 | 105 |
|
18361 | 106 |
fun newline_correct s = |
107 |
s |
|
108 |
|> space_explode "\n" |
|
109 |
|> map (implode o (fn [] => [] |
|
110 |
| (" "::xs) => xs |
|
111 |
| xs => xs) o explode) |
|
112 |
|> space_implode "\n"; |
|
18217 | 113 |
|
114 |
||
18454 | 115 |
(* shallo name spaces *) |
18217 | 116 |
|
117 |
val nsp_class = "class"; |
|
18454 | 118 |
val nsp_tyco = "tyco"; |
18217 | 119 |
val nsp_const = "const"; |
18454 | 120 |
val nsp_overl = "overl"; |
121 |
val nsp_dtcon = "dtcon"; |
|
18217 | 122 |
val nsp_mem = "mem"; |
123 |
val nsp_inst = "inst"; |
|
18385 | 124 |
val nsp_eq_inst = "eq_inst"; |
125 |
val nsp_eq_pred = "eq"; |
|
18217 | 126 |
|
127 |
||
18454 | 128 |
(* code generator data types *) |
129 |
||
130 |
structure InstNameMangler = NameManglerFun ( |
|
131 |
type ctxt = theory; |
|
132 |
type src = string * (class * string); |
|
133 |
val ord = prod_ord string_ord (prod_ord string_ord string_ord); |
|
134 |
fun mk thy ((thyname, (cls, tyco)), i) = |
|
135 |
NameSpace.base cls ^ "_" ^ NameSpace.base tyco ^ implode (replicate i "'") |
|
136 |
|> NameSpace.append thyname; |
|
137 |
fun is_valid _ _ = true; |
|
138 |
fun maybe_unique _ _ = NONE; |
|
139 |
fun re_mangle _ dst = error ("no such instance: " ^ quote dst); |
|
140 |
); |
|
141 |
||
142 |
structure ConstNameMangler = NameManglerFun ( |
|
143 |
type ctxt = theory; |
|
144 |
type src = string * (typ * typ); |
|
145 |
val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord); |
|
146 |
fun mk thy ((c, (ty_decl, ty)), i) = |
|
147 |
let |
|
148 |
fun mangle (Type (tyco, tys)) = |
|
149 |
NameSpace.base tyco :: Library.flat (List.mapPartial mangle tys) |> SOME |
|
150 |
| mangle _ = |
|
151 |
NONE |
|
152 |
in |
|
153 |
Vartab.empty |
|
154 |
|> Sign.typ_match thy (ty_decl, ty) |
|
155 |
|> map (snd o snd) o Vartab.dest |
|
156 |
|> List.mapPartial mangle |
|
157 |
|> Library.flat |
|
158 |
|> null ? K ["x"] |
|
159 |
|> cons c |
|
160 |
|> space_implode "_" |
|
161 |
|> curry (op ^ o swap) ((implode oo replicate) i "'") |
|
162 |
end; |
|
163 |
fun is_valid _ _ = true; |
|
164 |
fun maybe_unique _ _ = NONE; |
|
165 |
fun re_mangle _ dst = error ("no such constant: " ^ quote dst); |
|
166 |
); |
|
167 |
||
168 |
structure DatatypeconsNameMangler = NameManglerFun ( |
|
169 |
type ctxt = theory; |
|
170 |
type src = string * string; |
|
171 |
val ord = prod_ord string_ord string_ord; |
|
172 |
fun mk thy (("0", "nat"), _) = |
|
173 |
"Nat.Zero" |
|
174 |
| mk thy ((co, dtco), i) = |
|
175 |
let |
|
176 |
fun basename 0 = NameSpace.base co |
|
18455 | 177 |
| basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co |
18454 | 178 |
| basename i = NameSpace.base dtco ^ "_" ^ NameSpace.base co ^ "_" ^ (implode oo replicate) (i-1) "'"; |
179 |
fun strip_dtco name = |
|
180 |
case (rev o NameSpace.unpack) name |
|
181 |
of x1::x2::xs => |
|
182 |
if x2 = NameSpace.base dtco |
|
183 |
then NameSpace.pack (x1::xs) |
|
184 |
else name |
|
185 |
| _ => name; |
|
186 |
in |
|
187 |
NameSpace.append (NameSpace.drop_base dtco) (basename i) |
|
188 |
|> strip_dtco |
|
189 |
end; |
|
190 |
fun is_valid _ _ = true; |
|
191 |
fun maybe_unique _ _ = NONE; |
|
192 |
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); |
|
193 |
); |
|
194 |
||
195 |
type auxtab = ((typ * (term list * term)) Symtab.table * string Symtab.table) |
|
196 |
* (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); |
|
197 |
||
198 |
type appgen = theory -> auxtab -> ((string * typ) * term list, iexpr) gen_exprgen; |
|
199 |
type defgen = theory -> auxtab -> gen_defgen; |
|
200 |
||
201 |
||
18217 | 202 |
(* serializer *) |
203 |
||
204 |
val serializer_ml = |
|
205 |
let |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
206 |
val name_root = "Generated"; |
18282 | 207 |
val nsp_conn = [ |
18454 | 208 |
[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_eq_inst, nsp_eq_pred] |
18217 | 209 |
]; |
18516 | 210 |
in CodegenSerializer.ml_from_thingol nsp_conn nsp_class name_root end; |
18217 | 211 |
|
18282 | 212 |
val serializer_hs = |
213 |
let |
|
214 |
val name_root = "Generated"; |
|
215 |
val nsp_conn = [ |
|
18454 | 216 |
[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem, nsp_eq_pred], [nsp_dtcon], [nsp_inst, nsp_eq_inst] |
18282 | 217 |
]; |
18516 | 218 |
in CodegenSerializer.haskell_from_thingol nsp_conn nsp_dtcon name_root end; |
18217 | 219 |
|
220 |
||
18454 | 221 |
(* theory data for code generator *) |
18217 | 222 |
|
223 |
type gens = { |
|
18516 | 224 |
appconst: ((int * int) * (appgen * stamp)) Symtab.table, |
18335 | 225 |
appgens: (string * (appgen * stamp)) list, |
18217 | 226 |
defgens: (string * (defgen * stamp)) list |
227 |
}; |
|
228 |
||
18516 | 229 |
fun map_gens f { appconst, appgens, defgens } = |
18217 | 230 |
let |
18516 | 231 |
val (appconst, appgens, defgens) = |
232 |
f (appconst, appgens, defgens) |
|
233 |
in { appconst = appconst, appgens = appgens, defgens = defgens } : gens end; |
|
18217 | 234 |
|
235 |
fun merge_gens |
|
18516 | 236 |
({ appconst = appconst1 , appgens = appgens1, defgens = defgens1 }, |
237 |
{ appconst = appconst2 , appgens = appgens2, defgens = defgens2 }) = |
|
238 |
{ appconst = Symtab.merge |
|
239 |
(fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2) |
|
240 |
(appconst1, appconst2), |
|
18335 | 241 |
appgens = AList.merge (op =) (eq_snd (op =)) (appgens1, appgens2), |
18304 | 242 |
defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens; |
18217 | 243 |
|
244 |
type lookups = { |
|
245 |
lookups_tyco: string Symtab.table, |
|
246 |
lookups_const: (typ * iexpr) list Symtab.table |
|
247 |
} |
|
248 |
||
249 |
fun map_lookups f { lookups_tyco, lookups_const } = |
|
250 |
let |
|
251 |
val (lookups_tyco, lookups_const) = |
|
252 |
f (lookups_tyco, lookups_const) |
|
18454 | 253 |
in { lookups_tyco = lookups_tyco, lookups_const = lookups_const } : lookups end; |
18217 | 254 |
|
255 |
fun merge_lookups |
|
256 |
({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 }, |
|
257 |
{ lookups_tyco = lookups_tyco2, lookups_const = lookups_const2 }) = |
|
258 |
{ lookups_tyco = Symtab.merge (op =) (lookups_tyco1, lookups_tyco2), |
|
18304 | 259 |
lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) } : lookups; |
18217 | 260 |
|
261 |
type logic_data = { |
|
262 |
is_datatype: ((theory -> string -> bool) * stamp) option, |
|
18455 | 263 |
get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option, |
18217 | 264 |
alias: string Symtab.table * string Symtab.table |
265 |
}; |
|
266 |
||
18454 | 267 |
fun map_logic_data f { is_datatype, get_all_datatype_cons, alias } = |
18217 | 268 |
let |
18454 | 269 |
val ((is_datatype, get_all_datatype_cons), alias) = |
270 |
f ((is_datatype, get_all_datatype_cons), alias) |
|
271 |
in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, alias = alias } : logic_data end; |
|
18217 | 272 |
|
273 |
fun merge_logic_data |
|
18454 | 274 |
({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, alias = alias1 }, |
275 |
{ is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, alias = alias2 }) = |
|
18217 | 276 |
let |
277 |
fun merge_opt _ (x1, NONE) = x1 |
|
278 |
| merge_opt _ (NONE, x2) = x2 |
|
279 |
| merge_opt eq (SOME x1, SOME x2) = |
|
280 |
if eq (x1, x2) then SOME x1 else error ("incompatible options during merge"); |
|
281 |
in |
|
282 |
{ is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2), |
|
18454 | 283 |
get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2), |
18217 | 284 |
alias = (Symtab.merge (op =) (fst alias1, fst alias2), |
18304 | 285 |
Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data |
18217 | 286 |
end; |
287 |
||
288 |
type serialize_data = { |
|
289 |
serializer: CodegenSerializer.serializer, |
|
290 |
primitives: CodegenSerializer.primitives, |
|
18516 | 291 |
syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, |
292 |
syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table |
|
18217 | 293 |
}; |
294 |
||
295 |
fun map_serialize_data f { serializer, primitives, syntax_tyco, syntax_const } = |
|
296 |
let |
|
297 |
val (primitives, syntax_tyco, syntax_const) = |
|
298 |
f (primitives, syntax_tyco, syntax_const) |
|
299 |
in { serializer = serializer, primitives = primitives, |
|
18454 | 300 |
syntax_tyco = syntax_tyco, syntax_const = syntax_const } : serialize_data |
301 |
end; |
|
18217 | 302 |
|
303 |
fun merge_serialize_data |
|
304 |
({ serializer = serializer, primitives = primitives1, |
|
305 |
syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, |
|
18282 | 306 |
{serializer = _, primitives = primitives2, |
18217 | 307 |
syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = |
308 |
{ serializer = serializer, |
|
309 |
primitives = CodegenSerializer.merge_prims (primitives1, primitives2) : CodegenSerializer.primitives, |
|
18516 | 310 |
syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), |
311 |
syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : serialize_data; |
|
18217 | 312 |
|
313 |
structure CodegenData = TheoryDataFun |
|
314 |
(struct |
|
315 |
val name = "Pure/codegen_package"; |
|
316 |
type T = { |
|
317 |
modl: module, |
|
318 |
gens: gens, |
|
319 |
lookups: lookups, |
|
320 |
logic_data: logic_data, |
|
321 |
serialize_data: serialize_data Symtab.table |
|
322 |
}; |
|
323 |
val empty = { |
|
324 |
modl = empty_module, |
|
18516 | 325 |
gens = { appconst = Symtab.empty, appgens = [], defgens = [] } : gens, |
18217 | 326 |
lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups, |
18454 | 327 |
logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE, |
328 |
alias = (Symtab.empty, Symtab.empty) } : logic_data, |
|
18217 | 329 |
serialize_data = |
330 |
Symtab.empty |
|
331 |
|> Symtab.update ("ml", |
|
18231 | 332 |
{ serializer = serializer_ml : CodegenSerializer.serializer, |
18217 | 333 |
primitives = |
334 |
CodegenSerializer.empty_prims |
|
18385 | 335 |
|> CodegenSerializer.add_prim ("Eq", ("type 'a Eq = {eq: 'a -> 'a -> bool};", [])) |
18217 | 336 |
|> CodegenSerializer.add_prim ("fst", ("fun fst (x, _) = x;", [])) |
337 |
|> CodegenSerializer.add_prim ("snd", ("fun snd (_, y) = y;", [])) |
|
338 |
|> CodegenSerializer.add_prim ("wfrec", ("fun wfrec f x = f (wfrec f) x;", [])), |
|
339 |
syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |
|
340 |
|> Symtab.update ("haskell", |
|
18335 | 341 |
{ serializer = serializer_hs : CodegenSerializer.serializer, |
342 |
primitives = |
|
343 |
CodegenSerializer.empty_prims |
|
344 |
|> CodegenSerializer.add_prim ("wfrec", ("wfrec f x = f (wfrec f) x", [])), |
|
18217 | 345 |
syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |
346 |
} : T; |
|
347 |
val copy = I; |
|
348 |
val extend = I; |
|
349 |
fun merge _ ( |
|
350 |
{ modl = modl1, gens = gens1, lookups = lookups1, |
|
351 |
serialize_data = serialize_data1, logic_data = logic_data1 }, |
|
352 |
{ modl = modl2, gens = gens2, lookups = lookups2, |
|
353 |
serialize_data = serialize_data2, logic_data = logic_data2 } |
|
354 |
) = { |
|
355 |
modl = merge_module (modl1, modl2), |
|
356 |
gens = merge_gens (gens1, gens2), |
|
357 |
lookups = merge_lookups (lookups1, lookups2), |
|
358 |
logic_data = merge_logic_data (logic_data1, logic_data2), |
|
359 |
serialize_data = Symtab.join (K (merge_serialize_data #> SOME)) |
|
360 |
(serialize_data1, serialize_data2) |
|
361 |
}; |
|
362 |
fun print thy _ = writeln "sorry, this stuff is too complicated..."; |
|
363 |
end); |
|
364 |
||
365 |
fun map_codegen_data f thy = |
|
366 |
case CodegenData.get thy |
|
367 |
of { modl, gens, lookups, serialize_data, logic_data } => |
|
368 |
let val (modl, gens, lookups, serialize_data, logic_data) = |
|
369 |
f (modl, gens, lookups, serialize_data, logic_data) |
|
370 |
in CodegenData.put { modl = modl, gens = gens, lookups = lookups, |
|
371 |
serialize_data = serialize_data, logic_data = logic_data } thy end; |
|
372 |
||
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
373 |
val print_codegen_generated = writeln o Pretty.output o pretty_module o #modl o CodegenData.get; |
18217 | 374 |
|
18516 | 375 |
fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy = |
376 |
let |
|
377 |
val c = prep_const thy raw_c; |
|
378 |
in map_codegen_data |
|
18217 | 379 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
380 |
(modl, |
|
381 |
gens |> map_gens |
|
18516 | 382 |
(fn (appconst, appgens, defgens) => |
383 |
(appconst |
|
384 |
|> Symtab.update (c, (bounds, (ag, stamp ()))), |
|
385 |
appgens, defgens)), lookups, serialize_data, logic_data)) thy |
|
386 |
end; |
|
18217 | 387 |
|
18516 | 388 |
val add_appconst = gen_add_appconst Sign.intern_const; |
389 |
val add_appconst_i = gen_add_appconst (K I); |
|
18217 | 390 |
|
18335 | 391 |
fun add_appgen (name, ag) = |
392 |
map_codegen_data |
|
393 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
394 |
(modl, |
|
395 |
gens |> map_gens |
|
18516 | 396 |
(fn (appconst, appgens, defgens) => |
397 |
(appconst, appgens |
|
18335 | 398 |
|> Output.update_warn (op =) ("overwriting existing definition application generator " ^ name) (name, (ag, stamp ())), |
399 |
defgens)), lookups, serialize_data, logic_data)); |
|
400 |
||
18217 | 401 |
fun add_defgen (name, dg) = |
402 |
map_codegen_data |
|
403 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
404 |
(modl, |
|
405 |
gens |> map_gens |
|
18516 | 406 |
(fn (appconst, appgens, defgens) => |
407 |
(appconst, appgens, defgens |
|
18335 | 408 |
|> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))), |
18217 | 409 |
lookups, serialize_data, logic_data)); |
410 |
||
18454 | 411 |
fun get_defgens thy tabs = |
412 |
(map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy; |
|
18217 | 413 |
|
414 |
fun add_lookup_tyco (src, dst) = |
|
415 |
map_codegen_data |
|
416 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
417 |
(modl, gens, |
|
418 |
lookups |> map_lookups |
|
419 |
(fn (lookups_tyco, lookups_const) => |
|
420 |
(lookups_tyco |> Symtab.update_new (src, dst), |
|
18282 | 421 |
lookups_const)), |
18217 | 422 |
serialize_data, logic_data)); |
423 |
||
18454 | 424 |
val lookup_tyco = Symtab.lookup o #lookups_tyco o #lookups o CodegenData.get; |
425 |
||
18217 | 426 |
fun add_lookup_const ((src, ty), dst) = |
427 |
map_codegen_data |
|
428 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
429 |
(modl, gens, |
|
430 |
lookups |> map_lookups |
|
431 |
(fn (lookups_tyco, lookups_const) => |
|
432 |
(lookups_tyco, |
|
18282 | 433 |
lookups_const |> Symtab.update_multi (src, (ty, dst)))), |
18217 | 434 |
serialize_data, logic_data)); |
435 |
||
18454 | 436 |
fun lookup_const thy (f, ty) = |
437 |
(Symtab.lookup_multi o #lookups_const o #lookups o CodegenData.get) thy f |
|
438 |
|> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty); |
|
439 |
||
18217 | 440 |
fun set_is_datatype f = |
441 |
map_codegen_data |
|
442 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
443 |
(modl, gens, lookups, serialize_data, |
|
444 |
logic_data |
|
18454 | 445 |
|> map_logic_data ((apfst o apfst) (K (SOME (f, stamp ())))))); |
446 |
||
447 |
fun is_datatype thy = |
|
448 |
case (#is_datatype o #logic_data o CodegenData.get) thy |
|
449 |
of NONE => K false |
|
450 |
| SOME (f, _) => f thy; |
|
451 |
||
452 |
fun set_get_all_datatype_cons f = |
|
453 |
map_codegen_data |
|
454 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
455 |
(modl, gens, lookups, serialize_data, |
|
456 |
logic_data |
|
457 |
|> map_logic_data ((apfst o apsnd) (K (SOME (f, stamp ())))))); |
|
458 |
||
459 |
fun get_all_datatype_cons thy = |
|
460 |
case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy |
|
461 |
of NONE => [] |
|
462 |
| SOME (f, _) => f thy; |
|
18217 | 463 |
|
464 |
fun add_alias (src, dst) = |
|
465 |
map_codegen_data |
|
466 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
467 |
(modl, gens, lookups, serialize_data, |
|
468 |
logic_data |> map_logic_data |
|
469 |
(apsnd (fn (tab, tab_rev) => |
|
470 |
(tab |> Symtab.update (src, dst), |
|
471 |
tab_rev |> Symtab.update (dst, src)))))); |
|
472 |
||
473 |
||
18454 | 474 |
(* name handling *) |
18217 | 475 |
|
18454 | 476 |
val nsp_class = "class"; |
477 |
val nsp_tyco = "tyco"; |
|
478 |
val nsp_const = "const"; |
|
479 |
val nsp_overl = "overl"; |
|
480 |
val nsp_dtcon = "dtcon"; |
|
481 |
val nsp_mem = "mem"; |
|
482 |
val nsp_inst = "inst"; |
|
483 |
val nsp_eq_inst = "eq_inst"; |
|
484 |
val nsp_eq_pred = "eq"; |
|
18217 | 485 |
|
18454 | 486 |
val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get; |
487 |
val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get; |
|
18217 | 488 |
|
18454 | 489 |
fun add_nsp shallow name = |
490 |
name |
|
491 |
|> NameSpace.unpack |
|
492 |
|> split_last |
|
493 |
|> apsnd (single #> cons shallow) |
|
494 |
|> (op @) |
|
495 |
|> NameSpace.pack; |
|
496 |
fun dest_nsp nsp idf = |
|
18217 | 497 |
let |
498 |
val idf' = NameSpace.unpack idf; |
|
499 |
val (idf'', idf_base) = split_last idf'; |
|
500 |
val (modl, shallow) = split_last idf''; |
|
501 |
in |
|
502 |
if nsp = shallow |
|
18454 | 503 |
then (SOME o NameSpace.pack) (modl @ [idf_base]) |
18217 | 504 |
else NONE |
505 |
end; |
|
506 |
||
18454 | 507 |
fun idf_of_name thy shallow name = |
508 |
if is_number name |
|
509 |
then name |
|
18217 | 510 |
else |
18454 | 511 |
name |
512 |
|> alias_get thy |
|
513 |
|> add_nsp shallow; |
|
514 |
fun name_of_idf thy shallow idf = |
|
515 |
idf |
|
516 |
|> dest_nsp shallow |
|
517 |
|> Option.map (alias_rev thy); |
|
18217 | 518 |
|
18516 | 519 |
|
18454 | 520 |
(* code generator instantiation *) |
18217 | 521 |
|
18454 | 522 |
fun ensure_def_class thy tabs cls trns = |
523 |
let |
|
524 |
val cls' = idf_of_name thy nsp_class cls; |
|
525 |
in |
|
526 |
trns |
|
527 |
|> debug 4 (fn _ => "generating class " ^ quote cls) |
|
528 |
|> gen_ensure_def (get_defgens thy tabs) ("generating class " ^ quote cls) cls' |
|
529 |
|> pair cls' |
|
530 |
end; |
|
18217 | 531 |
|
18454 | 532 |
fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = |
533 |
let |
|
534 |
val thyname = (the o AList.lookup (op =) (ClassPackage.the_tycos thy cls)) tyco; |
|
535 |
val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); |
|
536 |
in |
|
537 |
trns |
|
538 |
|> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) |
|
539 |
|> gen_ensure_def (get_defgens thy tabs) ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst |
|
540 |
|> pair inst |
|
541 |
end; |
|
18335 | 542 |
|
18454 | 543 |
fun ensure_def_tyco thy tabs tyco trns = |
544 |
let |
|
545 |
val tyco' = idf_of_name thy nsp_tyco tyco; |
|
546 |
in case lookup_tyco thy tyco |
|
18217 | 547 |
of NONE => |
548 |
trns |
|
18231 | 549 |
|> debug 4 (fn _ => "generating type constructor " ^ quote tyco) |
18454 | 550 |
|> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco' |
551 |
|> pair tyco' |
|
18217 | 552 |
| SOME tyco => |
553 |
trns |
|
554 |
|> pair tyco |
|
18454 | 555 |
end; |
556 |
||
557 |
fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) = |
|
558 |
let |
|
18515 | 559 |
fun get_overloaded (c, ty) = |
560 |
case Symtab.lookup overltab1 c |
|
561 |
of SOME (ty_decl, tys) => |
|
562 |
(case find_first (curry (Sign.typ_instance thy) ty) tys |
|
563 |
of SOME ty' => ConstNameMangler.get thy overltab2 |
|
564 |
(idf_of_name thy nsp_overl c, (ty_decl, ty')) |> SOME |
|
565 |
| _ => NONE) |
|
566 |
| _ => NONE |
|
567 |
fun get_datatypecons (c, ty) = |
|
568 |
case (snd o strip_type) ty |
|
569 |
of Type (tyco, _) => |
|
570 |
try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco) |
|
571 |
| _ => NONE; |
|
572 |
in case get_overloaded (c, ty) |
|
573 |
of SOME idf => idf |
|
574 |
| NONE => case get_datatypecons (c, ty) |
|
575 |
of SOME c' => idf_of_name thy nsp_dtcon c' |
|
576 |
| NONE => case Symtab.lookup clsmemtab c |
|
577 |
of SOME _ => idf_of_name thy nsp_mem c |
|
578 |
| NONE => idf_of_name thy nsp_const c |
|
579 |
end; |
|
18217 | 580 |
|
18454 | 581 |
fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = |
582 |
case name_of_idf thy nsp_const idf |
|
583 |
of SOME c => SOME (c, Sign.the_const_constraint thy c) |
|
584 |
| NONE => ( |
|
585 |
case dest_nsp nsp_overl idf |
|
586 |
of SOME _ => |
|
587 |
idf |
|
588 |
|> ConstNameMangler.rev thy overltab2 |
|
589 |
|> apfst (the o name_of_idf thy nsp_overl) |
|
590 |
|> apsnd snd |
|
591 |
|> SOME |
|
592 |
| NONE => NONE |
|
593 |
); |
|
594 |
||
595 |
fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns = |
|
596 |
let |
|
597 |
val c' = idf_of_const thy tabs (c, ty); |
|
598 |
in case lookup_const thy (c, ty) |
|
18217 | 599 |
of NONE => |
600 |
trns |
|
18454 | 601 |
|> debug 4 (fn _ => "generating constant " ^ quote c) |
18516 | 602 |
|> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c' |
603 |
|> pair c' |
|
18454 | 604 |
| SOME (IConst (c, ty)) => |
18217 | 605 |
trns |
18454 | 606 |
|> pair c |
607 |
end; |
|
18217 | 608 |
|
18454 | 609 |
fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = |
610 |
let |
|
611 |
val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco; |
|
612 |
val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco; |
|
613 |
val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco; |
|
18515 | 614 |
val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity; |
18454 | 615 |
fun mk_eq_pred _ trns = |
616 |
trns |
|
617 |
|> succeed (eqpred, []) |
|
618 |
fun mk_eq_inst _ trns = |
|
619 |
trns |
|
620 |
|> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred |
|
18515 | 621 |
|> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])), []); |
18454 | 622 |
in |
623 |
trns |
|
624 |
|> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst |
|
625 |
end; |
|
626 |
||
18516 | 627 |
fun invoke_appgen thy tabs (app as ((f, ty), ts)) trns = |
628 |
gen_invoke |
|
629 |
((map (apsnd (fn (ag, _) => ag thy tabs)) o #appgens o #gens o CodegenData.get) thy) |
|
630 |
("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty |
|
631 |
^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) app trns; |
|
632 |
||
633 |
||
634 |
(* expression generators *) |
|
635 |
||
636 |
fun exprgen_sort thy tabs sort trns = |
|
637 |
trns |
|
638 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort) |
|
639 |
|-> (fn sort => pair sort); |
|
640 |
||
641 |
fun exprgen_type thy tabs (TVar _) trns = |
|
642 |
error "TVar encountered during code generation" |
|
643 |
| exprgen_type thy tabs (TFree (v, sort)) trns = |
|
644 |
trns |
|
645 |
|> exprgen_sort thy tabs sort |
|
646 |
|-> (fn sort => pair (IVarT (v |> unprefix "'", sort))) |
|
647 |
| exprgen_type thy tabs (Type ("fun", [t1, t2])) trns = |
|
648 |
trns |
|
649 |
|> exprgen_type thy tabs t1 |
|
650 |
||>> exprgen_type thy tabs t2 |
|
651 |
|-> (fn (t1', t2') => pair (t1' `-> t2')) |
|
652 |
| exprgen_type thy tabs (Type (tyco, tys)) trns = |
|
653 |
trns |
|
654 |
|> ensure_def_tyco thy tabs tyco |
|
655 |
||>> fold_map (exprgen_type thy tabs) tys |
|
656 |
|-> (fn (tyco, tys) => pair (tyco `%% tys)); |
|
657 |
||
658 |
fun exprgen_term thy tabs (Const (f, ty)) trns = |
|
659 |
trns |
|
660 |
|> invoke_appgen thy tabs ((f, ty), []) |
|
661 |
|-> (fn e => pair e) |
|
662 |
| exprgen_term thy tabs (Var ((v, i), ty)) trns = |
|
663 |
trns |
|
664 |
|> exprgen_type thy tabs ty |
|
665 |
|-> (fn ty => pair (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty))) |
|
666 |
| exprgen_term thy tabs (Free (v, ty)) trns = |
|
667 |
trns |
|
668 |
|> exprgen_type thy tabs ty |
|
669 |
|-> (fn ty => pair (IVarE (v, ty))) |
|
670 |
| exprgen_term thy tabs (Abs (v, ty, t)) trns = |
|
671 |
trns |
|
672 |
|> exprgen_type thy tabs ty |
|
673 |
||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t)) |
|
674 |
|-> (fn (ty, e) => pair ((v, ty) `|-> e)) |
|
675 |
| exprgen_term thy tabs (t as t1 $ t2) trns = |
|
676 |
let |
|
677 |
val (t', ts) = strip_comb t |
|
678 |
in case t' |
|
679 |
of Const (f, ty) => |
|
680 |
trns |
|
681 |
|> invoke_appgen thy tabs ((f, ty), ts) |
|
682 |
|-> (fn e => pair e) |
|
683 |
| _ => |
|
684 |
trns |
|
685 |
|> exprgen_term thy tabs t' |
|
686 |
||>> fold_map (exprgen_term thy tabs) ts |
|
687 |
|-> (fn (e, es) => pair (e `$$ es)) |
|
688 |
end; |
|
689 |
||
18454 | 690 |
|
691 |
(* code generator auxiliary *) |
|
692 |
||
693 |
fun mk_fun thy tabs eqs ty trns = |
|
18217 | 694 |
let |
695 |
val sortctxt = ClassPackage.extract_sortctxt thy ty; |
|
696 |
fun mk_sortvar (v, sort) trns = |
|
697 |
trns |
|
18516 | 698 |
|> exprgen_sort thy tabs sort |
18217 | 699 |
|-> (fn sort => pair (unprefix "'" v, sort)) |
700 |
fun mk_eq (args, rhs) trns = |
|
701 |
trns |
|
18516 | 702 |
|> fold_map (exprgen_term thy tabs o devarify_term) args |
703 |
||>> (exprgen_term thy tabs o devarify_term) rhs |
|
18217 | 704 |
|-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) |
705 |
in |
|
706 |
trns |
|
707 |
|> fold_map mk_eq eqs |
|
18516 | 708 |
||>> exprgen_type thy tabs (devarify_type ty) |
18217 | 709 |
||>> fold_map mk_sortvar sortctxt |
710 |
|-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) |
|
711 |
end; |
|
712 |
||
18515 | 713 |
fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns = |
714 |
trns |
|
715 |
|> ensure_def_class thy tabs cls |
|
716 |
||>> ensure_def_inst thy tabs inst |
|
717 |
||>> (fold_map o fold_map) (mk_lookup thy tabs) ls |
|
718 |
|-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) |
|
719 |
| mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = |
|
720 |
trns |
|
721 |
|> fold_map (ensure_def_class thy tabs) clss |
|
722 |
|-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); |
|
723 |
||
724 |
fun mk_itapp e [] = e |
|
725 |
| mk_itapp e lookup = IInst (e, lookup); |
|
726 |
||
18516 | 727 |
fun fix_nargs thy tabs gen (imin, imax) ((f, ty), ts) trns = |
728 |
let |
|
729 |
fun invoke ts trns = |
|
730 |
trns |
|
731 |
|> gen_invoke [("const application", gen)] ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty |
|
732 |
^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) |
|
733 |
((f, ty), ts) |
|
734 |
in if length ts < imin then |
|
735 |
let |
|
736 |
val d = imin - length ts; |
|
737 |
val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d; |
|
738 |
val tys = Library.take (d, ((fst o strip_type) ty)); |
|
739 |
in |
|
740 |
trns |
|
741 |
|> debug 10 (fn _ => "eta-expanding") |
|
742 |
|> fold_map (exprgen_type thy tabs) tys |
|
743 |
||>> invoke (ts @ map2 (curry Free) vs tys) |
|
744 |
|-> (fn (tys, e) => succeed ((vs ~~ tys) `|--> e)) |
|
745 |
end |
|
746 |
else if length ts > imax then |
|
747 |
trns |
|
748 |
|> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")") |
|
749 |
|> invoke (Library.take (imax, ts)) |
|
750 |
||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) |
|
751 |
|-> succeed o mk_apps |
|
752 |
else |
|
753 |
trns |
|
754 |
|> debug 10 (fn _ => "keeping arguments") |
|
755 |
|> invoke ts |
|
756 |
|-> succeed |
|
757 |
end; |
|
758 |
||
759 |
(* application generators *) |
|
760 |
||
18454 | 761 |
fun appgen_default thy tabs ((f, ty), ts) trns = |
18335 | 762 |
let |
763 |
val _ = debug 5 (fn _ => "making application of " ^ quote f) (); |
|
764 |
val ty_def = Sign.the_const_constraint thy f; |
|
765 |
in |
|
766 |
trns |
|
18454 | 767 |
|> ensure_def_const thy tabs (f, ty) |
18515 | 768 |
||>> (fold_map o fold_map) (mk_lookup thy tabs) (ClassPackage.extract_sortlookup thy (ty_def, ty)) |
18516 | 769 |
||>> exprgen_type thy tabs ty |
770 |
||>> fold_map (exprgen_term thy tabs) ts |
|
18335 | 771 |
|-> (fn (((f, lookup), ty), es) => |
772 |
succeed (mk_itapp (IConst (f, ty)) lookup `$$ es)) |
|
18515 | 773 |
end; |
18335 | 774 |
|
18516 | 775 |
fun appgen_appconst thy tabs ((f, ty), ts) trns = |
776 |
case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f |
|
777 |
of SOME (bounds, (ag, _)) => |
|
18335 | 778 |
trns |
18516 | 779 |
|> fix_nargs thy tabs (ag thy tabs) bounds ((f, ty), ts) |
780 |
| NONE => |
|
781 |
trns |
|
782 |
|> fail ("no constant in application table: " ^ quote f); |
|
18335 | 783 |
|
18516 | 784 |
fun appgen_neg thy tabs (("neg", Type ("fun", [ty, _])), ts) trns = |
785 |
trns |
|
786 |
|> exprgen_term thy tabs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty)) |
|
787 |
|-> succeed; |
|
18217 | 788 |
|
18516 | 789 |
fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns = |
790 |
trns |
|
791 |
|> invoke_eq (exprgen_type thy tabs) (ensure_def_eq thy tabs) ty |
|
792 |
|-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty) |
|
793 |
| true => fn trns => trns |
|
794 |
|> exprgen_term thy tabs t1 |
|
795 |
||>> exprgen_term thy tabs t2 |
|
796 |
|-> (fn (e1, e2) => succeed (Fun_eq `$ e1 `$ e2))); |
|
18217 | 797 |
|
798 |
(* definition generators *) |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
799 |
|
18454 | 800 |
fun defgen_tyco_fallback thy tabs tyco trns = |
18217 | 801 |
if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco) |
18282 | 802 |
((#serialize_data o CodegenData.get) thy) false |
18217 | 803 |
then |
804 |
trns |
|
18231 | 805 |
|> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco) |
18217 | 806 |
|> succeed (Nop, []) |
807 |
else |
|
808 |
trns |
|
809 |
|> fail ("no code generation fallback for " ^ quote tyco) |
|
810 |
||
18454 | 811 |
fun defgen_const_fallback thy tabs c trns = |
812 |
if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const c) |
|
18282 | 813 |
((#serialize_data o CodegenData.get) thy) false |
18217 | 814 |
then |
815 |
trns |
|
18454 | 816 |
|> debug 5 (fn _ => "trying defgen const fallback for " ^ quote c) |
18217 | 817 |
|> succeed (Nop, []) |
818 |
else |
|
819 |
trns |
|
18454 | 820 |
|> fail ("no code generation fallback for " ^ quote c) |
18217 | 821 |
|
18454 | 822 |
fun defgen_defs thy (tabs as ((deftab, _), _)) c trns = |
823 |
case Symtab.lookup deftab c |
|
824 |
of SOME (ty, (args, rhs)) => |
|
18217 | 825 |
trns |
18454 | 826 |
|> debug 5 (fn _ => "trying defgen def for " ^ quote c) |
827 |
|> mk_fun thy tabs [(args, rhs)] (devarify_type ty) |
|
18217 | 828 |
|-> (fn def => succeed (def, [])) |
18454 | 829 |
| _ => trns |> fail ("no definition found for " ^ quote c); |
18217 | 830 |
|
18454 | 831 |
fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) (cls : string) trns = |
18217 | 832 |
case name_of_idf thy nsp_class cls |
833 |
of SOME cls => |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
834 |
let |
18454 | 835 |
val memnames = ClassPackage.the_consts thy (cls : string); |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
836 |
val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames; |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
837 |
val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes; |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
838 |
val memidfs = map (idf_of_name thy nsp_mem) memnames; |
18454 | 839 |
fun mk_instname (tyco, thyname) = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))) |
840 |
val instnames = map mk_instname (ClassPackage.the_tycos thy cls); |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
841 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
842 |
trns |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
843 |
|> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) |
18454 | 844 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.get_superclasses thy cls) |
18516 | 845 |
||>> fold_map (exprgen_type thy tabs) memtypes |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
846 |
|-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []), |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
847 |
memidfs @ instnames)) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
848 |
end |
18217 | 849 |
| _ => |
850 |
trns |
|
851 |
|> fail ("no class definition found for " ^ quote cls); |
|
852 |
||
18454 | 853 |
fun defgen_clsmem thy tabs m trns = |
854 |
case name_of_idf thy nsp_mem m |
|
855 |
of SOME m => |
|
18360 | 856 |
trns |
18454 | 857 |
|> debug 5 (fn _ => "trying defgen class member for " ^ quote m) |
858 |
|> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
859 |
|-> (fn cls => succeed (Classmember cls, [])) |
18217 | 860 |
| _ => |
18454 | 861 |
trns |> fail ("no class member found for " ^ quote m) |
18217 | 862 |
|
18454 | 863 |
fun defgen_clsinst thy (tabs as (_, (insttab, _, _))) inst trns = |
864 |
case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) |
|
865 |
of SOME (_, (cls, tyco)) => |
|
18217 | 866 |
let |
18454 | 867 |
val arity = ClassPackage.get_arities thy [cls] tyco; |
868 |
val ms = map (fn m => (m, Sign.the_const_constraint thy m)) (ClassPackage.the_consts thy cls); |
|
869 |
val instmem_idfs = ClassPackage.get_inst_consts_sign thy (tyco, cls); |
|
18515 | 870 |
val supclss = ClassPackage.get_superclasses thy cls; |
18335 | 871 |
fun add_vars arity clsmems (trns as (_, modl)) = |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
872 |
case get_def modl (idf_of_name thy nsp_class cls) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
873 |
of Class (_, _, members, _) => ((Term.invent_names |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
874 |
(tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns) |
18515 | 875 |
val ad_hoc_arity = map (fn (v, sort) => map_index (fn (i, _) => (ClassPackage.Lookup ([], (v, i)))) sort); |
876 |
(*! THIS IS ACTUALLY VERY AD-HOC... !*) |
|
18217 | 877 |
in |
18515 | 878 |
(trns |
18231 | 879 |
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") |
18454 | 880 |
|> (fold_map o fold_map) (ensure_def_class thy tabs) arity |
881 |
||>> fold_map (ensure_def_const thy tabs) ms |
|
882 |
|-> (fn (arity, ms) => add_vars arity ms) |
|
883 |
||>> ensure_def_class thy tabs cls |
|
884 |
||>> ensure_def_tyco thy tabs tyco |
|
18515 | 885 |
||>> fold_map (fn supcls => ensure_def_inst thy tabs (supcls, tyco)) supclss |
886 |
||>> fold_map (fn supcls => (fold_map o fold_map) (mk_lookup thy tabs) |
|
887 |
(ClassPackage.extract_sortlookup thy |
|
888 |
(Type (tyco, map_index (fn (i, _) => TVar (("'a", i), [])) (ClassPackage.get_arities thy [supcls] tyco)), |
|
889 |
Type (tyco, map_index (fn (i, sort) => TFree (string_of_int i, sort)) arity)))) supclss |
|
890 |
||>> fold_map (ensure_def_const thy tabs) instmem_idfs) |
|
891 |
|-> (fn ((((((arity, ms), cls), tyco), supinsts), supinstlookup), instmem_idfs) |
|
892 |
: ((((((string * string list) list * string list) * string) * string) |
|
893 |
* string list) * ClassPackage.sortlookup list list list) * string list |
|
894 |
=> |
|
895 |
succeed (Classinst ((cls, (tyco, arity)), (supclss ~~ (supinsts ~~ supinstlookup), ms ~~ map (rpair (ad_hoc_arity arity)) instmem_idfs)), [])) |
|
18217 | 896 |
end |
897 |
| _ => |
|
18454 | 898 |
trns |> fail ("no class instance found for " ^ quote inst); |
18217 | 899 |
|
900 |
||
18515 | 901 |
(* trns |
902 |
|> ensure_def_const thy tabs (f, ty) |
|
903 |
||
18516 | 904 |
||>> exprgen_type thy tabs ty |
905 |
||>> fold_map (exprgen_term thy tabs) ts |
|
18515 | 906 |
|-> (fn (((f, lookup), ty), es) => |
907 |
succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))*) |
|
908 |
||
909 |
||
18217 | 910 |
(* parametrized generators, for instantiation in HOL *) |
911 |
||
18454 | 912 |
fun appgen_let strip_abs thy tabs (f as ("Let", _), ts) trns = |
18335 | 913 |
let |
914 |
fun dest_let (l as Const ("Let", _) $ t $ u) = |
|
915 |
(case strip_abs 1 u |
|
916 |
of ([p], u') => apfst (cons (p, t)) (dest_let u') |
|
917 |
| _ => ([], l)) |
|
918 |
| dest_let t = ([], t); |
|
919 |
fun mk_let (l, r) trns = |
|
18217 | 920 |
trns |
18516 | 921 |
|> exprgen_term thy tabs l |
922 |
||>> exprgen_term thy tabs r |
|
18335 | 923 |
|-> (fn (l, r) => pair (r, ipat_of_iexpr l)); |
18516 | 924 |
fun gen_let ((f, ty), [t2, t3]) trns = |
18335 | 925 |
let |
18516 | 926 |
val (lets, body) = dest_let (Const (f, ty) $ t2 $ t3) |
18335 | 927 |
in |
928 |
trns |
|
929 |
|> fold_map mk_let lets |
|
18516 | 930 |
||>> exprgen_term thy tabs body |
18335 | 931 |
|-> (fn (lets, body) => |
18516 | 932 |
succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body))) |
18335 | 933 |
end; |
934 |
in |
|
935 |
trns |
|
18516 | 936 |
|> fix_nargs thy tabs gen_let (2, 2) (f, ts) |
18335 | 937 |
end |
18454 | 938 |
| appgen_let strip_abs thy tabs ((f, _), _) trns = |
18335 | 939 |
trns |
940 |
|> fail ("not a let: " ^ quote f); |
|
18217 | 941 |
|
18454 | 942 |
fun appgen_split strip_abs thy tabs (f as ("split", _), ts) trns = |
18335 | 943 |
let |
18516 | 944 |
fun gen_split ((f, ty), [t2]) trns = |
18335 | 945 |
let |
18516 | 946 |
val ([p], body) = strip_abs 1 (Const (f, ty) $ t2) |
18335 | 947 |
in |
948 |
trns |
|
18516 | 949 |
|> exprgen_term thy tabs p |
950 |
||>> exprgen_term thy tabs body |
|
951 |
|-> (fn (IVarE v, body) => succeed (IAbs (v, body))) |
|
18335 | 952 |
end |
953 |
in |
|
954 |
trns |
|
18516 | 955 |
|> fix_nargs thy tabs gen_split (1, 1) (f, ts) |
18335 | 956 |
end |
18454 | 957 |
| appgen_split strip_abs thy tabs ((f, _), _) trns = |
18335 | 958 |
trns |
959 |
|> fail ("not a split: " ^ quote f); |
|
960 |
||
18454 | 961 |
fun appgen_number_of dest_binum mk_int_to_nat thy tabs (f as ("Numeral.number_of", |
18335 | 962 |
Type ("fun", [_, Type ("IntDef.int", [])])), ts) trns = |
963 |
let |
|
964 |
fun gen_num (_, [bin]) trns = |
|
18217 | 965 |
trns |
18516 | 966 |
|> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer)) |
18335 | 967 |
handle TERM _ |
968 |
=> error ("not a number: " ^ Sign.string_of_term thy bin)) |
|
969 |
in |
|
970 |
trns |
|
18516 | 971 |
|> fix_nargs thy tabs gen_num (1, 1) (f, ts) |
18335 | 972 |
end |
18454 | 973 |
| appgen_number_of dest_binum mk_int_to_nat thy tabs (f as ("Numeral.number_of", |
18335 | 974 |
Type ("fun", [_, Type ("nat", [])])), ts) trns = |
975 |
let |
|
976 |
fun gen_num (_, [bin]) trns = |
|
977 |
trns |
|
18516 | 978 |
|> exprgen_term thy tabs (mk_int_to_nat bin) |
979 |
|-> succeed |
|
18335 | 980 |
in |
981 |
trns |
|
18516 | 982 |
|> fix_nargs thy tabs gen_num (1, 1) (f, ts) |
18335 | 983 |
end |
18454 | 984 |
| appgen_number_of dest_binum mk_int_to_nat thy tabs ((f, _), _) trns = |
18217 | 985 |
trns |
18335 | 986 |
|> fail ("not a number_of: " ^ quote f); |
18217 | 987 |
|
18454 | 988 |
fun appgen_case get_case_const_data thy tabs ((f, ty), ts) trns = |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
989 |
let |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
990 |
fun cg_case_d gen_names dty (((cname, i), ty), t) trns = |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
991 |
let |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
992 |
val vs = gen_names i; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
993 |
val tys = Library.take (i, (fst o strip_type) ty); |
18330 | 994 |
val frees = map2 (curry Free) vs tys; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
995 |
val t' = Envir.beta_norm (list_comb (t, frees)); |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
996 |
in |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
997 |
trns |
18516 | 998 |
|> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees)) |
999 |
||>> exprgen_term thy tabs t' |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1000 |
|-> (fn (ep, e) => pair (ipat_of_iexpr ep, e)) |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1001 |
end; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1002 |
fun cg_case dty cs (_, ts) trns = |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1003 |
let |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1004 |
val (ts', t) = split_last ts |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1005 |
fun gen_names i = |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1006 |
variantlist (replicate i "x", foldr add_term_names |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1007 |
(map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1008 |
in |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1009 |
trns |
18516 | 1010 |
|> exprgen_term thy tabs t |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1011 |
||>> fold_map (cg_case_d gen_names dty) (cs ~~ ts') |
18516 | 1012 |
|-> (fn (t, ds) => succeed (ICase (t, ds))) |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1013 |
end; |
18335 | 1014 |
in |
1015 |
case get_case_const_data thy f |
|
1016 |
of NONE => |
|
1017 |
trns |
|
1018 |
|> fail ("not a case constant: " ^ quote f) |
|
1019 |
| SOME cs => |
|
1020 |
let |
|
1021 |
val (tys, dty) = (split_last o fst o strip_type) ty; |
|
1022 |
in |
|
1023 |
trns |
|
18454 | 1024 |
|> fix_nargs thy tabs (cg_case dty (cs ~~ tys)) |
18516 | 1025 |
(length cs + 1, length cs + 1) ((f, ty), ts) |
18335 | 1026 |
end |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1027 |
end; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1028 |
|
18454 | 1029 |
fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns = |
1030 |
case name_of_idf thy nsp_tyco dtco |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1031 |
of SOME dtco => |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1032 |
(case get_datatype thy dtco |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1033 |
of SOME (vars, cos) => |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1034 |
let |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1035 |
val cotys = map (the o get_datacons thy o rpair dtco) cos; |
18454 | 1036 |
val coidfs = map (fn co => (DatatypeconsNameMangler.get thy dtcontab (co, dtco)) |> |
1037 |
idf_of_name thy nsp_dtcon) cos; |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1038 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1039 |
trns |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1040 |
|> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) |
18516 | 1041 |
|> fold_map (exprgen_sort thy tabs) (map snd vars) |
1042 |
||>> (fold_map o fold_map) (exprgen_type thy tabs o devarify_type) cotys |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1043 |
|-> (fn (sorts, tys) => succeed (Datatype |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1044 |
(map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []), |
18454 | 1045 |
coidfs)) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1046 |
end |
18217 | 1047 |
| NONE => |
1048 |
trns |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1049 |
|> fail ("no datatype found for " ^ quote dtco)) |
18217 | 1050 |
| NONE => |
1051 |
trns |
|
18454 | 1052 |
|> fail ("not a type constructor: " ^ quote dtco) |
18335 | 1053 |
|
18454 | 1054 |
fun defgen_datacons get_datacons thy (tabs as (_, (_, _, dtcontab))) co trns = |
1055 |
case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) |
|
1056 |
of SOME (co, dtco) => |
|
1057 |
trns |
|
1058 |
|> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) |
|
1059 |
|> ensure_def_tyco thy tabs dtco |
|
1060 |
|-> (fn tyco => succeed (Datatypecons tyco, [])) |
|
1061 |
| _ => |
|
1062 |
trns |
|
1063 |
|> fail ("not a datatype constructor: " ^ quote co); |
|
18217 | 1064 |
|
18454 | 1065 |
fun defgen_recfun get_equations thy tabs c trns = |
1066 |
case recconst_of_idf thy tabs c |
|
1067 |
of SOME (c, ty) => |
|
18217 | 1068 |
let |
18454 | 1069 |
val (eqs, ty) = get_equations thy (c, ty); |
18217 | 1070 |
in |
1071 |
case eqs |
|
1072 |
of (_::_) => |
|
1073 |
trns |
|
18454 | 1074 |
|> debug 5 (fn _ => "trying defgen recfun for " ^ quote c) |
1075 |
|> mk_fun thy tabs eqs (devarify_type ty) |
|
18217 | 1076 |
|-> (fn def => succeed (def, [])) |
1077 |
| _ => |
|
1078 |
trns |
|
18454 | 1079 |
|> fail ("no recursive definition found for " ^ quote c) |
18217 | 1080 |
end |
1081 |
| NONE => |
|
1082 |
trns |
|
18454 | 1083 |
|> fail ("not a constant: " ^ quote c); |
18217 | 1084 |
|
1085 |
||
18516 | 1086 |
|
1087 |
(** theory interface **) |
|
18217 | 1088 |
|
18454 | 1089 |
fun mk_tabs thy = |
18217 | 1090 |
let |
18454 | 1091 |
fun extract_defs thy = |
18217 | 1092 |
let |
18454 | 1093 |
fun dest t = |
1094 |
let |
|
1095 |
val (lhs, rhs) = Logic.dest_equals t; |
|
1096 |
val (c, args) = strip_comb lhs; |
|
1097 |
val (s, T) = dest_Const c |
|
1098 |
in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE |
|
1099 |
end handle TERM _ => NONE; |
|
1100 |
fun prep_def def = (case Codegen.preprocess thy [def] of |
|
1101 |
[def'] => prop_of def' | _ => error "mk_auxtab: bad preprocessor"); |
|
1102 |
fun add_def (name, t) defs = (case dest t of |
|
1103 |
NONE => defs |
|
1104 |
| SOME _ => (case (dest o prep_def oo Thm.get_axiom) thy name of |
|
1105 |
NONE => defs |
|
1106 |
| SOME (s, (T, (args, rhs))) => Symtab.update |
|
1107 |
(s, (T, (split_last (args @ [rhs]))) :: |
|
1108 |
if_none (Symtab.lookup defs s) []) defs)) |
|
18217 | 1109 |
in |
18454 | 1110 |
Symtab.empty |
1111 |
|> fold (Symtab.fold add_def) (map |
|
1112 |
(snd o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) |
|
18217 | 1113 |
end; |
18454 | 1114 |
fun mk_insttab thy = |
1115 |
InstNameMangler.empty |
|
1116 |
|> Symtab.fold_map |
|
1117 |
(fn (cls, (_, clsinsts)) => fold_map |
|
1118 |
(fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts) |
|
1119 |
(ClassPackage.get_classtab thy) |
|
1120 |
|-> (fn _ => I); |
|
1121 |
fun mk_overltabs thy defs = |
|
1122 |
(Symtab.empty, ConstNameMangler.empty) |
|
1123 |
|> Symtab.fold |
|
1124 |
(fn (c, [_]) => I |
|
1125 |
| ("0", _) => I |
|
1126 |
| (c, tytab) => |
|
1127 |
(fn (overltab1, overltab2) => ( |
|
1128 |
overltab1 |
|
1129 |
|> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), |
|
1130 |
overltab2 |
|
1131 |
|> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab |
|
1132 |
))) defs; |
|
1133 |
fun mk_dtcontab thy = |
|
1134 |
DatatypeconsNameMangler.empty |
|
1135 |
|> fold_map |
|
18455 | 1136 |
(fn (_, co_dtco) => DatatypeconsNameMangler.declare_multi thy co_dtco) |
1137 |
(fold (fn (co, dtco) => |
|
1138 |
let |
|
1139 |
val key = ((NameSpace.drop_base o NameSpace.drop_base) co, NameSpace.base co) |
|
1140 |
in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end |
|
1141 |
) (get_all_datatype_cons thy) []) |
|
18454 | 1142 |
|-> (fn _ => I); |
1143 |
fun mk_deftab thy defs overltab = |
|
1144 |
Symtab.empty |
|
1145 |
|> Symtab.fold |
|
1146 |
(fn (c, [ty_cdef]) => |
|
1147 |
Symtab.update_new (idf_of_name thy nsp_const c, ty_cdef) |
|
1148 |
| ("0", _) => I |
|
1149 |
| (c, cdefs) => fold (fn (ty, cdef) => |
|
1150 |
let |
|
1151 |
val c' = ConstNameMangler.get thy overltab |
|
1152 |
(idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) |
|
1153 |
in Symtab.update_new (c', (ty, cdef)) end) cdefs) defs; |
|
1154 |
fun mk_clsmemtab thy = |
|
1155 |
Symtab.empty |
|
1156 |
|> Symtab.fold |
|
1157 |
(fn (class, (clsmems, _)) => fold |
|
1158 |
(fn clsmem => Symtab.update (clsmem, class)) clsmems) |
|
1159 |
(ClassPackage.get_classtab thy); |
|
1160 |
val defs = extract_defs thy; |
|
1161 |
val insttab = mk_insttab thy; |
|
1162 |
val overltabs = mk_overltabs thy defs; |
|
1163 |
val dtcontab = mk_dtcontab thy; |
|
1164 |
val deftab = mk_deftab thy defs (snd overltabs); |
|
1165 |
val clsmemtab = mk_clsmemtab thy; |
|
1166 |
in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end; |
|
18217 | 1167 |
|
18335 | 1168 |
fun check_for_serializer serial_name serialize_data = |
1169 |
if Symtab.defined serialize_data serial_name |
|
1170 |
then serialize_data |
|
1171 |
else error ("unknown code serializer: " ^ quote serial_name); |
|
1172 |
||
18516 | 1173 |
fun map_module f = |
1174 |
map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => |
|
1175 |
(f modl, gens, lookups, serialize_data, logic_data)); |
|
1176 |
||
18231 | 1177 |
fun expand_module defs gen thy = |
18516 | 1178 |
(#modl o CodegenData.get) thy |
1179 |
|> start_transact (gen thy defs) |
|
1180 |
|-> (fn x:'a => fn modl => (x, map_module (K modl) thy)); |
|
1181 |
||
1182 |
fun rename_inconsistent thy = |
|
18217 | 1183 |
let |
18516 | 1184 |
fun get_inconsistent thyname = |
1185 |
let |
|
1186 |
val thy = theory thyname; |
|
1187 |
fun own_tables get = |
|
1188 |
(get thy) |
|
1189 |
|> fold (Symtab.fold (Symtab.remove (K true)) o get) (Theory.parents_of thy) |
|
1190 |
|> Symtab.keys; |
|
1191 |
val names = own_tables (#2 o #types o Type.rep_tsig o Sign.tsig_of) |
|
1192 |
@ own_tables (#2 o #declarations o Consts.dest o #consts o Sign.rep_sg); |
|
1193 |
fun diff names = |
|
1194 |
fold (fn name => |
|
1195 |
if is_prefix (op =) (NameSpace.unpack thyname) (NameSpace.unpack name) |
|
1196 |
then I |
|
1197 |
else cons (name, NameSpace.append thyname (NameSpace.base name))) names []; |
|
1198 |
in diff names end; |
|
1199 |
val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat; |
|
1200 |
fun add (src, dst) thy = |
|
1201 |
if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src |
|
1202 |
then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy) |
|
1203 |
else add_alias (src, dst) thy |
|
1204 |
in fold add inconsistent thy end; |
|
1205 |
||
1206 |
||
1207 |
||
1208 |
(** target languages **) |
|
1209 |
||
1210 |
(* primitive definitions *) |
|
1211 |
||
1212 |
fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) deps thy = |
|
1213 |
let |
|
1214 |
val _ = if Symtab.defined ((#serialize_data o CodegenData.get) thy) target |
|
1215 |
then () else error ("unknown target language: " ^ quote target); |
|
1216 |
val tabs = mk_tabs thy; |
|
1217 |
val name = prep_name thy tabs raw_name; |
|
1218 |
val primdef = prep_primdef raw_primdef; |
|
18217 | 1219 |
in |
18516 | 1220 |
thy |
1221 |
|> map_module (CodegenThingol.add_prim name (target, primdef) deps) |
|
18217 | 1222 |
end; |
1223 |
||
18516 | 1224 |
val add_prim_i = gen_add_prim ((K o K) I) I; |
1225 |
val add_prim_class = gen_add_prim |
|
1226 |
(fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy)) |
|
1227 |
(Pretty.str o newline_correct o Symbol.strip_blanks); |
|
1228 |
val add_prim_tyco = gen_add_prim |
|
1229 |
(fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy)) |
|
1230 |
(Pretty.str o newline_correct o Symbol.strip_blanks); |
|
1231 |
val add_prim_const = gen_add_prim |
|
1232 |
(fn thy => fn tabs => idf_of_const thy tabs o |
|
1233 |
(fn (c, ty) => (Sign.intern_const thy c, Sign.read_typ (thy, K NONE) ty))) |
|
1234 |
(Pretty.str o newline_correct o Symbol.strip_blanks); |
|
1235 |
||
1236 |
val ensure_prim = (map_module o CodegenThingol.ensure_prim); |
|
18217 | 1237 |
|
1238 |
(* syntax *) |
|
1239 |
||
18516 | 1240 |
fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname prep_primdef serial_name ((raw_tyco, raw_mfx, fixity), primdef) thy = |
18217 | 1241 |
let |
1242 |
val tyco = prep_tyco thy raw_tyco; |
|
1243 |
val _ = if member (op =) prims tyco |
|
1244 |
then error ("attempted to re-define primitive " ^ quote tyco) |
|
1245 |
else () |
|
1246 |
fun add_primdef NONE = I |
|
1247 |
| add_primdef (SOME (name, (def, deps))) = |
|
18361 | 1248 |
CodegenSerializer.add_prim (prep_primname thy tyco name, (prep_primdef def, deps)) |
18217 | 1249 |
in |
1250 |
thy |
|
18516 | 1251 |
|> ensure_prim (idf_of_name thy nsp_tyco tyco) |
18217 | 1252 |
|> prep_mfx raw_mfx |
1253 |
|-> (fn mfx => map_codegen_data |
|
1254 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
1255 |
(modl, gens, lookups, |
|
18335 | 1256 |
serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name |
18217 | 1257 |
(map_serialize_data |
1258 |
(fn (primitives, syntax_tyco, syntax_const) => |
|
1259 |
(primitives |> add_primdef primdef, |
|
18516 | 1260 |
syntax_tyco |> Symtab.update_new |
1261 |
(idf_of_name thy nsp_tyco tyco, |
|
1262 |
(((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ())), |
|
18217 | 1263 |
syntax_const))), |
1264 |
logic_data))) |
|
1265 |
end; |
|
1266 |
||
18361 | 1267 |
val add_syntax_tyco_i = gen_add_syntax_tyco (K I) pair ((K o K) I) I; |
18217 | 1268 |
val add_syntax_tyco = |
1269 |
let |
|
1270 |
fun mk_name _ _ (SOME name) = name |
|
1271 |
| mk_name thy tyco NONE = |
|
1272 |
let |
|
1273 |
val name = Sign.extern_type thy tyco |
|
1274 |
in |
|
1275 |
if NameSpace.is_qualified name |
|
1276 |
then error ("no unique identifier for syntax definition: " ^ quote tyco) |
|
1277 |
else name |
|
1278 |
end; |
|
1279 |
fun prep_mfx mfx thy = |
|
1280 |
let |
|
1281 |
val proto_mfx = Codegen.parse_mixfix |
|
1282 |
(typ_of o read_ctyp thy) mfx; |
|
18516 | 1283 |
fun generate thy defs = fold_map (exprgen_type thy defs o devarify_type) |
18217 | 1284 |
(Codegen.quotes_of proto_mfx); |
1285 |
in |
|
1286 |
thy |
|
18454 | 1287 |
|> expand_module (mk_tabs thy) generate |
18217 | 1288 |
|-> (fn tys => pair (Codegen.replace_quotes tys proto_mfx)) |
1289 |
end; |
|
1290 |
in |
|
18454 | 1291 |
gen_add_syntax_tyco Sign.intern_type |
18361 | 1292 |
prep_mfx mk_name (newline_correct o Symbol.strip_blanks) |
18217 | 1293 |
end; |
1294 |
||
18516 | 1295 |
fun gen_add_syntax_const prep_const prep_mfx prep_primname prep_primdef serial_name ((raw_c, raw_mfx, fixity), primdef) thy = |
18217 | 1296 |
let |
18454 | 1297 |
val (c, ty) = prep_const thy raw_c; |
1298 |
val tabs = mk_tabs thy; |
|
1299 |
val _ = if member (op =) prims c |
|
1300 |
then error ("attempted to re-define primitive " ^ quote c) |
|
18217 | 1301 |
else () |
1302 |
fun add_primdef NONE = I |
|
1303 |
| add_primdef (SOME (name, (def, deps))) = |
|
18454 | 1304 |
CodegenSerializer.add_prim (prep_primname thy c name, (prep_primdef def, deps)) |
18217 | 1305 |
in |
1306 |
thy |
|
18516 | 1307 |
|> ensure_prim (idf_of_const thy tabs (c, ty)) |
18217 | 1308 |
|> prep_mfx raw_mfx |
1309 |
|-> (fn mfx => map_codegen_data |
|
1310 |
(fn (modl, gens, lookups, serialize_data, logic_data) => |
|
1311 |
(modl, gens, lookups, |
|
18335 | 1312 |
serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name |
18217 | 1313 |
(map_serialize_data |
1314 |
(fn (primitives, syntax_tyco, syntax_const) => |
|
1315 |
(primitives |> add_primdef primdef, |
|
1316 |
syntax_tyco, |
|
18516 | 1317 |
syntax_const |> Symtab.update_new |
1318 |
(idf_of_const thy tabs (c, ty), |
|
1319 |
(((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ()))))), |
|
18217 | 1320 |
logic_data))) |
1321 |
end; |
|
1322 |
||
18361 | 1323 |
val add_syntax_const_i = gen_add_syntax_const (K I) pair ((K o K) I) I; |
18217 | 1324 |
val add_syntax_const = |
1325 |
let |
|
18454 | 1326 |
fun prep_const thy (raw_c, raw_ty) = |
18217 | 1327 |
let |
18454 | 1328 |
val c = Sign.intern_const thy raw_c; |
18217 | 1329 |
val ty = |
1330 |
raw_ty |
|
1331 |
|> Option.map (Sign.read_tyname thy) |
|
18454 | 1332 |
|> the_default (Sign.the_const_constraint thy c); |
1333 |
in (c, ty) end; |
|
18217 | 1334 |
fun mk_name _ _ (SOME name) = name |
1335 |
| mk_name thy f NONE = |
|
1336 |
let |
|
1337 |
val name = Sign.extern_const thy f |
|
1338 |
in |
|
1339 |
if NameSpace.is_qualified name |
|
1340 |
then error ("no unique identifier for syntax definition: " ^ quote f) |
|
1341 |
else name |
|
1342 |
end; |
|
1343 |
fun prep_mfx mfx thy = |
|
1344 |
let |
|
1345 |
val proto_mfx = Codegen.parse_mixfix |
|
1346 |
(term_of o read_cterm thy o rpair TypeInfer.logicT) mfx; |
|
18516 | 1347 |
fun generate thy defs = fold_map (exprgen_term thy defs o devarify_term) |
18217 | 1348 |
(Codegen.quotes_of proto_mfx); |
1349 |
in |
|
1350 |
thy |
|
18454 | 1351 |
|> expand_module (mk_tabs thy) generate |
18217 | 1352 |
|-> (fn es => pair (Codegen.replace_quotes es proto_mfx)) |
1353 |
end; |
|
1354 |
in |
|
18361 | 1355 |
gen_add_syntax_const prep_const prep_mfx mk_name (newline_correct o Symbol.strip_blanks) |
18217 | 1356 |
end; |
1357 |
||
1358 |
||
18516 | 1359 |
|
1360 |
(** code generation **) |
|
18217 | 1361 |
|
18231 | 1362 |
fun get_serializer thy serial_name = |
1363 |
(#serializer o (fn data => (the oo Symtab.lookup) data serial_name) |
|
1364 |
o #serialize_data o CodegenData.get) thy; |
|
1365 |
||
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1366 |
fun mk_const thy (f, s_ty) = |
18217 | 1367 |
let |
18231 | 1368 |
val f' = Sign.intern_const thy f; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1369 |
val ty = case s_ty |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1370 |
of NONE => Sign.the_const_constraint thy f' |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1371 |
| SOME s => Sign.read_typ (thy, K NONE) s; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1372 |
in (f', ty) end; |
18231 | 1373 |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1374 |
fun generate_code consts thy = |
18231 | 1375 |
let |
18454 | 1376 |
val tabs = mk_tabs thy; |
1377 |
val consts' = map (mk_const thy) consts; |
|
1378 |
fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts' |
|
18217 | 1379 |
in |
1380 |
thy |
|
18454 | 1381 |
|> expand_module tabs generate |
1382 |
|-> (fn consts => pair consts) |
|
18217 | 1383 |
end; |
1384 |
||
1385 |
fun serialize_code serial_name filename consts thy = |
|
1386 |
let |
|
1387 |
val serialize_data = |
|
1388 |
thy |
|
1389 |
|> CodegenData.get |
|
1390 |
|> #serialize_data |
|
18335 | 1391 |
|> check_for_serializer serial_name |
18217 | 1392 |
|> (fn data => (the oo Symtab.lookup) data serial_name) |
18516 | 1393 |
val serializer' = (get_serializer thy serial_name) serial_name |
1394 |
((Option.map fst oo Symtab.lookup o #syntax_tyco) serialize_data) |
|
1395 |
((Option.map fst oo Symtab.lookup o #syntax_const) serialize_data) |
|
18231 | 1396 |
(#primitives serialize_data); |
1397 |
val _ = serializer' : string list option -> module -> Pretty.T; |
|
18217 | 1398 |
val compile_it = serial_name = "ml" andalso filename = "-"; |
18282 | 1399 |
fun use_code code = |
18217 | 1400 |
if compile_it |
1401 |
then use_text Context.ml_output false code |
|
1402 |
else File.write (Path.unpack filename) (code ^ "\n"); |
|
1403 |
in |
|
1404 |
thy |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1405 |
|> (if is_some consts then generate_code (the consts) else pair []) |
18231 | 1406 |
|-> (fn [] => `(serializer' NONE o #modl o CodegenData.get) |
1407 |
| consts => `(serializer' (SOME consts) o #modl o CodegenData.get)) |
|
18360 | 1408 |
|-> (fn code => ((use_code o Pretty.output) code; I)) |
18217 | 1409 |
end; |
1410 |
||
1411 |
||
18454 | 1412 |
|
18516 | 1413 |
(** toplevel interface **) |
18217 | 1414 |
|
1415 |
local |
|
1416 |
||
1417 |
structure P = OuterParse |
|
1418 |
and K = OuterKeyword |
|
1419 |
||
1420 |
in |
|
1421 |
||
18335 | 1422 |
val (classK, generateK, serializeK, syntax_tycoK, syntax_constK, aliasK) = |
1423 |
("code_class", "code_generate", "code_serialize", "code_syntax_tyco", "code_syntax_const", "code_alias"); |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1424 |
val (constantsK, definedK, dependingK) = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1425 |
("constants", "defined_by", "depending_on"); |
18335 | 1426 |
|
1427 |
val classP = |
|
1428 |
OuterSyntax.command classK "codegen data for classes" K.thy_decl ( |
|
1429 |
P.xname |
|
1430 |
-- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) |
|
1431 |
-- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) []) |
|
1432 |
>> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos))) |
|
1433 |
) |
|
18217 | 1434 |
|
1435 |
val generateP = |
|
18282 | 1436 |
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1437 |
Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
18217 | 1438 |
>> (fn consts => |
18231 | 1439 |
Toplevel.theory (generate_code consts #> snd)) |
18217 | 1440 |
); |
1441 |
||
1442 |
val serializeP = |
|
18282 | 1443 |
OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( |
18217 | 1444 |
P.name |
1445 |
-- P.name |
|
1446 |
-- Scan.option ( |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1447 |
P.$$$ constantsK |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1448 |
|-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
18217 | 1449 |
) |
1450 |
>> (fn ((serial_name, filename), consts) => |
|
1451 |
Toplevel.theory (serialize_code serial_name filename consts)) |
|
1452 |
); |
|
1453 |
||
1454 |
val aliasP = |
|
18282 | 1455 |
OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( |
18217 | 1456 |
P.name |
1457 |
-- P.name |
|
1458 |
>> (fn (src, dst) => Toplevel.theory (add_alias (src, dst))) |
|
1459 |
); |
|
1460 |
||
1461 |
val syntax_tycoP = |
|
1462 |
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( |
|
18335 | 1463 |
P.name |
18217 | 1464 |
-- Scan.repeat1 ( |
1465 |
P.xname -- (P.$$$ "(" |-- P.string --| P.$$$ ")") |
|
18516 | 1466 |
-- CodegenSerializer.parse_fixity |
18217 | 1467 |
-- Scan.option ( |
1468 |
P.$$$ definedK |
|
1469 |
|-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") |
|
18335 | 1470 |
-- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) |
18217 | 1471 |
) |
1472 |
) |
|
18231 | 1473 |
>> (fn (serial_name, xs) => |
18217 | 1474 |
(Toplevel.theory oo fold) |
18516 | 1475 |
(fn (((tyco, raw_mfx), fixity), raw_def) => |
1476 |
add_syntax_tyco serial_name ((tyco, raw_mfx, fixity), raw_def)) xs) |
|
18217 | 1477 |
); |
1478 |
||
1479 |
val syntax_constP = |
|
1480 |
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl ( |
|
18335 | 1481 |
P.name |
18217 | 1482 |
-- Scan.repeat1 ( |
1483 |
(P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) -- (P.$$$ "(" |-- P.string --| P.$$$ ")") |
|
18516 | 1484 |
-- CodegenSerializer.parse_fixity |
18217 | 1485 |
-- Scan.option ( |
1486 |
P.$$$ definedK |
|
1487 |
|-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") |
|
18335 | 1488 |
-- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) |
18217 | 1489 |
) |
1490 |
) |
|
18231 | 1491 |
>> (fn (serial_name, xs) => |
18217 | 1492 |
(Toplevel.theory oo fold) |
18516 | 1493 |
(fn (((c, raw_mfx), fixity), raw_def) => |
1494 |
add_syntax_const serial_name ((c, raw_mfx, fixity), raw_def)) xs) |
|
18217 | 1495 |
); |
1496 |
||
18335 | 1497 |
val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, syntax_tycoP, syntax_constP]; |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1498 |
val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", constantsK, definedK, dependingK]; |
18217 | 1499 |
|
1500 |
||
18516 | 1501 |
|
1502 |
(** setup **) |
|
1503 |
||
18217 | 1504 |
val _ = |
1505 |
let |
|
1506 |
val bool = Type ("bool", []); |
|
1507 |
val nat = Type ("nat", []); |
|
1508 |
val int = Type ("IntDef.int", []); |
|
1509 |
fun list t = Type ("List.list", [t]); |
|
1510 |
fun pair t1 t2 = Type ("*", [t1, t2]); |
|
1511 |
val A = TVar (("'a", 0), []); |
|
1512 |
val B = TVar (("'b", 0), []); |
|
1513 |
in Context.add_setup [ |
|
1514 |
CodegenData.init, |
|
18335 | 1515 |
add_appgen ("default", appgen_default), |
18516 | 1516 |
add_appgen ("appconst", appgen_appconst), |
1517 |
add_appconst_i ("neg", ((0, 0), appgen_neg)), |
|
1518 |
add_appconst_i ("op =", ((2, 2), appgen_eq)), |
|
18217 | 1519 |
add_defgen ("clsdecl", defgen_clsdecl), |
18231 | 1520 |
add_defgen ("tyco_fallback", defgen_tyco_fallback), |
1521 |
add_defgen ("const_fallback", defgen_const_fallback), |
|
18217 | 1522 |
add_defgen ("defs", defgen_defs), |
1523 |
add_defgen ("clsmem", defgen_clsmem), |
|
1524 |
add_defgen ("clsinst", defgen_clsinst), |
|
18454 | 1525 |
add_alias ("op -->", "HOL.op_implies"), |
1526 |
add_alias ("op +", "HOL.op_add"), |
|
1527 |
add_alias ("op -", "HOL.op_minus"), |
|
1528 |
add_alias ("op *", "HOL.op_times"), |
|
18455 | 1529 |
add_alias ("op <=", "Orderings.op_le"), |
1530 |
add_alias ("op <", "Orderings.op_lt"), |
|
18454 | 1531 |
add_alias ("List.op @", "List.append"), |
1532 |
add_alias ("List.op mem", "List.member"), |
|
1533 |
add_alias ("Divides.op div", "Divides.div"), |
|
1534 |
add_alias ("Divides.op dvd", "Divides.dvd"), |
|
1535 |
add_alias ("Divides.op mod", "Divides.mod"), |
|
18217 | 1536 |
add_lookup_tyco ("bool", type_bool), |
18454 | 1537 |
add_lookup_tyco ("*", type_pair), |
18217 | 1538 |
add_lookup_tyco ("IntDef.int", type_integer), |
1539 |
add_lookup_tyco ("List.list", type_list), |
|
18231 | 1540 |
add_lookup_const (("True", bool), Cons_true), |
18217 | 1541 |
add_lookup_const (("False", bool), Cons_false), |
1542 |
add_lookup_const (("Not", bool --> bool), Fun_not), |
|
1543 |
add_lookup_const (("op &", bool --> bool --> bool), Fun_and), |
|
1544 |
add_lookup_const (("op |", bool --> bool --> bool), Fun_or), |
|
1545 |
add_lookup_const (("HOL.If", bool --> A --> A --> A), Fun_if), |
|
1546 |
add_lookup_const (("Pair", A --> B --> pair A B), Cons_pair), |
|
1547 |
add_lookup_const (("fst", pair A B --> A), Fun_fst), |
|
1548 |
add_lookup_const (("snd", pair A B --> B), Fun_snd), |
|
18454 | 1549 |
add_lookup_const (("List.list.Cons", A --> list A --> list A), Cons_cons), |
1550 |
add_lookup_const (("List.list.Nil", list A), Cons_nil), |
|
18217 | 1551 |
add_lookup_const (("1", nat), |
1552 |
IApp ( |
|
1553 |
IConst ("const.Suc", IFun (IType ("type.nat", []), IFun (IType ("type.nat", []), IType ("type.nat", [])))), |
|
1554 |
IConst ("const.Zero", IType ("type.nat", [])) |
|
1555 |
)), |
|
1556 |
add_lookup_const (("0", int), Fun_0), |
|
1557 |
add_lookup_const (("1", int), Fun_1), |
|
1558 |
add_lookup_const (("op +", int --> int --> int), Fun_add), |
|
1559 |
add_lookup_const (("op *", int --> int --> int), Fun_mult), |
|
1560 |
add_lookup_const (("uminus", int --> int), Fun_minus), |
|
1561 |
add_lookup_const (("op <", int --> int --> bool), Fun_lt), |
|
1562 |
add_lookup_const (("op <=", int --> int --> bool), Fun_le), |
|
18454 | 1563 |
add_lookup_const (("Wellfounded_Recursion.wfrec", ((A --> B) --> A --> B) --> A --> B), Fun_wfrec) |
18217 | 1564 |
] end; |
1565 |
||
1566 |
(* "op /" ??? *) |
|
1567 |
||
1568 |
end; (* local *) |
|
1569 |
||
1570 |
end; (* struct *) |