# HG changeset patch
# User blanchet
# Date 1387473751 -3600
# Node ID 79745ba60a5a53f97a38d19026c14191a901bece
# Parent  037046aab457ab05be3d119703bed035591a9801
data structure rationalization

diff -r 037046aab457 -r 79745ba60a5a src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Dec 19 18:22:31 2013 +0100
@@ -93,7 +93,7 @@
 (* Precondition: The proof must be labeled canonically
    (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
 fun compress_proof isar_compress
-    ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface) proof =
+    ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface) proof =
   if isar_compress <= 1.0 then
     proof
   else
@@ -135,7 +135,7 @@
 
       fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
         if null subs orelse not (compress_further ()) then
-          (set_preplay_time l (false, time);
+          (set_preplay_result l (Preplay_Success (false, time));
            Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
         else
           (case subs of
@@ -145,7 +145,7 @@
               val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val (false, time') = get_preplay_time l'
+              val Preplay_Success (false, time') = get_preplay_result l'
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
@@ -174,9 +174,10 @@
           if subproofs = [] then
             step
           else
-            (case get_preplay_time l of
-              (true, _) => step (* timeout or fail *)
-            | (false, time) => elim_subproofs' time qs fix l t lfs gfs meth subproofs [])
+            (case get_preplay_result l of
+              Preplay_Success (false, time) =>
+              elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+            | _ => step)
 
       (** top_level compression: eliminate steps by merging them into their
           successors **)
@@ -210,9 +211,10 @@
           fun try_eliminate (i, l, _) succ_lbls steps =
             let
               (* only touch steps that can be preplayed successfully *)
-              val (false, time) = get_preplay_time l
+              val Preplay_Success (false, time) = get_preplay_result l
 
-              val succ_times = map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
+              val succ_times =
+                map (get_preplay_result #> (fn Preplay_Success (false, t) => t)) succ_lbls
               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
@@ -240,7 +242,7 @@
               val steps2 = update_steps steps2 succs'
             in
               decrement_step_count (); (* candidate successfully eliminated *)
-              map2 set_preplay_time succ_lbls preplay_times;
+              map2 (fn l => set_preplay_result l o Preplay_Success) succ_lbls preplay_times;
               map (replace_successor l succ_lbls) lfs;
               (* removing the step would mess up the indices -> replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2
diff -r 037046aab457 -r 79745ba60a5a src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Thu Dec 19 18:22:31 2013 +0100
@@ -25,11 +25,10 @@
 val slack = seconds 0.1
 
 fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
-  | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
+  | min_deps_of_step {get_preplay_result, set_preplay_result, preplay_quietly, ...}
       (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
-    (case get_preplay_time l of
-      (true, _) => step (* don't touch steps that time out or fail *)
-    | (false, time) =>
+    (case get_preplay_result l of
+      Preplay_Success (false, time) =>
       let
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
         val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
@@ -43,8 +42,9 @@
         val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
         val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
       in
-        set_preplay_time l (false, time); mk_step_lfs_gfs min_lfs min_gfs
-      end)
+        set_preplay_result l (Preplay_Success (false, time)); mk_step_lfs_gfs min_lfs min_gfs
+      end
+    | _ => step (* don't touch steps that time out or fail *))
 
 fun postprocess_remove_unreferenced_steps postproc_step =
   let
diff -r 037046aab457 -r 79745ba60a5a src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 18:22:31 2013 +0100
@@ -11,18 +11,16 @@
   type isar_step = Sledgehammer_Proof.isar_step
   type label = Sledgehammer_Proof.label
 
-  type preplay_result
+  datatype preplay_result =
+    Preplay_Success of bool * Time.time |
+    Preplay_Failure
 
   val trace: bool Config.T
-  val zero_preplay_time: bool * Time.time
-  val some_preplay_time: bool * Time.time
   val add_preplay_time: bool * Time.time -> bool * Time.time -> bool * Time.time
 
   type preplay_interface =
     {get_preplay_result: label -> preplay_result,
      set_preplay_result: label -> preplay_result -> unit,
-     get_preplay_time: label -> bool * Time.time,
-     set_preplay_time: label -> bool * Time.time -> unit,
      preplay_quietly: Time.time -> isar_step -> bool * Time.time,
      (* the returned flag signals a preplay failure *)
      overall_preplay_stats: isar_proof -> (bool * Time.time) * bool}
@@ -45,7 +43,6 @@
   Preplay_Failure
 
 val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
-val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
 
 fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+ (t1, t2))
 
@@ -166,8 +163,6 @@
 type preplay_interface =
   {get_preplay_result: label -> preplay_result,
    set_preplay_result: label -> preplay_result -> unit,
-   get_preplay_time: label -> bool * Time.time,
-   set_preplay_time: label -> bool * Time.time -> unit,
    preplay_quietly: Time.time -> isar_step -> bool * Time.time,
    (* the returned flag signals a preplay failure *)
    overall_preplay_stats: isar_proof -> (bool * Time.time) * bool}
@@ -201,8 +196,6 @@
     (* the dont_preplay option pretends that everything works just fine *)
     {get_preplay_result = K (Preplay_Success 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),
      overall_preplay_stats = K (zero_preplay_time, false)} : preplay_interface
   else
@@ -250,13 +243,6 @@
       fun set_preplay_result l result =
         preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
 
-      fun get_preplay_time l =
-        (case get_preplay_result l of
-          Preplay_Success preplay_time => preplay_time
-        | Preplay_Failure => some_preplay_time)
-
-      fun set_preplay_time l = set_preplay_result l o Preplay_Success
-
       val result_of_step =
         try (label_of_step #> the #> get_preplay_result)
         #> the_default (Preplay_Success zero_preplay_time)
@@ -271,8 +257,6 @@
     in
       {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,
        overall_preplay_stats = overall_preplay_stats}
     end
diff -r 037046aab457 -r 79745ba60a5a src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Thu Dec 19 18:22:31 2013 +0100
@@ -29,13 +29,13 @@
 
 fun try0_step _ _ (step as Let _) = step
   | try0_step preplay_timeout
-      ({preplay_quietly, get_preplay_time, set_preplay_time, ...} : preplay_interface)
+      ({preplay_quietly, get_preplay_result, set_preplay_result, ...} : preplay_interface)
       (step as Prove (_, _, l, _, _, _)) =
     let
       val timeout =
-        (case get_preplay_time l of
-          (true, _) => preplay_timeout
-        | (false, t) => Time.+ (t, slack))
+        (case get_preplay_result l of
+          Preplay_Success (false, t) => Time.+ (t, slack)
+        | _ => preplay_timeout)
 
       fun try_variant variant =
         (case preplay_quietly timeout variant of
@@ -43,7 +43,7 @@
         | time as (false, _) => SOME (variant, time))
     in
       (case Par_List.get_some try_variant (variants_of_step step) of
-        SOME (step, time) => (set_preplay_time l time; step)
+        SOME (step, time) => (set_preplay_result l (Preplay_Success time); step)
       | NONE => step)
     end