--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jul 12 19:03:08 2013 +0200
@@ -120,7 +120,7 @@
(* PRE CONDITION: the proof must be labeled canocially, see
Slegehammer_Proof.relabel_proof_canonically *)
fun compress_proof isar_compress isar_compress_degree merge_timeout_slack
- ({get_time, set_time, preplay_quietly, preplay_fail, ...} : preplay_interface)
+ ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface)
proof =
if isar_compress <= 1.0 then
proof
@@ -176,7 +176,7 @@
fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_time l (false, time);
+ (set_preplay_time l (false, time);
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs),
By_Metis (lfs, gfs)) )
else
@@ -189,7 +189,7 @@
By ((lfs', gfs'), MetisM))) = (try the_single) sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val (false, time') = get_time l'
+ val (false, time') = get_preplay_time l'
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -205,9 +205,8 @@
val (false, time'') = preplay_quietly timeout step''
in
- set_time l' zero_preplay_time; (* l' successfully eliminated! *)
+ decrement_step_count (); (* l' successfully eliminated! *)
map (replace_successor l' [l]) lfs';
- decrement_step_count ();
elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
end
handle Bind =>
@@ -219,8 +218,8 @@
| elim_subproofs
(step as Prove (qs, fix, l, t, subproofs, By ((lfs, gfs), MetisM))) =
if subproofs = [] then step else
- case get_time l of
- (true, _) => step (* timeout *)
+ case get_preplay_time l of
+ (true, _) => step (* timeout or fail *)
| (false, time) =>
elim_subproofs' time qs fix l t lfs gfs subproofs []
@@ -262,9 +261,10 @@
fun try_eliminate (cand as (i, l, _)) succ_lbls steps =
let
(* only touch steps that can be preplayed successfully *)
- val (false, time) = get_time l
+ val (false, time) = get_preplay_time l
- val succ_times = map (get_time #> (fn (false, t) => t)) succ_lbls
+ val succ_times =
+ map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
val timeslice =
time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
@@ -296,9 +296,8 @@
val steps2 = update_steps steps2 succs'
in
- set_time l zero_preplay_time; (* candidate successfully eliminated *)
- decrement_step_count ();
- map (uncurry set_time) (succ_lbls ~~ preplay_times);
+ decrement_step_count (); (* candidate successfully eliminated *)
+ map (uncurry set_preplay_time) (succ_lbls ~~ preplay_times);
map (replace_successor l succ_lbls) lfs;
(* removing the step would mess up the indices
-> replace with dummy step instead *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Jul 12 19:03:08 2013 +0200
@@ -24,11 +24,11 @@
val slack = 1.3
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
- | min_deps_of_step {get_time, set_time, preplay_quietly, set_preplay_fail, ...}
+ | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
- (case get_time l of
- (* don't touch steps that time out *)
- (true, _) => (set_preplay_fail true; step)
+ (case get_preplay_time l of
+ (* don't touch steps that time out or fail; minimizing won't help *)
+ (true, _) => step
| (false, time) =>
let
fun mk_step_lfs_gfs lfs gfs =
@@ -46,12 +46,11 @@
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
in
- set_time l (false, time);
+ set_preplay_time l (false, time);
mk_step_lfs_gfs min_lfs min_gfs
end)
-fun minimize_dependencies_and_remove_unrefed_steps (preplay_interface as
- {set_time, set_preplay_fail, ...} : preplay_interface) proof =
+fun minimize_dependencies_and_remove_unrefed_steps preplay_interface proof =
let
fun cons_to xs x = x :: xs
@@ -83,8 +82,7 @@
|>> Ord_List.union label_ord refed
||> cons_to accu
else
- (set_time l zero_preplay_time; (* remove unrefed step! *)
- (refed, accu))
+ (refed, accu)
and do_refed_step step =
min_deps_of_step preplay_interface step
@@ -104,7 +102,6 @@
end
in
- set_preplay_fail false; (* step(s) causing the failure may be removed *)
snd (do_proof proof)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 19:03:08 2013 +0200
@@ -12,20 +12,26 @@
type label = Sledgehammer_Proof.label
eqtype preplay_time
+
+ datatype preplay_result =
+ PplFail of exn |
+ PplSucc of preplay_time
+
val zero_preplay_time : preplay_time
val some_preplay_time : preplay_time
val add_preplay_time : preplay_time -> preplay_time -> preplay_time
val string_of_preplay_time : preplay_time -> string
- val preplay : bool -> bool -> string -> string -> Proof.context ->
- Time.time -> isar_step -> preplay_time
+ (*val preplay_raw : bool -> bool -> string -> string -> Proof.context ->
+ Time.time -> isar_step -> preplay_time*)
type preplay_interface =
- { get_time : label -> preplay_time,
- set_time : label -> preplay_time -> unit,
+ { get_preplay_result : label -> preplay_result,
+ set_preplay_result : label -> preplay_result -> unit,
+ get_preplay_time : label -> preplay_time,
+ set_preplay_time : label -> preplay_time -> unit,
preplay_quietly : Time.time -> isar_step -> preplay_time,
- preplay_fail : unit -> bool,
- set_preplay_fail : bool -> unit,
- overall_preplay_stats : unit -> preplay_time * bool }
+ (* the returned flag signals a preplay failure *)
+ overall_preplay_stats : isar_proof -> preplay_time * bool }
val proof_preplay_interface :
bool -> Proof.context -> string -> string -> bool -> Time.time -> bool
@@ -45,6 +51,10 @@
(t, true) = "> t ms" *)
type preplay_time = bool * Time.time
+datatype preplay_result =
+ PplFail of exn |
+ PplSucc of preplay_time
+
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *)
@@ -119,9 +129,9 @@
| _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
-(* main function for preplaying isar_steps *)
-fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time
- | preplay debug trace type_enc lam_trans ctxt timeout
+(* main function for preplaying isar_steps; may throw exceptions *)
+fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time
+ | preplay_raw debug trace type_enc lam_trans ctxt timeout
(Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
let
val (prop, obtain) =
@@ -167,12 +177,13 @@
(*** proof preplay interface ***)
type preplay_interface =
- { get_time : label -> preplay_time,
- set_time : label -> preplay_time -> unit,
- preplay_quietly : Time.time -> isar_step -> preplay_time,
- preplay_fail : unit -> bool,
- set_preplay_fail : bool -> unit,
- overall_preplay_stats : unit -> preplay_time * bool }
+{ get_preplay_result : label -> preplay_result,
+ set_preplay_result : label -> preplay_result -> unit,
+ get_preplay_time : label -> preplay_time,
+ set_preplay_time : label -> preplay_time -> unit,
+ preplay_quietly : Time.time -> isar_step -> preplay_time,
+ (* the returned flag signals a preplay failure *)
+ overall_preplay_stats : isar_proof -> preplay_time * bool }
(* enriches context with local proof facts *)
@@ -197,22 +208,25 @@
end
-(* Given a proof, produces an imperative preplay interface with a shared state.
- The preplay times are caluclated lazyly and cached to avoid repeated
+(* Given a proof, produces an imperative preplay interface with a shared table
+ mapping from labels to preplay results.
+ The preplay results are caluclated lazyly and cached to avoid repeated
calculation.
PRE CONDITION: the proof must be labeled canocially, see
Slegehammer_Proof.relabel_proof_canonically
*)
+
+
fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
preplay_timeout preplay_trace proof : preplay_interface =
if not do_preplay then
(* the dont_preplay option pretends that everything works just fine *)
- { get_time = K zero_preplay_time,
- set_time = K (K ()),
+ { get_preplay_result = K (PplSucc zero_preplay_time),
+ set_preplay_result = K (K ()),
+ get_preplay_time = K zero_preplay_time,
+ set_preplay_time = K (K ()),
preplay_quietly = K (K zero_preplay_time),
- preplay_fail = K false,
- set_preplay_fail = K (),
overall_preplay_stats = K (zero_preplay_time, false)}
else
let
@@ -220,20 +234,20 @@
(* add local proof facts to context *)
val ctxt = enrich_context proof ctxt
- val fail = Unsynchronized.ref false
- fun preplay_fail () = !fail
-
- fun set_preplay_fail b = fail := b
-
- val preplay = preplay debug preplay_trace type_enc lam_trans ctxt
+ fun preplay timeout step =
+ preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
+ |> PplSucc
+ handle exn =>
+ if Exn.is_interrupt exn orelse debug then reraise exn
+ else PplFail exn
- (* preplay steps without registering preplay_fails, treating exceptions
- like timeouts *)
+ (* preplay steps treating exceptions like timeouts *)
fun preplay_quietly timeout step =
- try (preplay timeout) step
- |> the_default (true, timeout)
+ case preplay timeout step of
+ PplSucc preplay_time => preplay_time
+ | PplFail _ => (true, timeout)
- val preplay_time_tab =
+ val preplay_tab =
let
fun add_step_to_tab step tab =
case label_of_step step of
@@ -250,34 +264,42 @@
|> Unsynchronized.ref
end
- fun register_preplay_fail lazy_time = Lazy.force lazy_time
- handle exn =>
- if Exn.is_interrupt exn orelse debug then reraise exn
- else (fail := true; some_preplay_time)
-
- fun get_time lbl =
- register_preplay_fail
- (Canonical_Lbl_Tab.lookup (!preplay_time_tab) lbl |> the)
+ fun get_preplay_result lbl =
+ Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
handle
Option.Option =>
raise Fail "Sledgehammer_Preplay: preplay time table"
- fun set_time lbl time =
- preplay_time_tab :=
- Canonical_Lbl_Tab.update (lbl, Lazy.value time) (!preplay_time_tab)
+ fun set_preplay_result lbl result =
+ preplay_tab :=
+ Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
+
+ fun get_preplay_time lbl =
+ case get_preplay_result lbl of
+ PplSucc preplay_time => preplay_time
+ | PplFail _ => some_preplay_time (* best approximation possible *)
+
+ fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
- fun total_preplay_time () =
- Canonical_Lbl_Tab.fold
- (snd #> register_preplay_fail #> add_preplay_time)
- (!preplay_time_tab) zero_preplay_time
+ fun overall_preplay_stats (Proof(_, _, steps)) =
+ let
+ fun result_of_step step =
+ try (label_of_step #> the #> get_preplay_result) step
+ |> the_default (PplSucc zero_preplay_time)
+ fun do_step step =
+ case result_of_step step of
+ PplSucc preplay_time => apfst (add_preplay_time preplay_time)
+ | PplFail _ => apsnd (K true)
+ in
+ fold_isar_steps do_step steps (zero_preplay_time, false)
+ end
- fun overall_preplay_stats () = (total_preplay_time (), preplay_fail ())
in
- { get_time = get_time,
- set_time = set_time,
+ { get_preplay_result = get_preplay_result,
+ set_preplay_result = set_preplay_result,
+ get_preplay_time = get_preplay_time,
+ set_preplay_time = set_preplay_time,
preplay_quietly = preplay_quietly,
- preplay_fail = preplay_fail,
- set_preplay_fail = set_preplay_fail,
overall_preplay_stats = overall_preplay_stats}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 19:03:08 2013 +0200
@@ -372,7 +372,7 @@
val (l, subst, next) =
(l, subst, next) |> fresh_label depth have_prefix
val sub = do_proofs subst depth sub
- val by = by |> do_byline subst depth
+ val by = by |> do_byline subst
in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
| do_steps subst depth next (step :: steps) =
step :: do_steps subst depth next steps
@@ -380,7 +380,7 @@
let val (assms, subst) = do_assms subst depth assms in
Proof (fix, assms, do_steps subst depth 1 steps)
end
- and do_byline subst depth byline =
+ and do_byline subst byline =
map_facts_of_byline (do_facts subst) byline
and do_proofs subst depth = map (do_proof subst (depth + 1))
in do_proof [] 0 end
@@ -588,7 +588,7 @@
|> relabel_proof_canonically
|> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
preplay_timeout preplay_trace)
- val isar_proof =
+ val ((preplay_time, preplay_fail), isar_proof) =
isar_proof
|> compress_proof
(if isar_proofs = SOME true then isar_compress else 1000.0)
@@ -596,11 +596,10 @@
merge_timeout_slack preplay_interface
|> try0 preplay_timeout preplay_interface
|> minimize_dependencies_and_remove_unrefed_steps preplay_interface
- |> clean_up_labels_in_proof
- val isar_text =
- string_of_proof ctxt type_enc lam_trans subgoal subgoal_count
- isar_proof
- val (preplay_time, preplay_fail) = overall_preplay_stats ()
+ |> `overall_preplay_stats
+ ||> clean_up_labels_in_proof
+ val isar_text = string_of_proof ctxt type_enc lam_trans subgoal
+ subgoal_count isar_proof
in
case isar_text of
"" =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 19:03:08 2013 +0200
@@ -35,15 +35,15 @@
end
fun try0_step _ _ (step as Let _) = step
- | try0_step preplay_timeout ({preplay_quietly, get_time, set_time,
- set_preplay_fail, ...} : preplay_interface)
+ | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
+ set_preplay_time, ...} : preplay_interface)
(step as Prove (_, _, l, _, _, _)) =
let
- val (preplay_fail, timeout) =
- case get_time l of
- (true, _) => (true, preplay_timeout)
- | (false, t) => (false, t)
+ val timeout =
+ case get_preplay_time l of
+ (true, _) => preplay_timeout
+ | (false, t) => t
fun try_variant variant =
case preplay_quietly timeout variant of
@@ -52,13 +52,11 @@
in
case Par_List.get_some try_variant (variants step) of
- SOME (step, time) => (set_time l time; step)
- | NONE => (if preplay_fail then set_preplay_fail true else (); step)
+ SOME (step, time) => (set_preplay_time l time; step)
+ | NONE => step
end
-fun try0 preplay_timeout
- (preplay_interface as {set_preplay_fail, ...} : preplay_interface) proof =
- (set_preplay_fail false; (* failure might be fixed *)
- map_isar_steps (try0_step preplay_timeout preplay_interface) proof)
+fun try0 preplay_timeout preplay_interface proof =
+ map_isar_steps (try0_step preplay_timeout preplay_interface) proof
end