generalized preplaying infrastructure to store various results for various methods

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -277,11 +277,15 @@
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
 
-        val preplay_data as {string_of_preplay_outcome, overall_preplay_outcome, ...} =
+        val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
           preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
             preplay_timeout isar_proof
 
-        fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ string_of_preplay_outcome l
+        fun str_of_preplay_outcome outcome =
+          if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
+
+        fun str_of_meth l meth =
+          string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
         fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
 
         fun trace_isar_proof label proof =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -79,14 +79,15 @@
     | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
   end
 
-(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+(* Tries merging the first step into the second step.
+   FIXME: Arbitrarily picks the second step's method. *)
 fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
-      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
     let
       val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
       val gfs = union (op =) gfs1 gfs2
     in
-      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
     end
   | try_merge _ _ = NONE
 
@@ -136,57 +137,55 @@
 
       (** elimination of trivial, one-step subproofs **)
 
-      fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+      fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
         if null subs orelse not (compress_further ()) then
-          (set_preplay_outcome l (Played time);
-           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+          (set_preplay_outcome l meth (Played time);
+           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
         else
           (case subs of
             (sub as Proof (_, assms, sub_steps)) :: subs =>
             (let
-              (* trivial subproofs have exactly one Prove step *)
-              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+              (* trivial subproofs have exactly one "Prove" step *)
+              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
+                try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val Played time' = preplay_outcome l'
+              val Played time' = Lazy.force (preplay_outcome l' meth')
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
-              val lfs'' =
-                subtract (op =) (map fst assms) lfs'
-                |> union (op =) lfs
+              val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
               val gfs'' = union (op =) gfs' gfs
-              val by = ((lfs'', gfs''), meth)
+              val by = ((lfs'', gfs''), methss(*FIXME*))
               val step'' = Prove (qs, fix, l, t, subs'', by)
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
               val Played time'' = preplay_quietly timeout step''
-
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
+              elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
             end
             handle Bind =>
-              elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+            elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
 
       fun elim_subproofs (step as Let _) = step
-        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
+            ((lfs, gfs), methss as (meth :: _) :: _))) =
           if subproofs = [] then
             step
           else
-            (case preplay_outcome l of
-              Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+            (case Lazy.force (preplay_outcome l meth) of
+              Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
             | _ => step)
 
       (** top_level compression: eliminate steps by merging them into their successors **)
-
       fun compress_top_level steps =
         let
           (* (#successors, (size_of_term t, position)) *)
-          fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
+          fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
 
           val compression_ord =
             prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
@@ -207,32 +206,36 @@
                 | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
             in
               (steps
-              |> split_last |> fst (* keep last step *)
-              |> fold_index add_cand) []
+               |> split_last |> fst (* keep last step *)
+               |> fold_index add_cand) []
             end
 
           fun try_eliminate (i, l, _) succ_lbls steps =
             let
+              val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
+                drop i steps
+
+              val succs = collect_successors steps' succ_lbls
+              val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
+
               (* only touch steps that can be preplayed successfully *)
-              val Played time = preplay_outcome l
+              val Played time = Lazy.force (preplay_outcome l meth)
 
-              val succ_times = map (preplay_outcome #> (fn Played t => t)) succ_lbls
+              val succs' = map (try_merge cand #> the) succs
+
+              val succ_times =
+                map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) 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 ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
-
               (* FIXME: debugging *)
               val _ =
-                if the (label_of_step cand) <> l then
+                if the (label_of_isar_step cand) <> l then
                   raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
                 else
                   ()
 
-              val succs = collect_successors steps' succ_lbls
-              val succs' = map (try_merge cand #> the) succs
-
               (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
               val play_outcomes = map2 preplay_quietly timeouts succs'
 
@@ -244,7 +247,7 @@
               val steps2 = update_steps steps2 succs'
             in
               decrement_step_count (); (* candidate successfully eliminated *)
-              map2 set_preplay_outcome succ_lbls play_outcomes;
+              map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
               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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -27,11 +27,11 @@
 
 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
   | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
-    (case preplay_outcome l of
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
+    (case Lazy.force (preplay_outcome l meth) of
       Played time =>
       let
-        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
         val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
@@ -43,7 +43,7 @@
         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_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
+        set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
       end
     | _ => step (* don't touch steps that time out or fail *))
 
@@ -62,7 +62,7 @@
           fold_rev do_step steps (refed, [concl])
         end
     and do_step step (refed, accu) =
-      (case label_of_step step of
+      (case label_of_isar_step step of
         NONE => (refed, step :: accu)
       | SOME l =>
         if Ord_List.member label_ord refed l then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -8,6 +8,7 @@
 signature SLEDGEHAMMER_ISAR_PREPLAY =
 sig
   type play_outcome = Sledgehammer_Reconstructor.play_outcome
+  type proof_method = Sledgehammer_Isar_Proof.proof_method
   type isar_step = Sledgehammer_Isar_Proof.isar_step
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   type label = Sledgehammer_Isar_Proof.label
@@ -15,9 +16,8 @@
   val trace : bool Config.T
 
   type isar_preplay_data =
-    {preplay_outcome: label -> play_outcome,
-     set_preplay_outcome: label -> play_outcome -> unit,
-     string_of_preplay_outcome: label -> string,
+    {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
@@ -106,9 +106,8 @@
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
-  | preplay_raw debug type_enc lam_trans ctxt timeout
-      (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
+fun preplay_raw debug type_enc lam_trans ctxt timeout meth
+      (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
     let
       val goal =
         (case xs of
@@ -147,9 +146,8 @@
     end
 
 type isar_preplay_data =
-  {preplay_outcome: label -> play_outcome,
-   set_preplay_outcome: label -> play_outcome -> unit,
-   string_of_preplay_outcome: label -> string,
+  {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
    overall_preplay_outcome: isar_proof -> play_outcome}
 
@@ -188,17 +186,16 @@
 fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   if not do_preplay then
     (* the "dont_preplay" option pretends that everything works just fine *)
-    {preplay_outcome = K (Played Time.zeroTime),
-     set_preplay_outcome = K (K ()),
-     string_of_preplay_outcome = K "",
+    {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
+     set_preplay_outcome = K (K (K ())),
      preplay_quietly = K (K (Played Time.zeroTime)),
      overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
   else
     let
       val ctxt = enrich_context_with_local_facts proof ctxt
 
-      fun preplay quietly timeout step =
-        preplay_raw debug type_enc lam_trans ctxt timeout step
+      fun preplay quietly timeout meth step =
+        preplay_raw debug type_enc lam_trans ctxt timeout meth step
         handle exn =>
           if Exn.is_interrupt exn then
             reraise exn
@@ -210,43 +207,42 @@
              Play_Failed)
 
       (* preplay steps treating exceptions like timeouts *)
-      fun preplay_quietly timeout = preplay true timeout
+      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
+          preplay true timeout meth step
+        | preplay_quietly _ _ = Played Time.zeroTime
+
+      fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
+          Canonical_Label_Tab.update_new
+            (l, maps (map (fn meth =>
+               (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+        | add_step_to_tab _ = I
 
       val preplay_tab =
-        let
-          fun add_step_to_tab step tab =
-            (case label_of_step step of
-              NONE => tab
-            | SOME l =>
-              Canonical_Label_Tab.update_new
-                (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
-            handle Canonical_Label_Tab.DUP _ =>
-              raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
-        in
-          Canonical_Label_Tab.empty
-          |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
-          |> Unsynchronized.ref
-        end
+        Canonical_Label_Tab.empty
+        |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
+        |> Unsynchronized.ref
 
-      fun preplay_outcome l =
-        Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
-        handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
+      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_outcome l result =
-        preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
+      fun set_preplay_outcome l meth result =
+        preplay_tab := Canonical_Label_Tab.map_entry l
+          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
 
-      fun string_of_preplay_outcome l = @{make_string} (preplay_outcome l)
-
-      val result_of_step =
-        try (label_of_step #> the #> preplay_outcome)
-        #> the_default (Played Time.zeroTime)
+      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)
     in
       {preplay_outcome = preplay_outcome,
        set_preplay_outcome = set_preplay_outcome,
-       string_of_preplay_outcome = string_of_preplay_outcome,
        preplay_quietly = preplay_quietly,
        overall_preplay_outcome = overall_preplay_outcome}
     end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -34,8 +34,8 @@
 
   val steps_of_proof : isar_proof -> isar_step list
 
-  val label_of_step : isar_step -> label option
-  val byline_of_step : isar_step -> (facts * proof_method list list) option
+  val label_of_isar_step : isar_step -> label option
+  val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
 
   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
   val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -103,17 +103,17 @@
 
 fun steps_of_proof (Proof (_, _, steps)) = steps
 
-fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
-  | label_of_step _ = NONE
+fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
+  | label_of_isar_step _ = NONE
 
-fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
-  | subproofs_of_step _ = NONE
+fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+  | subproofs_of_isar_step _ = NONE
 
-fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
-  | byline_of_step _ = NONE
+fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
+  | byline_of_isar_step _ = NONE
 
 fun fold_isar_step f step =
-  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
+  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
 and fold_isar_steps f = fold (fold_isar_step f)
 
 fun map_isar_steps f =
@@ -143,15 +143,15 @@
   | chain_isar_step _ step = step
 and chain_isar_steps _ [] = []
   | chain_isar_steps (prev as SOME _) (i :: is) =
-    chain_isar_step prev i :: chain_isar_steps (label_of_step i) is
-  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_step i) is
+    chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
+  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
 and chain_isar_proof (Proof (fix, assms, steps)) =
   Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
 
 fun kill_useless_labels_in_isar_proof proof =
   let
     val used_ls =
-      fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+      fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
         (steps_of_proof proof) []
 
     fun kill_label l = if member (op =) used_ls l then l else no_label

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -31,10 +31,10 @@
 fun try0_step _ _ (step as Let _) = step
   | try0_step preplay_timeout
       ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
-      (step as Prove (_, _, l, _, _, _)) =
+      (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
     let
       val timeout =
-        (case preplay_outcome l of
+        (case Lazy.force (preplay_outcome l meth) of
           Played time => Time.+ (time, slack)
         | _ => preplay_timeout)
 
@@ -44,7 +44,8 @@
         | _ => NONE)
     in
       (case Par_List.get_some try_variant (variants_of_step step) of
-        SOME (step', result) => (set_preplay_outcome l result; step')
+        SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
+        (set_preplay_outcome l meth' result; step')
       | NONE => step)
     end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -8,6 +8,7 @@
 sig
   val sledgehammerN : string
   val log2 : real -> real
+  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val app_hd : ('a -> 'a) -> 'a list -> 'a list
   val n_fold_cartesian_product : 'a list list -> 'a list list
   val plural_s : int -> string
@@ -38,6 +39,8 @@
 val log10_2 = Math.log10 2.0
 fun log2 n = Math.log10 n / log10_2
 
+fun map3 xs = Ctr_Sugar_Util.map3 xs
+
 fun app_hd f (x :: xs) = f x :: xs
 
 fun cartesian_product [] _ = []