# HG changeset patch
# User smolkas
# Date 1373648588 -7200
# Node ID 79a4e7f8d7586c88e4d19a71facb0843c64416aa
# Parent  b74bf6c0e5a10da691a713d81377aa5b386279f9
cleaner preplay interface

diff -r b74bf6c0e5a1 -r 79a4e7f8d758 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Jul 12 19:03:08 2013 +0200
@@ -120,7 +120,7 @@
 (* PRE CONDITION: the proof must be labeled canocially, see
    Slegehammer_Proof.relabel_proof_canonically *)
 fun compress_proof isar_compress isar_compress_degree merge_timeout_slack
-  ({get_time, set_time, preplay_quietly, preplay_fail, ...} : preplay_interface)
+  ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface)
   proof =
   if isar_compress <= 1.0 then
     proof
@@ -176,7 +176,7 @@
 
     fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
       if null subs orelse not (compress_further ()) then
-        (set_time l (false, time);
+        (set_preplay_time l (false, time);
          Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs),
                 By_Metis (lfs, gfs)) )
       else
@@ -189,7 +189,7 @@
                 By ((lfs', gfs'), MetisM))) = (try the_single) sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val (false, time') = get_time l'
+              val (false, time') = get_preplay_time l'
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
@@ -205,9 +205,8 @@
               val (false, time'') = preplay_quietly timeout step''
 
             in
-              set_time l' zero_preplay_time; (* l' successfully eliminated! *)
+              decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              decrement_step_count ();
               elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
             end
             handle Bind =>
@@ -219,8 +218,8 @@
       | elim_subproofs
         (step as Prove (qs, fix, l, t, subproofs, By ((lfs, gfs), MetisM))) =
           if subproofs = [] then step else
-            case get_time l of
-              (true, _) => step (* timeout *)
+            case get_preplay_time l of
+              (true, _) => step (* timeout or fail *)
             | (false, time) =>
                 elim_subproofs' time qs fix l t lfs gfs subproofs []
 
@@ -262,9 +261,10 @@
         fun try_eliminate (cand as (i, l, _)) succ_lbls steps =
           let
             (* only touch steps that can be preplayed successfully *)
-            val (false, time) = get_time l
+            val (false, time) = get_preplay_time l
 
-            val succ_times = map (get_time #> (fn (false, t) => t)) succ_lbls
+            val succ_times =
+              map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
 
             val timeslice =
               time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
@@ -296,9 +296,8 @@
             val steps2 = update_steps steps2 succs'
 
           in
-            set_time l zero_preplay_time; (* candidate successfully eliminated *)
-            decrement_step_count ();
-            map (uncurry set_time) (succ_lbls ~~ preplay_times);
+            decrement_step_count (); (* candidate successfully eliminated *)
+            map (uncurry set_preplay_time) (succ_lbls ~~ preplay_times);
             map (replace_successor l succ_lbls) lfs;
             (* removing the step would mess up the indices
                -> replace with dummy step instead *)
diff -r b74bf6c0e5a1 -r 79a4e7f8d758 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 19:03:08 2013 +0200
@@ -24,11 +24,11 @@
 val slack = 1.3
 
 fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
-  | min_deps_of_step {get_time, set_time, preplay_quietly, set_preplay_fail, ...}
+  | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
       (step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
-  (case get_time l of
-    (* don't touch steps that time out *)
-    (true, _) => (set_preplay_fail true; step)
+  (case get_preplay_time l of
+    (* don't touch steps that time out or fail; minimizing won't help *)
+    (true, _) => step
   | (false, time) =>
     let
       fun mk_step_lfs_gfs lfs gfs =
@@ -46,12 +46,11 @@
       val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
 
     in
-      set_time l (false, time);
+      set_preplay_time l (false, time);
       mk_step_lfs_gfs min_lfs min_gfs
     end)
 
-fun minimize_dependencies_and_remove_unrefed_steps (preplay_interface as
-  {set_time, set_preplay_fail, ...} : preplay_interface) proof =
+fun minimize_dependencies_and_remove_unrefed_steps preplay_interface proof =
   let
     fun cons_to xs x = x :: xs
 
@@ -83,8 +82,7 @@
             |>> Ord_List.union label_ord refed
             ||> cons_to accu
           else
-            (set_time l zero_preplay_time; (* remove unrefed step! *)
-             (refed, accu))
+            (refed, accu)
 
     and do_refed_step step =
       min_deps_of_step preplay_interface step
@@ -104,7 +102,6 @@
         end
 
   in
-    set_preplay_fail false; (* step(s) causing the failure may be removed *)
     snd (do_proof proof)
   end
 
diff -r b74bf6c0e5a1 -r 79a4e7f8d758 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 19:03:08 2013 +0200
@@ -12,20 +12,26 @@
   type label = Sledgehammer_Proof.label
 
   eqtype preplay_time
+
+  datatype preplay_result =
+    PplFail of exn |
+    PplSucc of preplay_time
+
   val zero_preplay_time : preplay_time
   val some_preplay_time : preplay_time
   val add_preplay_time : preplay_time -> preplay_time -> preplay_time
   val string_of_preplay_time : preplay_time -> string
-  val preplay : bool -> bool -> string -> string -> Proof.context ->
-    Time.time -> isar_step -> preplay_time
+  (*val preplay_raw : bool -> bool -> string -> string -> Proof.context ->
+    Time.time -> isar_step -> preplay_time*)
 
   type preplay_interface =
-  { get_time : label -> preplay_time,
-    set_time : label -> preplay_time -> unit,
+  { get_preplay_result : label -> preplay_result,
+    set_preplay_result : label -> preplay_result -> unit,
+    get_preplay_time : label -> preplay_time,
+    set_preplay_time : label -> preplay_time -> unit,
     preplay_quietly : Time.time -> isar_step -> preplay_time,
-    preplay_fail : unit -> bool,
-    set_preplay_fail : bool -> unit,
-    overall_preplay_stats : unit -> preplay_time * bool }
+    (* the returned flag signals a preplay failure *)
+    overall_preplay_stats : isar_proof -> preplay_time * bool }
 
   val proof_preplay_interface :
     bool -> Proof.context -> string -> string -> bool -> Time.time -> bool
@@ -45,6 +51,10 @@
       (t, true)  = "> t ms" *)
 type preplay_time = bool * Time.time
 
+datatype preplay_result =
+  PplFail of exn |
+  PplSucc of preplay_time
+
 val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
 val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
 
@@ -119,9 +129,9 @@
             | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
 
 
-(* main function for preplaying isar_steps *)
-fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time
-  | preplay debug trace type_enc lam_trans ctxt timeout
+(* main function for preplaying isar_steps; may throw exceptions *)
+fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time
+  | preplay_raw debug trace type_enc lam_trans ctxt timeout
       (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
   let
     val (prop, obtain) =
@@ -167,12 +177,13 @@
 (*** proof preplay interface ***)
 
 type preplay_interface =
-  { get_time : label -> preplay_time,
-    set_time : label -> preplay_time -> unit,
-    preplay_quietly : Time.time -> isar_step -> preplay_time,
-    preplay_fail : unit -> bool,
-    set_preplay_fail : bool -> unit,
-    overall_preplay_stats : unit -> preplay_time * bool }
+{ get_preplay_result : label -> preplay_result,
+  set_preplay_result : label -> preplay_result -> unit,
+  get_preplay_time : label -> preplay_time,
+  set_preplay_time : label -> preplay_time -> unit,
+  preplay_quietly : Time.time -> isar_step -> preplay_time,
+  (* the returned flag signals a preplay failure *)
+  overall_preplay_stats : isar_proof -> preplay_time * bool }
 
 
 (* enriches context with local proof facts *)
@@ -197,22 +208,25 @@
   end
 
 
-(* Given a proof, produces an imperative preplay interface with a shared state.
-   The preplay times are caluclated lazyly and cached to avoid repeated
+(* 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.
 
    PRE CONDITION: the proof must be labeled canocially, see
    Slegehammer_Proof.relabel_proof_canonically
 *)
+
+
 fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
       preplay_timeout preplay_trace proof : preplay_interface =
   if not do_preplay then
     (* the dont_preplay option pretends that everything works just fine *)
-    { get_time = K zero_preplay_time,
-      set_time = K (K ()),
+    { get_preplay_result = K (PplSucc zero_preplay_time),
+      set_preplay_result = K (K ()),
+      get_preplay_time = K zero_preplay_time,
+      set_preplay_time = K (K ()),
       preplay_quietly = K (K zero_preplay_time),
-      preplay_fail = K false,
-      set_preplay_fail = K (),
       overall_preplay_stats = K (zero_preplay_time, false)}
   else
     let
@@ -220,20 +234,20 @@
       (* add local proof facts to context *)
       val ctxt = enrich_context proof ctxt
 
-      val fail = Unsynchronized.ref false
-      fun preplay_fail () = !fail
-
-      fun set_preplay_fail b = fail := b
-
-      val preplay = preplay debug preplay_trace type_enc lam_trans ctxt
+      fun preplay timeout step =
+        preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
+        |> PplSucc
+        handle exn =>
+          if Exn.is_interrupt exn orelse debug then reraise exn
+          else PplFail exn
 
-      (* preplay steps without registering preplay_fails, treating exceptions
-         like timeouts *)
+      (* preplay steps treating exceptions like timeouts *)
       fun preplay_quietly timeout step =
-        try (preplay timeout) step
-        |> the_default (true, timeout)
+        case preplay timeout step of
+          PplSucc preplay_time => preplay_time
+        | PplFail _ => (true, timeout)
 
-      val preplay_time_tab =
+      val preplay_tab =
         let
           fun add_step_to_tab step tab =
             case label_of_step step of
@@ -250,34 +264,42 @@
           |> Unsynchronized.ref
         end
 
-      fun register_preplay_fail lazy_time = Lazy.force lazy_time
-        handle exn =>
-          if Exn.is_interrupt exn orelse debug then reraise exn
-          else (fail := true; some_preplay_time)
-
-      fun get_time lbl =
-        register_preplay_fail
-          (Canonical_Lbl_Tab.lookup (!preplay_time_tab) lbl |> the)
+      fun get_preplay_result lbl =
+        Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
         handle
           Option.Option =>
             raise Fail "Sledgehammer_Preplay: preplay time table"
 
-      fun set_time lbl time =
-        preplay_time_tab :=
-          Canonical_Lbl_Tab.update (lbl, Lazy.value time) (!preplay_time_tab)
+      fun set_preplay_result lbl result =
+        preplay_tab :=
+          Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
+
+      fun get_preplay_time lbl =
+        case get_preplay_result lbl of
+          PplSucc preplay_time => preplay_time
+        | PplFail _ => some_preplay_time (* best approximation possible *)
+
+      fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
 
-      fun total_preplay_time () =
-        Canonical_Lbl_Tab.fold
-          (snd #> register_preplay_fail #> add_preplay_time)
-          (!preplay_time_tab) zero_preplay_time
+      fun overall_preplay_stats (Proof(_, _, steps)) =
+        let
+          fun result_of_step step =
+            try (label_of_step #> the #> get_preplay_result) step
+            |> the_default (PplSucc zero_preplay_time)
+          fun do_step step =
+            case result_of_step step of
+              PplSucc preplay_time => apfst (add_preplay_time preplay_time)
+            | PplFail _ => apsnd (K true)
+        in
+          fold_isar_steps do_step steps (zero_preplay_time, false)
+        end
 
-      fun overall_preplay_stats () = (total_preplay_time (), preplay_fail ())
     in
-      { get_time = get_time,
-        set_time = set_time,
+      { get_preplay_result = get_preplay_result,
+        set_preplay_result = set_preplay_result,
+        get_preplay_time = get_preplay_time,
+        set_preplay_time = set_preplay_time,
         preplay_quietly = preplay_quietly,
-        preplay_fail = preplay_fail,
-        set_preplay_fail = set_preplay_fail,
         overall_preplay_stats = overall_preplay_stats}
     end
 
diff -r b74bf6c0e5a1 -r 79a4e7f8d758 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 19:03:08 2013 +0200
@@ -372,7 +372,7 @@
           val (l, subst, next) =
             (l, subst, next) |> fresh_label depth have_prefix
           val sub = do_proofs subst depth sub
-          val by = by |> do_byline subst depth
+          val by = by |> do_byline subst
         in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
       | do_steps subst depth next (step :: steps) =
         step :: do_steps subst depth next steps
@@ -380,7 +380,7 @@
       let val (assms, subst) = do_assms subst depth assms in
         Proof (fix, assms, do_steps subst depth 1 steps)
       end
-    and do_byline subst depth byline =
+    and do_byline subst byline =
       map_facts_of_byline (do_facts subst) byline
     and do_proofs subst depth = map (do_proof subst (depth + 1))
   in do_proof [] 0 end
@@ -588,7 +588,7 @@
           |> relabel_proof_canonically
           |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
                preplay_timeout preplay_trace)
-        val isar_proof =
+        val ((preplay_time, preplay_fail), isar_proof) =
           isar_proof
           |> compress_proof
                (if isar_proofs = SOME true then isar_compress else 1000.0)
@@ -596,11 +596,10 @@
                merge_timeout_slack preplay_interface
           |> try0 preplay_timeout preplay_interface
           |> minimize_dependencies_and_remove_unrefed_steps preplay_interface
-          |> clean_up_labels_in_proof
-        val isar_text =
-          string_of_proof ctxt type_enc lam_trans subgoal subgoal_count
-                          isar_proof
-        val (preplay_time, preplay_fail) = overall_preplay_stats ()
+          |> `overall_preplay_stats
+          ||> clean_up_labels_in_proof
+        val isar_text = string_of_proof ctxt type_enc lam_trans subgoal
+          subgoal_count isar_proof
       in
         case isar_text of
           "" =>
diff -r b74bf6c0e5a1 -r 79a4e7f8d758 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 18:16:50 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 19:03:08 2013 +0200
@@ -35,15 +35,15 @@
       end
 
 fun try0_step _ _ (step as Let _) = step
-  | try0_step preplay_timeout ({preplay_quietly, get_time, set_time,
-    set_preplay_fail, ...} : preplay_interface)
+  | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
+    set_preplay_time, ...} : preplay_interface)
     (step as Prove (_, _, l, _, _, _)) =
       let
 
-        val (preplay_fail, timeout) =
-          case get_time l of
-            (true, _) => (true, preplay_timeout)
-          | (false, t) => (false, t)
+        val timeout =
+          case get_preplay_time l of
+            (true, _) => preplay_timeout
+          | (false, t) => t
 
         fun try_variant variant =
            case preplay_quietly timeout variant of
@@ -52,13 +52,11 @@
 
       in
         case Par_List.get_some try_variant (variants step) of
-          SOME (step, time) => (set_time l time; step)
-        | NONE => (if preplay_fail then set_preplay_fail true else (); step)
+          SOME (step, time) => (set_preplay_time l time; step)
+        | NONE => step
       end
 
-fun try0 preplay_timeout
-  (preplay_interface as {set_preplay_fail, ...} : preplay_interface) proof =
-    (set_preplay_fail false; (* failure might be fixed *)
-     map_isar_steps (try0_step preplay_timeout preplay_interface) proof)
+fun try0 preplay_timeout preplay_interface proof =
+     map_isar_steps (try0_step preplay_timeout preplay_interface) proof
 
 end