author | wenzelm |
Thu, 19 Jan 2006 21:22:08 +0100 | |
changeset 18708 | 4b3dadb4fe33 |
parent 18704 | 2c86ced392a8 |
child 18756 | 5eb3df798405 |
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; |
18702 | 15 |
type eqextr = theory -> auxtab |
16 |
-> (string * typ) -> (thm list * typ) option; |
|
18217 | 17 |
type defgen; |
18702 | 18 |
type appgen = theory -> auxtab |
19 |
-> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; |
|
20 |
||
18516 | 21 |
val add_appconst: string * ((int * int) * appgen) -> theory -> theory; |
18517 | 22 |
val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory; |
18702 | 23 |
val add_eqextr: string * eqextr -> theory -> theory; |
18217 | 24 |
val add_defgen: string * defgen -> theory -> theory; |
18517 | 25 |
val add_prim_class: xstring -> string list -> (string * string) |
26 |
-> theory -> theory; |
|
27 |
val add_prim_tyco: xstring -> string list -> (string * string) |
|
28 |
-> theory -> theory; |
|
29 |
val add_prim_const: xstring * string option -> string list -> (string * string) |
|
30 |
-> theory -> theory; |
|
31 |
val add_prim_i: string -> string list -> (string * Pretty.T) |
|
32 |
-> theory -> theory; |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
33 |
val add_pretty_list: string -> string -> string * (int * string) |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
34 |
-> theory -> theory; |
18217 | 35 |
val add_alias: string * string -> theory -> theory; |
36 |
val set_is_datatype: (theory -> string -> bool) -> theory -> theory; |
|
18455 | 37 |
val set_get_all_datatype_cons : (theory -> (string * string) list) |
18454 | 38 |
-> theory -> theory; |
18702 | 39 |
val set_int_tyco: string -> theory -> theory; |
18217 | 40 |
|
18516 | 41 |
val exprgen_type: theory -> auxtab |
18217 | 42 |
-> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact; |
18516 | 43 |
val exprgen_term: theory -> auxtab |
18217 | 44 |
-> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; |
18702 | 45 |
val appgen_default: appgen; |
18217 | 46 |
|
18335 | 47 |
val appgen_let: (int -> term -> term list * term) |
48 |
-> appgen; |
|
49 |
val appgen_split: (int -> term -> term list * term) |
|
50 |
-> appgen; |
|
18702 | 51 |
val appgen_number_of: (term -> term) -> (term -> IntInf.int) -> string -> string |
18335 | 52 |
-> appgen; |
18702 | 53 |
val add_case_const: (theory -> string -> (string * int) list option) -> xstring |
18517 | 54 |
-> theory -> theory; |
18702 | 55 |
val add_case_const_i: (theory -> string -> (string * int) list option) -> string |
18517 | 56 |
-> theory -> theory; |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
57 |
val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option) |
18335 | 58 |
-> (theory -> string * string -> typ list option) |
18217 | 59 |
-> defgen; |
60 |
||
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
61 |
val print_codegen_generated: theory -> unit; |
18454 | 62 |
val rename_inconsistent: theory -> theory; |
18517 | 63 |
val ensure_datatype_case_consts: (theory -> string list) |
64 |
-> (theory -> string -> (string * int) list option) |
|
65 |
-> theory -> theory; |
|
18515 | 66 |
|
67 |
(*debugging purpose only*) |
|
18454 | 68 |
structure InstNameMangler: NAME_MANGLER; |
69 |
structure ConstNameMangler: NAME_MANGLER; |
|
70 |
structure DatatypeconsNameMangler: NAME_MANGLER; |
|
18231 | 71 |
structure CodegenData: THEORY_DATA; |
18454 | 72 |
val mk_tabs: theory -> auxtab; |
73 |
val alias_get: theory -> string -> string; |
|
18515 | 74 |
val idf_of_name: theory -> string -> string -> string; |
75 |
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
|
76 |
end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
77 |
|
18217 | 78 |
structure CodegenPackage : CODEGEN_PACKAGE = |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
79 |
struct |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
80 |
|
18385 | 81 |
open CodegenThingolOp; |
82 |
infix 8 `%%; |
|
83 |
infixr 6 `->; |
|
84 |
infixr 6 `-->; |
|
85 |
infix 4 `$; |
|
86 |
infix 4 `$$; |
|
87 |
infixr 5 `|->; |
|
88 |
infixr 5 `|-->; |
|
18217 | 89 |
|
90 |
(* auxiliary *) |
|
91 |
||
18454 | 92 |
fun devarify_type ty = (fst o Type.freeze_thaw_type) ty; |
18335 | 93 |
fun devarify_term t = (fst o Type.freeze_thaw) t; |
18454 | 94 |
|
95 |
val is_number = is_some o Int.fromString; |
|
18217 | 96 |
|
18702 | 97 |
fun merge_opt _ (x1, NONE) = x1 |
98 |
| merge_opt _ (NONE, x2) = x2 |
|
99 |
| merge_opt eq (SOME x1, SOME x2) = |
|
100 |
if eq (x1, x2) then SOME x1 else error ("incompatible options during merge"); |
|
18217 | 101 |
|
102 |
||
18702 | 103 |
(* shallow name spaces *) |
18217 | 104 |
|
105 |
val nsp_class = "class"; |
|
18454 | 106 |
val nsp_tyco = "tyco"; |
18217 | 107 |
val nsp_const = "const"; |
18454 | 108 |
val nsp_overl = "overl"; |
109 |
val nsp_dtcon = "dtcon"; |
|
18217 | 110 |
val nsp_mem = "mem"; |
111 |
val nsp_inst = "inst"; |
|
112 |
||
113 |
||
18702 | 114 |
(* code generator basics *) |
18454 | 115 |
|
116 |
structure InstNameMangler = NameManglerFun ( |
|
117 |
type ctxt = theory; |
|
118 |
type src = string * (class * string); |
|
119 |
val ord = prod_ord string_ord (prod_ord string_ord string_ord); |
|
120 |
fun mk thy ((thyname, (cls, tyco)), i) = |
|
121 |
NameSpace.base cls ^ "_" ^ NameSpace.base tyco ^ implode (replicate i "'") |
|
122 |
|> NameSpace.append thyname; |
|
123 |
fun is_valid _ _ = true; |
|
124 |
fun maybe_unique _ _ = NONE; |
|
125 |
fun re_mangle _ dst = error ("no such instance: " ^ quote dst); |
|
126 |
); |
|
127 |
||
128 |
structure ConstNameMangler = NameManglerFun ( |
|
129 |
type ctxt = theory; |
|
130 |
type src = string * (typ * typ); |
|
131 |
val ord = prod_ord string_ord (prod_ord Term.typ_ord Term.typ_ord); |
|
132 |
fun mk thy ((c, (ty_decl, ty)), i) = |
|
133 |
let |
|
134 |
fun mangle (Type (tyco, tys)) = |
|
135 |
NameSpace.base tyco :: Library.flat (List.mapPartial mangle tys) |> SOME |
|
136 |
| mangle _ = |
|
137 |
NONE |
|
138 |
in |
|
139 |
Vartab.empty |
|
140 |
|> Sign.typ_match thy (ty_decl, ty) |
|
141 |
|> map (snd o snd) o Vartab.dest |
|
142 |
|> List.mapPartial mangle |
|
143 |
|> Library.flat |
|
144 |
|> null ? K ["x"] |
|
145 |
|> cons c |
|
146 |
|> space_implode "_" |
|
147 |
|> curry (op ^ o swap) ((implode oo replicate) i "'") |
|
148 |
end; |
|
149 |
fun is_valid _ _ = true; |
|
150 |
fun maybe_unique _ _ = NONE; |
|
151 |
fun re_mangle _ dst = error ("no such constant: " ^ quote dst); |
|
152 |
); |
|
153 |
||
154 |
structure DatatypeconsNameMangler = NameManglerFun ( |
|
155 |
type ctxt = theory; |
|
156 |
type src = string * string; |
|
157 |
val ord = prod_ord string_ord string_ord; |
|
18702 | 158 |
fun mk thy ((co, dtco), i) = |
18454 | 159 |
let |
160 |
fun basename 0 = NameSpace.base co |
|
18455 | 161 |
| basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co |
18454 | 162 |
| basename i = NameSpace.base dtco ^ "_" ^ NameSpace.base co ^ "_" ^ (implode oo replicate) (i-1) "'"; |
163 |
fun strip_dtco name = |
|
164 |
case (rev o NameSpace.unpack) name |
|
165 |
of x1::x2::xs => |
|
166 |
if x2 = NameSpace.base dtco |
|
167 |
then NameSpace.pack (x1::xs) |
|
168 |
else name |
|
169 |
| _ => name; |
|
170 |
in |
|
171 |
NameSpace.append (NameSpace.drop_base dtco) (basename i) |
|
172 |
|> strip_dtco |
|
173 |
end; |
|
174 |
fun is_valid _ _ = true; |
|
175 |
fun maybe_unique _ _ = NONE; |
|
176 |
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); |
|
177 |
); |
|
178 |
||
18702 | 179 |
type auxtab = ((typ * thm) list Symtab.table * string Symtab.table) |
18454 | 180 |
* (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); |
18702 | 181 |
type eqextr = theory -> auxtab |
182 |
-> (string * typ) -> (thm list * typ) option; |
|
18454 | 183 |
type defgen = theory -> auxtab -> gen_defgen; |
18702 | 184 |
type appgen = theory -> auxtab -> (string * typ) * term list -> transact -> iexpr * transact; |
18217 | 185 |
|
18702 | 186 |
val serializers = ref ( |
187 |
Symtab.empty |
|
188 |
|> Symtab.update ( |
|
189 |
#ml CodegenSerializer.serializers |
|
190 |
|> apsnd (fn seri => seri |
|
191 |
(nsp_dtcon, nsp_class, "") |
|
192 |
[[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] |
|
193 |
) |
|
194 |
) |
|
195 |
|> Symtab.update ( |
|
196 |
#haskell CodegenSerializer.serializers |
|
197 |
|> apsnd (fn seri => seri |
|
198 |
nsp_dtcon |
|
199 |
[[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]] |
|
200 |
) |
|
201 |
) |
|
202 |
); |
|
18217 | 203 |
|
204 |
||
18454 | 205 |
(* theory data for code generator *) |
18217 | 206 |
|
207 |
type gens = { |
|
18516 | 208 |
appconst: ((int * int) * (appgen * stamp)) Symtab.table, |
18702 | 209 |
eqextrs: (string * (eqextr * stamp)) list, |
18217 | 210 |
defgens: (string * (defgen * stamp)) list |
211 |
}; |
|
212 |
||
18702 | 213 |
fun map_gens f { appconst, eqextrs, defgens } = |
18217 | 214 |
let |
18702 | 215 |
val (appconst, eqextrs, defgens) = |
216 |
f (appconst, eqextrs, defgens) |
|
217 |
in { appconst = appconst, eqextrs = eqextrs, defgens = defgens } : gens end; |
|
18217 | 218 |
|
219 |
fun merge_gens |
|
18702 | 220 |
({ appconst = appconst1 , eqextrs = eqextrs1, defgens = defgens1 }, |
221 |
{ appconst = appconst2 , eqextrs = eqextrs2, defgens = defgens2 }) = |
|
18516 | 222 |
{ appconst = Symtab.merge |
223 |
(fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2) |
|
224 |
(appconst1, appconst2), |
|
18702 | 225 |
eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2), |
226 |
defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) |
|
227 |
} : gens; |
|
18217 | 228 |
|
229 |
type logic_data = { |
|
230 |
is_datatype: ((theory -> string -> bool) * stamp) option, |
|
18455 | 231 |
get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option, |
18217 | 232 |
alias: string Symtab.table * string Symtab.table |
233 |
}; |
|
234 |
||
18454 | 235 |
fun map_logic_data f { is_datatype, get_all_datatype_cons, alias } = |
18217 | 236 |
let |
18454 | 237 |
val ((is_datatype, get_all_datatype_cons), alias) = |
238 |
f ((is_datatype, get_all_datatype_cons), alias) |
|
18702 | 239 |
in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, |
240 |
alias = alias } : logic_data end; |
|
18217 | 241 |
|
242 |
fun merge_logic_data |
|
18702 | 243 |
({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, |
244 |
alias = alias1 }, |
|
245 |
{ is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, |
|
246 |
alias = alias2 }) = |
|
18217 | 247 |
let |
248 |
in |
|
249 |
{ is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2), |
|
18454 | 250 |
get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2), |
18217 | 251 |
alias = (Symtab.merge (op =) (fst alias1, fst alias2), |
18304 | 252 |
Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data |
18217 | 253 |
end; |
254 |
||
18702 | 255 |
type target_data = { |
18516 | 256 |
syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, |
257 |
syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table |
|
18217 | 258 |
}; |
259 |
||
18702 | 260 |
fun map_target_data f { syntax_tyco, syntax_const } = |
18217 | 261 |
let |
18517 | 262 |
val (syntax_tyco, syntax_const) = |
263 |
f (syntax_tyco, syntax_const) |
|
18702 | 264 |
in { syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data |
18454 | 265 |
end; |
18217 | 266 |
|
18702 | 267 |
fun merge_target_data |
268 |
({ syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, |
|
269 |
{ syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = |
|
270 |
{ syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), |
|
271 |
syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data; |
|
18217 | 272 |
|
273 |
structure CodegenData = TheoryDataFun |
|
274 |
(struct |
|
275 |
val name = "Pure/codegen_package"; |
|
276 |
type T = { |
|
277 |
modl: module, |
|
278 |
gens: gens, |
|
279 |
logic_data: logic_data, |
|
18702 | 280 |
target_data: target_data Symtab.table |
18217 | 281 |
}; |
282 |
val empty = { |
|
283 |
modl = empty_module, |
|
18702 | 284 |
gens = { appconst = Symtab.empty, eqextrs = [], defgens = [] } : gens, |
18454 | 285 |
logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE, |
286 |
alias = (Symtab.empty, Symtab.empty) } : logic_data, |
|
18702 | 287 |
target_data = |
18217 | 288 |
Symtab.empty |
18702 | 289 |
|> Symtab.fold (fn (target, _) => |
290 |
Symtab.update (target, { syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |
|
291 |
) (! serializers) |
|
18217 | 292 |
} : T; |
293 |
val copy = I; |
|
294 |
val extend = I; |
|
295 |
fun merge _ ( |
|
18702 | 296 |
{ modl = modl1, gens = gens1, |
297 |
target_data = target_data1, logic_data = logic_data1 }, |
|
298 |
{ modl = modl2, gens = gens2, |
|
299 |
target_data = target_data2, logic_data = logic_data2 } |
|
18217 | 300 |
) = { |
301 |
modl = merge_module (modl1, modl2), |
|
302 |
gens = merge_gens (gens1, gens2), |
|
303 |
logic_data = merge_logic_data (logic_data1, logic_data2), |
|
18702 | 304 |
target_data = Symtab.join (K (merge_target_data #> SOME)) |
305 |
(target_data1, target_data2) |
|
18217 | 306 |
}; |
18708 | 307 |
fun print _ _ = (); |
18217 | 308 |
end); |
309 |
||
18708 | 310 |
val _ = Context.add_setup CodegenData.init; |
311 |
||
18217 | 312 |
fun map_codegen_data f thy = |
313 |
case CodegenData.get thy |
|
18702 | 314 |
of { modl, gens, target_data, logic_data } => |
315 |
let val (modl, gens, target_data, logic_data) = |
|
316 |
f (modl, gens, target_data, logic_data) |
|
317 |
in CodegenData.put { modl = modl, gens = gens, |
|
318 |
target_data = target_data, logic_data = logic_data } thy end; |
|
18217 | 319 |
|
18517 | 320 |
fun print_codegen_generated thy = |
321 |
let |
|
322 |
val module = (#modl o CodegenData.get) thy; |
|
323 |
in |
|
324 |
(writeln o Pretty.output o Pretty.chunks) [pretty_module module, pretty_deps module] |
|
325 |
end; |
|
18217 | 326 |
|
18516 | 327 |
fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy = |
328 |
let |
|
329 |
val c = prep_const thy raw_c; |
|
330 |
in map_codegen_data |
|
18702 | 331 |
(fn (modl, gens, target_data, logic_data) => |
18217 | 332 |
(modl, |
333 |
gens |> map_gens |
|
18702 | 334 |
(fn (appconst, eqextrs, defgens) => |
18516 | 335 |
(appconst |
336 |
|> Symtab.update (c, (bounds, (ag, stamp ()))), |
|
18702 | 337 |
eqextrs, defgens)), target_data, logic_data)) thy |
18516 | 338 |
end; |
18217 | 339 |
|
18516 | 340 |
val add_appconst = gen_add_appconst Sign.intern_const; |
341 |
val add_appconst_i = gen_add_appconst (K I); |
|
18217 | 342 |
|
343 |
fun add_defgen (name, dg) = |
|
344 |
map_codegen_data |
|
18702 | 345 |
(fn (modl, gens, target_data, logic_data) => |
18217 | 346 |
(modl, |
347 |
gens |> map_gens |
|
18702 | 348 |
(fn (appconst, eqextrs, defgens) => |
349 |
(appconst, eqextrs, defgens |
|
18335 | 350 |
|> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))), |
18702 | 351 |
target_data, logic_data)); |
18217 | 352 |
|
18454 | 353 |
fun get_defgens thy tabs = |
354 |
(map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy; |
|
18217 | 355 |
|
18702 | 356 |
fun add_eqextr (name, eqx) = |
18217 | 357 |
map_codegen_data |
18702 | 358 |
(fn (modl, gens, target_data, logic_data) => |
359 |
(modl, |
|
360 |
gens |> map_gens |
|
361 |
(fn (appconst, eqextrs, defgens) => |
|
362 |
(appconst, eqextrs |
|
363 |
|> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())), |
|
364 |
defgens)), |
|
365 |
target_data, logic_data)); |
|
18217 | 366 |
|
18702 | 367 |
fun get_eqextrs thy tabs = |
368 |
(map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy; |
|
18454 | 369 |
|
370 |
fun is_datatype thy = |
|
371 |
case (#is_datatype o #logic_data o CodegenData.get) thy |
|
372 |
of NONE => K false |
|
373 |
| SOME (f, _) => f thy; |
|
374 |
||
375 |
fun get_all_datatype_cons thy = |
|
376 |
case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy |
|
377 |
of NONE => [] |
|
378 |
| SOME (f, _) => f thy; |
|
18217 | 379 |
|
380 |
fun add_alias (src, dst) = |
|
381 |
map_codegen_data |
|
18702 | 382 |
(fn (modl, gens, target_data, logic_data) => |
383 |
(modl, gens, target_data, |
|
18217 | 384 |
logic_data |> map_logic_data |
385 |
(apsnd (fn (tab, tab_rev) => |
|
386 |
(tab |> Symtab.update (src, dst), |
|
387 |
tab_rev |> Symtab.update (dst, src)))))); |
|
388 |
||
389 |
||
18454 | 390 |
(* name handling *) |
18217 | 391 |
|
18454 | 392 |
val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get; |
393 |
val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get; |
|
18217 | 394 |
|
18454 | 395 |
fun add_nsp shallow name = |
396 |
name |
|
397 |
|> NameSpace.unpack |
|
398 |
|> split_last |
|
399 |
|> apsnd (single #> cons shallow) |
|
400 |
|> (op @) |
|
401 |
|> NameSpace.pack; |
|
18702 | 402 |
|
18454 | 403 |
fun dest_nsp nsp idf = |
18217 | 404 |
let |
405 |
val idf' = NameSpace.unpack idf; |
|
406 |
val (idf'', idf_base) = split_last idf'; |
|
407 |
val (modl, shallow) = split_last idf''; |
|
408 |
in |
|
409 |
if nsp = shallow |
|
18454 | 410 |
then (SOME o NameSpace.pack) (modl @ [idf_base]) |
18217 | 411 |
else NONE |
412 |
end; |
|
413 |
||
18454 | 414 |
fun idf_of_name thy shallow name = |
18702 | 415 |
name |
416 |
|> alias_get thy |
|
417 |
|> add_nsp shallow; |
|
418 |
||
18454 | 419 |
fun name_of_idf thy shallow idf = |
420 |
idf |
|
421 |
|> dest_nsp shallow |
|
422 |
|> Option.map (alias_rev thy); |
|
18217 | 423 |
|
18702 | 424 |
fun set_is_datatype f = |
425 |
map_codegen_data |
|
426 |
(fn (modl, gens, target_data, logic_data) => |
|
427 |
(modl, gens, target_data, |
|
428 |
logic_data |
|
429 |
|> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons) |
|
430 |
=> (SOME (f, stamp ()), get_all_datatype_cons))))); |
|
431 |
||
432 |
fun set_get_all_datatype_cons f = |
|
433 |
map_codegen_data |
|
434 |
(fn (modl, gens, target_data, logic_data) => |
|
435 |
(modl, gens, target_data, |
|
436 |
logic_data |
|
437 |
|> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons) |
|
438 |
=> (is_datatype, SOME (f, stamp ()))))))); |
|
439 |
||
440 |
fun set_int_tyco tyco thy = |
|
441 |
(serializers := ( |
|
442 |
! serializers |
|
443 |
|> Symtab.update ( |
|
444 |
#ml CodegenSerializer.serializers |
|
445 |
|> apsnd (fn seri => seri |
|
446 |
(nsp_dtcon, nsp_class, idf_of_name thy nsp_tyco tyco) |
|
447 |
[[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] |
|
448 |
) |
|
449 |
) |
|
450 |
); thy); |
|
451 |
||
18516 | 452 |
|
18454 | 453 |
(* code generator instantiation *) |
18217 | 454 |
|
18454 | 455 |
fun ensure_def_class thy tabs cls trns = |
456 |
let |
|
457 |
val cls' = idf_of_name thy nsp_class cls; |
|
458 |
in |
|
459 |
trns |
|
460 |
|> debug 4 (fn _ => "generating class " ^ quote cls) |
|
461 |
|> gen_ensure_def (get_defgens thy tabs) ("generating class " ^ quote cls) cls' |
|
462 |
|> pair cls' |
|
463 |
end; |
|
18217 | 464 |
|
18454 | 465 |
fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = |
466 |
let |
|
18702 | 467 |
val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; |
18454 | 468 |
val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); |
469 |
in |
|
470 |
trns |
|
471 |
|> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) |
|
472 |
|> gen_ensure_def (get_defgens thy tabs) ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst |
|
473 |
|> pair inst |
|
474 |
end; |
|
18335 | 475 |
|
18454 | 476 |
fun ensure_def_tyco thy tabs tyco trns = |
477 |
let |
|
478 |
val tyco' = idf_of_name thy nsp_tyco tyco; |
|
18702 | 479 |
in |
480 |
trns |
|
481 |
|> debug 4 (fn _ => "generating type constructor " ^ quote tyco) |
|
482 |
|> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco' |
|
483 |
|> pair tyco' |
|
18454 | 484 |
end; |
485 |
||
486 |
fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) = |
|
487 |
let |
|
18515 | 488 |
fun get_overloaded (c, ty) = |
489 |
case Symtab.lookup overltab1 c |
|
490 |
of SOME (ty_decl, tys) => |
|
491 |
(case find_first (curry (Sign.typ_instance thy) ty) tys |
|
492 |
of SOME ty' => ConstNameMangler.get thy overltab2 |
|
493 |
(idf_of_name thy nsp_overl c, (ty_decl, ty')) |> SOME |
|
494 |
| _ => NONE) |
|
495 |
| _ => NONE |
|
496 |
fun get_datatypecons (c, ty) = |
|
497 |
case (snd o strip_type) ty |
|
498 |
of Type (tyco, _) => |
|
499 |
try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco) |
|
500 |
| _ => NONE; |
|
18702 | 501 |
in case get_datatypecons (c, ty) |
502 |
of SOME c' => idf_of_name thy nsp_dtcon c' |
|
503 |
| NONE => case get_overloaded (c, ty) |
|
18515 | 504 |
of SOME idf => idf |
505 |
| NONE => case Symtab.lookup clsmemtab c |
|
506 |
of SOME _ => idf_of_name thy nsp_mem c |
|
507 |
| NONE => idf_of_name thy nsp_const c |
|
508 |
end; |
|
18217 | 509 |
|
18454 | 510 |
fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = |
511 |
case name_of_idf thy nsp_const idf |
|
18702 | 512 |
of SOME c => SOME (c, Sign.the_const_type thy c) |
18454 | 513 |
| NONE => ( |
514 |
case dest_nsp nsp_overl idf |
|
515 |
of SOME _ => |
|
516 |
idf |
|
517 |
|> ConstNameMangler.rev thy overltab2 |
|
518 |
|> apfst (the o name_of_idf thy nsp_overl) |
|
519 |
|> apsnd snd |
|
520 |
|> SOME |
|
521 |
| NONE => NONE |
|
522 |
); |
|
523 |
||
524 |
fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns = |
|
525 |
let |
|
526 |
val c' = idf_of_const thy tabs (c, ty); |
|
18702 | 527 |
in |
528 |
trns |
|
529 |
|> debug 4 (fn _ => "generating constant " ^ quote c) |
|
530 |
|> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c' |
|
531 |
|> pair c' |
|
18454 | 532 |
end; |
18217 | 533 |
|
18702 | 534 |
(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = |
18454 | 535 |
let |
536 |
val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco; |
|
537 |
val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco; |
|
538 |
val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco; |
|
18515 | 539 |
val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity; |
18454 | 540 |
fun mk_eq_pred _ trns = |
541 |
trns |
|
18702 | 542 |
|> succeed (eqpred) |
18454 | 543 |
fun mk_eq_inst _ trns = |
544 |
trns |
|
545 |
|> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred |
|
18702 | 546 |
|> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))]))); |
18454 | 547 |
in |
548 |
trns |
|
549 |
|> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst |
|
18702 | 550 |
end; *) |
18454 | 551 |
|
18516 | 552 |
|
553 |
(* expression generators *) |
|
554 |
||
18702 | 555 |
fun exprgen_tyvar_sort thy tabs (v, sort) trns = |
18516 | 556 |
trns |
557 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort) |
|
18702 | 558 |
|-> (fn sort => pair (unprefix "'" v, sort)); |
18516 | 559 |
|
560 |
fun exprgen_type thy tabs (TVar _) trns = |
|
561 |
error "TVar encountered during code generation" |
|
18702 | 562 |
| exprgen_type thy tabs (TFree v_s) trns = |
18516 | 563 |
trns |
18702 | 564 |
|> exprgen_tyvar_sort thy tabs v_s |
565 |
|-> (fn v_s => pair (IVarT v_s)) |
|
18516 | 566 |
| exprgen_type thy tabs (Type ("fun", [t1, t2])) trns = |
567 |
trns |
|
568 |
|> exprgen_type thy tabs t1 |
|
569 |
||>> exprgen_type thy tabs t2 |
|
570 |
|-> (fn (t1', t2') => pair (t1' `-> t2')) |
|
571 |
| exprgen_type thy tabs (Type (tyco, tys)) trns = |
|
572 |
trns |
|
573 |
|> ensure_def_tyco thy tabs tyco |
|
574 |
||>> fold_map (exprgen_type thy tabs) tys |
|
575 |
|-> (fn (tyco, tys) => pair (tyco `%% tys)); |
|
576 |
||
18517 | 577 |
fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns = |
578 |
trns |
|
579 |
|> ensure_def_class thy tabs cls |
|
580 |
||>> ensure_def_inst thy tabs inst |
|
581 |
||>> (fold_map o fold_map) (mk_lookup thy tabs) ls |
|
582 |
|-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) |
|
583 |
| mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = |
|
18516 | 584 |
trns |
18517 | 585 |
|> fold_map (ensure_def_class thy tabs) clss |
586 |
|-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); |
|
587 |
||
18702 | 588 |
fun appgen_default thy tabs ((c, ty), ts) trns = |
589 |
trns |
|
590 |
|> ensure_def_const thy tabs (c, ty) |
|
591 |
||>> (fold_map o fold_map) (mk_lookup thy tabs) |
|
592 |
(ClassPackage.extract_sortlookup thy (c, ty)) |
|
593 |
||>> exprgen_type thy tabs ty |
|
594 |
||>> fold_map (exprgen_term thy tabs) ts |
|
595 |
|-> (fn (((c, ls), ty), es) => |
|
596 |
pair (Library.foldl IInst ((IConst (c, ty)), ls) `$$ es)) |
|
597 |
and appgen thy tabs ((f, ty), ts) trns = |
|
18517 | 598 |
case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f |
599 |
of SOME ((imin, imax), (ag, _)) => |
|
18702 | 600 |
if length ts < imin then |
18517 | 601 |
let |
602 |
val d = imin - length ts; |
|
603 |
val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d; |
|
604 |
val tys = Library.take (d, ((fst o strip_type) ty)); |
|
605 |
in |
|
606 |
trns |
|
607 |
|> debug 10 (fn _ => "eta-expanding") |
|
608 |
|> fold_map (exprgen_type thy tabs) tys |
|
18702 | 609 |
||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys) |
18517 | 610 |
|-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e)) |
611 |
end |
|
612 |
else if length ts > imax then |
|
613 |
trns |
|
614 |
|> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")") |
|
18702 | 615 |
|> ag thy tabs ((f, ty), Library.take (imax, ts)) |
18517 | 616 |
||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) |
617 |
|-> (fn es => pair (mk_apps es)) |
|
618 |
else |
|
619 |
trns |
|
620 |
|> debug 10 (fn _ => "keeping arguments") |
|
18702 | 621 |
|> ag thy tabs ((f, ty), ts) |
18517 | 622 |
| NONE => |
623 |
trns |
|
18702 | 624 |
|> appgen_default thy tabs ((f, ty), ts) |
18517 | 625 |
and exprgen_term thy tabs (Const (f, ty)) trns = |
626 |
trns |
|
627 |
|> appgen thy tabs ((f, ty), []) |
|
18516 | 628 |
|-> (fn e => pair e) |
629 |
| exprgen_term thy tabs (Var ((v, i), ty)) trns = |
|
630 |
trns |
|
631 |
|> exprgen_type thy tabs ty |
|
632 |
|-> (fn ty => pair (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty))) |
|
633 |
| exprgen_term thy tabs (Free (v, ty)) trns = |
|
634 |
trns |
|
635 |
|> exprgen_type thy tabs ty |
|
636 |
|-> (fn ty => pair (IVarE (v, ty))) |
|
637 |
| exprgen_term thy tabs (Abs (v, ty, t)) trns = |
|
638 |
trns |
|
639 |
|> exprgen_type thy tabs ty |
|
640 |
||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t)) |
|
641 |
|-> (fn (ty, e) => pair ((v, ty) `|-> e)) |
|
642 |
| exprgen_term thy tabs (t as t1 $ t2) trns = |
|
643 |
let |
|
644 |
val (t', ts) = strip_comb t |
|
645 |
in case t' |
|
646 |
of Const (f, ty) => |
|
647 |
trns |
|
18517 | 648 |
|> appgen thy tabs ((f, ty), ts) |
18516 | 649 |
|-> (fn e => pair e) |
650 |
| _ => |
|
651 |
trns |
|
652 |
|> exprgen_term thy tabs t' |
|
653 |
||>> fold_map (exprgen_term thy tabs) ts |
|
654 |
|-> (fn (e, es) => pair (e `$$ es)) |
|
655 |
end; |
|
656 |
||
18454 | 657 |
|
18517 | 658 |
(* application generators *) |
659 |
||
18702 | 660 |
(* fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns = |
18517 | 661 |
trns |
662 |
|> invoke_eq (exprgen_type thy tabs) (ensure_def_eq thy tabs) ty |
|
663 |
|-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty) |
|
664 |
| true => fn trns => trns |
|
665 |
|> exprgen_term thy tabs t1 |
|
666 |
||>> exprgen_term thy tabs t2 |
|
18702 | 667 |
|-> (fn (e1, e2) => pair (Fun_eq `$ e1 `$ e2))); *) |
668 |
||
669 |
||
670 |
(* function extractors *) |
|
671 |
||
672 |
fun mk_fun thy tabs (c, ty) trns = |
|
673 |
case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs) |
|
674 |
of SOME (eq_thms, ty) => |
|
675 |
let |
|
676 |
val sortctxt = ClassPackage.extract_sortctxt thy ty; |
|
677 |
fun dest_eqthm eq_thm = |
|
678 |
eq_thm |
|
679 |
|> prop_of |
|
680 |
|> Logic.dest_equals |
|
681 |
|> apfst (strip_comb #> snd); |
|
682 |
fun mk_eq (args, rhs) trns = |
|
683 |
trns |
|
684 |
|> fold_map (exprgen_term thy tabs o devarify_term) args |
|
685 |
||>> (exprgen_term thy tabs o devarify_term) rhs |
|
686 |
|-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) |
|
687 |
in |
|
688 |
trns |
|
689 |
|> fold_map (mk_eq o dest_eqthm) eq_thms |
|
690 |
||>> exprgen_type thy tabs (devarify_type ty) |
|
691 |
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt |
|
692 |
|-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty))) |
|
693 |
end |
|
694 |
| NONE => (NONE, trns); |
|
695 |
||
696 |
fun eqextr_defs thy ((deftab, _), _) (c, ty) = |
|
697 |
let |
|
698 |
fun eq_typ (ty1, ty2) = |
|
699 |
Sign.typ_instance thy (ty1, ty2) |
|
700 |
andalso Sign.typ_instance thy (ty2, ty1) |
|
701 |
in |
|
702 |
Option.mapPartial (get_first (fn (ty', thm) => if eq_typ (ty, ty') |
|
703 |
then SOME ([thm], ty') |
|
704 |
else NONE |
|
705 |
)) (Symtab.lookup deftab c) |
|
706 |
end; |
|
18517 | 707 |
|
708 |
||
709 |
(* definition generators *) |
|
18454 | 710 |
|
18702 | 711 |
fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) cls trns = |
18217 | 712 |
case name_of_idf thy nsp_class cls |
713 |
of SOME cls => |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
714 |
let |
18702 | 715 |
val cs = (snd o ClassPackage.the_consts_sign thy) cls; |
716 |
val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs; |
|
717 |
val idfs = map (idf_of_name thy nsp_mem o fst) cs; |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
718 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
719 |
trns |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
720 |
|> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) |
18702 | 721 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) |
722 |
||>> fold_map (exprgen_type thy tabs o snd) cs |
|
723 |
||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts |
|
724 |
|-> (fn ((supcls, memtypes), sortctxts) => succeed |
|
725 |
(Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), []))) |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
726 |
end |
18217 | 727 |
| _ => |
728 |
trns |
|
729 |
|> fail ("no class definition found for " ^ quote cls); |
|
730 |
||
18702 | 731 |
fun defgen_funs thy tabs c trns = |
732 |
case recconst_of_idf thy tabs c |
|
733 |
of SOME (c, ty) => |
|
734 |
trns |
|
735 |
|> mk_fun thy tabs (c, ty) |
|
736 |
|-> (fn (SOME funn) => succeed (Fun funn) |
|
737 |
| NONE => fail ("no defining equations found for " ^ quote c)) |
|
738 |
| NONE => |
|
739 |
trns |
|
740 |
|> fail ("not a constant: " ^ quote c); |
|
741 |
||
742 |
fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns = |
|
743 |
case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) |
|
744 |
of SOME (co, dtco) => |
|
745 |
trns |
|
746 |
|> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) |
|
747 |
|> ensure_def_tyco thy tabs dtco |
|
748 |
|-> (fn dtco => succeed Undef) |
|
749 |
| _ => |
|
750 |
trns |
|
751 |
|> fail ("not a datatype constructor: " ^ quote co); |
|
752 |
||
18454 | 753 |
fun defgen_clsmem thy tabs m trns = |
754 |
case name_of_idf thy nsp_mem m |
|
755 |
of SOME m => |
|
18360 | 756 |
trns |
18454 | 757 |
|> debug 5 (fn _ => "trying defgen class member for " ^ quote m) |
758 |
|> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) |
|
18702 | 759 |
|-> (fn cls => succeed Undef) |
18217 | 760 |
| _ => |
18454 | 761 |
trns |> fail ("no class member found for " ^ quote m) |
18217 | 762 |
|
18454 | 763 |
fun defgen_clsinst thy (tabs as (_, (insttab, _, _))) inst trns = |
764 |
case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) |
|
765 |
of SOME (_, (cls, tyco)) => |
|
18217 | 766 |
let |
18702 | 767 |
val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco); |
768 |
fun gen_membr (m, ty) trns = |
|
769 |
trns |
|
770 |
|> mk_fun thy tabs (m, ty) |
|
771 |
|-> (fn SOME funn => pair (m, funn) |
|
772 |
| NONE => error ("could not derive definition for member " ^ quote m)); |
|
18217 | 773 |
in |
18702 | 774 |
trns |
18231 | 775 |
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") |
18702 | 776 |
|> ensure_def_class thy tabs cls |
18454 | 777 |
||>> ensure_def_tyco thy tabs tyco |
18702 | 778 |
||>> fold_map (exprgen_tyvar_sort thy tabs) arity |
779 |
||>> fold_map gen_membr memdefs |
|
780 |
|-> (fn (((cls, tyco), arity), memdefs) => |
|
781 |
succeed (Classinst ((cls, (tyco, arity)), memdefs))) |
|
18217 | 782 |
end |
783 |
| _ => |
|
18454 | 784 |
trns |> fail ("no class instance found for " ^ quote inst); |
18217 | 785 |
|
786 |
||
787 |
(* parametrized generators, for instantiation in HOL *) |
|
788 |
||
18702 | 789 |
fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns = |
18517 | 790 |
let |
18702 | 791 |
fun dest_let (l as Const (c', _) $ t $ u) = |
792 |
if c = c' then |
|
793 |
case strip_abs 1 u |
|
794 |
of ([p], u') => apfst (cons (p, t)) (dest_let u') |
|
795 |
| _ => ([], l) |
|
796 |
else ([], t) |
|
18517 | 797 |
| dest_let t = ([], t); |
798 |
fun mk_let (l, r) trns = |
|
18335 | 799 |
trns |
18517 | 800 |
|> exprgen_term thy tabs l |
801 |
||>> exprgen_term thy tabs r |
|
802 |
|-> (fn (l, r) => pair (r, ipat_of_iexpr l)); |
|
18702 | 803 |
val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3) |
18517 | 804 |
in |
805 |
trns |
|
806 |
|> fold_map mk_let lets |
|
807 |
||>> exprgen_term thy tabs body |
|
808 |
|-> (fn (lets, body) => |
|
18702 | 809 |
pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body))) |
18517 | 810 |
end |
18217 | 811 |
|
18517 | 812 |
fun appgen_split strip_abs thy tabs (c, [t2]) trns = |
813 |
let |
|
814 |
val ([p], body) = strip_abs 1 (Const c $ t2) |
|
815 |
in |
|
816 |
trns |
|
817 |
|> exprgen_term thy tabs p |
|
818 |
||>> exprgen_term thy tabs body |
|
18702 | 819 |
|-> (fn (IVarE v, body) => pair (IAbs (v, body))) |
18517 | 820 |
end; |
18335 | 821 |
|
18702 | 822 |
fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_, |
823 |
Type (_, [_, ty as Type (tyco, [])])), [bin]) trns = |
|
824 |
if tyco = tyco_int then |
|
825 |
trns |
|
826 |
|> exprgen_type thy tabs ty |
|
827 |
|-> (fn ty => pair (CodegenThingol.IConst ((IntInf.toString o bin_to_int) bin, ty))) |
|
828 |
else if tyco = tyco_nat then |
|
829 |
trns |
|
830 |
|> exprgen_term thy tabs (mk_int_to_nat bin) |
|
831 |
else error ("invalid type constructor for numeral: " ^ quote tyco); |
|
18217 | 832 |
|
18517 | 833 |
fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns = |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
834 |
let |
18517 | 835 |
val (ts', t) = split_last ts; |
836 |
val (tys, dty) = (split_last o fst o strip_type) ty; |
|
837 |
fun gen_names i = |
|
838 |
variantlist (replicate i "x", foldr add_term_names |
|
839 |
(map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts); |
|
840 |
fun cg_case_d (((cname, i), ty), t) trns = |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
841 |
let |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
842 |
val vs = gen_names i; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
843 |
val tys = Library.take (i, (fst o strip_type) ty); |
18330 | 844 |
val frees = map2 (curry Free) vs tys; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
845 |
val t' = Envir.beta_norm (list_comb (t, frees)); |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
846 |
in |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
847 |
trns |
18516 | 848 |
|> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees)) |
849 |
||>> exprgen_term thy tabs t' |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
850 |
|-> (fn (ep, e) => pair (ipat_of_iexpr ep, e)) |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
851 |
end; |
18517 | 852 |
in |
853 |
trns |
|
854 |
|> exprgen_term thy tabs t |
|
855 |
||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts') |
|
18702 | 856 |
|-> (fn (t, ds) => pair (ICase (t, ds))) |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
857 |
end; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
858 |
|
18702 | 859 |
fun gen_add_case_const prep_c get_case_const_data raw_c thy = |
18517 | 860 |
let |
861 |
val c = prep_c thy raw_c; |
|
18702 | 862 |
val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_type thy) c; |
18517 | 863 |
val cos = (the o get_case_const_data thy) c; |
864 |
val n_eta = length cos + 1; |
|
865 |
in |
|
866 |
thy |
|
867 |
|> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos)) |
|
868 |
end; |
|
869 |
||
18702 | 870 |
val add_case_const = gen_add_case_const Sign.intern_const; |
871 |
val add_case_const_i = gen_add_case_const (K I); |
|
18517 | 872 |
|
18454 | 873 |
fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns = |
874 |
case name_of_idf thy nsp_tyco dtco |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
875 |
of SOME dtco => |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
876 |
(case get_datatype thy dtco |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
877 |
of SOME (vars, cos) => |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
878 |
let |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
879 |
val cotys = map (the o get_datacons thy o rpair dtco) cos; |
18454 | 880 |
val coidfs = map (fn co => (DatatypeconsNameMangler.get thy dtcontab (co, dtco)) |> |
881 |
idf_of_name thy nsp_dtcon) cos; |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
882 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
883 |
trns |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
884 |
|> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) |
18702 | 885 |
|> fold_map (exprgen_tyvar_sort thy tabs) vars |
18516 | 886 |
||>> (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
|
887 |
|-> (fn (sorts, tys) => succeed (Datatype |
18702 | 888 |
((sorts, coidfs ~~ tys), []))) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
889 |
end |
18217 | 890 |
| NONE => |
891 |
trns |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
892 |
|> fail ("no datatype found for " ^ quote dtco)) |
18217 | 893 |
| NONE => |
894 |
trns |
|
18454 | 895 |
|> fail ("not a type constructor: " ^ quote dtco) |
18335 | 896 |
|
18217 | 897 |
|
18516 | 898 |
|
899 |
(** theory interface **) |
|
18217 | 900 |
|
18454 | 901 |
fun mk_tabs thy = |
18217 | 902 |
let |
18454 | 903 |
fun extract_defs thy = |
18217 | 904 |
let |
18702 | 905 |
fun dest tm = |
18454 | 906 |
let |
18702 | 907 |
val (lhs, rhs) = Logic.dest_equals (prop_of tm); |
908 |
val (t, args) = strip_comb lhs; |
|
909 |
val (c, ty) = dest_Const t |
|
910 |
in if forall is_Var args then SOME ((c, ty), tm) else NONE |
|
18454 | 911 |
end handle TERM _ => NONE; |
912 |
fun prep_def def = (case Codegen.preprocess thy [def] of |
|
18702 | 913 |
[def'] => def' | _ => error "mk_auxtab: bad preprocessor"); |
914 |
fun add_def (name, _) = |
|
915 |
case (dest o prep_def o Thm.get_axiom thy) name |
|
916 |
of SOME ((c, ty), tm) => |
|
917 |
Symtab.default (c, []) #> Symtab.map_entry c (cons (ty, tm)) |
|
918 |
| NONE => I |
|
18217 | 919 |
in |
18454 | 920 |
Symtab.empty |
18702 | 921 |
|> fold (Symtab.fold add_def o snd o #axioms o Theory.rep_theory) |
922 |
(thy :: Theory.ancestors_of thy) |
|
18217 | 923 |
end; |
18454 | 924 |
fun mk_insttab thy = |
925 |
InstNameMangler.empty |
|
926 |
|> Symtab.fold_map |
|
18702 | 927 |
(fn (cls, (clsmems, clsinsts)) => fold_map |
18454 | 928 |
(fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts) |
929 |
(ClassPackage.get_classtab thy) |
|
930 |
|-> (fn _ => I); |
|
18702 | 931 |
fun mk_overltabs thy deftab = |
18454 | 932 |
(Symtab.empty, ConstNameMangler.empty) |
933 |
|> Symtab.fold |
|
934 |
(fn (c, [_]) => I |
|
935 |
| (c, tytab) => |
|
936 |
(fn (overltab1, overltab2) => ( |
|
937 |
overltab1 |
|
938 |
|> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), |
|
939 |
overltab2 |
|
940 |
|> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab |
|
18702 | 941 |
))) deftab; |
18454 | 942 |
fun mk_dtcontab thy = |
943 |
DatatypeconsNameMangler.empty |
|
944 |
|> fold_map |
|
18455 | 945 |
(fn (_, co_dtco) => DatatypeconsNameMangler.declare_multi thy co_dtco) |
946 |
(fold (fn (co, dtco) => |
|
947 |
let |
|
948 |
val key = ((NameSpace.drop_base o NameSpace.drop_base) co, NameSpace.base co) |
|
949 |
in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end |
|
950 |
) (get_all_datatype_cons thy) []) |
|
18454 | 951 |
|-> (fn _ => I); |
952 |
fun mk_clsmemtab thy = |
|
953 |
Symtab.empty |
|
954 |
|> Symtab.fold |
|
955 |
(fn (class, (clsmems, _)) => fold |
|
956 |
(fn clsmem => Symtab.update (clsmem, class)) clsmems) |
|
957 |
(ClassPackage.get_classtab thy); |
|
18702 | 958 |
val deftab = extract_defs thy; |
18454 | 959 |
val insttab = mk_insttab thy; |
18702 | 960 |
val overltabs = mk_overltabs thy deftab; |
18454 | 961 |
val dtcontab = mk_dtcontab thy; |
962 |
val clsmemtab = mk_clsmemtab thy; |
|
963 |
in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end; |
|
18217 | 964 |
|
18702 | 965 |
fun check_for_target thy target = |
966 |
if (Symtab.defined o #target_data o CodegenData.get) thy target |
|
967 |
then () |
|
968 |
else error ("unknown code target language: " ^ quote target); |
|
18335 | 969 |
|
18516 | 970 |
fun map_module f = |
18702 | 971 |
map_codegen_data (fn (modl, gens, target_data, logic_data) => |
972 |
(f modl, gens, target_data, logic_data)); |
|
18516 | 973 |
|
18702 | 974 |
fun expand_module gen thy = |
18516 | 975 |
(#modl o CodegenData.get) thy |
18702 | 976 |
|> start_transact (gen thy (mk_tabs thy)) |
18516 | 977 |
|-> (fn x:'a => fn modl => (x, map_module (K modl) thy)); |
978 |
||
979 |
fun rename_inconsistent thy = |
|
18217 | 980 |
let |
18516 | 981 |
fun get_inconsistent thyname = |
982 |
let |
|
983 |
val thy = theory thyname; |
|
984 |
fun own_tables get = |
|
985 |
(get thy) |
|
986 |
|> fold (Symtab.fold (Symtab.remove (K true)) o get) (Theory.parents_of thy) |
|
987 |
|> Symtab.keys; |
|
988 |
val names = own_tables (#2 o #types o Type.rep_tsig o Sign.tsig_of) |
|
989 |
@ own_tables (#2 o #declarations o Consts.dest o #consts o Sign.rep_sg); |
|
990 |
fun diff names = |
|
991 |
fold (fn name => |
|
992 |
if is_prefix (op =) (NameSpace.unpack thyname) (NameSpace.unpack name) |
|
993 |
then I |
|
994 |
else cons (name, NameSpace.append thyname (NameSpace.base name))) names []; |
|
995 |
in diff names end; |
|
996 |
val inconsistent = map get_inconsistent (ThyInfo.names ()) |> Library.flat; |
|
997 |
fun add (src, dst) thy = |
|
998 |
if (is_some oo Symtab.lookup o fst o #alias o #logic_data o CodegenData.get) thy src |
|
999 |
then (warning ("code generator alias already defined for " ^ quote src ^ ", will not overwrite"); thy) |
|
1000 |
else add_alias (src, dst) thy |
|
1001 |
in fold add inconsistent thy end; |
|
1002 |
||
18517 | 1003 |
fun ensure_datatype_case_consts get_datatype_case_consts get_case_const_data thy = |
1004 |
let |
|
1005 |
fun ensure case_c thy = |
|
1006 |
if |
|
1007 |
Symtab.defined ((#appconst o #gens o CodegenData.get) thy) case_c |
|
1008 |
then |
|
1009 |
(warning ("case constant " ^ quote case_c ^ " already present in application table, will not overwrite"); thy) |
|
1010 |
else |
|
18702 | 1011 |
add_case_const_i get_case_const_data case_c thy; |
18517 | 1012 |
in |
1013 |
fold ensure (get_datatype_case_consts thy) thy |
|
1014 |
end; |
|
1015 |
||
18516 | 1016 |
|
1017 |
||
1018 |
(** target languages **) |
|
1019 |
||
1020 |
(* primitive definitions *) |
|
1021 |
||
18702 | 1022 |
fun read_typ thy = |
1023 |
Sign.read_typ (thy, K NONE); |
|
1024 |
||
18517 | 1025 |
fun read_const thy (raw_c, raw_ty) = |
1026 |
let |
|
1027 |
val c = Sign.intern_const thy raw_c; |
|
18702 | 1028 |
val _ = if Sign.declared_const thy c |
1029 |
then () |
|
1030 |
else error ("no such constant: " ^ quote c); |
|
18517 | 1031 |
val ty = case raw_ty |
1032 |
of NONE => Sign.the_const_constraint thy c |
|
18702 | 1033 |
| SOME raw_ty => read_typ thy raw_ty; |
18517 | 1034 |
in (c, ty) end; |
1035 |
||
18702 | 1036 |
fun read_quote reader gen raw thy = |
1037 |
expand_module |
|
1038 |
(fn thy => fn tabs => gen thy tabs (reader thy raw)) |
|
1039 |
thy; |
|
1040 |
||
18517 | 1041 |
fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy = |
18516 | 1042 |
let |
18702 | 1043 |
val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target |
18516 | 1044 |
then () else error ("unknown target language: " ^ quote target); |
1045 |
val tabs = mk_tabs thy; |
|
1046 |
val name = prep_name thy tabs raw_name; |
|
1047 |
val primdef = prep_primdef raw_primdef; |
|
18217 | 1048 |
in |
18516 | 1049 |
thy |
18517 | 1050 |
|> map_module (CodegenThingol.add_prim name deps (target, primdef)) |
18217 | 1051 |
end; |
1052 |
||
18516 | 1053 |
val add_prim_i = gen_add_prim ((K o K) I) I; |
1054 |
val add_prim_class = gen_add_prim |
|
1055 |
(fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy)) |
|
18702 | 1056 |
(Pretty.str o CodegenSerializer.parse_targetdef I); |
18516 | 1057 |
val add_prim_tyco = gen_add_prim |
1058 |
(fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy)) |
|
18702 | 1059 |
(Pretty.str o CodegenSerializer.parse_targetdef I); |
18516 | 1060 |
val add_prim_const = gen_add_prim |
18517 | 1061 |
(fn thy => fn tabs => idf_of_const thy tabs o read_const thy) |
18702 | 1062 |
(Pretty.str o CodegenSerializer.parse_targetdef I); |
18516 | 1063 |
|
18702 | 1064 |
val ensure_prim = (map_module oo CodegenThingol.ensure_prim); |
18217 | 1065 |
|
18517 | 1066 |
|
18217 | 1067 |
(* syntax *) |
1068 |
||
18702 | 1069 |
val parse_syntax_tyco = |
18217 | 1070 |
let |
18702 | 1071 |
fun mk reader raw_tyco target thy = |
1072 |
let |
|
1073 |
val _ = check_for_target thy target; |
|
1074 |
fun check_tyco tyco = |
|
1075 |
if Sign.declared_tyname thy tyco |
|
1076 |
then tyco |
|
1077 |
else error ("no such type constructor: " ^ quote tyco); |
|
1078 |
fun prep_tyco thy tyco = |
|
1079 |
tyco |
|
1080 |
|> Sign.intern_type thy |
|
1081 |
|> check_tyco |
|
1082 |
|> idf_of_name thy nsp_tyco; |
|
1083 |
val tyco = prep_tyco thy raw_tyco; |
|
1084 |
in |
|
1085 |
thy |
|
1086 |
|> ensure_prim tyco target |
|
1087 |
|> reader |
|
1088 |
|-> (fn pretty => map_codegen_data |
|
1089 |
(fn (modl, gens, target_data, logic_data) => |
|
1090 |
(modl, gens, |
|
1091 |
target_data |> Symtab.map_entry target |
|
1092 |
(map_target_data |
|
1093 |
(fn (syntax_tyco, syntax_const) => |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1094 |
(syntax_tyco |> Symtab.update |
18702 | 1095 |
(tyco, (pretty, stamp ())), |
1096 |
syntax_const))), |
|
1097 |
logic_data))) |
|
1098 |
end; |
|
18217 | 1099 |
in |
18702 | 1100 |
CodegenSerializer.parse_syntax (read_quote read_typ exprgen_type) |
1101 |
#-> (fn reader => pair (mk reader)) |
|
18217 | 1102 |
end; |
1103 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1104 |
fun add_pretty_syntax_const c target pretty = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1105 |
map_codegen_data |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1106 |
(fn (modl, gens, target_data, logic_data) => |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1107 |
(modl, gens, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1108 |
target_data |> Symtab.map_entry target |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1109 |
(map_target_data |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1110 |
(fn (syntax_tyco, syntax_const) => |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1111 |
(syntax_tyco, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1112 |
syntax_const |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1113 |
|> Symtab.update |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1114 |
(c, (pretty, stamp ()))))), |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1115 |
logic_data)); |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1116 |
|
18702 | 1117 |
val parse_syntax_const = |
18217 | 1118 |
let |
18702 | 1119 |
fun mk reader raw_const target thy = |
1120 |
let |
|
1121 |
val _ = check_for_target thy target; |
|
1122 |
val tabs = mk_tabs thy; |
|
1123 |
val c = idf_of_const thy tabs (read_const thy raw_const); |
|
1124 |
in |
|
1125 |
thy |
|
1126 |
|> ensure_prim c target |
|
1127 |
|> reader |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1128 |
|-> (fn pretty => add_pretty_syntax_const c target pretty) |
18702 | 1129 |
end; |
18217 | 1130 |
in |
18702 | 1131 |
CodegenSerializer.parse_syntax (read_quote Sign.read_term exprgen_term) |
1132 |
#-> (fn reader => pair (mk reader)) |
|
18217 | 1133 |
end; |
1134 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1135 |
fun add_pretty_list raw_nil raw_cons (target, seri) thy = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1136 |
let |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1137 |
val _ = check_for_target thy target; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1138 |
val tabs = mk_tabs thy; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1139 |
fun mk_const raw_name = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1140 |
let |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1141 |
val name = Sign.intern_const thy raw_name; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1142 |
in idf_of_const thy tabs (name, Sign.the_const_type thy name) end; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1143 |
val nil' = mk_const raw_nil; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1144 |
val cons' = mk_const raw_cons; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1145 |
val pr' = CodegenSerializer.pretty_list nil' cons' seri; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1146 |
in |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1147 |
thy |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1148 |
|> ensure_prim cons' target |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1149 |
|> add_pretty_syntax_const cons' target pr' |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1150 |
end; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
1151 |
|
18217 | 1152 |
|
18516 | 1153 |
|
1154 |
(** code generation **) |
|
18217 | 1155 |
|
18702 | 1156 |
fun generate_code raw_consts thy = |
18217 | 1157 |
let |
18702 | 1158 |
val consts = map (read_const thy) raw_consts; |
1159 |
fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts |
|
18217 | 1160 |
in |
1161 |
thy |
|
18702 | 1162 |
|> expand_module generate |
18217 | 1163 |
end; |
1164 |
||
18702 | 1165 |
fun serialize_code target filename raw_consts thy = |
18217 | 1166 |
let |
18702 | 1167 |
fun get_serializer thy target = |
1168 |
let |
|
1169 |
val _ = check_for_target thy target; |
|
1170 |
val target_data = |
|
1171 |
thy |
|
1172 |
|> CodegenData.get |
|
1173 |
|> #target_data |
|
1174 |
|> (fn data => (the oo Symtab.lookup) data target); |
|
1175 |
in |
|
1176 |
(the o Symtab.lookup (! serializers)) target ( |
|
1177 |
(Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, |
|
1178 |
(Option.map fst oo Symtab.lookup o #syntax_const) target_data |
|
1179 |
) |
|
1180 |
end; |
|
18282 | 1181 |
fun use_code code = |
18702 | 1182 |
if target = "ml" andalso filename = "-" |
18217 | 1183 |
then use_text Context.ml_output false code |
1184 |
else File.write (Path.unpack filename) (code ^ "\n"); |
|
18702 | 1185 |
fun serialize thy cs = |
1186 |
let |
|
1187 |
val module = (#modl o CodegenData.get) thy; |
|
1188 |
val seri = get_serializer thy target "Generated"; |
|
1189 |
in case cs |
|
1190 |
of [] => seri NONE module () |> fst |> Pretty.output |> use_code |
|
1191 |
| cs => seri (SOME cs) module () |> fst |> Pretty.output |> use_code |
|
1192 |
end; |
|
18217 | 1193 |
in |
1194 |
thy |
|
18702 | 1195 |
|> (if is_some raw_consts then generate_code (the raw_consts) else pair []) |
1196 |
|-> (fn cs => `(fn thy => serialize thy cs)) |
|
1197 |
|-> (fn _ => I) |
|
18217 | 1198 |
end; |
1199 |
||
1200 |
||
18454 | 1201 |
|
18516 | 1202 |
(** toplevel interface **) |
18217 | 1203 |
|
1204 |
local |
|
1205 |
||
1206 |
structure P = OuterParse |
|
1207 |
and K = OuterKeyword |
|
1208 |
||
1209 |
in |
|
1210 |
||
18517 | 1211 |
val (classK, generateK, serializeK, |
1212 |
primclassK, primtycoK, primconstK, |
|
1213 |
syntax_tycoK, syntax_constK, aliasK) = |
|
1214 |
("code_class", "code_generate", "code_serialize", |
|
1215 |
"code_primclass", "code_primtyco", "code_primconst", |
|
1216 |
"code_syntax_tyco", "code_syntax_const", "code_alias"); |
|
1217 |
val (constantsK, dependingK) = |
|
1218 |
("constants", "depending_on"); |
|
18335 | 1219 |
|
1220 |
val classP = |
|
1221 |
OuterSyntax.command classK "codegen data for classes" K.thy_decl ( |
|
1222 |
P.xname |
|
1223 |
-- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) |
|
1224 |
-- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) []) |
|
1225 |
>> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos))) |
|
1226 |
) |
|
18217 | 1227 |
|
1228 |
val generateP = |
|
18282 | 1229 |
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
|
1230 |
Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
18217 | 1231 |
>> (fn consts => |
18231 | 1232 |
Toplevel.theory (generate_code consts #> snd)) |
18217 | 1233 |
); |
1234 |
||
1235 |
val serializeP = |
|
18282 | 1236 |
OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( |
18217 | 1237 |
P.name |
1238 |
-- P.name |
|
1239 |
-- Scan.option ( |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1240 |
P.$$$ constantsK |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
1241 |
|-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) |
18217 | 1242 |
) |
18702 | 1243 |
>> (fn ((target, filename), raw_consts) => |
1244 |
Toplevel.theory (serialize_code target filename raw_consts)) |
|
18217 | 1245 |
); |
1246 |
||
1247 |
val aliasP = |
|
18282 | 1248 |
OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( |
18702 | 1249 |
Scan.repeat1 (P.name -- P.name) |
1250 |
>> (Toplevel.theory oo fold) add_alias |
|
18217 | 1251 |
); |
1252 |
||
18517 | 1253 |
val primclassP = |
1254 |
OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl ( |
|
1255 |
P.xname |
|
18702 | 1256 |
-- Scan.optional (P.$$$ dependingK |-- |
1257 |
P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] |
|
18517 | 1258 |
-- Scan.repeat1 (P.name -- P.text) |
18702 | 1259 |
>> (fn ((raw_class, depends), primdefs) => |
18517 | 1260 |
(Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs) |
1261 |
); |
|
1262 |
||
1263 |
val primtycoP = |
|
1264 |
OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl ( |
|
1265 |
P.xname |
|
18702 | 1266 |
-- Scan.optional (P.$$$ dependingK |-- |
1267 |
P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] |
|
18517 | 1268 |
-- Scan.repeat1 (P.name -- P.text) |
18702 | 1269 |
>> (fn ((raw_tyco, depends), primdefs) => |
18517 | 1270 |
(Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs) |
1271 |
); |
|
1272 |
||
1273 |
val primconstP = |
|
1274 |
OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl ( |
|
18702 | 1275 |
(P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) |
1276 |
-- Scan.optional (P.$$$ dependingK |-- |
|
1277 |
P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] |
|
18517 | 1278 |
-- Scan.repeat1 (P.name -- P.text) |
18702 | 1279 |
>> (fn ((raw_const, depends), primdefs) => |
18517 | 1280 |
(Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs) |
1281 |
); |
|
1282 |
||
18702 | 1283 |
val _ : OuterParse.token list -> (string -> string -> theory -> theory) * OuterParse.token list |
1284 |
= parse_syntax_tyco; |
|
1285 |
||
18217 | 1286 |
val syntax_tycoP = |
1287 |
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( |
|
18702 | 1288 |
Scan.repeat1 ( |
1289 |
P.xname |
|
1290 |
-- Scan.repeat1 ( |
|
1291 |
P.name -- parse_syntax_tyco |
|
1292 |
) |
|
1293 |
) |
|
1294 |
>> (Toplevel.theory oo fold) (fn (raw_tyco, syns) => |
|
1295 |
fold (fn (target, modifier) => modifier raw_tyco target) syns) |
|
18217 | 1296 |
); |
1297 |
||
1298 |
val syntax_constP = |
|
1299 |
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl ( |
|
18702 | 1300 |
Scan.repeat1 ( |
1301 |
(P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) |
|
1302 |
-- Scan.repeat1 ( |
|
1303 |
P.name -- parse_syntax_const |
|
1304 |
) |
|
1305 |
) |
|
1306 |
>> (Toplevel.theory oo fold) (fn (raw_c, syns) => |
|
1307 |
fold (fn (target, modifier) => modifier raw_c target) syns) |
|
18217 | 1308 |
); |
1309 |
||
18517 | 1310 |
val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, |
1311 |
primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP]; |
|
1312 |
val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", constantsK, dependingK]; |
|
18217 | 1313 |
|
1314 |
||
18516 | 1315 |
|
18708 | 1316 |
(** theory setup **) |
18516 | 1317 |
|
18708 | 1318 |
val _ = Context.add_setup |
1319 |
(add_eqextr ("defs", eqextr_defs) #> |
|
1320 |
add_defgen ("clsdecl", defgen_clsdecl) #> |
|
1321 |
add_defgen ("funs", defgen_funs) #> |
|
1322 |
add_defgen ("clsmem", defgen_clsmem) #> |
|
1323 |
add_defgen ("datatypecons", defgen_datatypecons)); |
|
1324 |
||
1325 |
(* add_appconst_i ("op =", ((2, 2), appgen_eq)) *) |
|
1326 |
(* add_defgen ("clsinst", defgen_clsinst) *) |
|
18217 | 1327 |
|
1328 |
end; (* local *) |
|
1329 |
||
1330 |
end; (* struct *) |