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