# HG changeset patch
# User blanchet
# Date 1379940823 -7200
# Node ID 44bc6ff8f350bf8f59faeb02be652ec42fef6480
# Parent  342e371395c66324ed9375b8a926809becca3c98
added "spy" option to Nitpick

diff -r 342e371395c6 -r 44bc6ff8f350 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Sep 23 14:53:43 2013 +0200
@@ -29,6 +29,7 @@
      debug: bool,
      verbose: bool,
      overlord: bool,
+     spy: bool,
      user_axioms: bool option,
      assms: bool,
      whacks: term list,
@@ -114,6 +115,7 @@
    debug: bool,
    verbose: bool,
    overlord: bool,
+   spy: bool,
    user_axioms: bool option,
    assms: bool,
    whacks: term list,
@@ -230,7 +232,7 @@
 *)
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
          boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
-         verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
+         verbose, overlord, spy, user_axioms, assms, whacks, merge_type_vars,
          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,
@@ -271,6 +273,7 @@
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
                    "goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
+    val _ = spying spy (fn () => "starting " ^ @{make_string} mode ^ " mode")
     val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
                      o Date.fromTimeLocal o Time.now)
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
@@ -1052,6 +1055,7 @@
     val _ = print_v (fn () =>
                 "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
                 ".")
+    val _ = spying spy (fn () => "outcome: " ^ outcome_code)
   in (outcome_code, !state_ref) end
 
 (* Give the inner timeout a chance. *)
diff -r 342e371395c6 -r 44bc6ff8f350 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 23 14:53:43 2013 +0200
@@ -71,6 +71,7 @@
    ("debug", "false"),
    ("verbose", "false"),
    ("overlord", "false"),
+   ("spy", "false"),
    ("show_datatypes", "false"),
    ("show_skolems", "true"),
    ("show_consts", "false"),
@@ -100,6 +101,7 @@
    ("no_debug", "debug"),
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
+   ("dont_spy", "spy"),
    ("hide_datatypes", "show_datatypes"),
    ("hide_skolems", "show_skolems"),
    ("hide_consts", "show_consts"),
@@ -142,7 +144,10 @@
 structure Data = Theory_Data
 (
   type T = raw_param list
-  val empty = map (apsnd single) default_default_params
+  val empty =
+    default_default_params
+    |> getenv "NITPICK_SPY" = "yes" ? AList.update (op =) ("spy", "true")
+    |> map (apsnd single)
   val extend = I
   fun merge data = AList.merge (op =) (K true) data
 )
@@ -253,6 +258,7 @@
     val debug = (mode <> Auto_Try andalso lookup_bool "debug")
     val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
+    val spy = lookup_bool "spy"
     val user_axioms = lookup_bool_option "user_axioms"
     val assms = lookup_bool "assms"
     val whacks = lookup_term_list_option_polymorphic "whack" |> these
@@ -287,24 +293,19 @@
       | NONE => if debug then 1 else 50
     val expect = lookup_string "expect"
   in
-    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
-     iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
-     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, whacks = whacks,
-     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,
-     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,
-     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}
+    {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns, iters_assigns = iters_assigns,
+     bitss = bitss, bisim_depths = bisim_depths, boxes = boxes, finitizes = finitizes,
+     monos = monos, stds = stds, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
+     falsify = falsify, debug = debug, verbose = verbose, overlord = overlord, spy = spy,
+     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, total_consts = total_consts, 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, 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
 
 fun default_params thy =
diff -r 342e371395c6 -r 44bc6ff8f350 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Sep 23 14:53:43 2013 +0200
@@ -53,6 +53,7 @@
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
   val string_of_time : Time.time -> string
+  val spying : bool -> (unit -> string) -> unit
   val nat_subscript : int -> string
   val flip_polarity : polarity -> polarity
   val prop_T : typ
@@ -95,6 +96,8 @@
 
 val nitpick_prefix = "Nitpick" ^ Long_Name.separator
 
+val timestamp = ATP_Util.timestamp
+
 fun curry3 f = fn x => fn y => fn z => f (x, y, z)
 
 fun pairf f g x = (f x, g x)
@@ -238,6 +241,15 @@
 val parse_time_option = Sledgehammer_Util.parse_time_option
 val string_of_time = ATP_Util.string_of_time
 
+val spying_version = "a"
+
+fun spying false _ = ()
+  | spying true f =
+    let val message = f () in
+      File.append (Path.explode "$ISABELLE_HOME_USER/spy_nitpick")
+        (spying_version ^ " " ^ timestamp () ^ ": " ^ message ^ "\n")
+    end
+
 val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
 fun nat_subscript n =
   n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
@@ -299,9 +311,12 @@
     if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
   end
 
-fun hashw_term (t1 $ t2) = ATP_Util.hashw (hashw_term t1, hashw_term t2)
-  | hashw_term (Const (s, _)) = ATP_Util.hashw_string (s, 0w0)
-  | hashw_term (Free (s, _)) = ATP_Util.hashw_string (s, 0w0)
+val hashw = ATP_Util.hashw
+val hashw_string = ATP_Util.hashw_string
+
+fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
+  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
+  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
   | hashw_term _ = 0w0
 
 val hash_term = Word.toInt o hashw_term