--- a/doc-src/Nitpick/nitpick.tex Thu Mar 03 10:55:41 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:20:48 2011 +0100
@@ -2465,17 +2465,17 @@
{\small See also \textit{debug} (\S\ref{output-format}).}
-\opargboolorsmart{preconstr}{term}{dont\_preconstr}
-Specifies whether a datatype value should be preconstructed, meaning Nitpick
+\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, preconstructing
-it can speed up the search significantly, especially for high cardinalities. By
-default, Nitpick inspects the conjecture to infer terms that can be
-preconstructed.
-
-\opsmart{preconstr}{dont\_preconstr}
-Specifies the default preconstruction setting to use. This can be overridden on
-a per-term basis using the \textit{preconstr}~\qty{term} option described above.
+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.
\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 10:55:41 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,
- preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names,
+ needs = [], 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 10:55:41 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,
- preconstrs: (term option * bool option) list,
+ needs: (term option * bool option) list,
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,
- preconstrs: (term option * bool option) list,
+ needs: (term option * bool option) list,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -199,7 +199,7 @@
fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us
| check_constr_nut _ =
- error "The \"preconstr\" option requires a constructor term."
+ error "The \"need\" option requires a constructor term."
fun pick_them_nits_in_term deadline state (params : params) auto i n step
subst assm_ts orig_t =
@@ -217,7 +217,7 @@
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,
- total_consts, preconstrs, peephole_optim, datatype_sym_break,
+ total_consts, needs, 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
@@ -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 preconstrs
+ val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst 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 preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees))
- val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
+ val needs = needs |> map (apfst (Option.map merge_tfrees))
+ val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
val original_max_potential = max_potential
val original_max_genuine = max_genuine
val max_bisim_depth = fold Integer.max bisim_depths ~1
@@ -289,7 +289,7 @@
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
star_linear_preds = star_linear_preds, total_consts = total_consts,
- preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
+ needs = needs, tac_timeout = tac_timeout, evals = 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,
@@ -302,7 +302,7 @@
val real_frees = fold Term.add_frees conj_ts []
val _ = null (fold Term.add_tvars conj_ts []) orelse
error "Nitpick cannot handle goals with schematic type variables."
- val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
+ val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
no_poly_user_axioms, binarize) =
preprocess_formulas hol_ctxt assm_ts neg_t
val got_all_user_axioms =
@@ -332,8 +332,8 @@
val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
- val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
- val _ = List.app check_constr_nut preconstr_us
+ val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
+ val _ = List.app check_constr_nut need_us
val (free_names, const_names) =
fold add_free_and_const_names (nondef_us @ def_us) ([], [])
val (sel_names, nonsel_names) =
@@ -526,8 +526,8 @@
def_us |> map (choose_reps_in_nut scope unsound rep_table true)
val nondef_us =
nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
- val preconstr_us =
- preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false)
+ val need_us =
+ need_us |> map (choose_reps_in_nut scope unsound rep_table false)
(*
val _ = List.app (print_g o string_for_nut ctxt)
(free_names @ sel_names @ nonsel_names @
@@ -541,8 +541,7 @@
rename_free_vars nonsel_names pool rel_table
val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
- val preconstr_us =
- preconstr_us |> map (rename_vars_in_nut pool rel_table)
+ val need_us = need_us |> map (rename_vars_in_nut pool rel_table)
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
@@ -568,7 +567,7 @@
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
val dtype_axioms =
- declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
+ declarative_axioms_for_datatypes hol_ctxt binarize need_us
datatype_sym_break bits ofs kk rel_table datatypes
val declarative_axioms = plain_axioms @ dtype_axioms
val univ_card = Int.max (univ_card nat_card int_card main_j0
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 10:55:41 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,
- preconstrs: (term option * bool option) list,
+ needs: (term option * bool option) list,
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,
- preconstrs: (term option * bool option) list,
+ needs: (term option * bool option) list,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 10:55:41 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:20:48 2011 +0100
@@ -59,7 +59,7 @@
("specialize", "true"),
("star_linear_preds", "true"),
("total_consts", "smart"),
- ("preconstr", "smart"),
+ ("need", "smart"),
("peephole_optim", "true"),
("datatype_sym_break", "5"),
("kodkod_sym_break", "15"),
@@ -93,7 +93,7 @@
("dont_specialize", "specialize"),
("dont_star_linear_preds", "star_linear_preds"),
("partial_consts", "total_consts"),
- ("dont_preconstr", "preconstr"),
+ ("dont_need", "need"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
("quiet", "verbose"),
@@ -109,8 +109,8 @@
member (op =) ["max", "show_all", "whack", "eval", "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", "preconstr",
- "dont_preconstr", "format", "atoms"]
+ "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need",
+ "dont_need", "format", "atoms"]
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
@@ -256,8 +256,7 @@
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 needs = lookup_bool_option_assigns read_term_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"
@@ -289,7 +288,7 @@
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
star_linear_preds = star_linear_preds, total_consts = total_consts,
- preconstrs = preconstrs, peephole_optim = peephole_optim,
+ needs = needs, 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,
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 10:55:41 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 11:20:48 2011 +0100
@@ -1478,8 +1478,8 @@
"malformed Kodkod formula")
end
-fun preconstructed_value_axioms_for_datatype [] _ _ _ = []
- | preconstructed_value_axioms_for_datatype preconstr_us ofs kk
+fun needed_value_axioms_for_datatype [] _ _ _ = []
+ | needed_value_axioms_for_datatype need_us ofs kk
({typ, card, constrs, ...} : datatype_spec) =
let
fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
@@ -1507,10 +1507,9 @@
else
accum)
| aux u =
- raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\
- \.aux", [u])
+ raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
in
- case SOME (index_seq 0 card, []) |> fold aux preconstr_us of
+ case SOME (index_seq 0 card, []) |> fold aux need_us of
SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
| NONE => [KK.False]
end
@@ -1654,14 +1653,14 @@
nfas dtypes)
end
-fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) =
- T = T' orelse exists (is_datatype_in_preconstructed_value T) us
- | is_datatype_in_preconstructed_value _ _ = false
+fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
+ T = T' orelse exists (is_datatype_in_needed_value T) us
+ | is_datatype_in_needed_value _ _ = false
val min_sym_break_card = 7
-fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
- datatype_sym_break kk rel_table nfas dtypes =
+fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
+ kk rel_table nfas dtypes =
if datatype_sym_break = 0 then
[]
else
@@ -1673,8 +1672,7 @@
o binder_types o snd o #const) constrs)
|> filter_out
(fn {typ, ...} =>
- exists (is_datatype_in_preconstructed_value typ)
- preconstr_us)
+ exists (is_datatype_in_needed_value typ) need_us)
|> (fn dtypes' =>
dtypes' |> length dtypes' > datatype_sym_break
? (sort (datatype_ord o swap)
@@ -1779,7 +1777,7 @@
partition_axioms_for_datatype j0 kk rel_table dtype
end
-fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
+fun declarative_axioms_for_datatypes hol_ctxt binarize need_us
datatype_sym_break bits ofs kk rel_table dtypes =
let
val nfas =
@@ -1788,9 +1786,9 @@
|> strongly_connected_sub_nfas
in
acyclicity_axioms_for_datatypes kk nfas @
- maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @
- sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
- datatype_sym_break kk rel_table nfas dtypes @
+ maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @
+ sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
+ kk rel_table nfas dtypes @
maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
dtypes
end
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 10:55:41 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 11:20:48 2011 +0100
@@ -862,7 +862,7 @@
fun reconstruct_hol_model {show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
- star_linear_preds, total_consts, preconstrs, tac_timeout,
+ star_linear_preds, total_consts, needs, tac_timeout,
evals, case_names, def_tables, nondef_table, user_nondefs,
simp_table, psimp_table, choice_spec_table, intro_table,
ground_thm_table, ersatz_table, skolems, special_funs,
@@ -880,7 +880,7 @@
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
star_linear_preds = star_linear_preds, total_consts = total_consts,
- preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
+ needs = needs, tac_timeout = tac_timeout, evals = 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,
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 10:55:41 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:20:48 2011 +0100
@@ -1244,7 +1244,7 @@
fun preprocess_formulas
(hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
- preconstrs, ...}) assm_ts neg_t =
+ needs, ...}) assm_ts neg_t =
let
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
neg_t |> unfold_defs_in_term hol_ctxt
@@ -1281,18 +1281,17 @@
#> close_form
#> Term.map_abs_vars shortest_name
val nondef_ts = nondef_ts |> map (do_middle false)
- val preconstr_ts =
- (* FIXME: Implement preconstruction inference. *)
- preconstrs
- |> map_filter (fn (SOME t, SOME true) =>
- SOME (t |> unfold_defs_in_term hol_ctxt
- |> do_middle false)
- | _ => NONE)
+ 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)
val nondef_ts = nondef_ts |> map (do_tail false)
val def_ts = def_ts |> map (do_middle true #> do_tail true)
in
- (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
- no_poly_user_axioms, binarize)
+ (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms,
+ binarize)
end
end;