--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
@@ -688,13 +688,13 @@
and do_case outer (c, infs) =
Assume (label_of_clause c, prop_of_clause c) ::
map (do_inf outer) infs
- val (isar_proof, ext_time) =
+ val (isar_proof, (preplay_fail, ext_time)) =
ref_graph
|> redirect_graph axioms tainted
|> map (do_inf true)
|> append assms
|> (if not preplay andalso isar_shrink <= 1.0
- then pair (true, seconds 0.0) #> swap
+ then pair (false, (true, seconds 0.0)) #> swap
else shrink_proof debug ctxt type_enc lam_trans preplay
preplay_timeout (if isar_proofs then isar_shrink else 1000.0))
(* |>> reorder_proof_to_minimize_jumps (* ? *) *)
@@ -714,15 +714,23 @@
else
""
| _ =>
- "\n\nStructured proof" ^
- (if verbose then
- " (" ^ string_of_int num_steps ^ " metis step" ^ plural_s num_steps ^
- (if preplay then ", " ^ string_from_ext_time ext_time
- else "") ^ ")"
- else if preplay then
- " (" ^ string_from_ext_time ext_time ^ ")"
- else
- "") ^ ":\n" ^ Sendback.markup isar_text
+ let
+ val preplay_msg = if preplay_fail
+ then "(!) proof may fail - preplaying was unsuccessful"
+ else string_from_ext_time ext_time
+ in
+ "\n\nStructured proof"
+ ^ (if verbose then
+ " (" ^ string_of_int num_steps
+ ^ " metis step" ^ plural_s num_steps
+ |> preplay ? suffix (", " ^ preplay_msg)
+ |> suffix ")"
+ else if preplay then
+ " (" ^ preplay_msg ^ ")"
+ else
+ "")
+ ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
+ end
end
val isar_proof =
if debug then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
@@ -10,7 +10,7 @@
type isar_step = Sledgehammer_Proof.isar_step
val shrink_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time -> real
- -> isar_step list -> isar_step list * (bool * Time.time)
+ -> isar_step list -> isar_step list * (bool * (bool * Time.time))
end
structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
@@ -28,21 +28,6 @@
type key = label
val ord = label_ord)
-(* Timing *)
-fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val no_time = (false, seconds 0.0)
-fun take_time timeout tac arg =
- let val timing = Timing.start () in
- (TimeLimit.timeLimit timeout tac arg;
- Timing.result timing |> #cpu |> SOME)
- handle _ => NONE
- end
-fun sum_up_time timeout lazy_time_vector =
- Vector.foldl
- ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
- | (NONE, (_, ts)) => (true, Time.+(ts, timeout))) o apfst Lazy.force)
- no_time lazy_time_vector
-
(* clean vector interface *)
fun get i v = Vector.sub (v, i)
fun replace x i v = Vector.update (v, i, x)
@@ -58,10 +43,34 @@
fun pop_max tab = pop tab (the (Inttab.max_key tab))
fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
+(* Timing *)
+fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
+val no_time = (false, seconds 0.0)
+fun take_time timeout tac arg =
+ let val timing = Timing.start () in
+ (TimeLimit.timeLimit timeout tac arg;
+ Timing.result timing |> #cpu |> SOME)
+ handle TimeLimit.TimeOut => NONE
+ end
+
+
(* Main function for shrinking proofs *)
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
isar_shrink proof =
let
+ (* handle metis preplay fail *)
+ local
+ open Unsynchronized
+ val metis_fail = ref false
+ in
+ fun handle_metis_fail try_metis () =
+ try_metis () handle _ => (metis_fail := true ; SOME (seconds 0.0))
+ fun get_time lazy_time =
+ if !metis_fail then SOME (seconds 0.0) else Lazy.force lazy_time
+ val metis_fail = fn () => !metis_fail
+ end
+
+ (* Shrink top level proof - do not shrink case splits *)
fun shrink_top_level on_top_level ctxt proof =
let
(* proof vector *)
@@ -119,11 +128,21 @@
take_time timeout (fn () => goal tac)
end
(* FIXME: Add case_split preplaying *)
- | try_metis _ _ = (fn () => SOME (seconds 0.0) )
+ | try_metis _ _ = (fn () => SOME (seconds 0.0) )
+
+ val try_metis_quietly = the_default NONE oo try oo try_metis
- (* Lazy metis time vector = cache *)
+ (* cache metis preplay times in lazy time vector *)
val metis_time =
- Vector.map (Lazy.lazy o try_metis preplay_timeout o the) proof_vect
+ Vector.map
+ (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout o the)
+ proof_vect
+ fun sum_up_time lazy_time_vector =
+ Vector.foldl
+ ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
+ | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout)))
+ o apfst get_time)
+ no_time lazy_time_vector
(* Merging *)
fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1)))
@@ -132,6 +151,8 @@
val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end
+ | merge _ _ = error "Internal error: Tring to merge unmergable isar steps"
+
fun try_merge metis_time (s1, i) (s2, j) =
(case get i metis_time |> Lazy.force of
NONE => (NONE, metis_time)
@@ -143,7 +164,7 @@
val s12 = merge s1 s2
val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
in
- case try_metis timeout s12 () of
+ case try_metis_quietly timeout s12 () of
NONE => (NONE, metis_time)
| some_t12 =>
(SOME s12, metis_time
@@ -160,7 +181,7 @@
(Vector.foldr
(fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
[] proof_vect,
- sum_up_time preplay_timeout metis_time)
+ sum_up_time metis_time)
else
let
val (i, cand_tab) = pop_max cand_tab
@@ -213,8 +234,8 @@
and shrink_case_splits ctxt proof =
let
fun shrink_each_and_collect_time shrink candidates =
- let fun f_m cand time = shrink cand ||> ext_time_add time
- in fold_map f_m candidates no_time end
+ let fun f_m cand time = shrink cand ||> ext_time_add time
+ in fold_map f_m candidates no_time end
val shrink_case_split = shrink_each_and_collect_time (shrink_proof' false ctxt)
fun shrink (Prove (qs, lbl, t, Case_Split (cases, facts))) =
let val (cases, time) = shrink_case_split cases
@@ -225,6 +246,7 @@
end
in
shrink_proof' true ctxt proof
+ |> apsnd (pair (metis_fail () ) )
end
end