# HG changeset patch # User blanchet # Date 1298911990 -3600 # Node ID 7244589c8ccc98e37321934be78eaa6ce18fd739 # Parent c3b6e69da3862adf5473049a2c58267bc0b83bac added "total_consts" option diff -r c3b6e69da386 -r 7244589c8ccc src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r c3b6e69da386 -r 7244589c8ccc src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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, diff -r c3b6e69da386 -r 7244589c8ccc src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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) =