--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 13 15:04:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 10:28:04 2010 +0100
@@ -247,7 +247,7 @@
(if i <> 1 orelse n <> 1 then
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
else
- "goal")) [orig_t]))
+ "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
val assms_t = if assms orelse auto then
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Feb 13 15:04:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 10:28:04 2010 +0100
@@ -1724,10 +1724,11 @@
(tac ctxt (auto_tac (clasimpset_of ctxt))))
#> the #> Goal.finish ctxt) goal
-val max_cached_wfs = 100
-val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
-val cached_wf_props : (term * bool) list Unsynchronized.ref =
- Unsynchronized.ref []
+val max_cached_wfs = 50
+val cached_timeout =
+ Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
+val cached_wf_props =
+ Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
val termination_tacs = [Lexicographic_Order.lex_order_tac true,
ScnpReconstruct.sizechange_tac]
@@ -1758,19 +1759,20 @@
else
()
in
- if tac_timeout = (!cached_timeout) andalso
- length (!cached_wf_props) < max_cached_wfs then
+ if tac_timeout = Synchronized.value cached_timeout andalso
+ length (Synchronized.value cached_wf_props) < max_cached_wfs then
()
else
- (cached_wf_props := []; cached_timeout := tac_timeout);
- case AList.lookup (op =) (!cached_wf_props) prop of
+ (Synchronized.change cached_wf_props (K []);
+ Synchronized.change cached_timeout (K tac_timeout));
+ case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
SOME wf => wf
| NONE =>
let
val goal = prop |> cterm_of thy |> Goal.init
val wf = exists (terminates_by ctxt tac_timeout goal)
termination_tacs
- in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
+ in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
end)
handle List.Empty => false
| NO_TRIPLE () => false
@@ -1785,14 +1787,14 @@
SOME (SOME b) => b
| _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
case AList.lookup (op =) (!wf_cache) x of
- SOME (_, wf) => wf
- | NONE =>
- let
- val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
- in
- Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
- end
+ SOME (_, wf) => wf
+ | NONE =>
+ let
+ val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+ val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
+ in
+ Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
+ end
(* typ list -> typ -> typ -> term -> term *)
fun ap_curry [_] _ _ t = t