--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
@@ -15,14 +15,15 @@
val trace : bool Config.T
- type isar_preplay_data =
- {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
- preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
- overall_preplay_outcome: isar_proof -> play_outcome}
+ 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_data_of_isar_proof : Proof.context -> Time.time -> isar_proof -> isar_preplay_data
+ val set_preplay_outcomes_of_isar_step : isar_preplay_data Unsynchronized.ref -> label ->
+ (proof_method * play_outcome Lazy.lazy) list -> unit
+ val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
+ play_outcome Lazy.lazy
+ val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome
end;
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
@@ -53,11 +54,11 @@
enrich_with_proof proof ctxt
end
-fun preplay_trace ctxt assmsp concl result =
+fun preplay_trace ctxt assmsp concl outcome =
let
val ctxt = ctxt |> Config.put show_markup true
val assms = op @ assmsp
- val time = Pretty.str ("[" ^ string_of_play_outcome result ^ "]")
+ val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
val concl = Syntax.pretty_term ctxt concl
in
@@ -153,60 +154,37 @@
end
fun preplay_isar_step ctxt timeout meth =
- try (raw_preplay_step ctxt timeout meth)
- #> the_default Play_Failed
+ try (raw_preplay_step ctxt timeout meth) #> the_default Play_Failed
-type isar_preplay_data =
- {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> unit,
- preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
- overall_preplay_outcome: isar_proof -> play_outcome}
+type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
fun time_of_play (Played time) = time
| time_of_play (Play_Timed_Out time) = time
-fun merge_preplay_outcomes Play_Failed _ = Play_Failed
- | merge_preplay_outcomes _ Play_Failed = Play_Failed
- | merge_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
- | merge_preplay_outcomes play1 play2 =
+fun add_preplay_outcomes Play_Failed _ = Play_Failed
+ | add_preplay_outcomes _ Play_Failed = Play_Failed
+ | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
+ | add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
-(* Given a (canonically labeled) proof, produces an imperative preplay interface with a shared table
- mapping from labels to preplay results. The preplay results are caluclated lazily and cached to
- avoid repeated calculation. *)
-fun preplay_data_of_isar_proof ctxt preplay_timeout proof =
- let
- val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
-
- fun set_preplay_outcomes l meths_outcomes =
- preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
- (!preplay_tab)
-
- fun preplay_outcome l meth =
- (case Canonical_Label_Tab.lookup (!preplay_tab) l of
- SOME meths_outcomes =>
- (case AList.lookup (op =) meths_outcomes meth of
- SOME outcome => outcome
- | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
- | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
+fun set_preplay_outcomes_of_isar_step preplay_data l meths_outcomes =
+ preplay_data := Canonical_Label_Tab.map_default (l, [])
+ (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
- fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
- Lazy.force (preplay_outcome l meth)
- | result_of_step _ = Played Time.zeroTime
-
- fun overall_preplay_outcome (Proof (_, _, steps)) =
- fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
+fun preplay_outcome_of_isar_step preplay_data l meth =
+ (case Canonical_Label_Tab.lookup preplay_data l of
+ SOME meths_outcomes =>
+ (case AList.lookup (op =) meths_outcomes meth of
+ SOME outcome => outcome
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
+ | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
- fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
- preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
- (meth, Lazy.lazy (fn () => preplay_isar_step ctxt preplay_timeout meth step))) meths)
- (!preplay_tab)
- | reset_preplay_outcomes _ = ()
+fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meth :: _))) =
+ Lazy.force (preplay_outcome_of_isar_step preplay_data l meth)
+ | forced_outcome_of_step _ _ = Played Time.zeroTime
- val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
- in
- {set_preplay_outcomes = set_preplay_outcomes,
- preplay_outcome = preplay_outcome,
- overall_preplay_outcome = overall_preplay_outcome}
- end
+fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
+ fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps
+ (Played Time.zeroTime)
end;