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