# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 66709d41601e52d1101ea0c36ffc930b3d07b7ee
# Parent  413ec965f95dd95aec954589afcfddd426f8de93
reset timing information after changes

diff -r 413ec965f95d -r 66709d41601e src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -20,15 +20,14 @@
 structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE =
 struct
 
-(* Util *)
 fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
   | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
   | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
   | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
   | post_traverse_term_type' f env (Abs (x, T1, b)) s =
-    let
-      val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
-    in f (Abs (x, T1, b')) (T1 --> T2) s' end
+    let val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s in
+      f (Abs (x, T1, b')) (T1 --> T2) s'
+    end
   | post_traverse_term_type' f env (u $ v) s =
     let
       val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
@@ -49,25 +48,13 @@
         end
   | _ => f T s
 
-(** get unique elements of a list **)
-local
-  fun unique' b x [] = if b then [x] else []
-    | unique' b x (y :: ys) =
-      if x = y then unique' false x ys
-      else unique' true y ys |> b ? cons x
-in
-  fun unique ord xs =
-    case sort ord xs of x :: ys => unique' true x ys | [] => []
-end
-
-(** Data structures, orders **)
 val indexname_ord = Term_Ord.fast_indexname_ord
 val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
+
 structure Var_Set_Tab = Table(
   type key = indexname list
   val ord = list_ord indexname_ord)
 
-(* (1) Generalize types *)
 fun generalize_types ctxt t =
   let
     val erase_types = map_types (fn _ => dummyT)
@@ -78,7 +65,6 @@
      t |> erase_types |> infer_types
   end
 
-(* (2) match types *)
 fun match_types ctxt t1 t2 =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -88,17 +74,14 @@
     handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types"
   end
 
-
-(* (3) handle trivial tfrees  *)
 fun handle_trivial_tfrees ctxt (t', subst) =
   let
-    val add_tfree_names =
-      snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
+    val add_tfree_names = snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
 
     val trivial_tfree_names =
       Vartab.fold add_tfree_names subst []
       |> filter_out (Variable.is_declared ctxt)
-      |> unique fast_string_ord
+      |> distinct (op =)
     val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
 
     val trivial_tvar_names =
@@ -128,30 +111,26 @@
     (t', subst)
   end
 
-(* (4) Typing-spot table *)
-local
 fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
   | key_of_atype _ = I
 fun key_of_type T = fold_atyps key_of_atype T []
+
 fun update_tab t T (tab, pos) =
-  (case key_of_type T of
+  ((case key_of_type T of
      [] => tab
    | key =>
      let val cost = (size_of_typ T, (size_of_term t, pos)) in
-       case Var_Set_Tab.lookup tab key of
+       (case Var_Set_Tab.lookup tab key of
          NONE => Var_Set_Tab.update_new (key, cost) tab
        | SOME old_cost =>
          (case cost_ord (cost, old_cost) of
-            LESS => Var_Set_Tab.update (key, cost) tab
-          | _ => tab)
-     end,
+           LESS => Var_Set_Tab.update (key, cost) tab
+         | _ => tab))
+     end),
    pos + 1)
-in
-val typing_spot_table =
-  post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
-end
 
-(* (5) Reverse-greedy *)
+val typing_spot_table = post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
+
 fun reverse_greedy typing_spot_tab =
   let
     fun update_count z =
@@ -159,53 +138,53 @@
         let val c = Vartab.lookup tab tvar |> the_default 0 in
           Vartab.update (tvar, c + z) tab
         end)
-    fun superfluous tcount =
-      forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
+    fun superfluous tcount = forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
     fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
       if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
       else (spot :: spots, tcount)
+
     val (typing_spots, tvar_count_tab) =
-      Var_Set_Tab.fold
-        (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
+      Var_Set_Tab.fold (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
         typing_spot_tab ([], Vartab.empty)
       |>> sort_distinct (rev_order o cost_ord o pairself snd)
-  in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
+  in
+    fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst
+  end
 
-(* (6) Introduce annotations *)
 fun introduce_annotations subst spots t t' =
   let
     fun subst_atype (T as TVar (idxn, S)) subst =
         (Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst)
       | subst_atype T subst = (T, subst)
+
     val subst_type = fold_map_atypes subst_atype
+
     fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
         if p <> cp then
           (subst, cp + 1, ps, annots)
         else
           let val (T, subst) = subst_type T subst in
-            (subst, cp + 1, ps', (p, T)::annots)
+            (subst, cp + 1, ps', (p, T) :: annots)
           end
       | collect_annot _ _ x = x
-    val (_, _, _, annots) =
-      post_fold_term_type collect_annot (subst, 0, spots, []) t'
+
+    val (_, _, _, annots) = post_fold_term_type collect_annot (subst, 0, spots, []) t'
+
     fun insert_annot t _ (cp, annots as (p, T) :: annots') =
         if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots'))
       | insert_annot t _ x = (t, x)
   in
-    t |> post_traverse_term_type insert_annot (0, rev annots)
-      |> fst
+    t |> post_traverse_term_type insert_annot (0, rev annots) |> fst
   end
 
-(* (7) Annotate *)
 fun annotate_types_in_term ctxt t =
   let
     val t' = generalize_types ctxt t
     val subst = match_types ctxt t' t
     val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
-    val typing_spots =
-      t' |> typing_spot_table
-         |> reverse_greedy
-         |> sort int_ord
-  in introduce_annotations subst typing_spots t t' end
+    val typing_spots = t' |> typing_spot_table |> reverse_greedy |> sort int_ord
+  in
+    introduce_annotations subst typing_spots t t'
+  end
 
 end;
diff -r 413ec965f95d -r 66709d41601e src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -135,8 +135,7 @@
           (get_successors, replace_successor)
         end
 
-      (** elimination of trivial, one-step subproofs **)
-
+      (* elimination of trivial, one-step subproofs *)
       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 meth (Played time);
@@ -249,7 +248,7 @@
               decrement_step_count (); (* candidate successfully eliminated *)
               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 *)
+              (* removing the step would mess up the indices; replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2
             end
             handle Bind => steps
diff -r 413ec965f95d -r 66709d41601e src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -26,7 +26,8 @@
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
-  | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+  | minimize_isar_step_dependencies
+      {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
       (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
     (case Lazy.force (preplay_outcome l meth) of
       Played time =>
@@ -42,8 +43,12 @@
 
         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
+
+        val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
-        set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
+        reset_preplay_outcomes step';
+        set_preplay_outcome l meth (Played time);
+        step'
       end
     | _ => step (* don't touch steps that time out or fail *))
 
diff -r 413ec965f95d -r 66709d41601e src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -16,8 +16,9 @@
   val trace : bool Config.T
 
   type isar_preplay_data =
-    {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+    {reset_preplay_outcomes: isar_step -> unit,
      set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
@@ -146,8 +147,9 @@
     end
 
 type isar_preplay_data =
-  {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+  {reset_preplay_outcomes: isar_step -> unit,
    set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+   preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
    overall_preplay_outcome: isar_proof -> play_outcome}
 
@@ -186,8 +188,9 @@
 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 (K (Lazy.value (Played Time.zeroTime))),
+    {reset_preplay_outcomes = K (),
      set_preplay_outcome = K (K (K ())),
+     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
      preplay_quietly = K (K (Played Time.zeroTime)),
      overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
   else
@@ -211,16 +214,17 @@
           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 = Unsynchronized.ref Canonical_Label_Tab.empty
 
-      val preplay_tab =
-        Canonical_Label_Tab.empty
-        |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
-        |> Unsynchronized.ref
+      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
+          preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
+              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+            (!preplay_tab)
+        | reset_preplay_outcomes _ = ()
+
+      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 preplay_outcome l meth =
         (case Canonical_Label_Tab.lookup (!preplay_tab) l of
@@ -230,9 +234,7 @@
           | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
         | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
 
-      fun set_preplay_outcome l meth result =
-        preplay_tab := Canonical_Label_Tab.map_entry l
-          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
+      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
 
       fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
           Lazy.force (preplay_outcome l meth)
@@ -241,8 +243,9 @@
       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,
+      {reset_preplay_outcomes = reset_preplay_outcomes,
        set_preplay_outcome = set_preplay_outcome,
+       preplay_outcome = preplay_outcome,
        preplay_quietly = preplay_quietly,
        overall_preplay_outcome = overall_preplay_outcome}
     end
diff -r 413ec965f95d -r 66709d41601e src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -43,6 +43,7 @@
           result as Played _ => SOME (variant, result)
         | _ => NONE)
     in
+      (* FIXME: create variant after success *)
       (case Par_List.get_some try_variant (variants_of_step step) of
         SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
         (set_preplay_outcome l meth' result; step')