--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 28 17:53:10 2011 +0100
@@ -34,6 +34,7 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
+ total_consts: bool option,
preconstrs: (term option * bool option) list,
peephole_optim: bool,
datatype_sym_break: int,
@@ -108,6 +109,7 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
+ total_consts: bool option,
preconstrs: (term option * bool option) list,
peephole_optim: bool,
datatype_sym_break: int,
@@ -211,10 +213,10 @@
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
binary_ints, destroy_constrs, specialize, star_linear_preds,
- preconstrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
- tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
- atomss, max_potential, max_genuine, check_potential, check_genuine,
- batch_size, ...} = params
+ total_consts, preconstrs, peephole_optim, datatype_sym_break,
+ kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
+ show_consts, evals, formats, atomss, max_potential, max_genuine,
+ check_potential, check_genuine, batch_size, ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
if auto then
@@ -487,7 +489,10 @@
string_of_int j0))
(Typtab.dest ofs)
*)
- val all_exact = forall (is_exact_type datatypes true) all_Ts
+ val total_consts =
+ case total_consts of
+ SOME b => b
+ | NONE => forall (is_exact_type datatypes true) all_Ts
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
@@ -500,7 +505,7 @@
NameTable.empty
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
val (nonsel_names, rep_table) =
- choose_reps_for_consts scope all_exact nonsel_names rep_table
+ choose_reps_for_consts scope total_consts nonsel_names rep_table
val (guiltiest_party, min_highest_arity) =
NameTable.fold (fn (name, R) => fn (s, n) =>
let val n' = arity_of_rep R in