author | haftmann |
Mon, 21 Aug 2006 11:02:40 +0200 | |
changeset 20401 | f01ae74f29f2 |
parent 20389 | 8b6ecb22ef35 |
child 20428 | 67fa1c6ba89e |
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 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
9 |
signature CODEGEN_PACKAGE = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
10 |
sig |
20105 | 11 |
val codegen_term: term -> theory -> CodegenThingol.iterm * theory; |
20389 | 12 |
val eval_term: (string (*reference name!*) * 'a ref) * term |
13 |
-> theory -> 'a * theory; |
|
19884 | 14 |
val is_dtcon: string -> bool; |
15 |
val consts_of_idfs: theory -> string list -> (string * typ) list; |
|
16 |
val idfs_of_consts: theory -> (string * typ) list -> string list; |
|
19967 | 17 |
val get_root_module: theory -> CodegenThingol.module * theory; |
19884 | 18 |
val get_ml_fun_datatype: theory -> (string -> string) |
19 |
-> ((string * CodegenThingol.funn) list -> Pretty.T) |
|
20 |
* ((string * CodegenThingol.datatyp) list -> Pretty.T); |
|
18702 | 21 |
|
20401 | 22 |
val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T) |
23 |
-> ((string -> string) * (string -> string)) option -> int * string |
|
24 |
-> theory -> theory; |
|
25 |
val add_pretty_ml_string: string -> string -> string -> string |
|
26 |
-> (string -> string) -> (string -> string) -> string -> theory -> theory; |
|
20175 | 27 |
val purge_code: theory -> theory; |
18217 | 28 |
|
19884 | 29 |
type appgen; |
20105 | 30 |
val add_appconst: xstring * appgen -> theory -> theory; |
31 |
val add_appconst_i: string * appgen -> theory -> theory; |
|
18702 | 32 |
val appgen_default: appgen; |
20353 | 33 |
val appgen_rep_bin: (theory -> term -> IntInf.int) -> appgen; |
19607
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
34 |
val appgen_char: (term -> int option) -> appgen; |
20105 | 35 |
val appgen_case: (theory -> term |
36 |
-> ((string * typ) list * ((term * typ) * (term * term) list)) option) |
|
37 |
-> appgen; |
|
38 |
val appgen_let: appgen; |
|
19038 | 39 |
val appgen_wfrec: appgen; |
18217 | 40 |
|
19008 | 41 |
val print_code: theory -> unit; |
18515 | 42 |
|
18231 | 43 |
structure CodegenData: THEORY_DATA; |
19884 | 44 |
type auxtab; |
20353 | 45 |
val mk_tabs: theory -> string list option -> (string * typ) list -> auxtab; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
46 |
end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
47 |
|
18217 | 48 |
structure CodegenPackage : CODEGEN_PACKAGE = |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
49 |
struct |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
50 |
|
18850 | 51 |
open CodegenThingol; |
18217 | 52 |
|
18702 | 53 |
(* shallow name spaces *) |
18217 | 54 |
|
20216 | 55 |
val nsp_module = ""; (*a dummy by convention*) |
18217 | 56 |
val nsp_class = "class"; |
18454 | 57 |
val nsp_tyco = "tyco"; |
18217 | 58 |
val nsp_const = "const"; |
18454 | 59 |
val nsp_dtcon = "dtcon"; |
18217 | 60 |
val nsp_mem = "mem"; |
61 |
val nsp_inst = "inst"; |
|
19213 | 62 |
val nsp_instmem = "instmem"; |
20216 | 63 |
val nsp_eval = "EVAL"; (*only for evaluation*) |
18217 | 64 |
|
19038 | 65 |
fun add_nsp shallow name = |
66 |
name |
|
67 |
|> NameSpace.unpack |
|
68 |
|> split_last |
|
69 |
|> apsnd (single #> cons shallow) |
|
70 |
|> (op @) |
|
71 |
|> NameSpace.pack; |
|
72 |
||
73 |
fun dest_nsp nsp idf = |
|
74 |
let |
|
75 |
val idf' = NameSpace.unpack idf; |
|
76 |
val (idf'', idf_base) = split_last idf'; |
|
77 |
val (modl, shallow) = split_last idf''; |
|
78 |
in |
|
79 |
if nsp = shallow |
|
80 |
then (SOME o NameSpace.pack) (modl @ [idf_base]) |
|
81 |
else NONE |
|
82 |
end; |
|
83 |
||
20386 | 84 |
fun if_nsp nsp f idf = |
85 |
Option.map f (dest_nsp nsp idf); |
|
19956 | 86 |
|
87 |
||
18702 | 88 |
(* code generator basics *) |
18454 | 89 |
|
20386 | 90 |
type auxtab = (bool * string list option) * CodegenTheorems.thmtab; |
18865 | 91 |
type appgen = theory -> auxtab |
20105 | 92 |
-> (string * typ) * term list -> transact -> iterm * transact; |
18217 | 93 |
|
18702 | 94 |
val serializers = ref ( |
95 |
Symtab.empty |
|
96 |
|> Symtab.update ( |
|
97 |
#ml CodegenSerializer.serializers |
|
98 |
|> apsnd (fn seri => seri |
|
20183 | 99 |
nsp_dtcon |
20389 | 100 |
[[nsp_module], [nsp_class, nsp_tyco], |
101 |
[nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]] |
|
18702 | 102 |
) |
103 |
) |
|
104 |
|> Symtab.update ( |
|
105 |
#haskell CodegenSerializer.serializers |
|
106 |
|> apsnd (fn seri => seri |
|
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
107 |
(nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon]) |
20389 | 108 |
[[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_mem], |
109 |
[nsp_dtcon], [nsp_inst], [nsp_instmem]] |
|
18702 | 110 |
) |
111 |
) |
|
112 |
); |
|
18217 | 113 |
|
114 |
||
18454 | 115 |
(* theory data for code generator *) |
18217 | 116 |
|
20105 | 117 |
type appgens = (int * (appgen * stamp)) Symtab.table |
18217 | 118 |
|
20386 | 119 |
fun merge_appgens (x : appgens * appgens) = |
20105 | 120 |
Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => |
121 |
bounds1 = bounds2 andalso stamp1 = stamp2) x |
|
18217 | 122 |
|
18702 | 123 |
type target_data = { |
18865 | 124 |
syntax_class: string Symtab.table, |
18516 | 125 |
syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, |
20105 | 126 |
syntax_const: (iterm CodegenSerializer.pretty_syntax * stamp) Symtab.table |
18217 | 127 |
}; |
128 |
||
18865 | 129 |
fun map_target_data f { syntax_class, syntax_tyco, syntax_const } = |
18217 | 130 |
let |
18865 | 131 |
val (syntax_class, syntax_tyco, syntax_const) = |
132 |
f (syntax_class, syntax_tyco, syntax_const) |
|
133 |
in { |
|
134 |
syntax_class = syntax_class, |
|
135 |
syntax_tyco = syntax_tyco, |
|
136 |
syntax_const = syntax_const } : target_data |
|
18454 | 137 |
end; |
18217 | 138 |
|
18702 | 139 |
fun merge_target_data |
18865 | 140 |
({ syntax_class = syntax_class1, syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, |
141 |
{ syntax_class = syntax_class2, syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = |
|
142 |
{ syntax_class = Symtab.merge (op =) (syntax_class1, syntax_class2), |
|
143 |
syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), |
|
18702 | 144 |
syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data; |
18217 | 145 |
|
146 |
structure CodegenData = TheoryDataFun |
|
147 |
(struct |
|
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
148 |
val name = "Pure/codegen_package"; |
18217 | 149 |
type T = { |
150 |
modl: module, |
|
20105 | 151 |
appgens: appgens, |
18702 | 152 |
target_data: target_data Symtab.table |
18217 | 153 |
}; |
154 |
val empty = { |
|
155 |
modl = empty_module, |
|
20105 | 156 |
appgens = Symtab.empty, |
18702 | 157 |
target_data = |
18217 | 158 |
Symtab.empty |
18702 | 159 |
|> Symtab.fold (fn (target, _) => |
18865 | 160 |
Symtab.update (target, |
161 |
{ syntax_class = Symtab.empty, syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |
|
18702 | 162 |
) (! serializers) |
18217 | 163 |
} : T; |
164 |
val copy = I; |
|
165 |
val extend = I; |
|
166 |
fun merge _ ( |
|
20105 | 167 |
{ modl = modl1, appgens = appgens1, |
20386 | 168 |
target_data = target_data1 }, |
20105 | 169 |
{ modl = modl2, appgens = appgens2, |
20386 | 170 |
target_data = target_data2 } |
18217 | 171 |
) = { |
172 |
modl = merge_module (modl1, modl2), |
|
20105 | 173 |
appgens = merge_appgens (appgens1, appgens2), |
19025 | 174 |
target_data = Symtab.join (K merge_target_data) (target_data1, target_data2) |
18217 | 175 |
}; |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
176 |
fun print thy (data : T) = |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
177 |
let |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
178 |
val module = #modl data |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
179 |
in |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
180 |
(Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module] |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
181 |
end; |
18217 | 182 |
end); |
183 |
||
18708 | 184 |
val _ = Context.add_setup CodegenData.init; |
185 |
||
18217 | 186 |
fun map_codegen_data f thy = |
187 |
case CodegenData.get thy |
|
20386 | 188 |
of { modl, appgens, target_data } => |
189 |
let val (modl, appgens, target_data) = |
|
190 |
f (modl, appgens, target_data) |
|
20105 | 191 |
in CodegenData.put { modl = modl, appgens = appgens, |
20386 | 192 |
target_data = target_data } thy end; |
18217 | 193 |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
194 |
val print_code = CodegenData.print; |
18217 | 195 |
|
20386 | 196 |
val purge_code = map_codegen_data (fn (_, appgens, target_data) => |
197 |
(empty_module, appgens, target_data)); |
|
18454 | 198 |
|
18865 | 199 |
|
20386 | 200 |
(* name handling *) |
201 |
||
202 |
fun idf_of_class thy class = |
|
203 |
CodegenNames.class thy class |
|
204 |
|> add_nsp nsp_class; |
|
205 |
||
206 |
fun class_of_idf thy = if_nsp nsp_class (CodegenNames.class_rev thy); |
|
207 |
||
208 |
fun idf_of_tyco thy tyco = |
|
209 |
CodegenNames.tyco thy tyco |
|
210 |
|> add_nsp nsp_tyco; |
|
211 |
||
212 |
fun tyco_of_idf thy = if_nsp nsp_tyco (CodegenNames.tyco_rev thy); |
|
213 |
||
214 |
fun idf_of_inst thy inst = |
|
215 |
CodegenNames.instance thy inst |
|
216 |
|> add_nsp nsp_inst; |
|
217 |
||
218 |
fun inst_of_idf thy = if_nsp nsp_inst (CodegenNames.instance_rev thy); |
|
219 |
||
220 |
fun idf_of_const thy thmtab (c_ty as (c, ty)) = |
|
221 |
if is_some (CodegenTheorems.get_dtyp_of_cons thmtab c_ty) then |
|
222 |
CodegenNames.const thy c_ty |
|
223 |
|> add_nsp nsp_dtcon |
|
224 |
else if (is_some o CodegenConsts.class_of_classop thy o CodegenConsts.typinst_of_typ thy) c_ty then |
|
225 |
CodegenNames.const thy c_ty |
|
226 |
|> add_nsp nsp_mem |
|
227 |
else |
|
228 |
CodegenNames.const thy c_ty |
|
229 |
|> add_nsp nsp_const; |
|
230 |
||
231 |
fun const_of_idf thy idf = |
|
232 |
case dest_nsp nsp_const idf |
|
233 |
of SOME c => CodegenNames.const_rev thy c |> SOME |
|
234 |
| _ => (case dest_nsp nsp_dtcon idf |
|
235 |
of SOME c => CodegenNames.const_rev thy c |> SOME |
|
236 |
| _ => (case dest_nsp nsp_mem idf |
|
237 |
of SOME c => CodegenNames.const_rev thy c |> SOME |
|
238 |
| _ => NONE)); |
|
239 |
||
240 |
||
241 |
(* application generators *) |
|
18865 | 242 |
|
20105 | 243 |
fun gen_add_appconst prep_const (raw_c, appgen) thy = |
18454 | 244 |
let |
18865 | 245 |
val c = prep_const thy raw_c; |
20105 | 246 |
val i = (length o fst o strip_type o Sign.the_const_type thy) c |
18865 | 247 |
in map_codegen_data |
20386 | 248 |
(fn (modl, appgens, target_data) => |
18865 | 249 |
(modl, |
20105 | 250 |
appgens |> Symtab.update (c, (i, (appgen, stamp ()))), |
20386 | 251 |
target_data)) thy |
18454 | 252 |
end; |
18217 | 253 |
|
18865 | 254 |
val add_appconst = gen_add_appconst Sign.intern_const; |
255 |
val add_appconst_i = gen_add_appconst (K I); |
|
256 |
||
257 |
||
20386 | 258 |
(* extraction kernel *) |
18865 | 259 |
|
20386 | 260 |
fun check_strict thy f x ((false, _), _) = |
19884 | 261 |
false |
20386 | 262 |
| check_strict thy f x ((_, SOME targets), _) = |
19884 | 263 |
exists ( |
20389 | 264 |
is_none o (fn tab => Symtab.lookup tab x) o f o the |
265 |
o (Symtab.lookup ((#target_data o CodegenData.get) thy)) |
|
19884 | 266 |
) targets |
20386 | 267 |
| check_strict thy f x ((true, _), _) = |
19884 | 268 |
true; |
269 |
||
20386 | 270 |
fun no_strict ((_, targets), thmtab) = ((false, targets), thmtab); |
271 |
||
272 |
fun sortlookups_const thy thmtab (c, typ_ctxt) = |
|
273 |
let |
|
274 |
val typ_decl = case CodegenTheorems.get_fun_thms thmtab (c, typ_ctxt) |
|
275 |
of thms as thm :: _ => CodegenTheorems.extr_typ thy thm |
|
276 |
| [] => (case AxClass.class_of_param thy c |
|
277 |
of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) => |
|
278 |
(Logic.varifyT o map_type_tfree (fn u as (w, _) => |
|
279 |
if w = v then TFree (v, [class]) else TFree u)) |
|
280 |
((the o AList.lookup (op =) cs) c)) |
|
281 |
| NONE => Sign.the_const_type thy c); |
|
282 |
in |
|
283 |
Vartab.empty |
|
284 |
|> Sign.typ_match thy (typ_decl, typ_ctxt) |
|
285 |
|> Vartab.dest |
|
20389 | 286 |
|> map (fn (_, (sort, ty)) => ClassPackage.sortlookup thy (ty, sort)) |
20386 | 287 |
|> filter_out null |
288 |
end; |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
289 |
|
18865 | 290 |
fun ensure_def_class thy tabs cls trns = |
18454 | 291 |
let |
20386 | 292 |
fun defgen_class thy (tabs as (_, thmtab)) cls trns = |
293 |
case class_of_idf thy cls |
|
18865 | 294 |
of SOME cls => |
295 |
let |
|
19283 | 296 |
val (v, cs) = (ClassPackage.the_consts_sign thy) cls; |
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
297 |
val sortctxts = map (ClassPackage.sortcontext_of_typ thy o snd) cs; |
20386 | 298 |
val idfs = map (idf_of_const thy thmtab) cs; |
18865 | 299 |
in |
300 |
trns |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
301 |
|> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls) |
18865 | 302 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
303 |
||>> (fold_map (exprgen_type thy tabs) o map snd) cs |
18865 | 304 |
||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts |
305 |
|-> (fn ((supcls, memtypes), sortctxts) => succeed |
|
19283 | 306 |
(Class (supcls, (unprefix "'" v, idfs ~~ (sortctxts ~~ memtypes))))) |
18865 | 307 |
end |
308 |
| _ => |
|
309 |
trns |
|
20389 | 310 |
|> fail ("No class definition found for " ^ quote cls); |
20386 | 311 |
val cls' = idf_of_class thy cls; |
18454 | 312 |
in |
313 |
trns |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
314 |
|> debug_msg (fn _ => "generating class " ^ quote cls) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
315 |
|> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls' |
18865 | 316 |
|> pair cls' |
317 |
end |
|
20386 | 318 |
and ensure_def_tyco thy (tabs as (_, thmtab)) tyco trns = |
18865 | 319 |
let |
20386 | 320 |
val tyco' = idf_of_tyco thy tyco; |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
321 |
val strict = check_strict thy #syntax_tyco tyco' tabs; |
20386 | 322 |
fun defgen_datatype thy (tabs as (_, thmtab)) dtco trns = |
323 |
case tyco_of_idf thy dtco |
|
18963 | 324 |
of SOME dtco => |
20353 | 325 |
(case CodegenTheorems.get_dtyp_spec thmtab dtco |
326 |
of SOME (vars, cos) => |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
327 |
trns |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
328 |
|> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco) |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
329 |
|> fold_map (exprgen_tyvar_sort thy tabs) vars |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
330 |
||>> fold_map (fn (c, tys) => |
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
331 |
fold_map (exprgen_type thy tabs) tys |
20386 | 332 |
#-> (fn tys' => pair (idf_of_const thy thmtab (c, tys ---> Type (dtco, map TFree vars)), tys'))) cos |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
333 |
|-> (fn (vars, cos) => succeed (Datatype |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
334 |
(vars, cos))) |
18963 | 335 |
| NONE => |
336 |
trns |
|
20389 | 337 |
|> fail ("No datatype found for " ^ quote dtco)) |
18963 | 338 |
| NONE => |
339 |
trns |
|
20389 | 340 |
|> fail ("Not a type constructor: " ^ quote dtco) |
18865 | 341 |
in |
342 |
trns |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
343 |
|> debug_msg (fn _ => "generating type constructor " ^ quote tyco) |
20389 | 344 |
|> ensure_def (defgen_datatype thy tabs) strict |
345 |
("generating type constructor " ^ quote tyco) tyco' |
|
18865 | 346 |
|> pair tyco' |
347 |
end |
|
348 |
and exprgen_tyvar_sort thy tabs (v, sort) trns = |
|
18516 | 349 |
trns |
18885 | 350 |
|> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort) |
18865 | 351 |
|-> (fn sort => pair (unprefix "'" v, sort)) |
352 |
and exprgen_type thy tabs (TVar _) trns = |
|
20389 | 353 |
error "TVar encountered in typ during code generation" |
18702 | 354 |
| exprgen_type thy tabs (TFree v_s) trns = |
18516 | 355 |
trns |
18702 | 356 |
|> exprgen_tyvar_sort thy tabs v_s |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
357 |
|-> (fn (v, sort) => pair (ITyVar v)) |
18516 | 358 |
| exprgen_type thy tabs (Type ("fun", [t1, t2])) trns = |
359 |
trns |
|
360 |
|> exprgen_type thy tabs t1 |
|
361 |
||>> exprgen_type thy tabs t2 |
|
362 |
|-> (fn (t1', t2') => pair (t1' `-> t2')) |
|
363 |
| exprgen_type thy tabs (Type (tyco, tys)) trns = |
|
364 |
trns |
|
365 |
|> ensure_def_tyco thy tabs tyco |
|
366 |
||>> fold_map (exprgen_type thy tabs) tys |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
367 |
|-> (fn (tyco, tys) => pair (tyco `%% tys)); |
18516 | 368 |
|
18885 | 369 |
fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns = |
18517 | 370 |
trns |
18885 | 371 |
|> ensure_def_inst thy tabs inst |
372 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls |
|
373 |
|-> (fn (inst, ls) => pair (Instance (inst, ls))) |
|
19253 | 374 |
| exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, (i, j)))) trns = |
18516 | 375 |
trns |
18517 | 376 |
|> fold_map (ensure_def_class thy tabs) clss |
19253 | 377 |
|-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i)))) |
20386 | 378 |
and mk_fun thy (tabs as (_, thmtab)) (c, ty) trns = |
379 |
case CodegenTheorems.get_fun_thms thmtab (c, ty) |
|
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
380 |
of eq_thms as eq_thm :: _ => |
18865 | 381 |
let |
19884 | 382 |
val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms); |
20386 | 383 |
val ty = (Logic.unvarifyT o CodegenTheorems.extr_typ thy) eq_thm |
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
384 |
val sortcontext = ClassPackage.sortcontext_of_typ thy ty; |
18865 | 385 |
fun dest_eqthm eq_thm = |
386 |
let |
|
387 |
val ((t, args), rhs) = |
|
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
388 |
(apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify o prop_of) eq_thm; |
18865 | 389 |
in case t |
390 |
of Const (c', _) => if c' = c then (args, rhs) |
|
20389 | 391 |
else error ("Illegal function equation for " ^ quote c |
18865 | 392 |
^ ", actually defining " ^ quote c') |
20389 | 393 |
| _ => error ("Illegal function equation for " ^ quote c) |
18865 | 394 |
end; |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
395 |
fun exprgen_eq (args, rhs) trns = |
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
396 |
trns |
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
397 |
|> fold_map (exprgen_term thy tabs) args |
19884 | 398 |
||>> exprgen_term thy tabs rhs; |
20105 | 399 |
fun checkvars (args, rhs) = |
400 |
if CodegenThingol.vars_distinct args then (args, rhs) |
|
20389 | 401 |
else error ("Repeated variables on left hand side of function") |
18865 | 402 |
in |
18517 | 403 |
trns |
19884 | 404 |
|> message msg (fn trns => trns |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
405 |
|> fold_map (exprgen_eq o dest_eqthm) eq_thms |
20105 | 406 |
|-> (fn eqs => pair (map checkvars eqs)) |
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
407 |
||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
408 |
||>> exprgen_type thy tabs ty |
20389 | 409 |
|-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), |
410 |
map snd sortcontext))) |
|
18865 | 411 |
end |
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
412 |
| [] => (NONE, trns) |
20386 | 413 |
and ensure_def_inst thy tabs (cls, tyco) trns = |
18865 | 414 |
let |
20386 | 415 |
fun defgen_inst thy (tabs as (_, thmtab)) inst trns = |
416 |
case inst_of_idf thy inst |
|
19956 | 417 |
of SOME (class, tyco) => |
18865 | 418 |
let |
18885 | 419 |
val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco); |
20389 | 420 |
val (_, members) = ClassPackage.the_consts_sign thy class; |
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
421 |
val arity_typ = Type (tyco, (map TFree arity)); |
20389 | 422 |
val operational_arity = map_filter (fn (v, sort) => |
423 |
case ClassPackage.operational_sort_of thy sort |
|
424 |
of [] => NONE |
|
425 |
| sort => SOME (v, sort)) arity; |
|
20386 | 426 |
fun mk_instmemname (m, ty) = |
427 |
NameSpace.append (NameSpace.append ((NameSpace.drop_base o NameSpace.drop_base) |
|
428 |
inst) nsp_instmem) (NameSpace.base (idf_of_const thy thmtab (m, ty))); |
|
18865 | 429 |
fun gen_suparity supclass trns = |
430 |
trns |
|
19136 | 431 |
|> ensure_def_class thy tabs supclass |
19953
2f54a51f1801
class package refinements, slight code generation refinements
haftmann
parents:
19884
diff
changeset
|
432 |
||>> fold_map (exprgen_classlookup thy tabs) |
20386 | 433 |
(ClassPackage.sortlookup thy (arity_typ, [supclass])); |
434 |
fun gen_membr ((m0, ty0), (m, ty)) trns = |
|
18865 | 435 |
trns |
20389 | 436 |
|> ensure_def_const thy tabs (m0, ty0) |
437 |
||>> exprgen_term thy tabs (Const (m, ty)); |
|
18865 | 438 |
in |
439 |
trns |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
440 |
|> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls |
18865 | 441 |
^ ", " ^ quote tyco ^ ")") |
18885 | 442 |
|> ensure_def_class thy tabs class |
18865 | 443 |
||>> ensure_def_tyco thy tabs tyco |
444 |
||>> fold_map (exprgen_tyvar_sort thy tabs) arity |
|
18885 | 445 |
||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class) |
20389 | 446 |
||>> fold_map gen_membr (members ~~ memdefs) |
18885 | 447 |
|-> (fn ((((class, tyco), arity), suparities), memdefs) => |
20389 | 448 |
succeed (Classinst ((class, (tyco, arity)), (suparities, memdefs)))) |
18865 | 449 |
end |
450 |
| _ => |
|
20389 | 451 |
trns |> fail ("No class instance found for " ^ quote inst); |
20386 | 452 |
val inst = idf_of_inst thy (cls, tyco); |
18865 | 453 |
in |
454 |
trns |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
455 |
|> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
456 |
|> ensure_def (defgen_inst thy tabs) true |
18865 | 457 |
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst |
458 |
|> pair inst |
|
459 |
end |
|
20386 | 460 |
and ensure_def_const thy (tabs as (_, thmtab)) (c, ty) trns = |
18865 | 461 |
let |
20386 | 462 |
fun defgen_datatypecons thy (tabs as (_, thmtab)) co trns = |
463 |
case CodegenTheorems.get_dtyp_of_cons thmtab ((the o const_of_idf thy) co) |
|
464 |
of SOME tyco => |
|
18865 | 465 |
trns |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
466 |
|> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co) |
20386 | 467 |
|> ensure_def_tyco thy tabs tyco |
468 |
|-> (fn _ => succeed Bot) |
|
18865 | 469 |
| _ => |
470 |
trns |
|
20389 | 471 |
|> fail ("Not a datatype constructor: " |
472 |
^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)); |
|
20386 | 473 |
fun defgen_clsmem thy (tabs as (_, thmtab)) m trns = |
474 |
case CodegenConsts.class_of_classop thy |
|
475 |
((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m) |
|
476 |
of SOME class => |
|
477 |
trns |
|
478 |
|> debug_msg (fn _ => "trying defgen class member for " ^ quote m) |
|
479 |
|> ensure_def_class thy tabs class |
|
480 |
|-> (fn _ => succeed Bot) |
|
481 |
| _ => |
|
20389 | 482 |
trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)) |
20386 | 483 |
fun defgen_funs thy (tabs as (_, thmtab)) c' trns = |
484 |
trns |
|
485 |
|> mk_fun thy tabs ((the o const_of_idf thy) c') |
|
486 |
|-> (fn SOME (funn, _) => succeed (Fun funn) |
|
20389 | 487 |
| NONE => fail ("No defining equations found for " |
488 |
^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))) |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
489 |
fun get_defgen tabs idf strict = |
20386 | 490 |
if (is_some oo dest_nsp) nsp_const idf |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
491 |
then defgen_funs thy tabs strict |
20386 | 492 |
else if (is_some oo dest_nsp) nsp_mem idf |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
493 |
then defgen_clsmem thy tabs strict |
20386 | 494 |
else if (is_some oo dest_nsp) nsp_dtcon idf |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
495 |
then defgen_datatypecons thy tabs strict |
20389 | 496 |
else error ("Illegal shallow name space for constant: " ^ quote idf); |
20386 | 497 |
val idf = idf_of_const thy thmtab (c, ty); |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
498 |
val strict = check_strict thy #syntax_const idf tabs; |
18865 | 499 |
in |
500 |
trns |
|
20389 | 501 |
|> debug_msg (fn _ => "generating constant " |
502 |
^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)) |
|
503 |
|> ensure_def (get_defgen tabs idf) strict ("generating constant " |
|
504 |
^ CodegenConsts.string_of_const_typ thy (c, ty)) idf |
|
18963 | 505 |
|> pair idf |
18865 | 506 |
end |
18517 | 507 |
and exprgen_term thy tabs (Const (f, ty)) trns = |
508 |
trns |
|
509 |
|> appgen thy tabs ((f, ty), []) |
|
18516 | 510 |
|-> (fn e => pair e) |
18912 | 511 |
| exprgen_term thy tabs (Var _) trns = |
20389 | 512 |
error "Var encountered in term during code generation" |
18516 | 513 |
| exprgen_term thy tabs (Free (v, ty)) trns = |
514 |
trns |
|
18912 | 515 |
|> exprgen_type thy tabs ty |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
516 |
|-> (fn ty => pair (IVar v)) |
19967 | 517 |
| exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns = |
19136 | 518 |
let |
20386 | 519 |
val (v, t) = Syntax.variant_abs (CodegenNames.purify_var raw_v, ty, raw_t); |
19136 | 520 |
in |
521 |
trns |
|
522 |
|> exprgen_type thy tabs ty |
|
523 |
||>> exprgen_term thy tabs t |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
524 |
|-> (fn (ty, e) => pair ((v, ty) `|-> e)) |
19136 | 525 |
end |
18516 | 526 |
| exprgen_term thy tabs (t as t1 $ t2) trns = |
527 |
let |
|
528 |
val (t', ts) = strip_comb t |
|
529 |
in case t' |
|
530 |
of Const (f, ty) => |
|
531 |
trns |
|
18517 | 532 |
|> appgen thy tabs ((f, ty), ts) |
18516 | 533 |
|-> (fn e => pair e) |
534 |
| _ => |
|
535 |
trns |
|
536 |
|> exprgen_term thy tabs t' |
|
537 |
||>> fold_map (exprgen_term thy tabs) ts |
|
538 |
|-> (fn (e, es) => pair (e `$$ es)) |
|
18865 | 539 |
end |
20386 | 540 |
and appgen_default thy (tabs as (_, thmtab)) ((c, ty), ts) trns = |
18865 | 541 |
trns |
542 |
|> ensure_def_const thy tabs (c, ty) |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
543 |
||>> exprgen_type thy tabs ty |
18885 | 544 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
20386 | 545 |
(sortlookups_const thy thmtab (c, ty)) |
18912 | 546 |
||>> fold_map (exprgen_term thy tabs) ts |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
547 |
|-> (fn (((c, ty), ls), es) => |
19202 | 548 |
pair (IConst (c, (ls, ty)) `$$ es)) |
18865 | 549 |
and appgen thy tabs ((f, ty), ts) trns = |
20105 | 550 |
case Symtab.lookup ((#appgens o CodegenData.get) thy) f |
551 |
of SOME (i, (ag, _)) => |
|
552 |
if length ts < i then |
|
18865 | 553 |
let |
20105 | 554 |
val tys = Library.take (i - length ts, ((fst o strip_type) ty)); |
20192
956cd30ef3be
renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
haftmann
parents:
20191
diff
changeset
|
555 |
val vs = Name.names (Name.declare f Name.context) "a" tys; |
18865 | 556 |
in |
557 |
trns |
|
18912 | 558 |
|> fold_map (exprgen_type thy tabs) tys |
20105 | 559 |
||>> ag thy tabs ((f, ty), ts @ map Free vs) |
560 |
|-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e)) |
|
18865 | 561 |
end |
20105 | 562 |
else if length ts > i then |
18865 | 563 |
trns |
20105 | 564 |
|> ag thy tabs ((f, ty), Library.take (i, ts)) |
565 |
||>> fold_map (exprgen_term thy tabs) (Library.drop (i, ts)) |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
566 |
|-> (fn (e, es) => pair (e `$$ es)) |
18865 | 567 |
else |
568 |
trns |
|
569 |
|> ag thy tabs ((f, ty), ts) |
|
570 |
| NONE => |
|
571 |
trns |
|
572 |
|> appgen_default thy tabs ((f, ty), ts); |
|
18516 | 573 |
|
18702 | 574 |
|
18217 | 575 |
(* parametrized generators, for instantiation in HOL *) |
576 |
||
20353 | 577 |
fun appgen_rep_bin int_of_numeral thy tabs (app as (c as (_, ty), [bin])) trns = |
578 |
case try (int_of_numeral thy) bin |
|
579 |
of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*) |
|
580 |
trns |
|
581 |
|> appgen_default thy (no_strict tabs) app |
|
19884 | 582 |
else |
583 |
trns |
|
20353 | 584 |
|> exprgen_term thy (no_strict tabs) (Const c) |
19884 | 585 |
||>> exprgen_term thy (no_strict tabs) bin |
20353 | 586 |
|-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2))) |
19884 | 587 |
| NONE => |
588 |
trns |
|
589 |
|> appgen_default thy tabs app; |
|
18217 | 590 |
|
19607
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
591 |
fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns = |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
592 |
case (char_to_index o list_comb o apfst Const) app |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
593 |
of SOME i => |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
594 |
trns |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
595 |
|> exprgen_type thy tabs ty |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
596 |
||>> appgen_default thy tabs app |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
597 |
|-> (fn (_, e0) => pair (IChar (chr i, e0))) |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
598 |
| NONE => |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
599 |
trns |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
600 |
|> appgen_default thy tabs app; |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
601 |
|
20105 | 602 |
fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns = |
603 |
let |
|
604 |
val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts)); |
|
605 |
fun clausegen (dt, bt) trns = |
|
606 |
trns |
|
607 |
|> exprgen_term thy tabs dt |
|
608 |
||>> exprgen_term thy tabs bt; |
|
609 |
in |
|
610 |
trns |
|
611 |
|> exprgen_term thy tabs st |
|
612 |
||>> exprgen_type thy tabs sty |
|
613 |
||>> fold_map clausegen ds |
|
614 |
||>> appgen_default thy tabs app |
|
615 |
|-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0))) |
|
616 |
end; |
|
617 |
||
618 |
fun appgen_let thy tabs (app as (_, [st, ct])) trns = |
|
619 |
trns |
|
620 |
|> exprgen_term thy tabs ct |
|
621 |
||>> exprgen_term thy tabs st |
|
622 |
||>> appgen_default thy tabs app |
|
623 |
|-> (fn (((v, ty) `|-> be, se), e0) => |
|
624 |
pair (ICase (((se, ty), case be |
|
625 |
of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)] |
|
626 |
| _ => [(IVar v, be)] |
|
627 |
), e0)) |
|
628 |
| (_, e0) => pair e0); |
|
629 |
||
20386 | 630 |
fun appgen_wfrec thy (tabs as (_, thmtab)) ((c, ty), [_, tf, tx]) trns = |
19038 | 631 |
let |
20386 | 632 |
val ty_def = (op ---> o apfst tl o strip_type o Logic.unvarifyT o Sign.the_const_type thy) c; |
19038 | 633 |
val ty' = (op ---> o apfst tl o strip_type) ty; |
20386 | 634 |
val idf = idf_of_const thy thmtab (c, ty); |
19038 | 635 |
in |
636 |
trns |
|
20386 | 637 |
|> ensure_def ((K o fail) "no extraction for wfrec") false ("generating wfrec") idf |
19136 | 638 |
|> exprgen_type thy tabs ty' |
639 |
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
|
20386 | 640 |
(sortlookups_const thy thmtab (c, ty)) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
641 |
||>> exprgen_type thy tabs ty_def |
19136 | 642 |
||>> exprgen_term thy tabs tf |
643 |
||>> exprgen_term thy tabs tx |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
644 |
|-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx)) |
19038 | 645 |
end; |
646 |
||
18217 | 647 |
|
18516 | 648 |
|
649 |
(** theory interface **) |
|
18217 | 650 |
|
20353 | 651 |
fun mk_tabs thy targets cs = |
20386 | 652 |
((true, targets), CodegenTheorems.mk_thmtab thy cs); |
18217 | 653 |
|
18756 | 654 |
fun get_serializer target = |
655 |
case Symtab.lookup (!serializers) target |
|
656 |
of SOME seri => seri |
|
20389 | 657 |
| NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) (); |
18335 | 658 |
|
18516 | 659 |
fun map_module f = |
20386 | 660 |
map_codegen_data (fn (modl, gens, target_data) => |
661 |
(f modl, gens, target_data)); |
|
18516 | 662 |
|
19884 | 663 |
fun purge_defs NONE thy = |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
664 |
map_module (K CodegenThingol.empty_module) thy |
20191 | 665 |
| purge_defs (SOME []) thy = |
666 |
thy |
|
19884 | 667 |
| purge_defs (SOME cs) thy = |
20191 | 668 |
map_module (K CodegenThingol.empty_module) thy; |
669 |
(*let |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
670 |
val tabs = mk_tabs thy NONE; |
19884 | 671 |
val idfs = map (idf_of_const' thy tabs) cs; |
672 |
fun purge idfs modl = |
|
673 |
CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
674 |
in |
19884 | 675 |
map_module (purge idfs) thy |
20191 | 676 |
end;*) |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
677 |
|
20353 | 678 |
fun expand_module targets cs init gen arg thy = |
19597 | 679 |
thy |
680 |
|> CodegenTheorems.notify_dirty |
|
681 |
|> `(#modl o CodegenData.get) |
|
682 |
|> (fn (modl, thy) => |
|
20353 | 683 |
(start_transact init (gen thy (mk_tabs thy targets cs) arg) modl, thy)) |
19597 | 684 |
|-> (fn (x, modl) => map_module (K modl) #> pair x); |
18516 | 685 |
|
20353 | 686 |
fun consts_of t = |
687 |
fold_aterms (fn Const c => cons c | _ => I) t []; |
|
688 |
||
20105 | 689 |
fun codegen_term t thy = |
20353 | 690 |
let |
691 |
val _ = Thm.cterm_of thy t; |
|
692 |
(* val _ = writeln "STARTING GENERATION"; *) |
|
693 |
(* val _ = (writeln o Sign.string_of_term thy) t; *) |
|
694 |
in |
|
695 |
thy |
|
696 |
|> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) (consts_of t) NONE exprgen_term t |
|
697 |
end; |
|
19136 | 698 |
|
699 |
val is_dtcon = has_nsp nsp_dtcon; |
|
700 |
||
701 |
fun consts_of_idfs thy = |
|
20386 | 702 |
map (the o const_of_idf thy); |
19150 | 703 |
|
20353 | 704 |
fun idfs_of_consts thy cs = |
20386 | 705 |
map (idf_of_const thy (snd (mk_tabs thy NONE cs))) cs; |
19150 | 706 |
|
19967 | 707 |
fun get_root_module thy = |
708 |
thy |
|
709 |
|> CodegenTheorems.notify_dirty |
|
710 |
|> `(#modl o CodegenData.get); |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
711 |
|
20213 | 712 |
fun eval_term (ref_spec, t) thy = |
713 |
let |
|
20401 | 714 |
val _ = Term.fold_atyps (fn _ => |
715 |
error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic")) |
|
716 |
(Term.fastype_of t); |
|
20389 | 717 |
fun preprocess_term t = |
718 |
let |
|
719 |
val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t); |
|
720 |
(* fake definition *) |
|
721 |
val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) |
|
722 |
(Logic.mk_equals (x, t)); |
|
723 |
fun err () = error "preprocess_term: bad preprocessor" |
|
724 |
in case map prop_of (CodegenTheorems.preprocess thy [eq]) |
|
725 |
of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err () |
|
726 |
| _ => err () |
|
727 |
end; |
|
20213 | 728 |
val target_data = |
729 |
((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; |
|
20386 | 730 |
val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]] |
20213 | 731 |
((Option.map fst oo Symtab.lookup) (#syntax_tyco target_data), |
732 |
(Option.map fst oo Symtab.lookup) (#syntax_const target_data)) |
|
733 |
(Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data)) |
|
734 |
in |
|
735 |
thy |
|
20389 | 736 |
|> codegen_term (preprocess_term t) |
20213 | 737 |
||>> `(#modl o CodegenData.get) |
738 |
|-> (fn (t', modl) => `(fn _ => eval (ref_spec, t') modl)) |
|
739 |
end; |
|
740 |
||
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
741 |
fun get_ml_fun_datatype thy resolv = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
742 |
let |
19150 | 743 |
val target_data = |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
744 |
((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
745 |
in |
20183 | 746 |
CodegenSerializer.ml_fun_datatype nsp_dtcon |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
747 |
((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
748 |
(Option.map fst oo Symtab.lookup o #syntax_const) target_data) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
749 |
resolv |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
750 |
end; |
18516 | 751 |
|
752 |
||
753 |
(** target languages **) |
|
754 |
||
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
755 |
(* syntax *) |
18516 | 756 |
|
18702 | 757 |
fun read_typ thy = |
758 |
Sign.read_typ (thy, K NONE); |
|
759 |
||
20353 | 760 |
fun read_quote get reader consts_of gen raw thy = |
761 |
let |
|
762 |
val it = reader thy raw; |
|
763 |
val cs = consts_of it; |
|
764 |
in |
|
765 |
thy |
|
766 |
|> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) cs ((SOME o get) thy) |
|
767 |
(fn thy => fn tabs => gen thy tabs) [it] |
|
768 |
|-> (fn [x] => pair x) |
|
769 |
end; |
|
18702 | 770 |
|
18865 | 771 |
fun gen_add_syntax_class prep_class class target pretty thy = |
772 |
thy |
|
773 |
|> map_codegen_data |
|
20386 | 774 |
(fn (modl, gens, target_data) => |
18865 | 775 |
(modl, gens, |
776 |
target_data |> Symtab.map_entry target |
|
777 |
(map_target_data |
|
778 |
(fn (syntax_class, syntax_tyco, syntax_const) => |
|
779 |
(syntax_class |
|
20386 | 780 |
|> Symtab.update (prep_class thy class, pretty), syntax_tyco, syntax_const))))); |
18865 | 781 |
|
782 |
val add_syntax_class = gen_add_syntax_class Sign.intern_class; |
|
783 |
||
18963 | 784 |
fun parse_syntax_tyco raw_tyco = |
18217 | 785 |
let |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
786 |
fun prep_tyco thy raw_tyco = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
787 |
raw_tyco |
18963 | 788 |
|> Sign.intern_type thy |
20386 | 789 |
|> idf_of_tyco thy; |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
790 |
fun no_args_tyco thy raw_tyco = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
791 |
AList.lookup (op =) ((NameSpace.dest_table o #types o Type.rep_tsig o Sign.tsig_of) thy) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
792 |
(Sign.intern_type thy raw_tyco) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
793 |
|> (fn SOME ((Type.LogicalType i), _) => i); |
18963 | 794 |
fun mk reader target thy = |
18702 | 795 |
let |
18756 | 796 |
val _ = get_serializer target; |
18702 | 797 |
val tyco = prep_tyco thy raw_tyco; |
798 |
in |
|
799 |
thy |
|
800 |
|> reader |
|
801 |
|-> (fn pretty => map_codegen_data |
|
20386 | 802 |
(fn (modl, gens, target_data) => |
18702 | 803 |
(modl, gens, |
804 |
target_data |> Symtab.map_entry target |
|
805 |
(map_target_data |
|
18865 | 806 |
(fn (syntax_class, syntax_tyco, syntax_const) => |
807 |
(syntax_class, syntax_tyco |> Symtab.update |
|
18702 | 808 |
(tyco, (pretty, stamp ())), |
20386 | 809 |
syntax_const)))))) |
18702 | 810 |
end; |
18217 | 811 |
in |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
812 |
CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco) |
20353 | 813 |
(read_quote (fn thy => prep_tyco thy raw_tyco) read_typ (K []) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
814 |
(fn thy => fn tabs => fold_map (exprgen_type thy tabs))) |
18702 | 815 |
#-> (fn reader => pair (mk reader)) |
18217 | 816 |
end; |
817 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
818 |
fun add_pretty_syntax_const c target pretty = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
819 |
map_codegen_data |
20386 | 820 |
(fn (modl, gens, target_data) => |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
821 |
(modl, gens, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
822 |
target_data |> Symtab.map_entry target |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
823 |
(map_target_data |
18865 | 824 |
(fn (syntax_class, syntax_tyco, syntax_const) => |
825 |
(syntax_class, syntax_tyco, |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
826 |
syntax_const |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
827 |
|> Symtab.update |
20386 | 828 |
(c, (pretty, stamp ()))))))); |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
829 |
|
18963 | 830 |
fun parse_syntax_const raw_const = |
18217 | 831 |
let |
18963 | 832 |
fun prep_const thy raw_const = |
20353 | 833 |
let |
20386 | 834 |
val c_ty = CodegenConsts.read_const_typ thy raw_const |
835 |
in idf_of_const thy (snd (mk_tabs thy NONE [c_ty])) c_ty end; |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
836 |
fun no_args_const thy raw_const = |
20386 | 837 |
(length o fst o strip_type o snd o CodegenConsts.read_const_typ thy) raw_const; |
18963 | 838 |
fun mk reader target thy = |
18702 | 839 |
let |
18756 | 840 |
val _ = get_serializer target; |
18963 | 841 |
val c = prep_const thy raw_const; |
18702 | 842 |
in |
843 |
thy |
|
844 |
|> reader |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
845 |
|-> (fn pretty => add_pretty_syntax_const c target pretty) |
18702 | 846 |
end; |
18217 | 847 |
in |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
848 |
CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const) |
20353 | 849 |
(read_quote (fn thy => prep_const thy raw_const) Sign.read_term consts_of |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
850 |
(fn thy => fn tabs => fold_map (exprgen_term thy tabs))) |
18702 | 851 |
#-> (fn reader => pair (mk reader)) |
18217 | 852 |
end; |
853 |
||
20401 | 854 |
fun add_pretty_list target raw_nil raw_cons mk_list mk_char_string target_cons thy = |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
855 |
let |
18756 | 856 |
val _ = get_serializer target; |
20353 | 857 |
fun prep_const raw = |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
858 |
let |
20353 | 859 |
val c = Sign.intern_const thy raw |
860 |
in (c, Sign.the_const_type thy c) end; |
|
861 |
val nil' = prep_const raw_nil; |
|
862 |
val cons' = prep_const raw_cons; |
|
863 |
val tabs = mk_tabs thy NONE [nil', cons']; |
|
864 |
fun mk_const c_ty = |
|
20386 | 865 |
idf_of_const thy (snd tabs) c_ty; |
20353 | 866 |
val nil'' = mk_const nil'; |
867 |
val cons'' = mk_const cons'; |
|
20401 | 868 |
val pr = CodegenSerializer.pretty_list nil'' cons'' mk_list mk_char_string target_cons; |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
869 |
in |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
870 |
thy |
20353 | 871 |
|> add_pretty_syntax_const cons'' target pr |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
872 |
end; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
873 |
|
20401 | 874 |
fun add_pretty_ml_string target raw_nil raw_cons raw_str mk_char mk_string target_implode thy = |
875 |
let |
|
876 |
val _ = get_serializer target; |
|
877 |
fun prep_const raw = |
|
878 |
let |
|
879 |
val c = Sign.intern_const thy raw |
|
880 |
in (c, Sign.the_const_type thy c) end; |
|
881 |
val cs' = map prep_const [raw_nil, raw_cons, raw_str]; |
|
882 |
val tabs = mk_tabs thy NONE cs'; |
|
883 |
fun mk_const c_ty = |
|
884 |
idf_of_const thy (snd tabs) c_ty; |
|
885 |
val [nil', cons', str'] = map mk_const cs'; |
|
886 |
val pr = CodegenSerializer.pretty_ml_string nil' cons' mk_char mk_string target_implode; |
|
887 |
in |
|
888 |
thy |
|
889 |
|> add_pretty_syntax_const str' target pr |
|
890 |
end; |
|
891 |
||
18217 | 892 |
|
18516 | 893 |
|
19884 | 894 |
(** code basis change notifications **) |
895 |
||
896 |
val _ = Context.add_setup (CodegenTheorems.add_notify purge_defs); |
|
897 |
||
898 |
||
899 |
||
18756 | 900 |
(** toplevel interface **) |
901 |
||
902 |
local |
|
19150 | 903 |
|
19884 | 904 |
fun generate_code targets (SOME raw_consts) thy = |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
905 |
let |
20386 | 906 |
val consts = map (CodegenConsts.read_const_typ thy) raw_consts; |
19884 | 907 |
val _ = case targets of SOME targets => (map get_serializer targets; ()) | _ => (); |
18756 | 908 |
in |
909 |
thy |
|
20353 | 910 |
|> expand_module targets consts NONE (fold_map oo ensure_def_const) consts |
18756 | 911 |
|-> (fn cs => pair (SOME cs)) |
912 |
end |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
913 |
| generate_code _ NONE thy = |
18756 | 914 |
(NONE, thy); |
915 |
||
916 |
fun serialize_code target seri raw_consts thy = |
|
18217 | 917 |
let |
18756 | 918 |
fun serialize cs thy = |
18702 | 919 |
let |
18756 | 920 |
val module = (#modl o CodegenData.get) thy; |
18702 | 921 |
val target_data = |
922 |
thy |
|
923 |
|> CodegenData.get |
|
924 |
|> #target_data |
|
925 |
|> (fn data => (the oo Symtab.lookup) data target); |
|
20216 | 926 |
val s_class = #syntax_class target_data |
927 |
val s_tyco = #syntax_tyco target_data |
|
928 |
val s_const = #syntax_const target_data |
|
19884 | 929 |
in |
20216 | 930 |
(seri ( |
931 |
Symtab.lookup s_class, |
|
932 |
(Option.map fst oo Symtab.lookup) s_tyco, |
|
933 |
(Option.map fst oo Symtab.lookup) s_const |
|
934 |
) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy) |
|
19884 | 935 |
end; |
18217 | 936 |
in |
937 |
thy |
|
19884 | 938 |
|> generate_code (SOME [target]) raw_consts |
18756 | 939 |
|-> (fn cs => serialize cs) |
18217 | 940 |
end; |
941 |
||
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
942 |
fun purge_consts raw_ts thy = |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
943 |
let |
20386 | 944 |
val cs = map (CodegenConsts.read_const_typ thy) raw_ts; |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
945 |
in fold CodegenTheorems.purge_defs cs thy end; |
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
946 |
|
18217 | 947 |
structure P = OuterParse |
948 |
and K = OuterKeyword |
|
949 |
||
950 |
in |
|
951 |
||
18850 | 952 |
val (generateK, serializeK, |
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
953 |
syntax_classK, syntax_tycoK, syntax_constK, |
20386 | 954 |
purgeK) = |
18850 | 955 |
("code_generate", "code_serialize", |
19884 | 956 |
"code_classapp", "code_typapp", "code_constapp", |
20386 | 957 |
"code_purge"); |
18335 | 958 |
|
18217 | 959 |
val generateP = |
18282 | 960 |
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( |
19884 | 961 |
(Scan.option (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") |
962 |
>> (fn SOME ["-"] => SOME [] | ts => ts)) |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19806
diff
changeset
|
963 |
-- Scan.repeat1 P.term |
19884 | 964 |
>> (fn (targets, raw_consts) => |
965 |
Toplevel.theory (generate_code targets (SOME raw_consts) #> snd)) |
|
18217 | 966 |
); |
967 |
||
968 |
val serializeP = |
|
18282 | 969 |
OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( |
18217 | 970 |
P.name |
19136 | 971 |
-- Scan.option (Scan.repeat1 P.term) |
18756 | 972 |
#-> (fn (target, raw_consts) => |
18850 | 973 |
P.$$$ "(" |
974 |
|-- get_serializer target |
|
975 |
--| P.$$$ ")" |
|
18756 | 976 |
>> (fn seri => |
977 |
Toplevel.theory (serialize_code target seri raw_consts) |
|
978 |
)) |
|
18217 | 979 |
); |
980 |
||
18865 | 981 |
val syntax_classP = |
19884 | 982 |
OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl ( |
18865 | 983 |
Scan.repeat1 ( |
984 |
P.xname |
|
985 |
-- Scan.repeat1 ( |
|
986 |
P.name -- P.string |
|
987 |
) |
|
988 |
) |
|
989 |
>> (Toplevel.theory oo fold) (fn (raw_class, syns) => |
|
990 |
fold (fn (target, p) => add_syntax_class raw_class target p) syns) |
|
991 |
); |
|
992 |
||
18217 | 993 |
val syntax_tycoP = |
994 |
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( |
|
18702 | 995 |
Scan.repeat1 ( |
996 |
P.xname |
|
18963 | 997 |
#-> (fn raw_tyco => Scan.repeat1 ( |
998 |
P.name -- parse_syntax_tyco raw_tyco |
|
999 |
)) |
|
18702 | 1000 |
) |
18963 | 1001 |
>> (Toplevel.theory oo fold o fold) |
1002 |
(fn (target, modifier) => modifier target) |
|
18217 | 1003 |
); |
1004 |
||
1005 |
val syntax_constP = |
|
1006 |
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl ( |
|
18702 | 1007 |
Scan.repeat1 ( |
19136 | 1008 |
P.term |
18963 | 1009 |
#-> (fn raw_const => Scan.repeat1 ( |
1010 |
P.name -- parse_syntax_const raw_const |
|
1011 |
)) |
|
18702 | 1012 |
) |
19008 | 1013 |
>> (Toplevel.theory oo fold o fold) |
18963 | 1014 |
(fn (target, modifier) => modifier target) |
18217 | 1015 |
); |
1016 |
||
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19283
diff
changeset
|
1017 |
val purgeP = |
20175 | 1018 |
OuterSyntax.command purgeK "purge all incrementally generated code" K.thy_decl |
1019 |
(Scan.succeed (Toplevel.theory purge_code)); |
|
18516 | 1020 |
|
19884 | 1021 |
val _ = OuterSyntax.add_parsers [generateP, serializeP, |
1022 |
syntax_classP, syntax_tycoP, syntax_constP, |
|
20386 | 1023 |
purgeP]; |
18217 | 1024 |
|
1025 |
end; (* local *) |
|
1026 |
||
1027 |
end; (* struct *) |