--- 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
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 28 17:53:10 2011 +0100
@@ -58,6 +58,7 @@
("destroy_constrs", "true"),
("specialize", "true"),
("star_linear_preds", "true"),
+ ("total_consts", "smart"),
("preconstr", "smart"),
("peephole_optim", "true"),
("datatype_sym_break", "5"),
@@ -91,6 +92,7 @@
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_star_linear_preds", "star_linear_preds"),
+ ("partial_consts", "total_consts"),
("dont_preconstr", "preconstr"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
@@ -253,6 +255,7 @@
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val star_linear_preds = lookup_bool "star_linear_preds"
+ val total_consts = lookup_bool_option "total_consts"
val preconstrs =
lookup_bool_option_assigns read_term_polymorphic "preconstr"
val peephole_optim = lookup_bool "peephole_optim"
@@ -285,8 +288,9 @@
user_axioms = user_axioms, assms = assms, whacks = whacks,
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, preconstrs = preconstrs,
- peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
+ star_linear_preds = star_linear_preds, total_consts = total_consts,
+ preconstrs = preconstrs, peephole_optim = peephole_optim,
+ datatype_sym_break = datatype_sym_break,
kodkod_sym_break = kodkod_sym_break, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
show_datatypes = show_datatypes, show_consts = show_consts,
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 28 17:53:10 2011 +0100
@@ -649,7 +649,7 @@
best_non_opt_set_rep_for_type) scope (type_of v)
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
-fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
+fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v
(vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
@@ -657,7 +657,7 @@
rep_for_abs_fun
else if is_rep_fun ctxt x then
Func oo best_non_opt_symmetric_reps_for_fun_type
- else if all_exact orelse is_skolem_name v orelse
+ else if total_consts orelse is_skolem_name v orelse
member (op =) [@{const_name bisim},
@{const_name bisim_iterator_max}]
(original_name s) then
@@ -674,8 +674,8 @@
fun choose_reps_for_free_vars scope pseudo_frees vs table =
fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
-fun choose_reps_for_consts scope all_exact vs table =
- fold (choose_rep_for_const scope all_exact) vs ([], table)
+fun choose_reps_for_consts scope total_consts vs table =
+ fold (choose_rep_for_const scope total_consts) vs ([], table)
fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
(x as (_, T)) n (vs, table) =