18 | Module |
18 | Module |
19 | Pretty of Pretty.T |
19 | Pretty of Pretty.T |
20 | Quote of 'a; |
20 | Quote of 'a; |
21 |
21 |
22 type deftab |
22 type deftab |
|
23 type node |
23 type codegr |
24 type codegr |
24 type 'a codegen |
25 type 'a codegen |
25 |
26 |
26 val add_codegen: string -> term codegen -> theory -> theory |
27 val add_codegen: string -> term codegen -> theory -> theory |
27 val add_tycodegen: string -> typ codegen -> theory -> theory |
28 val add_tycodegen: string -> typ codegen -> theory -> theory |
28 val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory |
29 val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory |
29 val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory |
30 val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory |
30 val preprocess: theory -> thm list -> thm list |
31 val preprocess: theory -> thm list -> thm list |
31 val print_codegens: theory -> unit |
32 val print_codegens: theory -> unit |
32 val generate_code: theory -> (string * string) list -> (string * string) list |
33 val generate_code: theory -> string list -> string -> (string * string) list -> |
33 val generate_code_i: theory -> (string * term) list -> (string * string) list |
34 (string * string) list * codegr |
|
35 val generate_code_i: theory -> string list -> string -> (string * term) list -> |
|
36 (string * string) list * codegr |
34 val assoc_consts: (xstring * string option * (term mixfix list * |
37 val assoc_consts: (xstring * string option * (term mixfix list * |
35 (string * string) list)) list -> theory -> theory |
38 (string * string) list)) list -> theory -> theory |
36 val assoc_consts_i: (xstring * typ option * (term mixfix list * |
39 val assoc_consts_i: (xstring * typ option * (term mixfix list * |
37 (string * string) list)) list -> theory -> theory |
40 (string * string) list)) list -> theory -> theory |
38 val assoc_types: (xstring * (typ mixfix list * |
41 val assoc_types: (xstring * (typ mixfix list * |
39 (string * string) list)) list -> theory -> theory |
42 (string * string) list)) list -> theory -> theory |
40 val get_assoc_code: theory -> string -> typ -> |
43 val get_assoc_code: theory -> string -> typ -> |
41 (term mixfix list * (string * string) list) option |
44 (term mixfix list * (string * string) list) option |
42 val get_assoc_type: theory -> string -> |
45 val get_assoc_type: theory -> string -> |
43 (typ mixfix list * (string * string) list) option |
46 (typ mixfix list * (string * string) list) option |
|
47 val codegen_error: codegr -> string -> string -> 'a |
44 val invoke_codegen: theory -> deftab -> string -> string -> bool -> |
48 val invoke_codegen: theory -> deftab -> string -> string -> bool -> |
45 codegr * term -> codegr * Pretty.T |
49 codegr * term -> codegr * Pretty.T |
46 val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> |
50 val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> |
47 codegr * typ -> codegr * Pretty.T |
51 codegr * typ -> codegr * Pretty.T |
48 val mk_id: string -> string |
52 val mk_id: string -> string |
49 val mk_const_id: theory -> string -> string -> string -> string |
53 val mk_qual_id: string -> string * string -> string |
50 val mk_type_id: theory -> string -> string -> string -> string |
54 val mk_const_id: string -> string -> codegr -> codegr * (string * string) |
|
55 val get_const_id: string -> codegr -> string * string |
|
56 val mk_type_id: string -> string -> codegr -> codegr * (string * string) |
|
57 val get_type_id: string -> codegr -> string * string |
51 val thyname_of_type: string -> theory -> string |
58 val thyname_of_type: string -> theory -> string |
52 val thyname_of_const: string -> theory -> string |
59 val thyname_of_const: string -> theory -> string |
53 val rename_terms: term list -> term list |
60 val rename_terms: term list -> term list |
54 val rename_term: term -> term |
61 val rename_term: term -> term |
55 val new_names: term -> string list -> string list |
62 val new_names: term -> string list -> string list |
56 val new_name: term -> string -> string |
63 val new_name: term -> string -> string |
|
64 val if_library: 'a -> 'a -> 'a |
57 val get_defn: theory -> deftab -> string -> typ -> |
65 val get_defn: theory -> deftab -> string -> typ -> |
58 ((typ * (string * (term list * term))) * int option) option |
66 ((typ * (string * (term list * term))) * int option) option |
59 val is_instance: theory -> typ -> typ -> bool |
67 val is_instance: theory -> typ -> typ -> bool |
60 val parens: Pretty.T -> Pretty.T |
68 val parens: Pretty.T -> Pretty.T |
61 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T |
69 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T |
62 val eta_expand: term -> term list -> int -> term |
70 val eta_expand: term -> term list -> int -> term |
63 val strip_tname: string -> string |
71 val strip_tname: string -> string |
64 val mk_type: bool -> typ -> Pretty.T |
72 val mk_type: bool -> typ -> Pretty.T |
65 val mk_term_of: theory -> string -> bool -> typ -> Pretty.T |
73 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T |
66 val mk_gen: theory -> string -> bool -> string list -> string -> typ -> Pretty.T |
74 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T |
67 val test_fn: (int -> (string * term) list option) ref |
75 val test_fn: (int -> (string * term) list option) ref |
68 val test_term: theory -> int -> int -> term -> (string * term) list option |
76 val test_term: theory -> int -> int -> term -> (string * term) list option |
69 val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list |
77 val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list |
70 val mk_deftab: theory -> deftab |
78 val mk_deftab: theory -> deftab |
|
79 val get_node: codegr -> string -> node |
|
80 val add_edge: string * string -> codegr -> codegr |
|
81 val add_edge_acyclic: string * string -> codegr -> codegr |
|
82 val del_nodes: string list -> codegr -> codegr |
|
83 val map_node: string -> (node -> node) -> codegr -> codegr |
|
84 val new_node: string * node -> codegr -> codegr |
71 end; |
85 end; |
72 |
86 |
73 structure Codegen : CODEGEN = |
87 structure Codegen : CODEGEN = |
74 struct |
88 struct |
75 |
89 |
173 tycodegens : (string * typ codegen) list, |
199 tycodegens : (string * typ codegen) list, |
174 consts : ((string * typ) * (term mixfix list * (string * string) list)) list, |
200 consts : ((string * typ) * (term mixfix list * (string * string) list)) list, |
175 types : (string * (typ mixfix list * (string * string) list)) list, |
201 types : (string * (typ mixfix list * (string * string) list)) list, |
176 attrs: (string * (Args.T list -> theory attribute * Args.T list)) list, |
202 attrs: (string * (Args.T list -> theory attribute * Args.T list)) list, |
177 preprocs: (stamp * (theory -> thm list -> thm list)) list, |
203 preprocs: (stamp * (theory -> thm list -> thm list)) list, |
|
204 modules: codegr Symtab.table, |
178 test_params: test_params}; |
205 test_params: test_params}; |
179 |
206 |
180 val empty = |
207 val empty = |
181 {codegens = [], tycodegens = [], consts = [], types = [], attrs = [], |
208 {codegens = [], tycodegens = [], consts = [], types = [], attrs = [], |
182 preprocs = [], test_params = default_test_params}; |
209 preprocs = [], modules = Symtab.empty, test_params = default_test_params}; |
183 val copy = I; |
210 val copy = I; |
184 val extend = I; |
211 val extend = I; |
185 |
212 |
186 fun merge _ |
213 fun merge _ |
187 ({codegens = codegens1, tycodegens = tycodegens1, |
214 ({codegens = codegens1, tycodegens = tycodegens1, |
188 consts = consts1, types = types1, attrs = attrs1, |
215 consts = consts1, types = types1, attrs = attrs1, |
189 preprocs = preprocs1, test_params = test_params1}, |
216 preprocs = preprocs1, modules = modules1, test_params = test_params1}, |
190 {codegens = codegens2, tycodegens = tycodegens2, |
217 {codegens = codegens2, tycodegens = tycodegens2, |
191 consts = consts2, types = types2, attrs = attrs2, |
218 consts = consts2, types = types2, attrs = attrs2, |
192 preprocs = preprocs2, test_params = test_params2}) = |
219 preprocs = preprocs2, modules = modules2, test_params = test_params2}) = |
193 {codegens = merge_alists' codegens1 codegens2, |
220 {codegens = merge_alists' codegens1 codegens2, |
194 tycodegens = merge_alists' tycodegens1 tycodegens2, |
221 tycodegens = merge_alists' tycodegens1 tycodegens2, |
195 consts = merge_alists consts1 consts2, |
222 consts = merge_alists consts1 consts2, |
196 types = merge_alists types1 types2, |
223 types = merge_alists types1 types2, |
197 attrs = merge_alists attrs1 attrs2, |
224 attrs = merge_alists attrs1 attrs2, |
198 preprocs = merge_alists' preprocs1 preprocs2, |
225 preprocs = merge_alists' preprocs1 preprocs2, |
|
226 modules = Symtab.merge (K true) (modules1, modules2), |
199 test_params = merge_test_params test_params1 test_params2}; |
227 test_params = merge_test_params test_params1 test_params2}; |
200 |
228 |
201 fun print _ ({codegens, tycodegens, ...} : T) = |
229 fun print _ ({codegens, tycodegens, ...} : T) = |
202 Pretty.writeln (Pretty.chunks |
230 Pretty.writeln (Pretty.chunks |
203 [Pretty.strs ("term code generators:" :: map fst codegens), |
231 [Pretty.strs ("term code generators:" :: map fst codegens), |
211 (**** access parameters for random testing ****) |
239 (**** access parameters for random testing ****) |
212 |
240 |
213 fun get_test_params thy = #test_params (CodegenData.get thy); |
241 fun get_test_params thy = #test_params (CodegenData.get thy); |
214 |
242 |
215 fun map_test_params f thy = |
243 fun map_test_params f thy = |
216 let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = |
244 let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = |
217 CodegenData.get thy; |
245 CodegenData.get thy; |
218 in CodegenData.put {codegens = codegens, tycodegens = tycodegens, |
246 in CodegenData.put {codegens = codegens, tycodegens = tycodegens, |
219 consts = consts, types = types, attrs = attrs, preprocs = preprocs, |
247 consts = consts, types = types, attrs = attrs, preprocs = preprocs, |
220 test_params = f test_params} thy |
248 modules = modules, test_params = f test_params} thy |
|
249 end; |
|
250 |
|
251 |
|
252 (**** access modules ****) |
|
253 |
|
254 fun get_modules thy = #modules (CodegenData.get thy); |
|
255 |
|
256 fun map_modules f thy = |
|
257 let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = |
|
258 CodegenData.get thy; |
|
259 in CodegenData.put {codegens = codegens, tycodegens = tycodegens, |
|
260 consts = consts, types = types, attrs = attrs, preprocs = preprocs, |
|
261 modules = f modules, test_params = test_params} thy |
221 end; |
262 end; |
222 |
263 |
223 |
264 |
224 (**** add new code generators to theory ****) |
265 (**** add new code generators to theory ****) |
225 |
266 |
226 fun add_codegen name f thy = |
267 fun add_codegen name f thy = |
227 let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = |
268 let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = |
228 CodegenData.get thy |
269 CodegenData.get thy |
229 in (case assoc (codegens, name) of |
270 in (case assoc (codegens, name) of |
230 NONE => CodegenData.put {codegens = (name, f) :: codegens, |
271 NONE => CodegenData.put {codegens = (name, f) :: codegens, |
231 tycodegens = tycodegens, consts = consts, types = types, |
272 tycodegens = tycodegens, consts = consts, types = types, |
232 attrs = attrs, preprocs = preprocs, test_params = test_params} thy |
273 attrs = attrs, preprocs = preprocs, modules = modules, |
|
274 test_params = test_params} thy |
233 | SOME _ => error ("Code generator " ^ name ^ " already declared")) |
275 | SOME _ => error ("Code generator " ^ name ^ " already declared")) |
234 end; |
276 end; |
235 |
277 |
236 fun add_tycodegen name f thy = |
278 fun add_tycodegen name f thy = |
237 let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = |
279 let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = |
238 CodegenData.get thy |
280 CodegenData.get thy |
239 in (case assoc (tycodegens, name) of |
281 in (case assoc (tycodegens, name) of |
240 NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens, |
282 NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens, |
241 codegens = codegens, consts = consts, types = types, |
283 codegens = codegens, consts = consts, types = types, |
242 attrs = attrs, preprocs = preprocs, test_params = test_params} thy |
284 attrs = attrs, preprocs = preprocs, modules = modules, |
|
285 test_params = test_params} thy |
243 | SOME _ => error ("Code generator " ^ name ^ " already declared")) |
286 | SOME _ => error ("Code generator " ^ name ^ " already declared")) |
244 end; |
287 end; |
245 |
288 |
246 |
289 |
247 (**** code attribute ****) |
290 (**** code attribute ****) |
248 |
291 |
249 fun add_attribute name att thy = |
292 fun add_attribute name att thy = |
250 let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = |
293 let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = |
251 CodegenData.get thy |
294 CodegenData.get thy |
252 in (case assoc (attrs, name) of |
295 in (case assoc (attrs, name) of |
253 NONE => CodegenData.put {tycodegens = tycodegens, |
296 NONE => CodegenData.put {tycodegens = tycodegens, |
254 codegens = codegens, consts = consts, types = types, |
297 codegens = codegens, consts = consts, types = types, |
255 attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs, |
298 attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs, |
256 preprocs = preprocs, |
299 preprocs = preprocs, modules = modules, |
257 test_params = test_params} thy |
300 test_params = test_params} thy |
258 | SOME _ => error ("Code attribute " ^ name ^ " already declared")) |
301 | SOME _ => error ("Code attribute " ^ name ^ " already declared")) |
259 end; |
302 end; |
260 |
303 |
261 fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p; |
304 fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p; |
375 (List.concat (map (check_str o Symbol.explode) (NameSpace.unpack s))) |
418 (List.concat (map (check_str o Symbol.explode) (NameSpace.unpack s))) |
376 in |
419 in |
377 if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' |
420 if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' |
378 end; |
421 end; |
379 |
422 |
380 fun extrn thy f thyname s = |
423 fun mk_long_id (p as (tab, used)) module s = |
381 let |
424 let |
382 val xs = NameSpace.unpack s; |
425 fun find_name [] = sys_error "mk_long_id" |
383 val s' = setmp NameSpace.long_names false (setmp NameSpace.short_names false |
426 | find_name (ys :: yss) = |
384 (setmp NameSpace.unique_names true (f thy))) s; |
427 let |
385 val xs' = NameSpace.unpack s' |
428 val s' = NameSpace.pack ys |
386 in |
429 val s'' = NameSpace.append module s' |
387 if "modular" mem !mode andalso length xs = length xs' andalso hd xs' = thyname |
430 in case Symtab.lookup (used, s'') of |
388 then NameSpace.pack (tl xs') else s' |
431 NONE => ((module, s'), (Symtab.update_new ((s, (module, s')), tab), |
389 end; |
432 Symtab.update_new ((s'', ()), used))) |
390 |
433 | SOME _ => find_name yss |
391 (* thyname: theory name for caller *) |
434 end |
392 (* thyname': theory name for callee *) |
435 in case Symtab.lookup (tab, s) of |
393 (* if caller and callee reside in different theories, use qualified access *) |
436 NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) |
394 |
437 | SOME name => (name, p) |
395 fun mk_const_id thy thyname thyname' s = |
438 end; |
396 let |
439 |
397 val s' = mk_id (extrn thy Sign.extern_const thyname' s); |
440 (* module: module name for caller *) |
|
441 (* module': module name for callee *) |
|
442 (* if caller and callee reside in different modules, use qualified access *) |
|
443 |
|
444 fun mk_qual_id module (module', s) = |
|
445 if module = module' orelse module' = "" then s else module' ^ "." ^ s; |
|
446 |
|
447 fun mk_const_id module cname (gr, (tab1, tab2)) = |
|
448 let |
|
449 val ((module, s), tab1') = mk_long_id tab1 module cname |
|
450 val s' = mk_id s; |
398 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
451 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
399 in |
452 in ((gr, (tab1', tab2)), (module, s'')) end; |
400 if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> "" |
453 |
401 then thyname' ^ "." ^ s'' else s'' |
454 fun get_const_id cname (gr, (tab1, tab2)) = |
402 end; |
455 case Symtab.lookup (fst tab1, cname) of |
403 |
456 NONE => error ("get_const_id: no such constant: " ^ quote cname) |
404 fun mk_type_id' f thy thyname thyname' s = |
457 | SOME (module, s) => |
405 let |
458 let |
406 val s' = mk_id (extrn thy Sign.extern_type thyname' s); |
459 val s' = mk_id s; |
407 val s'' = f (if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s') |
460 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' |
408 in |
461 in (module, s'') end; |
409 if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> "" |
462 |
410 then thyname' ^ "." ^ s'' else s'' |
463 fun mk_type_id module tyname (gr, (tab1, tab2)) = |
411 end; |
464 let |
412 |
465 val ((module, s), tab2') = mk_long_id tab2 module tyname |
413 val mk_type_id = mk_type_id' I; |
466 val s' = mk_id s; |
|
467 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
|
468 in ((gr, (tab1, tab2')), (module, s'')) end; |
|
469 |
|
470 fun get_type_id tyname (gr, (tab1, tab2)) = |
|
471 case Symtab.lookup (fst tab2, tyname) of |
|
472 NONE => error ("get_type_id: no such type: " ^ quote tyname) |
|
473 | SOME (module, s) => |
|
474 let |
|
475 val s' = mk_id s; |
|
476 val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' |
|
477 in (module, s'') end; |
|
478 |
|
479 fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab); |
|
480 |
|
481 fun get_node (gr, x) k = Graph.get_node gr k; |
|
482 fun add_edge e (gr, x) = (Graph.add_edge e gr, x); |
|
483 fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x); |
|
484 fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x); |
|
485 fun map_node k f (gr, x) = (Graph.map_node k f gr, x); |
|
486 fun new_node p (gr, x) = (Graph.new_node p gr, x); |
414 |
487 |
415 fun theory_of_type s thy = |
488 fun theory_of_type s thy = |
416 if Sign.declared_tyname thy s |
489 if Sign.declared_tyname thy s |
417 then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy) |
490 then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy) |
418 else NONE; |
491 else NONE; |
562 map (fst o fst o dest_Var) (term_vars t) union |
636 map (fst o fst o dest_Var) (term_vars t) union |
563 add_term_names (t, ThmDatabase.ml_reserved)); |
637 add_term_names (t, ThmDatabase.ml_reserved)); |
564 |
638 |
565 fun new_name t x = hd (new_names t [x]); |
639 fun new_name t x = hd (new_names t [x]); |
566 |
640 |
567 fun default_codegen thy defs gr dep thyname brack t = |
641 fun if_library x y = if "library" mem !mode then x else y; |
|
642 |
|
643 fun default_codegen thy defs gr dep module brack t = |
568 let |
644 let |
569 val (u, ts) = strip_comb t; |
645 val (u, ts) = strip_comb t; |
570 fun codegens brack = foldl_map (invoke_codegen thy defs dep thyname brack) |
646 fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) |
571 in (case u of |
647 in (case u of |
572 Var ((s, i), T) => |
648 Var ((s, i), T) => |
573 let |
649 let |
574 val (gr', ps) = codegens true (gr, ts); |
650 val (gr', ps) = codegens true (gr, ts); |
575 val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T) |
651 val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) |
576 in SOME (gr'', mk_app brack (Pretty.str (s ^ |
652 in SOME (gr'', mk_app brack (Pretty.str (s ^ |
577 (if i=0 then "" else string_of_int i))) ps) |
653 (if i=0 then "" else string_of_int i))) ps) |
578 end |
654 end |
579 |
655 |
580 | Free (s, T) => |
656 | Free (s, T) => |
581 let |
657 let |
582 val (gr', ps) = codegens true (gr, ts); |
658 val (gr', ps) = codegens true (gr, ts); |
583 val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T) |
659 val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) |
584 in SOME (gr'', mk_app brack (Pretty.str s) ps) end |
660 in SOME (gr'', mk_app brack (Pretty.str s) ps) end |
585 |
661 |
586 | Const (s, T) => |
662 | Const (s, T) => |
587 (case get_assoc_code thy s T of |
663 (case get_assoc_code thy s T of |
588 SOME (ms, aux) => |
664 SOME (ms, aux) => |
589 let val i = num_args ms |
665 let val i = num_args ms |
590 in if length ts < i then |
666 in if length ts < i then |
591 default_codegen thy defs gr dep thyname brack (eta_expand u ts i) |
667 default_codegen thy defs gr dep module brack (eta_expand u ts i) |
592 else |
668 else |
593 let |
669 let |
594 val (ts1, ts2) = args_of ms ts; |
670 val (ts1, ts2) = args_of ms ts; |
595 val (gr1, ps1) = codegens false (gr, ts1); |
671 val (gr1, ps1) = codegens false (gr, ts1); |
596 val (gr2, ps2) = codegens true (gr1, ts2); |
672 val (gr2, ps2) = codegens true (gr1, ts2); |
597 val (gr3, ps3) = codegens false (gr2, quotes_of ms); |
673 val (gr3, ps3) = codegens false (gr2, quotes_of ms); |
598 val (thyname', suffix) = (case get_defn thy defs s T of |
674 val (module', suffix) = (case get_defn thy defs s T of |
599 NONE => (thyname_of_const s thy, "") |
675 NONE => (if_library (thyname_of_const s thy) module, "") |
600 | SOME ((U, (thyname', _)), NONE) => (thyname', "") |
676 | SOME ((U, (module', _)), NONE) => |
601 | SOME ((U, (thyname', _)), SOME i) => |
677 (if_library module' module, "") |
602 (thyname', "_def" ^ string_of_int i)); |
678 | SOME ((U, (module', _)), SOME i) => |
|
679 (if_library module' module, " def" ^ string_of_int i)); |
603 val node_id = s ^ suffix; |
680 val node_id = s ^ suffix; |
604 val p = mk_app brack (Pretty.block |
681 fun p module' = mk_app brack (Pretty.block |
605 (pretty_mixfix thyname thyname' ms ps1 ps3)) ps2 |
682 (pretty_mixfix module module' ms ps1 ps3)) ps2 |
606 in SOME (case try (Graph.get_node gr3) node_id of |
683 in SOME (case try (get_node gr3) node_id of |
607 NONE => (case get_aux_code aux of |
684 NONE => (case get_aux_code aux of |
608 [] => (gr3, p) |
685 [] => (gr3, p module) |
609 | xs => (Graph.add_edge (node_id, dep) (Graph.new_node |
686 | xs => (add_edge (node_id, dep) (new_node |
610 (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr3), p)) |
687 (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr3), |
611 | SOME _ => (Graph.add_edge (node_id, dep) gr3, p)) |
688 p module')) |
|
689 | SOME (_, module'', _) => |
|
690 (add_edge (node_id, dep) gr3, p module'')) |
612 end |
691 end |
613 end |
692 end |
614 | NONE => (case get_defn thy defs s T of |
693 | NONE => (case get_defn thy defs s T of |
615 NONE => NONE |
694 NONE => NONE |
616 | SOME ((U, (thyname', (args, rhs))), k) => |
695 | SOME ((U, (thyname, (args, rhs))), k) => |
617 let |
696 let |
618 val suffix = (case k of NONE => "" | SOME i => "_def" ^ string_of_int i); |
697 val module' = if_library thyname module; |
|
698 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i); |
619 val node_id = s ^ suffix; |
699 val node_id = s ^ suffix; |
620 val def_id = mk_const_id thy thyname' thyname' s ^ suffix; |
700 val (gr', (ps, def_id)) = codegens true (gr, ts) |>>> |
621 val call_id = mk_const_id thy thyname thyname' s ^ suffix; |
701 mk_const_id module' (s ^ suffix); |
622 val (gr', ps) = codegens true (gr, ts); |
702 val p = mk_app brack (Pretty.str (mk_qual_id module def_id)) ps |
623 in |
703 in SOME (case try (get_node gr') node_id of |
624 SOME (Graph.add_edge (node_id, dep) gr' handle Graph.UNDEF _ => |
704 NONE => |
625 let |
705 let |
626 val _ = message ("expanding definition of " ^ s); |
706 val _ = message ("expanding definition of " ^ s); |
627 val (Ts, _) = strip_type T; |
707 val (Ts, _) = strip_type T; |
628 val (args', rhs') = |
708 val (args', rhs') = |
629 if not (null args) orelse null Ts then (args, rhs) else |
709 if not (null args) orelse null Ts then (args, rhs) else |
630 let val v = Free (new_name rhs "x", hd Ts) |
710 let val v = Free (new_name rhs "x", hd Ts) |
631 in ([v], betapply (rhs, v)) end; |
711 in ([v], betapply (rhs, v)) end; |
632 val (gr1, p) = invoke_codegen thy defs node_id thyname' false |
712 val (gr1, p') = invoke_codegen thy defs node_id module' false |
633 (Graph.add_edge (node_id, dep) |
713 (add_edge (node_id, dep) |
634 (Graph.new_node (node_id, (NONE, "", "")) gr'), rhs'); |
714 (new_node (node_id, (NONE, "", "")) gr'), rhs'); |
635 val (gr2, xs) = codegens false (gr1, args'); |
715 val (gr2, xs) = codegens false (gr1, args'); |
636 val (gr3, _) = invoke_tycodegen thy defs dep thyname false (gr2, T); |
716 val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T); |
637 val (gr4, ty) = invoke_tycodegen thy defs node_id thyname' false (gr3, U); |
717 val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U); |
638 in Graph.map_node node_id (K (NONE, thyname', Pretty.string_of |
718 in (map_node node_id (K (NONE, module', Pretty.string_of |
639 (Pretty.block (separate (Pretty.brk 1) |
719 (Pretty.block (separate (Pretty.brk 1) |
640 (if null args' then |
720 (if null args' then |
641 [Pretty.str ("val " ^ def_id ^ " :"), ty] |
721 [Pretty.str ("val " ^ snd def_id ^ " :"), ty] |
642 else Pretty.str ("fun " ^ def_id) :: xs) @ |
722 else Pretty.str ("fun " ^ snd def_id) :: xs) @ |
643 [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr4 |
723 [Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4, |
644 end, mk_app brack (Pretty.str call_id) ps) |
724 p) |
|
725 end |
|
726 | SOME _ => (add_edge (node_id, dep) gr', p)) |
645 end)) |
727 end)) |
646 |
728 |
647 | Abs _ => |
729 | Abs _ => |
648 let |
730 let |
649 val (bs, Ts) = ListPair.unzip (strip_abs_vars u); |
731 val (bs, Ts) = ListPair.unzip (strip_abs_vars u); |
650 val t = strip_abs_body u |
732 val t = strip_abs_body u |
651 val bs' = new_names t bs; |
733 val bs' = new_names t bs; |
652 val (gr1, ps) = codegens true (gr, ts); |
734 val (gr1, ps) = codegens true (gr, ts); |
653 val (gr2, p) = invoke_codegen thy defs dep thyname false |
735 val (gr2, p) = invoke_codegen thy defs dep module false |
654 (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); |
736 (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); |
655 in |
737 in |
656 SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ |
738 SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ |
657 [Pretty.str ")"])) ps) |
739 [Pretty.str ")"])) ps) |
658 end |
740 end |
659 |
741 |
660 | _ => NONE) |
742 | _ => NONE) |
661 end; |
743 end; |
662 |
744 |
663 fun default_tycodegen thy defs gr dep thyname brack (TVar ((s, i), _)) = |
745 fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) = |
664 SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i))) |
746 SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i))) |
665 | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) = |
747 | default_tycodegen thy defs gr dep module brack (TFree (s, _)) = |
666 SOME (gr, Pretty.str s) |
748 SOME (gr, Pretty.str s) |
667 | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = |
749 | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) = |
668 (case assoc (#types (CodegenData.get thy), s) of |
750 (case assoc (#types (CodegenData.get thy), s) of |
669 NONE => NONE |
751 NONE => NONE |
670 | SOME (ms, aux) => |
752 | SOME (ms, aux) => |
671 let |
753 let |
672 val (gr', ps) = foldl_map |
754 val (gr', ps) = foldl_map |
673 (invoke_tycodegen thy defs dep thyname false) |
755 (invoke_tycodegen thy defs dep module false) |
674 (gr, fst (args_of ms Ts)); |
756 (gr, fst (args_of ms Ts)); |
675 val (gr'', qs) = foldl_map |
757 val (gr'', qs) = foldl_map |
676 (invoke_tycodegen thy defs dep thyname false) |
758 (invoke_tycodegen thy defs dep module false) |
677 (gr', quotes_of ms); |
759 (gr', quotes_of ms); |
678 val thyname' = thyname_of_type s thy; |
760 val module' = if_library (thyname_of_type s thy) module; |
679 val node_id = s ^ " (type)"; |
761 val node_id = s ^ " (type)"; |
680 val p = Pretty.block (pretty_mixfix thyname thyname' ms ps qs) |
762 fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) |
681 in SOME (case try (Graph.get_node gr'') node_id of |
763 in SOME (case try (get_node gr'') node_id of |
682 NONE => (case get_aux_code aux of |
764 NONE => (case get_aux_code aux of |
683 [] => (gr'', p) |
765 [] => (gr'', p module') |
684 | xs => (Graph.add_edge (node_id, dep) (Graph.new_node |
766 | xs => (fst (mk_type_id module' s |
685 (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr''), p)) |
767 (add_edge (node_id, dep) (new_node (node_id, |
686 | SOME _ => (Graph.add_edge (node_id, dep) gr'', p)) |
768 (NONE, module', space_implode "\n" xs ^ "\n")) gr''))), |
|
769 p module')) |
|
770 | SOME (_, module'', _) => |
|
771 (add_edge (node_id, dep) gr'', p module'')) |
687 end); |
772 end); |
688 |
773 |
689 val _ = Context.add_setup |
774 val _ = Context.add_setup |
690 [add_codegen "default" default_codegen, |
775 [add_codegen "default" default_codegen, |
691 add_tycodegen "default" default_tycodegen]; |
776 add_tycodegen "default" default_tycodegen]; |
694 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n"; |
779 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n"; |
695 |
780 |
696 fun add_to_module name s ms = |
781 fun add_to_module name s ms = |
697 overwrite (ms, (name, the (assoc (ms, name)) ^ s)); |
782 overwrite (ms, (name, the (assoc (ms, name)) ^ s)); |
698 |
783 |
699 fun output_code gr xs = |
784 fun output_code gr module xs = |
700 let |
785 let |
701 val code = |
786 val code = List.mapPartial (fn s => |
702 map (fn s => (s, Graph.get_node gr s)) (rev (Graph.all_preds gr xs)) |
787 let val c as (_, module', _) = Graph.get_node gr s |
|
788 in if module = "" orelse module = module' then SOME (s, c) else NONE end) |
|
789 (rev (Graph.all_preds gr xs)); |
703 fun string_of_cycle (a :: b :: cs) = |
790 fun string_of_cycle (a :: b :: cs) = |
704 let val SOME (x, y) = get_first (fn (x, (_, a', _)) => |
791 let val SOME (x, y) = get_first (fn (x, (_, a', _)) => |
705 if a = a' then Option.map (pair x) |
792 if a = a' then Option.map (pair x) |
706 (find_first (equal b o #2 o Graph.get_node gr) |
793 (find_first (equal b o #2 o Graph.get_node gr) |
707 (Graph.imm_succs gr x)) |
794 (Graph.imm_succs gr x)) |
708 else NONE) code |
795 else NONE) code |
709 in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end |
796 in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end |
710 | string_of_cycle _ = "" |
797 | string_of_cycle _ = "" |
711 in |
798 in |
712 if "modular" mem !mode then |
799 if module = "" then |
713 let |
800 let |
714 val modules = distinct (map (#2 o snd) code); |
801 val modules = distinct (map (#2 o snd) code); |
715 val mod_gr = foldr (uncurry Graph.add_edge_acyclic) |
802 val mod_gr = foldr (uncurry Graph.add_edge_acyclic) |
716 (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules) |
803 (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules) |
717 (List.concat (map (fn (s, (_, thyname, _)) => map (pair thyname) |
804 (List.concat (map (fn (s, (_, module, _)) => map (pair module) |
718 (filter_out (equal thyname) (map (#2 o Graph.get_node gr) |
805 (filter_out (equal module) (map (#2 o Graph.get_node gr) |
719 (Graph.imm_succs gr s)))) code)); |
806 (Graph.imm_succs gr s)))) code)); |
720 val modules' = |
807 val modules' = |
721 rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) |
808 rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) |
722 in |
809 in |
723 foldl (fn ((_, (_, thyname, s)), ms) => add_to_module thyname s ms) |
810 foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms) |
724 (map (rpair "") modules') code |
811 (map (rpair "") modules') code |
725 end handle Graph.CYCLES (cs :: _) => |
812 end handle Graph.CYCLES (cs :: _) => |
726 error ("Cyclic dependency of modules:\n" ^ commas cs ^ |
813 error ("Cyclic dependency of modules:\n" ^ commas cs ^ |
727 "\n" ^ string_of_cycle cs) |
814 "\n" ^ string_of_cycle cs) |
728 else [("Generated", implode (map (#3 o snd) code))] |
815 else [(module, implode (map (#3 o snd) code))] |
729 end; |
816 end; |
730 |
817 |
731 fun gen_generate_code prep_term thy = |
818 fun gen_generate_code prep_term thy modules module = |
732 setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => |
819 setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => |
733 let |
820 let |
|
821 val _ = assert (module <> "" orelse |
|
822 "library" mem !mode andalso forall (equal "" o fst) xs) |
|
823 "missing module name"; |
|
824 val graphs = get_modules thy; |
734 val defs = mk_deftab thy; |
825 val defs = mk_deftab thy; |
735 val gr = Graph.new_node ("<Top>", (NONE, "Generated", "")) Graph.empty; |
826 val gr = new_node ("<Top>", (NONE, module, "")) |
|
827 (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => |
|
828 (Graph.merge (fn ((_, module, _), (_, module', _)) => |
|
829 module = module') (gr, gr'), |
|
830 (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr |
|
831 (map (fn s => case Symtab.lookup (graphs, s) of |
|
832 NONE => error ("Undefined code module: " ^ s) |
|
833 | SOME gr => gr) modules)) |
|
834 handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); |
736 fun expand (t as Abs _) = t |
835 fun expand (t as Abs _) = t |
737 | expand t = (case fastype_of t of |
836 | expand t = (case fastype_of t of |
738 Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t); |
837 Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t); |
739 val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) |
838 val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) |
740 (invoke_codegen thy defs "<Top>" "Generated" false (gr, t))) |
839 (invoke_codegen thy defs "<Top>" module false (gr, t))) |
741 (gr, map (apsnd (expand o prep_term thy)) xs); |
840 (gr, map (apsnd (expand o prep_term thy)) xs); |
742 val code = |
841 val code = List.mapPartial |
743 space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block |
842 (fn ("", _) => NONE |
744 [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^ |
843 | (s', p) => SOME (Pretty.string_of (Pretty.block |
745 "\n\n" |
844 [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps; |
|
845 val code' = space_implode "\n\n" code ^ "\n\n"; |
|
846 val code'' = |
|
847 List.mapPartial (fn (name, s) => |
|
848 if "library" mem !mode andalso name = module andalso null code |
|
849 then NONE |
|
850 else SOME (name, mk_struct name s)) |
|
851 ((if null code then I |
|
852 else add_to_module module code') |
|
853 (output_code (fst gr') (if_library "" module) ["<Top>"])) |
746 in |
854 in |
747 map (fn (name, s) => (name, mk_struct name s)) |
855 (code'', del_nodes ["<Top>"] gr') |
748 (add_to_module "Generated" code (output_code gr' ["<Top>"])) |
|
749 end)); |
856 end)); |
750 |
857 |
751 val generate_code_i = gen_generate_code (K I); |
858 val generate_code_i = gen_generate_code (K I); |
752 val generate_code = gen_generate_code |
859 val generate_code = gen_generate_code |
753 (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT); |
860 (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT); |
766 | mk_type p (TFree (s, _)) = Pretty.str (strip_tname s ^ "T") |
873 | mk_type p (TFree (s, _)) = Pretty.str (strip_tname s ^ "T") |
767 | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block |
874 | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block |
768 [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","), |
875 [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","), |
769 Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]); |
876 Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]); |
770 |
877 |
771 fun mk_term_of thy thyname p (TVar ((s, i), _)) = Pretty.str |
878 fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str |
772 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F") |
879 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F") |
773 | mk_term_of thy thyname p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F") |
880 | mk_term_of gr module p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F") |
774 | mk_term_of thy thyname p (Type (s, Ts)) = (if p then parens else I) |
881 | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I) |
775 (Pretty.block (separate (Pretty.brk 1) |
882 (Pretty.block (separate (Pretty.brk 1) |
776 (Pretty.str (mk_type_id' (fn s' => "term_of_" ^ s') |
883 (Pretty.str (mk_qual_id module |
777 thy thyname (thyname_of_type s thy) s) :: |
884 (get_type_id' (fn s' => "term_of_" ^ s') s gr)) :: |
778 List.concat (map (fn T => |
885 List.concat (map (fn T => |
779 [mk_term_of thy thyname true T, mk_type true T]) Ts)))); |
886 [mk_term_of gr module true T, mk_type true T]) Ts)))); |
780 |
887 |
781 |
888 |
782 (**** Test data generators ****) |
889 (**** Test data generators ****) |
783 |
890 |
784 fun mk_gen thy thyname p xs a (TVar ((s, i), _)) = Pretty.str |
891 fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str |
785 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") |
892 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") |
786 | mk_gen thy thyname p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") |
893 | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") |
787 | mk_gen thy thyname p xs a (Type (s, Ts)) = (if p then parens else I) |
894 | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I) |
788 (Pretty.block (separate (Pretty.brk 1) |
895 (Pretty.block (separate (Pretty.brk 1) |
789 (Pretty.str (mk_type_id' (fn s' => "gen_" ^ s') |
896 (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ |
790 thy thyname (thyname_of_type s thy) s ^ |
|
791 (if s mem xs then "'" else "")) :: |
897 (if s mem xs then "'" else "")) :: |
792 map (mk_gen thy thyname true xs a) Ts @ |
898 map (mk_gen gr module true xs a) Ts @ |
793 (if s mem xs then [Pretty.str a] else [])))); |
899 (if s mem xs then [Pretty.str a] else [])))); |
794 |
900 |
795 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
901 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
796 |
902 |
797 fun test_term thy sz i = setmp print_mode [] (fn t => |
903 fun test_term thy sz i = setmp print_mode [] (fn t => |
800 "Term to be tested contains type variables"; |
906 "Term to be tested contains type variables"; |
801 val _ = assert (null (term_vars t)) |
907 val _ = assert (null (term_vars t)) |
802 "Term to be tested contains schematic variables"; |
908 "Term to be tested contains schematic variables"; |
803 val frees = map dest_Free (term_frees t); |
909 val frees = map dest_Free (term_frees t); |
804 val szname = variant (map fst frees) "i"; |
910 val szname = variant (map fst frees) "i"; |
805 val code = space_implode "\n" (map snd |
911 val (code, gr) = setmp mode ["term_of", "test"] |
806 (setmp mode ["term_of", "test"] (generate_code_i thy) |
912 (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))]; |
807 [("testf", list_abs_free (frees, t))])); |
913 val s = "structure TestTerm =\nstruct\n\n" ^ |
808 val s = "structure TestTerm =\nstruct\n\n" ^ code ^ |
914 space_implode "\n" (map snd code) ^ |
809 "\nopen Generated;\n\n" ^ Pretty.string_of |
915 "\nopen Generated;\n\n" ^ Pretty.string_of |
810 (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", |
916 (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", |
811 Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1, |
917 Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1, |
812 Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, |
918 Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, |
813 Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) => |
919 Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) => |
814 Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1, |
920 Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1, |
815 mk_gen thy "" false [] "" T, Pretty.brk 1, |
921 mk_gen gr "Generated" false [] "" T, Pretty.brk 1, |
816 Pretty.str (szname ^ ";")]) frees)), |
922 Pretty.str (szname ^ ";")]) frees)), |
817 Pretty.brk 1, Pretty.str "in", Pretty.brk 1, |
923 Pretty.brk 1, Pretty.str "in", Pretty.brk 1, |
818 Pretty.block [Pretty.str "if ", |
924 Pretty.block [Pretty.str "if ", |
819 mk_app false (Pretty.str "testf") (map (Pretty.str o mk_id o fst) frees), |
925 mk_app false (Pretty.str "testf") (map (Pretty.str o mk_id o fst) frees), |
820 Pretty.brk 1, Pretty.str "then NONE", |
926 Pretty.brk 1, Pretty.str "then NONE", |
821 Pretty.brk 1, Pretty.str "else ", |
927 Pretty.brk 1, Pretty.str "else ", |
822 Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" :: |
928 Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" :: |
823 List.concat (separate [Pretty.str ",", Pretty.brk 1] |
929 List.concat (separate [Pretty.str ",", Pretty.brk 1] |
824 (map (fn (s, T) => [Pretty.block |
930 (map (fn (s, T) => [Pretty.block |
825 [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1, |
931 [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1, |
826 mk_app false (mk_term_of thy "" false T) |
932 mk_app false (mk_term_of gr "Generated" false T) |
827 [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @ |
933 [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @ |
828 [Pretty.str "]"])]], |
934 [Pretty.str "]"])]], |
829 Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ |
935 Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ |
830 "\n\nend;\n"; |
936 "\n\nend;\n"; |
831 val _ = use_text Context.ml_output false s; |
937 val _ = use_text Context.ml_output false s; |
922 (fn xs => Toplevel.theory (fn thy => assoc_consts |
1028 (fn xs => Toplevel.theory (fn thy => assoc_consts |
923 (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix |
1029 (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix |
924 (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) |
1030 (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) |
925 xs) thy))); |
1031 xs) thy))); |
926 |
1032 |
927 val generate_codeP = |
1033 fun parse_code lib = |
928 OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl |
1034 Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) -- |
929 (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- |
1035 (if lib then Scan.optional P.name "" else P.name) -- |
930 Scan.optional (P.$$$ "[" |-- P.enum "," P.xname --| P.$$$ "]") (!mode) -- |
1036 Scan.option (P.$$$ "file" |-- P.name) -- |
931 Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) >> |
1037 (if lib then Scan.succeed [] |
932 (fn ((opt_fname, mode'), xs) => Toplevel.theory (fn thy => |
1038 else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --| |
933 let val code = setmp mode mode' (generate_code thy) xs |
1039 P.$$$ "contains" -- |
934 in ((case opt_fname of |
1040 ( Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) |
935 NONE => use_text Context.ml_output false |
1041 || Scan.repeat1 (P.term >> pair "")) >> |
936 (space_implode "\n" (map snd code) ^ "\nopen Generated;\n") |
1042 (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => |
937 | SOME fname => |
1043 let |
938 if "modular" mem mode' then |
1044 val mode'' = if lib then "library" ins (mode' \ "library") |
939 app (fn (name, s) => File.write |
1045 else mode' \ "library"; |
940 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) |
1046 val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs |
941 (("ROOT", implode (map (fn (name, _) => |
1047 in ((case opt_fname of |
942 "use \"" ^ name ^ ".ML\";\n") code)) :: code) |
1048 NONE => use_text Context.ml_output false |
943 else File.write (Path.unpack fname) (snd (hd code))); thy) |
1049 (space_implode "\n" (map snd code)) |
944 end))); |
1050 | SOME fname => |
|
1051 if lib then |
|
1052 app (fn (name, s) => File.write |
|
1053 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s) |
|
1054 (("ROOT", implode (map (fn (name, _) => |
|
1055 "use \"" ^ name ^ ".ML\";\n") code)) :: code) |
|
1056 else File.write (Path.unpack fname) (snd (hd code))); |
|
1057 if lib then thy |
|
1058 else map_modules (fn graphs => |
|
1059 Symtab.update ((module, gr), graphs)) thy) |
|
1060 end)); |
|
1061 |
|
1062 val code_libraryP = |
|
1063 OuterSyntax.command "code_library" |
|
1064 "generates code for terms (one structure for each theory)" K.thy_decl |
|
1065 (parse_code true); |
|
1066 |
|
1067 val code_moduleP = |
|
1068 OuterSyntax.command "code_module" |
|
1069 "generates code for terms (single structure, incremental)" K.thy_decl |
|
1070 (parse_code false); |
945 |
1071 |
946 val params = |
1072 val params = |
947 [("size", P.nat >> (K o set_size)), |
1073 [("size", P.nat >> (K o set_size)), |
948 ("iterations", P.nat >> (K o set_iterations)), |
1074 ("iterations", P.nat >> (K o set_iterations)), |
949 ("default_type", P.typ >> set_default_type)]; |
1075 ("default_type", P.typ >> set_default_type)]; |