--- a/NEWS Thu Mar 17 14:43:53 2011 +0100
+++ b/NEWS Thu Mar 17 22:07:17 2011 +0100
@@ -42,6 +42,7 @@
* Nitpick:
- Added "need" and "total_consts" options.
+ - Reintroduced "show_skolems" option by popular demand.
- Renamed attribute: nitpick_def ~> nitpick_unfold.
INCOMPATIBILITY.
--- a/doc-src/Nitpick/nitpick.tex Thu Mar 17 14:43:53 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 17 22:07:17 2011 +0100
@@ -2193,6 +2193,12 @@
investigating whether a potentially spurious counterexample is genuine, but
their potential for clutter is real.
+\optrue{show\_skolems}{hide\_skolem}
+Specifies whether the values of Skolem constants should be displayed as part of
+counterexamples. Skolem constants correspond to bound variables in the original
+formula and usually help us to understand why the counterexample falsifies the
+formula.
+
\opfalse{show\_consts}{hide\_consts}
Specifies whether the values of constants occurring in the formula (including
its axioms) should be displayed along with any counterexample. These values are
@@ -2200,7 +2206,8 @@
genuine, but they can clutter the output.
\opnodefault{show\_all}{bool}
-Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
+Abbreviation for \textit{show\_datatypes}, \textit{show\_skolems}, and
+\textit{show\_consts}.
\opdefault{max\_potential}{int}{\upshape 1}
Specifies the maximum number of potentially spurious counterexamples to display.
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 17 14:43:53 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 17 22:07:17 2011 +0100
@@ -43,6 +43,7 @@
tac_timeout: Time.time option,
max_threads: int,
show_datatypes: bool,
+ show_skolems: bool,
show_consts: bool,
evals: term list,
formats: (term option * int list) list,
@@ -118,6 +119,7 @@
tac_timeout: Time.time option,
max_threads: int,
show_datatypes: bool,
+ show_skolems: bool,
show_consts: bool,
evals: term list,
formats: (term option * int list) list,
@@ -215,8 +217,8 @@
binary_ints, destroy_constrs, specialize, star_linear_preds,
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
+ show_skolems, 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
@@ -638,8 +640,9 @@
: problem_extension) =
let
val (reconstructed_model, codatatypes_ok) =
- reconstruct_hol_model {show_datatypes = show_datatypes,
- show_consts = show_consts}
+ reconstruct_hol_model
+ {show_datatypes = show_datatypes, show_skolems = show_skolems,
+ show_consts = show_consts}
scope formats atomss real_frees pseudo_frees free_names sel_names
nonsel_names rel_table bounds
val genuine_means_genuine =
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 17 14:43:53 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 17 22:07:17 2011 +0100
@@ -69,6 +69,7 @@
("verbose", "false"),
("overlord", "false"),
("show_datatypes", "false"),
+ ("show_skolems", "true"),
("show_consts", "false"),
("format", "1"),
("max_potential", "1"),
@@ -97,6 +98,7 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("hide_datatypes", "show_datatypes"),
+ ("hide_skolems", "show_skolems"),
("hide_consts", "show_consts"),
("trust_potential", "check_potential"),
("trust_genuine", "check_genuine")]
@@ -129,7 +131,8 @@
| [] => ["false"]
| _ => value)]
| NONE => if name = "show_all" then
- [("show_datatypes", value), ("show_consts", value)]
+ [("show_datatypes", value), ("show_skolems", value),
+ ("show_consts", value)]
else
[(name, value)]
@@ -263,6 +266,7 @@
val tac_timeout = lookup_time "tac_timeout"
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_skolems = debug orelse lookup_bool "show_skolems"
val show_consts = debug orelse lookup_bool "show_consts"
val evals = lookup_term_list_option_polymorphic "eval" |> these
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
@@ -291,9 +295,9 @@
datatype_sym_break = datatype_sym_break,
kodkod_sym_break = kodkod_sym_break, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
- show_datatypes = show_datatypes, show_consts = show_consts,
- evals = evals, formats = formats, atomss = atomss,
- max_potential = max_potential, max_genuine = max_genuine,
+ show_datatypes = show_datatypes, show_skolems = show_skolems,
+ show_consts = show_consts, evals = evals, formats = formats,
+ atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
check_potential = check_potential, check_genuine = check_genuine,
batch_size = batch_size, expect = expect}
end
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 17 14:43:53 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 17 22:07:17 2011 +0100
@@ -14,6 +14,7 @@
type params =
{show_datatypes: bool,
+ show_skolems: bool,
show_consts: bool}
type term_postprocessor =
@@ -58,6 +59,7 @@
type params =
{show_datatypes: bool,
+ show_skolems: bool,
show_consts: bool}
type term_postprocessor =
@@ -859,7 +861,7 @@
t1 = t2
end
-fun reconstruct_hol_model {show_datatypes, show_consts}
+fun reconstruct_hol_model {show_datatypes, show_skolems, 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, needs, tac_timeout,
@@ -991,7 +993,7 @@
||> append (map_filter (free_name_for_term false) pseudo_frees)
val real_free_names = map_filter (free_name_for_term true) real_frees
val chunks = block_of_names true "Free variable" real_free_names @
- block_of_names true "Skolem constant" skolem_names @
+ block_of_names show_skolems "Skolem constant" skolem_names @
block_of_names true "Evaluated term" eval_names @
block_of_datatypes @ block_of_codatatypes @
block_of_names show_consts "Constant"