--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 11:30:53 2014 +0100
@@ -18,10 +18,12 @@
type isar_preplay_data
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
- val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome
+ val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
+ play_outcome
+ val preplay_isar_step : Proof.context -> Time.time -> isar_step ->
+ (proof_method * play_outcome) list
val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
- isar_preplay_data Unsynchronized.ref -> isar_step ->
- (proof_method * play_outcome Lazy.lazy) list -> unit
+ isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
play_outcome Lazy.lazy
@@ -120,7 +122,8 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step ctxt timeout meth (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
+fun raw_preplay_step_for_method ctxt timeout meth
+ (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
let
val goal =
(case xs of
@@ -156,8 +159,20 @@
play_outcome)
end
-fun preplay_isar_step ctxt timeout meth =
- try (raw_preplay_step ctxt timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt timeout meth =
+ try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
+
+fun preplay_isar_step ctxt timeout step =
+ let
+ fun try_method meth =
+ (case preplay_isar_step_for_method ctxt timeout meth step of
+ outcome as Played _ => SOME (meth, outcome)
+ | _ => NONE)
+
+ val meths = snd (byline_of_isar_step step)
+ in
+ the_list (Par_List.get_some try_method meths)
+ end
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
@@ -173,9 +188,11 @@
fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
(step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
let
- fun preplay meth = Lazy.lazy (fn () => preplay_isar_step ctxt timeout meth step)
- val meths_outcomes =
- fold (fn meth => AList.default (op =) (meth, preplay meth)) meths meths_outcomes0
+ fun lazy_preplay meth =
+ Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+ val meths_outcomes = meths_outcomes0
+ |> map (apsnd Lazy.value)
+ |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
in
preplay_data := Canonical_Label_Tab.map_default (l, [])
(fold (AList.update (op =)) meths_outcomes) (!preplay_data)