# HG changeset patch
# User blanchet
# Date 1300396037 -3600
# Node ID bd6296de14327b3d77d0e0d4c3437b93f35a5555
# Parent  0e4716fa330a7f24a8d03c6af3b6774ceb3ae184
reintroduced "show_skolems" option -- useful when too many Skolems are displayed

diff -r 0e4716fa330a -r bd6296de1432 NEWS
--- 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.
 
diff -r 0e4716fa330a -r bd6296de1432 doc-src/Nitpick/nitpick.tex
--- 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.
diff -r 0e4716fa330a -r bd6296de1432 src/HOL/Tools/Nitpick/nitpick.ML
--- 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 =
diff -r 0e4716fa330a -r bd6296de1432 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- 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
diff -r 0e4716fa330a -r bd6296de1432 src/HOL/Tools/Nitpick/nitpick_model.ML
--- 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"