1 (* Title: Pure/codegen.ML
3 Author: Stefan Berghofer, TU Muenchen
5 Generic code generator.
10 val quiet_mode : bool ref
11 val message : string -> unit
12 val mode : string list ref
14 val string_of : Pretty.T -> string
15 val str : string -> Pretty.T
29 val add_codegen: string -> term codegen -> theory -> theory
30 val add_tycodegen: string -> typ codegen -> theory -> theory
31 val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
32 val preprocess: theory -> thm list -> thm list
33 val preprocess_term: theory -> term -> term
34 val print_codegens: theory -> unit
35 val generate_code: theory -> string list -> string -> (string * string) list ->
36 (string * string) list * codegr
37 val generate_code_i: theory -> string list -> string -> (string * term) list ->
38 (string * string) list * codegr
39 val assoc_const: string * (term mixfix list *
40 (string * string) list) -> theory -> theory
41 val assoc_const_i: (string * typ) * (term mixfix list *
42 (string * string) list) -> theory -> theory
43 val assoc_type: xstring * (typ mixfix list *
44 (string * string) list) -> theory -> theory
45 val get_assoc_code: theory -> string * typ ->
46 (term mixfix list * (string * string) list) option
47 val get_assoc_type: theory -> string ->
48 (typ mixfix list * (string * string) list) option
49 val codegen_error: codegr -> string -> string -> 'a
50 val invoke_codegen: theory -> deftab -> string -> string -> bool ->
51 codegr * term -> codegr * Pretty.T
52 val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
53 codegr * typ -> codegr * Pretty.T
54 val mk_id: string -> string
55 val mk_qual_id: string -> string * string -> string
56 val mk_const_id: string -> string -> codegr -> codegr * (string * string)
57 val get_const_id: string -> codegr -> string * string
58 val mk_type_id: string -> string -> codegr -> codegr * (string * string)
59 val get_type_id: string -> codegr -> string * string
60 val thyname_of_type: string -> theory -> string
61 val thyname_of_const: string -> theory -> string
62 val rename_terms: term list -> term list
63 val rename_term: term -> term
64 val new_names: term -> string list -> string list
65 val new_name: term -> string -> string
66 val if_library: 'a -> 'a -> 'a
67 val get_defn: theory -> deftab -> string -> typ ->
68 ((typ * (string * (term list * term))) * int option) option
69 val is_instance: typ -> typ -> bool
70 val parens: Pretty.T -> Pretty.T
71 val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
72 val mk_tuple: Pretty.T list -> Pretty.T
73 val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
74 val eta_expand: term -> term list -> int -> term
75 val strip_tname: string -> string
76 val mk_type: bool -> typ -> Pretty.T
77 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
78 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
79 val test_fn: (int -> (string * term) list option) ref
80 val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
81 val auto_quickcheck: bool ref
82 val auto_quickcheck_time_limit: int ref
83 val eval_result: (unit -> term) ref
84 val eval_term: theory -> term -> term
85 val evaluation_conv: cterm -> thm
86 val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
87 val quotes_of: 'a mixfix list -> 'a list
88 val num_args_of: 'a mixfix list -> int
89 val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
90 val mk_deftab: theory -> deftab
91 val add_unfold: thm -> theory -> theory
93 val get_node: codegr -> string -> node
94 val add_edge: string * string -> codegr -> codegr
95 val add_edge_acyclic: string * string -> codegr -> codegr
96 val del_nodes: string list -> codegr -> codegr
97 val map_node: string -> (node -> node) -> codegr -> codegr
98 val new_node: string * node -> codegr -> codegr
101 structure Codegen : CODEGEN =
104 val quiet_mode = ref true;
105 fun message s = if !quiet_mode then () else writeln s;
107 val mode = ref ([] : string list);
111 fun string_of p = (Pretty.string_of |>
112 PrintMode.setmp [] |>
113 Pretty.setmp_margin (!margin)) p;
115 val str = PrintMode.setmp [] Pretty.str;
117 (**** Mixfix syntax ****)
126 fun is_arg Arg = true
127 | is_arg Ignore = true
130 fun quotes_of [] = []
131 | quotes_of (Quote q :: ms) = q :: quotes_of ms
132 | quotes_of (_ :: ms) = quotes_of ms;
134 fun args_of [] xs = ([], xs)
135 | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
136 | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
137 | args_of (_ :: ms) xs = args_of ms xs;
139 fun num_args_of x = length (List.filter is_arg x);
142 (**** theory data ****)
144 (* preprocessed definition table *)
147 (typ * (* type of constant *)
148 (string * (* name of theory containing definition of constant *)
149 (term list * (* parameters *)
150 term))) (* right-hand side *)
153 (* code dependency graph *)
155 type nametab = (string * string) Symtab.table * unit Symtab.table;
157 fun merge_nametabs ((tab, used), (tab', used')) =
158 (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
161 (exn option * (* slot for arbitrary data *)
162 string * (* name of structure containing piece of code *)
163 string); (* piece of code *)
167 (nametab * (* table for assigned constant names *)
168 nametab); (* table for assigned type names *)
170 val emptygr : codegr = (Graph.empty,
171 ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
173 (* type of code generators *)
176 theory -> (* theory in which generate_code was called *)
177 deftab -> (* definition table (for efficiency) *)
178 codegr -> (* code dependency graph *)
179 string -> (* node name of caller (for recording dependencies) *)
180 string -> (* module name of caller (for modular code generation) *)
181 bool -> (* whether to parenthesize generated expression *)
182 'a -> (* item to generate code from *)
183 (codegr * Pretty.T) option;
185 (* parameters for random testing *)
188 {size: int, iterations: int, default_type: typ option};
190 fun merge_test_params
191 {size = size1, iterations = iterations1, default_type = default_type1}
192 {size = size2, iterations = iterations2, default_type = default_type2} =
193 {size = Int.max (size1, size2),
194 iterations = Int.max (iterations1, iterations2),
195 default_type = case default_type1 of
196 NONE => default_type2
197 | _ => default_type1};
199 val default_test_params : test_params =
200 {size = 10, iterations = 100, default_type = NONE};
202 fun set_size size ({iterations, default_type, ...} : test_params) =
203 {size = size, iterations = iterations, default_type = default_type};
205 fun set_iterations iterations ({size, default_type, ...} : test_params) =
206 {size = size, iterations = iterations, default_type = default_type};
208 fun set_default_type s thy ({size, iterations, ...} : test_params) =
209 {size = size, iterations = iterations,
210 default_type = SOME (Syntax.read_typ_global thy s)};
215 structure CodegenData = TheoryDataFun
218 {codegens : (string * term codegen) list,
219 tycodegens : (string * typ codegen) list,
220 consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
221 types : (string * (typ mixfix list * (string * string) list)) list,
222 preprocs: (stamp * (theory -> thm list -> thm list)) list,
223 modules: codegr Symtab.table,
224 test_params: test_params};
227 {codegens = [], tycodegens = [], consts = [], types = [],
228 preprocs = [], modules = Symtab.empty, test_params = default_test_params};
233 ({codegens = codegens1, tycodegens = tycodegens1,
234 consts = consts1, types = types1,
235 preprocs = preprocs1, modules = modules1, test_params = test_params1},
236 {codegens = codegens2, tycodegens = tycodegens2,
237 consts = consts2, types = types2,
238 preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
239 {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
240 tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
241 consts = AList.merge (op =) (K true) (consts1, consts2),
242 types = AList.merge (op =) (K true) (types1, types2),
243 preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
244 modules = Symtab.merge (K true) (modules1, modules2),
245 test_params = merge_test_params test_params1 test_params2};
248 fun print_codegens thy =
249 let val {codegens, tycodegens, ...} = CodegenData.get thy in
250 Pretty.writeln (Pretty.chunks
251 [Pretty.strs ("term code generators:" :: map fst codegens),
252 Pretty.strs ("type code generators:" :: map fst tycodegens)])
257 (**** access parameters for random testing ****)
259 fun get_test_params thy = #test_params (CodegenData.get thy);
261 fun map_test_params f thy =
262 let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
264 in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
265 consts = consts, types = types, preprocs = preprocs,
266 modules = modules, test_params = f test_params} thy
270 (**** access modules ****)
272 fun get_modules thy = #modules (CodegenData.get thy);
274 fun map_modules f thy =
275 let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
277 in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
278 consts = consts, types = types, preprocs = preprocs,
279 modules = f modules, test_params = test_params} thy
283 (**** add new code generators to theory ****)
285 fun add_codegen name f thy =
286 let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
288 in (case AList.lookup (op =) codegens name of
289 NONE => CodegenData.put {codegens = (name, f) :: codegens,
290 tycodegens = tycodegens, consts = consts, types = types,
291 preprocs = preprocs, modules = modules,
292 test_params = test_params} thy
293 | SOME _ => error ("Code generator " ^ name ^ " already declared"))
296 fun add_tycodegen name f thy =
297 let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
299 in (case AList.lookup (op =) tycodegens name of
300 NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
301 codegens = codegens, consts = consts, types = types,
302 preprocs = preprocs, modules = modules,
303 test_params = test_params} thy
304 | SOME _ => error ("Code generator " ^ name ^ " already declared"))
308 (**** preprocessors ****)
310 fun add_preprocessor p thy =
311 let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
313 in CodegenData.put {tycodegens = tycodegens,
314 codegens = codegens, consts = consts, types = types,
315 preprocs = (stamp (), p) :: preprocs,
316 modules = modules, test_params = test_params} thy
320 let val {preprocs, ...} = CodegenData.get thy
321 in fold (fn (_, f) => f thy) preprocs end;
323 fun preprocess_term thy t =
325 val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
326 (* fake definition *)
327 val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
328 (Logic.mk_equals (x, t));
329 fun err () = error "preprocess_term: bad preprocessor"
330 in case map prop_of (preprocess thy [eq]) of
331 [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
337 val thy = Thm.theory_of_thm eqn;
338 val ctxt = ProofContext.init thy;
339 val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn;
340 val names = term_consts (fst (Logic.dest_equals (prop_of eqn')));
341 fun prep thy = map (fn th =>
342 let val prop = prop_of th
344 if forall (fn name => exists_Const (equal name o fst) prop) names
345 then rewrite_rule [eqn'] (Thm.transfer thy th)
348 in add_preprocessor prep end;
352 fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
354 Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
355 (fn thm => add_unfold thm #> Code.add_inline thm))))
359 (**** associate constants with target language code ****)
361 fun gen_assoc_const prep_const (raw_const, syn) thy =
363 val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
365 val (cname, T) = prep_const thy raw_const;
367 if num_args_of (fst syn) > length (binder_types T) then
368 error ("More arguments than in corresponding type of " ^ cname)
369 else case AList.lookup (op =) consts (cname, T) of
370 NONE => CodegenData.put {codegens = codegens,
371 tycodegens = tycodegens,
372 consts = ((cname, T), syn) :: consts,
373 types = types, preprocs = preprocs,
374 modules = modules, test_params = test_params} thy
375 | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
378 val assoc_const_i = gen_assoc_const (K I);
379 val assoc_const = gen_assoc_const CodeUnit.read_bare_const;
382 (**** associate types with target language types ****)
384 fun assoc_type (s, syn) thy =
386 val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
388 val tc = Sign.intern_type thy s;
390 case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
391 SOME ((Type.LogicalType i, _), _) =>
392 if num_args_of (fst syn) > i then
393 error ("More arguments than corresponding type constructor " ^ s)
394 else (case AList.lookup (op =) types tc of
395 NONE => CodegenData.put {codegens = codegens,
396 tycodegens = tycodegens, consts = consts,
397 types = (tc, syn) :: types,
398 preprocs = preprocs, modules = modules, test_params = test_params} thy
399 | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
400 | _ => error ("Not a type constructor: " ^ s)
403 fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
406 (**** make valid ML identifiers ****)
408 fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse
409 Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
411 fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (explode s))) of
412 ("<" :: "^" :: xs, ">") => (true, implode xs)
413 | ("<" :: xs, ">") => (false, implode xs)
414 | _ => sys_error "dest_sym");
416 fun mk_id s = if s = "" then "" else
418 fun check_str [] = []
419 | check_str xs = (case take_prefix is_ascii_letdig xs of
420 ([], " " :: zs) => check_str zs
422 if size z = 1 then string_of_int (ord z) :: check_str zs
423 else (case dest_sym z of
424 (true, "isub") => check_str zs
425 | (true, "isup") => "" :: check_str zs
426 | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
427 | (ys, zs) => implode ys :: check_str zs);
428 val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
430 if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
433 fun mk_long_id (p as (tab, used)) module s =
435 fun find_name [] = sys_error "mk_long_id"
436 | find_name (ys :: yss) =
438 val s' = NameSpace.implode ys
439 val s'' = NameSpace.append module s'
440 in case Symtab.lookup used s'' of
441 NONE => ((module, s'),
442 (Symtab.update_new (s, (module, s')) tab,
443 Symtab.update_new (s'', ()) used))
444 | SOME _ => find_name yss
446 in case Symtab.lookup tab s of
447 NONE => find_name (Library.suffixes1 (NameSpace.explode s))
448 | SOME name => (name, p)
451 (* module: module name for caller *)
452 (* module': module name for callee *)
453 (* if caller and callee reside in different modules, use qualified access *)
455 fun mk_qual_id module (module', s) =
456 if module = module' orelse module' = "" then s else module' ^ "." ^ s;
458 fun mk_const_id module cname (gr, (tab1, tab2)) =
460 val ((module, s), tab1') = mk_long_id tab1 module cname
462 val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
463 in ((gr, (tab1', tab2)), (module, s'')) end;
465 fun get_const_id cname (gr, (tab1, tab2)) =
466 case Symtab.lookup (fst tab1) cname of
467 NONE => error ("get_const_id: no such constant: " ^ quote cname)
468 | SOME (module, s) =>
471 val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
472 in (module, s'') end;
474 fun mk_type_id module tyname (gr, (tab1, tab2)) =
476 val ((module, s), tab2') = mk_long_id tab2 module tyname
478 val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
479 in ((gr, (tab1, tab2')), (module, s'')) end;
481 fun get_type_id tyname (gr, (tab1, tab2)) =
482 case Symtab.lookup (fst tab2) tyname of
483 NONE => error ("get_type_id: no such type: " ^ quote tyname)
484 | SOME (module, s) =>
487 val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
488 in (module, s'') end;
490 fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab);
492 fun get_node (gr, x) k = Graph.get_node gr k;
493 fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
494 fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
495 fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
496 fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
497 fun new_node p (gr, x) = (Graph.new_node p gr, x);
499 fun theory_of_type s thy =
500 if Sign.declared_tyname thy s
501 then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy)))
504 fun theory_of_const s thy =
505 if Sign.declared_const thy s
506 then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy)))
509 fun thyname_of_type s thy = (case theory_of_type s thy of
510 NONE => error ("thyname_of_type: no such type: " ^ quote s)
511 | SOME thy' => Context.theory_name thy');
513 fun thyname_of_const s thy = (case theory_of_const s thy of
514 NONE => error ("thyname_of_const: no such constant: " ^ quote s)
515 | SOME thy' => Context.theory_name thy');
517 fun rename_terms ts =
519 val names = List.foldr add_term_names
520 (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
521 val reserved = filter ML_Syntax.is_reserved names;
522 val (illegal, alt_names) = split_list (map_filter (fn s =>
523 let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
524 val ps = (reserved @ illegal) ~~
525 Name.variant_list names (map (suffix "'") reserved @ alt_names);
527 fun rename_id s = AList.lookup (op =) ps s |> the_default s;
529 fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
530 | rename (Free (a, T)) = Free (rename_id a, T)
531 | rename (Abs (s, T, t)) = Abs (s, T, rename t)
532 | rename (t $ u) = rename t $ rename u
538 val rename_term = hd o rename_terms o single;
541 (**** retrieve definition of constant ****)
543 fun is_instance T1 T2 =
544 Type.raw_instance (T1, Logic.legacy_varifyT T2);
546 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
547 s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
549 fun get_aux_code xs = map_filter (fn (m, code) =>
550 if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
554 val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
555 (thy :: Theory.ancestors_of thy);
556 fun prep_def def = (case preprocess thy [def] of
557 [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
560 val (lhs, rhs) = Logic.dest_equals t;
561 val (c, args) = strip_comb lhs;
562 val (s, T) = dest_Const c
563 in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
564 end handle TERM _ => NONE;
565 fun add_def thyname (name, t) = (case dest t of
567 | SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of
569 | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, [])
570 (cons (T, (thyname, split_last (rename_terms (args @ [rhs])))))))
572 fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty
575 fun get_defn thy defs s T = (case Symtab.lookup defs s of
578 let val i = find_index (is_instance T o fst) ds
580 SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i)
585 (**** invoke suitable code generator for term / type ****)
587 fun codegen_error (gr, _) dep s =
588 error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
590 fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
591 (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
592 NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
593 Syntax.string_of_term_global thy t)
596 fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
597 (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
598 NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
599 Syntax.string_of_typ_global thy T)
603 (**** code generator for mixfix expressions ****)
605 fun parens p = Pretty.block [str "(", p, str ")"];
607 fun pretty_fn [] p = [p]
608 | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") ::
609 Pretty.brk 1 :: pretty_fn xs p;
611 fun pretty_mixfix _ _ [] [] _ = []
612 | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs =
613 p :: pretty_mixfix module module' ms ps qs
614 | pretty_mixfix module module' (Ignore :: ms) ps qs =
615 pretty_mixfix module module' ms ps qs
616 | pretty_mixfix module module' (Module :: ms) ps qs =
617 (if module <> module'
618 then cons (str (module' ^ ".")) else I)
619 (pretty_mixfix module module' ms ps qs)
620 | pretty_mixfix module module' (Pretty p :: ms) ps qs =
621 p :: pretty_mixfix module module' ms ps qs
622 | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) =
623 q :: pretty_mixfix module module' ms ps qs;
625 fun replace_quotes [] [] = []
626 | replace_quotes xs (Arg :: ms) =
627 Arg :: replace_quotes xs ms
628 | replace_quotes xs (Ignore :: ms) =
629 Ignore :: replace_quotes xs ms
630 | replace_quotes xs (Module :: ms) =
631 Module :: replace_quotes xs ms
632 | replace_quotes xs (Pretty p :: ms) =
633 Pretty p :: replace_quotes xs ms
634 | replace_quotes (x::xs) (Quote _ :: ms) =
635 Quote x :: replace_quotes xs ms;
638 (**** default code generators ****)
640 fun eta_expand t ts i =
643 val Ts = Library.drop (k, binder_types (fastype_of t));
646 List.foldr (fn (T, t) => Abs ("x", T, t))
647 (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
650 fun mk_app _ p [] = p
651 | mk_app brack p ps = if brack then
652 Pretty.block (str "(" ::
653 separate (Pretty.brk 1) (p :: ps) @ [str ")"])
654 else Pretty.block (separate (Pretty.brk 1) (p :: ps));
656 fun new_names t xs = Name.variant_list
657 (map (fst o fst o dest_Var) (term_vars t) union
658 add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
660 fun new_name t x = hd (new_names t [x]);
662 fun if_library x y = if member (op =) (!mode) "library" then x else y;
664 fun default_codegen thy defs gr dep module brack t =
666 val (u, ts) = strip_comb t;
667 fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack)
671 val (gr', ps) = codegens true (gr, ts);
672 val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
673 in SOME (gr'', mk_app brack (str (s ^
674 (if i=0 then "" else string_of_int i))) ps)
679 val (gr', ps) = codegens true (gr, ts);
680 val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
681 in SOME (gr'', mk_app brack (str s) ps) end
684 (case get_assoc_code thy (s, T) of
686 let val i = num_args_of ms
687 in if length ts < i then
688 default_codegen thy defs gr dep module brack (eta_expand u ts i)
691 val (ts1, ts2) = args_of ms ts;
692 val (gr1, ps1) = codegens false (gr, ts1);
693 val (gr2, ps2) = codegens true (gr1, ts2);
694 val (gr3, ps3) = codegens false (gr2, quotes_of ms);
695 val (gr4, _) = invoke_tycodegen thy defs dep module false
696 (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
697 val (module', suffix) = (case get_defn thy defs s T of
698 NONE => (if_library (thyname_of_const s thy) module, "")
699 | SOME ((U, (module', _)), NONE) =>
700 (if_library module' module, "")
701 | SOME ((U, (module', _)), SOME i) =>
702 (if_library module' module, " def" ^ string_of_int i));
703 val node_id = s ^ suffix;
704 fun p module' = mk_app brack (Pretty.block
705 (pretty_mixfix module module' ms ps1 ps3)) ps2
706 in SOME (case try (get_node gr4) node_id of
707 NONE => (case get_aux_code aux of
708 [] => (gr4, p module)
709 | xs => (add_edge (node_id, dep) (new_node
710 (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4),
712 | SOME (_, module'', _) =>
713 (add_edge (node_id, dep) gr4, p module''))
716 | NONE => (case get_defn thy defs s T of
718 | SOME ((U, (thyname, (args, rhs))), k) =>
720 val module' = if_library thyname module;
721 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
722 val node_id = s ^ suffix;
723 val (gr', (ps, def_id)) = codegens true (gr, ts) |>>>
724 mk_const_id module' (s ^ suffix);
725 val p = mk_app brack (str (mk_qual_id module def_id)) ps
726 in SOME (case try (get_node gr') node_id of
729 val _ = message ("expanding definition of " ^ s);
730 val (Ts, _) = strip_type U;
732 if not (null args) orelse null Ts then (args, rhs) else
733 let val v = Free (new_name rhs "x", hd Ts)
734 in ([v], betapply (rhs, v)) end;
735 val (gr1, p') = invoke_codegen thy defs node_id module' false
736 (add_edge (node_id, dep)
737 (new_node (node_id, (NONE, "", "")) gr'), rhs');
738 val (gr2, xs) = codegens false (gr1, args');
739 val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T);
740 val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U);
741 in (map_node node_id (K (NONE, module', string_of
742 (Pretty.block (separate (Pretty.brk 1)
744 [str ("val " ^ snd def_id ^ " :"), ty]
745 else str ("fun " ^ snd def_id) :: xs) @
746 [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4,
749 | SOME _ => (add_edge (node_id, dep) gr', p))
754 val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
755 val t = strip_abs_body u
756 val bs' = new_names t bs;
757 val (gr1, ps) = codegens true (gr, ts);
758 val (gr2, p) = invoke_codegen thy defs dep module false
759 (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
761 SOME (gr2, mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
768 fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
769 SOME (gr, str (s ^ (if i = 0 then "" else string_of_int i)))
770 | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
772 | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
773 (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
777 val (gr', ps) = foldl_map
778 (invoke_tycodegen thy defs dep module false)
779 (gr, fst (args_of ms Ts));
780 val (gr'', qs) = foldl_map
781 (invoke_tycodegen thy defs dep module false)
783 val module' = if_library (thyname_of_type s thy) module;
784 val node_id = s ^ " (type)";
785 fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
786 in SOME (case try (get_node gr'') node_id of
787 NONE => (case get_aux_code aux of
788 [] => (gr'', p module')
789 | xs => (fst (mk_type_id module' s
790 (add_edge (node_id, dep) (new_node (node_id,
791 (NONE, module', cat_lines xs ^ "\n")) gr''))),
793 | SOME (_, module'', _) =>
794 (add_edge (node_id, dep) gr'', p module''))
797 val _ = Context.>> (Context.map_theory
798 (add_codegen "default" default_codegen #>
799 add_tycodegen "default" default_tycodegen));
803 | mk_tuple ps = Pretty.block (str "(" ::
804 List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @
807 fun mk_let bindings body =
808 Pretty.blk (0, [str "let", Pretty.brk 1,
809 Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
810 Pretty.block [str "val ", pat, str " =", Pretty.brk 1,
811 rhs, str ";"]) bindings)),
812 Pretty.brk 1, str "in", Pretty.brk 1, body,
813 Pretty.brk 1, str "end"]);
815 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
817 fun add_to_module name s = AList.map_entry (op =) name (suffix s);
819 fun output_code gr module xs =
821 val code = map_filter (fn s =>
822 let val c as (_, module', _) = Graph.get_node gr s
823 in if module = "" orelse module = module' then SOME (s, c) else NONE end)
824 (rev (Graph.all_preds gr xs));
825 fun string_of_cycle (a :: b :: cs) =
826 let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
827 if a = a' then Option.map (pair x)
828 (find_first (equal b o #2 o Graph.get_node gr)
829 (Graph.imm_succs gr x))
831 in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
832 | string_of_cycle _ = ""
836 val modules = distinct (op =) (map (#2 o snd) code);
837 val mod_gr = fold_rev Graph.add_edge_acyclic
838 (maps (fn (s, (_, module, _)) => map (pair module)
839 (filter_out (equal module) (map (#2 o Graph.get_node gr)
840 (Graph.imm_succs gr s)))) code)
841 (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
843 rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
845 List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
846 (map (rpair "") modules') code
847 end handle Graph.CYCLES (cs :: _) =>
848 error ("Cyclic dependency of modules:\n" ^ commas cs ^
849 "\n" ^ string_of_cycle cs)
850 else [(module, implode (map (#3 o snd) code))]
853 fun gen_generate_code prep_term thy modules module xs =
855 val _ = (module <> "" orelse
856 member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
857 orelse error "missing module name";
858 val graphs = get_modules thy;
859 val defs = mk_deftab thy;
860 val gr = new_node ("<Top>", (NONE, module, ""))
861 (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
862 (Graph.merge (fn ((_, module, _), (_, module', _)) =>
863 module = module') (gr, gr'),
864 (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
865 (map (fn s => case Symtab.lookup graphs s of
866 NONE => error ("Undefined code module: " ^ s)
867 | SOME gr => gr) modules))
868 handle Graph.DUP k => error ("Duplicate code for " ^ k);
869 fun expand (t as Abs _) = t
870 | expand t = (case fastype_of t of
871 Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
872 val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
873 (invoke_codegen thy defs "<Top>" module false (gr, t)))
874 (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs);
875 val code = map_filter
877 | (s', p) => SOME (string_of (Pretty.block
878 [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps;
879 val code' = space_implode "\n\n" code ^ "\n\n";
881 map_filter (fn (name, s) =>
882 if member (op =) (!mode) "library" andalso name = module andalso null code
884 else SOME (name, mk_struct name s))
885 ((if null code then I
886 else add_to_module module code')
887 (output_code (fst gr') (if_library "" module) ["<Top>"]))
889 (code'', del_nodes ["<Top>"] gr')
892 val generate_code_i = gen_generate_code Sign.cert_term;
893 val generate_code = gen_generate_code OldGoals.read_term;
896 (**** Reflection ****)
898 val strip_tname = implode o tl o explode;
900 fun pretty_list xs = Pretty.block (str "[" ::
901 flat (separate [str ",", Pretty.brk 1] (map single xs)) @
904 fun mk_type p (TVar ((s, i), _)) = str
905 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
906 | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T")
907 | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
908 [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","),
909 Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]);
911 fun mk_term_of gr module p (TVar ((s, i), _)) = str
912 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
913 | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F")
914 | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
915 (Pretty.block (separate (Pretty.brk 1)
916 (str (mk_qual_id module
917 (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
919 [mk_term_of gr module true T, mk_type true T]) Ts)));
922 (**** Test data generators ****)
924 fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
925 (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
926 | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
927 | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
928 (Pretty.block (separate (Pretty.brk 1)
929 (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
930 (if member (op =) xs s then "'" else "")) ::
933 [mk_term_of gr module true T, mk_type true T,
934 mk_gen gr module true xs a U, mk_type true U]
936 [mk_gen gr module true xs a T, mk_type true T]) Ts) @
937 (if member (op =) xs s then [str a] else []))));
939 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
941 fun test_term thy quiet sz i t =
943 val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
944 error "Term to be tested contains type variables";
945 val _ = null (term_vars t) orelse
946 error "Term to be tested contains schematic variables";
947 val frees = map dest_Free (term_frees t);
948 val frees' = frees ~~
949 map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
950 val (code, gr) = setmp mode ["term_of", "test"]
951 (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
952 val s = "structure TestTerm =\nstruct\n\n" ^
953 cat_lines (map snd code) ^
954 "\nopen Generated;\n\n" ^ string_of
955 (Pretty.block [str "val () = Codegen.test_fn :=",
956 Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
957 mk_let (map (fn ((s, T), s') =>
958 (mk_tuple [str s', str (s' ^ "_t")],
959 Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
961 (Pretty.block [str "if ",
962 mk_app false (str "testf") (map (str o snd) frees'),
963 Pretty.brk 1, str "then NONE",
964 Pretty.brk 1, str "else ",
965 Pretty.block [str "SOME ", Pretty.block (str "[" ::
966 flat (separate [str ",", Pretty.brk 1]
967 (map (fn ((s, T), s') => [Pretty.block
968 [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
969 str (s' ^ "_t ())")]]) frees')) @
973 val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
974 fun iter f k = if k > i then NONE
975 else (case (f () handle Match =>
977 else warning "Exception Match raised in generated code"; NONE)) of
978 NONE => iter f (k+1) | SOME x => SOME x);
979 fun test k = if k > sz then NONE
980 else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
981 case iter (fn () => !test_fn k) 1 of
982 NONE => test (k+1) | SOME x => SOME x);
985 fun test_goal quiet ({size, iterations, default_type}, tvinsts) i assms state =
987 val thy = Proof.theory_of state;
988 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
990 val (_, (_, st)) = Proof.get_goal state;
991 val (gi, frees) = Logic.goal_params (prop_of st) i;
992 val gi' = ObjectLogic.atomize_term thy (map_types
993 (map_type_tfree (fn p as (s, S) =>
994 let val T = the_default (the_default (TFree p) default_type)
995 (AList.lookup (op =) tvinsts s)
996 in if Sign.of_sort thy (T, S) then T
997 else error ("Type " ^ Syntax.string_of_typ_global thy T ^
998 " to be substituted for variable " ^
999 Syntax.string_of_typ_global thy (TFree p) ^ "\ndoes not have sort " ^
1000 Syntax.string_of_sort_global thy S)
1002 (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
1003 in test_term thy quiet size iterations gi' end;
1005 fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
1006 | pretty_counterex ctxt (SOME cex) =
1007 Pretty.chunks (Pretty.str "Counterexample found:\n" ::
1009 Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
1011 val auto_quickcheck = ref false;
1012 val auto_quickcheck_time_limit = ref 5000;
1014 fun test_goal' int state =
1016 val ctxt = Proof.context_of state;
1017 val assms = map term_of (Assumption.assms_of ctxt);
1018 val params = get_test_params (Proof.theory_of state);
1021 val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
1022 (try (test_goal true (params, []) 1 assms)) state;
1026 | SOME NONE => state
1027 | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
1028 Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
1029 end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
1031 if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
1036 val _ = Context.>> (Specification.add_theorem_hook test_goal');
1039 (**** Evaluator for terms ****)
1041 val eval_result = ref (fn () => Bound 0);
1043 fun eval_term thy t =
1046 val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
1047 error "Term to be evaluated contains type variables";
1048 val _ = (null (term_vars t) andalso null (term_frees t)) orelse
1049 error "Term to be evaluated contains variables";
1050 val (code, gr) = setmp mode ["term_of"]
1051 (generate_code_i thy [] "Generated")
1052 [("result", Abs ("x", TFree ("'a", []), t))];
1053 val s = "structure EvalTerm =\nstruct\n\n" ^
1054 cat_lines (map snd code) ^
1055 "\nopen Generated;\n\n" ^ string_of
1056 (Pretty.block [str "val () = Codegen.eval_result := (fn () =>",
1058 mk_app false (mk_term_of gr "Generated" false (fastype_of t))
1059 [str "(result ())"],
1062 val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
1063 in !eval_result end;
1066 fun print_evaluated_term s = Toplevel.keep (fn state =>
1068 val ctxt = Toplevel.context_of state;
1069 val thy = ProofContext.theory_of ctxt;
1070 val t = eval_term thy (Syntax.read_term ctxt s);
1071 val T = Term.type_of t;
1074 (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
1075 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
1078 exception Evaluation of term;
1080 fun evaluation_oracle (thy, Evaluation t) =
1081 Logic.mk_equals (t, eval_term thy t);
1083 fun evaluation_conv ct =
1084 let val thy = Thm.theory_of_cterm ct
1085 in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
1087 val _ = Context.>> (Context.map_theory
1088 (Theory.add_oracle ("evaluation", evaluation_oracle)));
1091 (**** Interface ****)
1093 fun parse_mixfix rd s =
1094 (case Scan.finite Symbol.stopper (Scan.repeat
1096 || $$ "?" >> K Ignore
1097 || $$ "\\<module>" >> K Module
1098 || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length)
1099 || $$ "{" |-- $$ "*" |-- Scan.repeat1
1100 ( $$ "'" |-- Scan.one Symbol.is_regular
1101 || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --|
1102 $$ "*" --| $$ "}" >> (Quote o rd o implode)
1104 ( $$ "'" |-- Scan.one Symbol.is_regular
1105 || Scan.unless ($$ "_" || $$ "?" || $$ "\\<module>" || $$ "/" || $$ "{" |-- $$ "*")
1106 (Scan.one Symbol.is_regular)) >> (Pretty o str o implode)))
1107 (Symbol.explode s) of
1109 | _ => error ("Malformed annotation: " ^ quote s));
1112 structure P = OuterParse and K = OuterKeyword;
1114 val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
1116 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
1117 (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
1119 val parse_attach = Scan.repeat (P.$$$ "attach" |--
1120 Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
1121 (P.verbatim >> strip_whitespace));
1124 OuterSyntax.command "types_code"
1125 "associate types with target language types" K.thy_decl
1126 (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
1127 (fn xs => Toplevel.theory (fn thy => fold (assoc_type o
1128 (fn ((name, mfx), aux) => (name, (parse_mixfix
1129 (Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
1132 OuterSyntax.command "consts_code"
1133 "associate constants with target language code" K.thy_decl
1136 P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
1137 (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
1138 (fn ((const, mfx), aux) =>
1139 (const, (parse_mixfix (OldGoals.read_term thy) mfx, aux)))) xs thy)));
1141 fun parse_code lib =
1142 Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
1143 (if lib then Scan.optional P.name "" else P.name) --
1144 Scan.option (P.$$$ "file" |-- P.name) --
1145 (if lib then Scan.succeed []
1146 else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --|
1148 ( Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
1149 || Scan.repeat1 (P.term >> pair "")) >>
1150 (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
1152 val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
1153 val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
1154 in ((case opt_fname of
1156 ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
1157 (cat_lines (map snd code))
1160 app (fn (name, s) => File.write
1161 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s)
1162 (("ROOT", implode (map (fn (name, _) =>
1163 "use \"" ^ name ^ ".ML\";\n") code)) :: code)
1164 else File.write (Path.explode fname) (snd (hd code)));
1166 else map_modules (Symtab.update (module, gr)) thy)
1170 OuterSyntax.command "code_library"
1171 "generates code for terms (one structure for each theory)" K.thy_decl
1175 OuterSyntax.command "code_module"
1176 "generates code for terms (single structure, incremental)" K.thy_decl
1180 [("size", P.nat >> (K o set_size)),
1181 ("iterations", P.nat >> (K o set_iterations)),
1182 ("default_type", P.typ >> set_default_type)];
1184 val parse_test_params = P.short_ident :|-- (fn s =>
1185 P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
1187 fun parse_tyinst xs =
1188 (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
1189 fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
1192 OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
1193 (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
1194 (fn fs => Toplevel.theory (fn thy =>
1195 map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
1198 OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
1199 (Scan.option (P.$$$ "[" |-- P.list1
1200 ( parse_test_params >> (fn f => fn thy => apfst (f thy))
1201 || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
1202 (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |>
1203 test_goal false (Library.apply (the_default []
1204 (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
1205 (get_test_params (Toplevel.theory_of st), [])) g [] |>
1206 pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
1209 OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
1210 (P.term >> (Toplevel.no_timing oo print_evaluated_term));
1214 val auto_quickcheck = Codegen.auto_quickcheck;
1215 val auto_quickcheck_time_limit = Codegen.auto_quickcheck_time_limit;