32 merge_type_vars: bool, |
32 merge_type_vars: bool, |
33 binary_ints: bool option, |
33 binary_ints: bool option, |
34 destroy_constrs: bool, |
34 destroy_constrs: bool, |
35 specialize: bool, |
35 specialize: bool, |
36 star_linear_preds: bool, |
36 star_linear_preds: bool, |
|
37 total_consts: bool option, |
37 preconstrs: (term option * bool option) list, |
38 preconstrs: (term option * bool option) list, |
38 peephole_optim: bool, |
39 peephole_optim: bool, |
39 datatype_sym_break: int, |
40 datatype_sym_break: int, |
40 kodkod_sym_break: int, |
41 kodkod_sym_break: int, |
41 timeout: Time.time option, |
42 timeout: Time.time option, |
106 merge_type_vars: bool, |
107 merge_type_vars: bool, |
107 binary_ints: bool option, |
108 binary_ints: bool option, |
108 destroy_constrs: bool, |
109 destroy_constrs: bool, |
109 specialize: bool, |
110 specialize: bool, |
110 star_linear_preds: bool, |
111 star_linear_preds: bool, |
|
112 total_consts: bool option, |
111 preconstrs: (term option * bool option) list, |
113 preconstrs: (term option * bool option) list, |
112 peephole_optim: bool, |
114 peephole_optim: bool, |
113 datatype_sym_break: int, |
115 datatype_sym_break: int, |
114 kodkod_sym_break: int, |
116 kodkod_sym_break: int, |
115 timeout: Time.time option, |
117 timeout: Time.time option, |
209 *) |
211 *) |
210 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
212 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, |
211 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
213 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, |
212 verbose, overlord, user_axioms, assms, whacks, merge_type_vars, |
214 verbose, overlord, user_axioms, assms, whacks, merge_type_vars, |
213 binary_ints, destroy_constrs, specialize, star_linear_preds, |
215 binary_ints, destroy_constrs, specialize, star_linear_preds, |
214 preconstrs, peephole_optim, datatype_sym_break, kodkod_sym_break, |
216 total_consts, preconstrs, peephole_optim, datatype_sym_break, |
215 tac_timeout, max_threads, show_datatypes, show_consts, evals, formats, |
217 kodkod_sym_break, tac_timeout, max_threads, show_datatypes, |
216 atomss, max_potential, max_genuine, check_potential, check_genuine, |
218 show_consts, evals, formats, atomss, max_potential, max_genuine, |
217 batch_size, ...} = params |
219 check_potential, check_genuine, batch_size, ...} = params |
218 val state_ref = Unsynchronized.ref state |
220 val state_ref = Unsynchronized.ref state |
219 val pprint = |
221 val pprint = |
220 if auto then |
222 if auto then |
221 Unsynchronized.change state_ref o Proof.goal_message o K |
223 Unsynchronized.change state_ref o Proof.goal_message o K |
222 o Pretty.chunks o cons (Pretty.str "") o single |
224 o Pretty.chunks o cons (Pretty.str "") o single |
485 val _ = List.app (fn (T, j0) => |
487 val _ = List.app (fn (T, j0) => |
486 print_g (string_for_type ctxt T ^ " = " ^ |
488 print_g (string_for_type ctxt T ^ " = " ^ |
487 string_of_int j0)) |
489 string_of_int j0)) |
488 (Typtab.dest ofs) |
490 (Typtab.dest ofs) |
489 *) |
491 *) |
490 val all_exact = forall (is_exact_type datatypes true) all_Ts |
492 val total_consts = |
|
493 case total_consts of |
|
494 SOME b => b |
|
495 | NONE => forall (is_exact_type datatypes true) all_Ts |
491 val main_j0 = offset_of_type ofs bool_T |
496 val main_j0 = offset_of_type ofs bool_T |
492 val (nat_card, nat_j0) = spec_of_type scope nat_T |
497 val (nat_card, nat_j0) = spec_of_type scope nat_T |
493 val (int_card, int_j0) = spec_of_type scope int_T |
498 val (int_card, int_j0) = spec_of_type scope int_T |
494 val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse |
499 val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse |
495 raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope", |
500 raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope", |
498 val (free_names, rep_table) = |
503 val (free_names, rep_table) = |
499 choose_reps_for_free_vars scope pseudo_frees free_names |
504 choose_reps_for_free_vars scope pseudo_frees free_names |
500 NameTable.empty |
505 NameTable.empty |
501 val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table |
506 val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table |
502 val (nonsel_names, rep_table) = |
507 val (nonsel_names, rep_table) = |
503 choose_reps_for_consts scope all_exact nonsel_names rep_table |
508 choose_reps_for_consts scope total_consts nonsel_names rep_table |
504 val (guiltiest_party, min_highest_arity) = |
509 val (guiltiest_party, min_highest_arity) = |
505 NameTable.fold (fn (name, R) => fn (s, n) => |
510 NameTable.fold (fn (name, R) => fn (s, n) => |
506 let val n' = arity_of_rep R in |
511 let val n' = arity_of_rep R in |
507 if n' > n then (nickname_of name, n') else (s, n) |
512 if n' > n then (nickname_of name, n') else (s, n) |
508 end) rep_table ("", 1) |
513 end) rep_table ("", 1) |