--- a/doc-src/Nitpick/nitpick.tex Thu Aug 05 18:33:07 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Thu Aug 05 20:17:50 2010 +0200
@@ -2494,6 +2494,14 @@
{\small See also \textit{debug} (\S\ref{output-format}).}
+\opnodefault{whack}{term\_list}
+Specifies a list of atomic terms (usually constants, but also free and schematic
+variables) that should be taken as being $\unk$ (unknown). This can be useful to
+reduce the size of the Kodkod problem if you can guess in advance that a
+constant might not be needed to find a countermodel.
+
+{\small See also \textit{debug} (\S\ref{output-format}).}
+
\optrue{peephole\_optim}{no\_peephole\_optim}
Specifies whether Nitpick should simplify the generated Kodkod formulas using a
peephole optimizer. These optimizations can make a significant difference.
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 05 18:33:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 05 20:17:50 2010 +0200
@@ -28,6 +28,7 @@
overlord: bool,
user_axioms: bool option,
assms: bool,
+ whacks: term list,
merge_type_vars: bool,
binary_ints: bool option,
destroy_constrs: bool,
@@ -101,6 +102,7 @@
overlord: bool,
user_axioms: bool option,
assms: bool,
+ whacks: term list,
merge_type_vars: bool,
binary_ints: bool option,
destroy_constrs: bool,
@@ -193,12 +195,12 @@
*)
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
- verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
- destroy_constrs, specialize, star_linear_preds, fast_descrs,
- 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
+ verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
+ binary_ints, destroy_constrs, specialize, star_linear_preds,
+ fast_descrs, 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
@@ -263,15 +265,16 @@
val (hol_ctxt as {wf_cache, ...}) =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
- binary_ints = binary_ints, destroy_constrs = destroy_constrs,
- specialize = specialize, star_linear_preds = star_linear_preds,
- fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_table = def_table,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+ whacks = whacks, binary_ints = binary_ints,
+ destroy_constrs = destroy_constrs, specialize = specialize,
+ star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_table = def_table, nondef_table = nondef_table,
+ user_nondefs = user_nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val pseudo_frees = fold Term.add_frees assm_ts []
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 18:33:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 20:17:50 2010 +0200
@@ -22,6 +22,7 @@
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
+ whacks: term list,
binary_ints: bool option,
destroy_constrs: bool,
specialize: bool,
@@ -236,6 +237,7 @@
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
+ whacks: term list,
binary_ints: bool option,
destroy_constrs: bool,
specialize: bool,
@@ -1578,9 +1580,9 @@
val def_inline_threshold_for_booleans = 50
val def_inline_threshold_for_non_booleans = 20
-fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names,
- def_table, ground_thm_table, ersatz_table,
- ...}) =
+fun unfold_defs_in_term
+ (hol_ctxt as {thy, ctxt, stds, whacks, fast_descrs, case_names,
+ def_table, ground_thm_table, ersatz_table, ...}) =
let
fun do_term depth Ts t =
case t of
@@ -1628,10 +1630,12 @@
(case strip_comb t of
(Const x, ts) => do_const depth Ts t x ts
| _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2))
- | Free _ => t
- | Var _ => t
| Bound _ => t
| Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
+ | _ => if member (term_match thy) whacks t then
+ Const (@{const_name unknown}, fastype_of1 (Ts, t))
+ else
+ t
and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
(Abs (Name.uu, body_type T,
select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
@@ -1641,7 +1645,9 @@
select_nth_constr_arg_with_args depth Ts
(@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T
and do_const depth Ts t (x as (s, T)) ts =
- case AList.lookup (op =) ersatz_table s of
+ if member (term_match thy) whacks (Const x) then
+ Const (@{const_name unknown}, fastype_of1 (Ts, t))
+ else case AList.lookup (op =) ersatz_table s of
SOME s' =>
do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
| NONE =>
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Aug 05 18:33:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Aug 05 20:17:50 2010 +0200
@@ -101,7 +101,7 @@
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", "eval", "expect"] s orelse
+ member (op =) ["max", "show_all", "whack", "eval", "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", "format",
@@ -214,13 +214,13 @@
case lookup name of
NONE => NONE
| SOME s => parse_time_option name s
- val lookup_term_list =
- AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
val read_type_polymorphic =
Syntax.read_typ ctxt #> Logic.mk_type
#> 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 read_const_polymorphic = read_term_polymorphic #> dest_Const
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
@@ -240,6 +240,7 @@
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 merge_type_vars = lookup_bool "merge_type_vars"
val binary_ints = lookup_bool_option "binary_ints"
val destroy_constrs = lookup_bool "destroy_constrs"
@@ -256,7 +257,7 @@
val show_consts = debug orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
- val evals = lookup_term_list "eval"
+ val evals = lookup_term_list_polymorphic "eval"
val max_potential =
if auto then 0 else Int.max (0, lookup_int "max_potential")
val max_genuine = Int.max (0, lookup_int "max_genuine")
@@ -273,7 +274,7 @@
boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
debug = debug, verbose = verbose, overlord = overlord,
- user_axioms = user_axioms, assms = assms,
+ 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, fast_descrs = fast_descrs,
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Aug 05 18:33:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Aug 05 20:17:50 2010 +0200
@@ -852,7 +852,7 @@
fun reconstruct_hol_model {show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
- debug, binary_ints, destroy_constrs, specialize,
+ debug, whacks, binary_ints, destroy_constrs, specialize,
star_linear_preds, fast_descrs, tac_timeout, evals,
case_names, def_table, nondef_table, user_nondefs,
simp_table, psimp_table, choice_spec_table, intro_table,
@@ -868,17 +868,17 @@
val hol_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
- binary_ints = binary_ints, destroy_constrs = destroy_constrs,
- specialize = specialize, star_linear_preds = star_linear_preds,
- fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_table = def_table,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = skolems, special_funs = special_funs,
- unrolled_preds = unrolled_preds, wf_cache = wf_cache,
- constr_cache = constr_cache}
+ whacks = whacks, binary_ints = binary_ints,
+ destroy_constrs = destroy_constrs, specialize = specialize,
+ star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_table = def_table, nondef_table = nondef_table,
+ user_nondefs = user_nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = skolems,
+ special_funs = special_funs, unrolled_preds = unrolled_preds,
+ wf_cache = wf_cache, constr_cache = constr_cache}
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}