added "total_consts" option
authorblanchet
Mon Feb 28 17:53:10 2011 +0100 (2011-02-28 ago)
changeset 418567244589c8ccc
parent 41855 c3b6e69da386
child 41857 07573743208f
added "total_consts" option
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Feb 26 20:40:45 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 28 17:53:10 2011 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4       destroy_constrs: bool,
     1.5       specialize: bool,
     1.6       star_linear_preds: bool,
     1.7 +     total_consts: bool option,
     1.8       preconstrs: (term option * bool option) list,
     1.9       peephole_optim: bool,
    1.10       datatype_sym_break: int,
    1.11 @@ -108,6 +109,7 @@
    1.12     destroy_constrs: bool,
    1.13     specialize: bool,
    1.14     star_linear_preds: bool,
    1.15 +   total_consts: bool option,
    1.16     preconstrs: (term option * bool option) list,
    1.17     peephole_optim: bool,
    1.18     datatype_sym_break: int,
    1.19 @@ -211,10 +213,10 @@
    1.20           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    1.21           verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
    1.22           binary_ints, destroy_constrs, specialize, star_linear_preds,
    1.23 -         preconstrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
    1.24 -         tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
    1.25 -         atomss, max_potential, max_genuine, check_potential, check_genuine,
    1.26 -         batch_size, ...} = params
    1.27 +         total_consts, preconstrs, peephole_optim, datatype_sym_break,
    1.28 +         kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
    1.29 +         show_consts, evals, formats, atomss, max_potential, max_genuine,
    1.30 +         check_potential, check_genuine, batch_size, ...} = params
    1.31      val state_ref = Unsynchronized.ref state
    1.32      val pprint =
    1.33        if auto then
    1.34 @@ -487,7 +489,10 @@
    1.35                                      string_of_int j0))
    1.36                           (Typtab.dest ofs)
    1.37  *)
    1.38 -        val all_exact = forall (is_exact_type datatypes true) all_Ts
    1.39 +        val total_consts =
    1.40 +          case total_consts of
    1.41 +            SOME b => b
    1.42 +          | NONE => forall (is_exact_type datatypes true) all_Ts
    1.43          val main_j0 = offset_of_type ofs bool_T
    1.44          val (nat_card, nat_j0) = spec_of_type scope nat_T
    1.45          val (int_card, int_j0) = spec_of_type scope int_T
    1.46 @@ -500,7 +505,7 @@
    1.47                                      NameTable.empty
    1.48          val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
    1.49          val (nonsel_names, rep_table) =
    1.50 -          choose_reps_for_consts scope all_exact nonsel_names rep_table
    1.51 +          choose_reps_for_consts scope total_consts nonsel_names rep_table
    1.52          val (guiltiest_party, min_highest_arity) =
    1.53            NameTable.fold (fn (name, R) => fn (s, n) =>
    1.54                               let val n' = arity_of_rep R in
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Feb 26 20:40:45 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 28 17:53:10 2011 +0100
     2.3 @@ -58,6 +58,7 @@
     2.4     ("destroy_constrs", "true"),
     2.5     ("specialize", "true"),
     2.6     ("star_linear_preds", "true"),
     2.7 +   ("total_consts", "smart"),
     2.8     ("preconstr", "smart"),
     2.9     ("peephole_optim", "true"),
    2.10     ("datatype_sym_break", "5"),
    2.11 @@ -91,6 +92,7 @@
    2.12     ("dont_destroy_constrs", "destroy_constrs"),
    2.13     ("dont_specialize", "specialize"),
    2.14     ("dont_star_linear_preds", "star_linear_preds"),
    2.15 +   ("partial_consts", "total_consts"),
    2.16     ("dont_preconstr", "preconstr"),
    2.17     ("no_peephole_optim", "peephole_optim"),
    2.18     ("no_debug", "debug"),
    2.19 @@ -253,6 +255,7 @@
    2.20      val destroy_constrs = lookup_bool "destroy_constrs"
    2.21      val specialize = lookup_bool "specialize"
    2.22      val star_linear_preds = lookup_bool "star_linear_preds"
    2.23 +    val total_consts = lookup_bool_option "total_consts"
    2.24      val preconstrs =
    2.25        lookup_bool_option_assigns read_term_polymorphic "preconstr"
    2.26      val peephole_optim = lookup_bool "peephole_optim"
    2.27 @@ -285,8 +288,9 @@
    2.28       user_axioms = user_axioms, assms = assms, whacks = whacks,
    2.29       merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    2.30       destroy_constrs = destroy_constrs, specialize = specialize,
    2.31 -     star_linear_preds = star_linear_preds, preconstrs = preconstrs,
    2.32 -     peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
    2.33 +     star_linear_preds = star_linear_preds, total_consts = total_consts,
    2.34 +     preconstrs = preconstrs, peephole_optim = peephole_optim,
    2.35 +     datatype_sym_break = datatype_sym_break,
    2.36       kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    2.37       tac_timeout = tac_timeout, max_threads = max_threads,
    2.38       show_datatypes = show_datatypes, show_consts = show_consts,
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Sat Feb 26 20:40:45 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Feb 28 17:53:10 2011 +0100
     3.3 @@ -649,7 +649,7 @@
     3.4                 best_non_opt_set_rep_for_type) scope (type_of v)
     3.5      val v = modify_name_rep v R
     3.6    in (v :: vs, NameTable.update (v, R) table) end
     3.7 -fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
     3.8 +fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v
     3.9                           (vs, table) =
    3.10    let
    3.11      val x as (s, T) = (nickname_of v, type_of v)
    3.12 @@ -657,7 +657,7 @@
    3.13                 rep_for_abs_fun
    3.14               else if is_rep_fun ctxt x then
    3.15                 Func oo best_non_opt_symmetric_reps_for_fun_type
    3.16 -             else if all_exact orelse is_skolem_name v orelse
    3.17 +             else if total_consts orelse is_skolem_name v orelse
    3.18                       member (op =) [@{const_name bisim},
    3.19                                      @{const_name bisim_iterator_max}]
    3.20                              (original_name s) then
    3.21 @@ -674,8 +674,8 @@
    3.22  
    3.23  fun choose_reps_for_free_vars scope pseudo_frees vs table =
    3.24    fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
    3.25 -fun choose_reps_for_consts scope all_exact vs table =
    3.26 -  fold (choose_rep_for_const scope all_exact) vs ([], table)
    3.27 +fun choose_reps_for_consts scope total_consts vs table =
    3.28 +  fold (choose_rep_for_const scope total_consts) vs ([], table)
    3.29  
    3.30  fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
    3.31                                        (x as (_, T)) n (vs, table) =