# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 6c317e374614602212211d0f63d2e4f2e6a1cb31
# Parent  eceebcea3e001bcddd19e8b2e205cdb7eaa5cc49
refactored data structure (step 3)

diff -r eceebcea3e00 -r 6c317e374614 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -270,7 +270,7 @@
 
         val trace = Config.get ctxt trace
 
-        val isar_proof =
+        val canonical_isar_proof =
           refute_graph
           |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
           |> redirect_graph axioms tainted bot
@@ -279,9 +279,13 @@
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
 
+        val preplay_ctxt = ctxt
+          |> enrich_context_with_local_facts canonical_isar_proof
+          |> silence_reconstructors debug
+
         val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
-          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans preplay_timeout
-            isar_proof
+          preplay_data_of_isar_proof preplay_ctxt metis_type_enc metis_lam_trans preplay_timeout
+            canonical_isar_proof
 
         fun str_of_preplay_outcome outcome =
           if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
@@ -298,7 +302,7 @@
             ()
 
         val (play_outcome, isar_proof) =
-          isar_proof
+          canonical_isar_proof
           |> tap (trace_isar_proof "Original")
           |> compress_isar_proof compress_isar preplay_data
           |> tap (trace_isar_proof "Compressed")
@@ -351,7 +355,7 @@
   | Not_Played => false)
 
 fun proof_text ctxt debug isar_proofs isar_params num_chained
-               (one_line_params as (preplay, _, _, _, _, _)) =
+    (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
      isar_proof_text ctxt debug isar_proofs isar_params
diff -r eceebcea3e00 -r 6c317e374614 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- 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
@@ -21,8 +21,9 @@
      preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
-  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time ->
-    isar_proof -> isar_preplay_data
+  val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
+  val preplay_data_of_isar_proof : Proof.context -> string -> string -> Time.time -> isar_proof ->
+    isar_preplay_data
 end;
 
 structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
@@ -34,6 +35,24 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
 
+fun enrich_context_with_local_facts proof ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt
+
+    fun enrich_with_fact l t =
+      Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
+
+    val enrich_with_assms = fold (uncurry enrich_with_fact)
+
+    fun enrich_with_proof (Proof (_, assms, isar_steps)) =
+      enrich_with_assms assms #> fold enrich_with_step isar_steps
+    and enrich_with_step (Let _) = I
+      | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
+        enrich_with_fact l t #> fold enrich_with_proof subproofs
+  in
+    enrich_with_proof proof ctxt
+  end
+
 fun preplay_trace ctxt assmsp concl result =
   let
     val ctxt = ctxt |> Config.put show_markup true
@@ -95,7 +114,7 @@
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step debug type_enc lam_trans ctxt timeout meth
+fun raw_preplay_step type_enc lam_trans ctxt timeout meth
       (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
     let
       val goal =
@@ -121,10 +140,8 @@
         resolve_fact_names ctxt fact_names
         |>> append (map (thm_of_proof ctxt) subproofs)
 
-      val ctxt' = ctxt |> silence_reconstructors debug
-
       fun prove () =
-        Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
+        Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
           HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
         handle ERROR msg => error ("Preplay error: " ^ msg)
 
@@ -140,44 +157,22 @@
    preplay_step: Time.time -> proof_method -> isar_step -> play_outcome,
    overall_preplay_outcome: isar_proof -> play_outcome}
 
-fun enrich_context_with_local_facts proof ctxt =
-  let
-    val thy = Proof_Context.theory_of ctxt
-
-    fun enrich_with_fact l t =
-      Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
-
-    val enrich_with_assms = fold (uncurry enrich_with_fact)
-
-    fun enrich_with_proof (Proof (_, assms, isar_steps)) =
-      enrich_with_assms assms #> fold enrich_with_step isar_steps
-    and enrich_with_step (Let _) = I
-      | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
-        enrich_with_fact l t #> fold enrich_with_proof subproofs
-  in
-    enrich_with_proof proof ctxt
-  end
+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 (Play_Timed_Out t1) (Play_Timed_Out t2) =
-    Play_Timed_Out (Time.+ (t1, t2))
-  | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
-  | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
-  | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))
+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 =
+    Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
 
-(* 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.
-
-   Precondition: The proof must be labeled canonically; cf.
-   "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
-fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans preplay_timeout proof =
+(* 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 type_enc lam_trans preplay_timeout proof =
   let
-    val ctxt = enrich_context_with_local_facts proof ctxt
-
     fun preplay_step timeout meth =
-      try (raw_preplay_step debug type_enc lam_trans ctxt timeout meth)
+      try (raw_preplay_step type_enc lam_trans ctxt timeout meth)
       #> the_default Play_Failed
 
     val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty