--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 01 19:57:58 2016 +0100
@@ -19,10 +19,10 @@
val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
- val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
- play_outcome
- val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
- (proof_method * play_outcome) list
+ val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method ->
+ isar_step -> play_outcome
+ val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list ->
+ 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) list -> unit
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
@@ -126,7 +126,8 @@
end
(* may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
+fun raw_preplay_step_for_method ctxt chained timeout meth
+ (Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
@@ -150,6 +151,7 @@
val assmsp =
resolve_fact_names ctxt facts
|>> append (map (thm_of_proof ctxt) subproofs)
+ |>> append chained
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
@@ -162,14 +164,14 @@
play_outcome
end
-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_for_method ctxt chained timeout meth =
+ try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed
val min_preplay_timeout = seconds 0.002
-fun preplay_isar_step ctxt timeout0 hopeless step =
+fun preplay_isar_step ctxt chained timeout0 hopeless step =
let
- fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt timeout meth step)
+ fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step)
fun get_time (_, Played time) = SOME time
| get_time _ = NONE
@@ -194,7 +196,7 @@
(step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
- Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+ 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