# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID 43473497fb65557cf6eba1466c4407b6329bbc6f
# Parent  4d63fffcde8d5daefc3a251eccdb498ca0f4cb0d
centralize preplaying

diff -r 4d63fffcde8d -r 43473497fb65 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -135,10 +135,8 @@
         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
 
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
-        val (_, ctxt) =
-          params
-          |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
-          |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
+        val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
+        val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
 
         val do_preplay = preplay_timeout <> Time.zeroTime
         val try0_isar = try0_isar andalso do_preplay
@@ -283,19 +281,14 @@
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
 
-        val preplay_ctxt = ctxt
+        val ctxt = ctxt
           |> enrich_context_with_local_facts canonical_isar_proof
           |> silence_reconstructors debug
 
         val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
 
-        fun init_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
-            set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth,
-                Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step)))
-              meths)
-          | init_preplay_outcomes _ = ()
-
-        val _ = fold_isar_steps (K o init_preplay_outcomes)
+        val _ = fold_isar_steps (fn meth =>
+            K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
           (steps_of_isar_proof canonical_isar_proof) ()
 
         fun str_of_preplay_outcome outcome =
@@ -316,12 +309,12 @@
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
-          |> compress_isar_proof preplay_ctxt compress_isar preplay_data
+          |> compress_isar_proof ctxt compress_isar preplay_data
           |> tap (trace_isar_proof "Compressed")
-          |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
+          |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
           |> tap (trace_isar_proof "Tried0")
           |> postprocess_isar_proof_remove_unreferenced_steps
-               (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
+               (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> chain_isar_proof
diff -r 4d63fffcde8d -r 43473497fb65 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -137,11 +137,16 @@
         end
 
       (* elimination of trivial, one-step subproofs *)
-      fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: meths') subs nontriv_subs =
+      fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
         if null subs orelse not (compress_further ()) then
-          (set_preplay_outcomes_of_isar_step preplay_data l ((meth, Lazy.value (Played time)) ::
-             map (rpair (Lazy.value Not_Played)(*FIXME*)) meths');
-           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
+          let
+            val subproofs = List.revAppend (nontriv_subs, subs)
+            val step = Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))
+          in
+            set_preplay_outcomes_of_isar_step ctxt time preplay_data step
+              [(meth, Lazy.value (Played time))];
+            step
+          end
         else
           (case subs of
             (sub as Proof (_, assms, sub_steps)) :: subs =>
@@ -166,11 +171,11 @@
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              elim_subproofs' time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
+              elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
             end
             handle Bind =>
-            elim_subproofs' time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
-          | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
+              elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
+          | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
 
       fun elim_subproofs (step as Let _) = step
         | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
@@ -179,7 +184,7 @@
             step
           else
             (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
-              Played time => elim_subproofs' time qs fix l t lfs gfs meths subproofs []
+              Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
             | _ => step)
 
       fun compress_top_level steps =
@@ -210,25 +215,22 @@
                |> fold_index add_cand) []
             end
 
-          fun try_eliminate (i, l, _) succ_lbls steps =
+          fun try_eliminate (i, l, _) labels steps =
             let
               val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
 
-              val succs = collect_successors steps' succ_lbls
-              val succ_methss = map (snd o the o byline_of_isar_step) succs
-              val succ_meths = map hd succ_methss (* FIXME *)
+              val succs = collect_successors steps' labels
+              val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
 
               (* only touch steps that can be preplayed successfully *)
               val Played time = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth)
 
               val succs' = map (try_merge cand #> the) succs
 
-              val succ_times =
-                map2 ((fn Played t => t) o Lazy.force oo
-                  preplay_outcome_of_isar_step (!preplay_data)) succ_lbls succ_meths
-              val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
-              val timeouts =
-                map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
+              val times0 = map2 ((fn Played time => time) o Lazy.force oo
+                preplay_outcome_of_isar_step (!preplay_data)) labels succ_meths
+              val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
+              val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
 
               (* FIXME: debugging *)
               val _ =
@@ -241,19 +243,20 @@
               val play_outcomes = map3 (preplay_isar_step ctxt) timeouts succ_meths succs'
 
               (* ensure none of the modified successors timed out *)
-              val true = forall (fn Played _ => true) play_outcomes
+              val times = map (fn Played time => time) play_outcomes
 
               val (steps1, _ :: steps2) = chop i steps
               (* replace successors with their modified versions *)
               val steps2 = update_steps steps2 succs'
 
               val succ_meths_outcomess =
-                map2 (fn meth :: meths => fn outcome => (meth, Lazy.value outcome) ::
-                  map (rpair (Lazy.value Not_Played)(*FIXME*)) meths) succ_methss play_outcomes
+                map2 (fn meth => fn outcome => [(meth, Lazy.value outcome)]) succ_meths
+                  play_outcomes
             in
               decrement_step_count (); (* candidate successfully eliminated *)
-              map2 (set_preplay_outcomes_of_isar_step preplay_data) succ_lbls succ_meths_outcomess;
-              map (replace_successor l succ_lbls) lfs;
+              map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
+                succs succ_meths_outcomess;
+              map (replace_successor l labels) lfs;
               (* removing the step would mess up the indices; replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2
             end
diff -r 4d63fffcde8d -r 43473497fb65 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -43,9 +43,12 @@
 
         val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs) time [] lfs
         val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+
+        val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
-        set_preplay_outcomes_of_isar_step preplay_data l [(meth, Lazy.value (Played time))];
-        mk_step_lfs_gfs min_lfs min_gfs
+        set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
+          [(meth, Lazy.value (Played time))];
+        step'
       end
     | _ => step (* don't touch steps that time out or fail *))
 
diff -r 4d63fffcde8d -r 43473497fb65 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -19,7 +19,8 @@
 
   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 set_preplay_outcomes_of_isar_step : isar_preplay_data Unsynchronized.ref -> label ->
+  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
   val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
     play_outcome Lazy.lazy
@@ -167,9 +168,17 @@
   | add_preplay_outcomes play1 play2 =
     Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
 
-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 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
+    in
+      preplay_data := Canonical_Label_Tab.map_default (l, [])
+        (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
+    end
+  | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
 
 fun preplay_outcome_of_isar_step preplay_data l meth =
   (case Canonical_Label_Tab.lookup preplay_data l of
diff -r 4d63fffcde8d -r 43473497fb65 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -45,8 +45,11 @@
       (* FIXME: create variant after success *)
       (case Par_List.get_some try_method meths of
         SOME (meth', outcome) =>
-        (set_preplay_outcomes_of_isar_step preplay_data l [(meth', Lazy.value outcome)];
-         step_with_method meth' step)
+        let val step' = step_with_method meth' step in
+          (set_preplay_outcomes_of_isar_step ctxt timeout preplay_data step'
+             [(meth', Lazy.value outcome)];
+           step')
+        end
       | NONE => step)
     end