--- 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. *)
--- 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 =
--- 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