src/HOL/Tools/Nitpick/nitpick.ML
changeset 41856 7244589c8ccc
parent 41803 ef13e3b7cbaf
child 41858 37ce158d6266
     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