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