--- a/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:20:48 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:20:48 2011 +0100
@@ -2465,17 +2465,13 @@
{\small See also \textit{debug} (\S\ref{output-format}).}
-\opargboolorsmart{need}{term}{dont\_need}
-Specifies whether a datatype value is required by the problem, meaning Nitpick
-will reserve a Kodkod atom for it. If a value must necessarily belong to the
-subset of representable values that approximates a datatype, specifying it can
-speed up the search significantly, especially for high cardinalities. By
-default, Nitpick inspects the conjecture to infer needed datatype values.
-
-\opsmart{need}{dont\_need}
-Specifies the default needed datatype value setting to use. This can be
-overridden on a per-term basis using the \textit{preconstr}~\qty{term} option
-described above.
+\opnodefault{need}{term\_list}
+Specifies a list of datatype values (ground constructor terms) that should be
+part of the subterm-closed subsets used to approximate datatypes. If you know
+that a value must necessarily belong to the subset of representable values that
+approximates a datatype, specifying it can speed up the search, especially for
+high cardinalities. By default, Nitpick inspects the conjecture to infer needed
+datatype values.
\opsmart{total\_consts}{partial\_consts}
Specifies whether constants occurring in the problem other than constructors can
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 11:20:48 2011 +0100
@@ -39,7 +39,7 @@
stds = stds, wfs = [], user_axioms = NONE, debug = false,
whacks = [], binary_ints = SOME false, destroy_constrs = true,
specialize = false, star_linear_preds = false, total_consts = NONE,
- needs = [], tac_timeout = NONE, evals = [], case_names = case_names,
+ needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
def_tables = def_tables, nondef_table = nondef_table,
user_nondefs = user_nondefs, simp_table = simp_table,
psimp_table = psimp_table, choice_spec_table = choice_spec_table,
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 11:20:48 2011 +0100
@@ -35,7 +35,7 @@
specialize: bool,
star_linear_preds: bool,
total_consts: bool option,
- needs: (term option * bool option) list,
+ needs: term list option,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -110,7 +110,7 @@
specialize: bool,
star_linear_preds: bool,
total_consts: bool option,
- needs: (term option * bool option) list,
+ needs: term list option,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -258,7 +258,7 @@
o Date.fromTimeLocal o Time.now)
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
- val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
+ val conj_ts = neg_t :: assm_ts @ evals @ these needs
val tfree_table =
if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
else []
@@ -266,8 +266,8 @@
val neg_t = neg_t |> merge_tfrees
val assm_ts = assm_ts |> map merge_tfrees
val evals = evals |> map merge_tfrees
- val needs = needs |> map (apfst (Option.map merge_tfrees))
- val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
+ val needs = needs |> Option.map (map merge_tfrees)
+ val conj_ts = neg_t :: assm_ts @ evals @ these needs
val original_max_potential = max_potential
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 11:20:48 2011 +0100
@@ -28,7 +28,7 @@
specialize: bool,
star_linear_preds: bool,
total_consts: bool option,
- needs: (term option * bool option) list,
+ needs: term list option,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
@@ -261,7 +261,7 @@
specialize: bool,
star_linear_preds: bool,
total_consts: bool option,
- needs: (term option * bool option) list,
+ needs: term list option,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:20:48 2011 +0100
@@ -59,7 +59,6 @@
("specialize", "true"),
("star_linear_preds", "true"),
("total_consts", "smart"),
- ("need", "smart"),
("peephole_optim", "true"),
("datatype_sym_break", "5"),
("kodkod_sym_break", "15"),
@@ -93,7 +92,6 @@
("dont_specialize", "specialize"),
("dont_star_linear_preds", "star_linear_preds"),
("partial_consts", "total_consts"),
- ("dont_need", "need"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
("quiet", "verbose"),
@@ -106,11 +104,12 @@
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
AList.defined (op =) negated_params s orelse
- member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
+ member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",
+ "expect"] s orelse
exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
- "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need",
- "dont_need", "format", "atoms"]
+ "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
+ "atoms"]
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
@@ -226,8 +225,8 @@
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
val read_term_polymorphic =
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
- val lookup_term_list_polymorphic =
- AList.lookup (op =) raw_params #> these #> map read_term_polymorphic
+ val lookup_term_list_option_polymorphic =
+ AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
val read_const_polymorphic = read_term_polymorphic #> dest_Const
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
|> auto ? map (apsnd (take max_auto_scopes))
@@ -249,14 +248,14 @@
val overlord = lookup_bool "overlord"
val user_axioms = lookup_bool_option "user_axioms"
val assms = lookup_bool "assms"
- val whacks = lookup_term_list_polymorphic "whack"
+ val whacks = lookup_term_list_option_polymorphic "whack" |> these
val merge_type_vars = lookup_bool "merge_type_vars"
val binary_ints = lookup_bool_option "binary_ints"
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 needs = lookup_bool_option_assigns read_term_polymorphic "need"
+ val needs = lookup_term_list_option_polymorphic "need"
val peephole_optim = lookup_bool "peephole_optim"
val datatype_sym_break = lookup_int "datatype_sym_break"
val kodkod_sym_break = lookup_int "kodkod_sym_break"
@@ -265,7 +264,7 @@
val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
val show_datatypes = debug orelse lookup_bool "show_datatypes"
val show_consts = debug orelse lookup_bool "show_consts"
- val evals = lookup_term_list_polymorphic "eval"
+ val evals = lookup_term_list_option_polymorphic "eval" |> these
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
val max_potential =
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:20:48 2011 +0100
@@ -1282,11 +1282,10 @@
#> Term.map_abs_vars shortest_name
val nondef_ts = nondef_ts |> map (do_middle false)
val need_ts =
- (* FIXME: Implement inference. *)
- needs |> map_filter (fn (SOME t, SOME true) =>
- SOME (t |> unfold_defs_in_term hol_ctxt
- |> do_middle false)
- | _ => NONE)
+ case needs of
+ SOME needs =>
+ needs |> map (unfold_defs_in_term hol_ctxt #> do_middle false)
+ | NONE => [] (* FIXME: Implement inference. *)
val nondef_ts = nondef_ts |> map (do_tail false)
val def_ts = def_ts |> map (do_middle true #> do_tail true)
in