reset timing information after changes
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 5524366709d41601e
parent 55242 413ec965f95d
child 55244 12e1a5d8ee48
reset timing information after changes
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Feb 02 19:15:25 2014 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -20,15 +20,14 @@
     1.4  structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE =
     1.5  struct
     1.6  
     1.7 -(* Util *)
     1.8  fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
     1.9    | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
    1.10    | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
    1.11    | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
    1.12    | post_traverse_term_type' f env (Abs (x, T1, b)) s =
    1.13 -    let
    1.14 -      val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
    1.15 -    in f (Abs (x, T1, b')) (T1 --> T2) s' end
    1.16 +    let val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s in
    1.17 +      f (Abs (x, T1, b')) (T1 --> T2) s'
    1.18 +    end
    1.19    | post_traverse_term_type' f env (u $ v) s =
    1.20      let
    1.21        val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
    1.22 @@ -49,25 +48,13 @@
    1.23          end
    1.24    | _ => f T s
    1.25  
    1.26 -(** get unique elements of a list **)
    1.27 -local
    1.28 -  fun unique' b x [] = if b then [x] else []
    1.29 -    | unique' b x (y :: ys) =
    1.30 -      if x = y then unique' false x ys
    1.31 -      else unique' true y ys |> b ? cons x
    1.32 -in
    1.33 -  fun unique ord xs =
    1.34 -    case sort ord xs of x :: ys => unique' true x ys | [] => []
    1.35 -end
    1.36 -
    1.37 -(** Data structures, orders **)
    1.38  val indexname_ord = Term_Ord.fast_indexname_ord
    1.39  val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
    1.40 +
    1.41  structure Var_Set_Tab = Table(
    1.42    type key = indexname list
    1.43    val ord = list_ord indexname_ord)
    1.44  
    1.45 -(* (1) Generalize types *)
    1.46  fun generalize_types ctxt t =
    1.47    let
    1.48      val erase_types = map_types (fn _ => dummyT)
    1.49 @@ -78,7 +65,6 @@
    1.50       t |> erase_types |> infer_types
    1.51    end
    1.52  
    1.53 -(* (2) match types *)
    1.54  fun match_types ctxt t1 t2 =
    1.55    let
    1.56      val thy = Proof_Context.theory_of ctxt
    1.57 @@ -88,17 +74,14 @@
    1.58      handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types"
    1.59    end
    1.60  
    1.61 -
    1.62 -(* (3) handle trivial tfrees  *)
    1.63  fun handle_trivial_tfrees ctxt (t', subst) =
    1.64    let
    1.65 -    val add_tfree_names =
    1.66 -      snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
    1.67 +    val add_tfree_names = snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
    1.68  
    1.69      val trivial_tfree_names =
    1.70        Vartab.fold add_tfree_names subst []
    1.71        |> filter_out (Variable.is_declared ctxt)
    1.72 -      |> unique fast_string_ord
    1.73 +      |> distinct (op =)
    1.74      val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
    1.75  
    1.76      val trivial_tvar_names =
    1.77 @@ -128,30 +111,26 @@
    1.78      (t', subst)
    1.79    end
    1.80  
    1.81 -(* (4) Typing-spot table *)
    1.82 -local
    1.83  fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
    1.84    | key_of_atype _ = I
    1.85  fun key_of_type T = fold_atyps key_of_atype T []
    1.86 +
    1.87  fun update_tab t T (tab, pos) =
    1.88 -  (case key_of_type T of
    1.89 +  ((case key_of_type T of
    1.90       [] => tab
    1.91     | key =>
    1.92       let val cost = (size_of_typ T, (size_of_term t, pos)) in
    1.93 -       case Var_Set_Tab.lookup tab key of
    1.94 +       (case Var_Set_Tab.lookup tab key of
    1.95           NONE => Var_Set_Tab.update_new (key, cost) tab
    1.96         | SOME old_cost =>
    1.97           (case cost_ord (cost, old_cost) of
    1.98 -            LESS => Var_Set_Tab.update (key, cost) tab
    1.99 -          | _ => tab)
   1.100 -     end,
   1.101 +           LESS => Var_Set_Tab.update (key, cost) tab
   1.102 +         | _ => tab))
   1.103 +     end),
   1.104     pos + 1)
   1.105 -in
   1.106 -val typing_spot_table =
   1.107 -  post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
   1.108 -end
   1.109  
   1.110 -(* (5) Reverse-greedy *)
   1.111 +val typing_spot_table = post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
   1.112 +
   1.113  fun reverse_greedy typing_spot_tab =
   1.114    let
   1.115      fun update_count z =
   1.116 @@ -159,53 +138,53 @@
   1.117          let val c = Vartab.lookup tab tvar |> the_default 0 in
   1.118            Vartab.update (tvar, c + z) tab
   1.119          end)
   1.120 -    fun superfluous tcount =
   1.121 -      forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
   1.122 +    fun superfluous tcount = forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
   1.123      fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
   1.124        if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
   1.125        else (spot :: spots, tcount)
   1.126 +
   1.127      val (typing_spots, tvar_count_tab) =
   1.128 -      Var_Set_Tab.fold
   1.129 -        (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
   1.130 +      Var_Set_Tab.fold (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
   1.131          typing_spot_tab ([], Vartab.empty)
   1.132        |>> sort_distinct (rev_order o cost_ord o pairself snd)
   1.133 -  in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
   1.134 +  in
   1.135 +    fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst
   1.136 +  end
   1.137  
   1.138 -(* (6) Introduce annotations *)
   1.139  fun introduce_annotations subst spots t t' =
   1.140    let
   1.141      fun subst_atype (T as TVar (idxn, S)) subst =
   1.142          (Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst)
   1.143        | subst_atype T subst = (T, subst)
   1.144 +
   1.145      val subst_type = fold_map_atypes subst_atype
   1.146 +
   1.147      fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
   1.148          if p <> cp then
   1.149            (subst, cp + 1, ps, annots)
   1.150          else
   1.151            let val (T, subst) = subst_type T subst in
   1.152 -            (subst, cp + 1, ps', (p, T)::annots)
   1.153 +            (subst, cp + 1, ps', (p, T) :: annots)
   1.154            end
   1.155        | collect_annot _ _ x = x
   1.156 -    val (_, _, _, annots) =
   1.157 -      post_fold_term_type collect_annot (subst, 0, spots, []) t'
   1.158 +
   1.159 +    val (_, _, _, annots) = post_fold_term_type collect_annot (subst, 0, spots, []) t'
   1.160 +
   1.161      fun insert_annot t _ (cp, annots as (p, T) :: annots') =
   1.162          if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots'))
   1.163        | insert_annot t _ x = (t, x)
   1.164    in
   1.165 -    t |> post_traverse_term_type insert_annot (0, rev annots)
   1.166 -      |> fst
   1.167 +    t |> post_traverse_term_type insert_annot (0, rev annots) |> fst
   1.168    end
   1.169  
   1.170 -(* (7) Annotate *)
   1.171  fun annotate_types_in_term ctxt t =
   1.172    let
   1.173      val t' = generalize_types ctxt t
   1.174      val subst = match_types ctxt t' t
   1.175      val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
   1.176 -    val typing_spots =
   1.177 -      t' |> typing_spot_table
   1.178 -         |> reverse_greedy
   1.179 -         |> sort int_ord
   1.180 -  in introduce_annotations subst typing_spots t t' end
   1.181 +    val typing_spots = t' |> typing_spot_table |> reverse_greedy |> sort int_ord
   1.182 +  in
   1.183 +    introduce_annotations subst typing_spots t t'
   1.184 +  end
   1.185  
   1.186  end;
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 19:15:25 2014 +0000
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     2.3 @@ -135,8 +135,7 @@
     2.4            (get_successors, replace_successor)
     2.5          end
     2.6  
     2.7 -      (** elimination of trivial, one-step subproofs **)
     2.8 -
     2.9 +      (* elimination of trivial, one-step subproofs *)
    2.10        fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
    2.11          if null subs orelse not (compress_further ()) then
    2.12            (set_preplay_outcome l meth (Played time);
    2.13 @@ -249,7 +248,7 @@
    2.14                decrement_step_count (); (* candidate successfully eliminated *)
    2.15                map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
    2.16                map (replace_successor l succ_lbls) lfs;
    2.17 -              (* removing the step would mess up the indices -> replace with dummy step instead *)
    2.18 +              (* removing the step would mess up the indices; replace with dummy step instead *)
    2.19                steps1 @ dummy_isar_step :: steps2
    2.20              end
    2.21              handle Bind => steps
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 19:15:25 2014 +0000
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
     3.3 @@ -26,7 +26,8 @@
     3.4  val slack = seconds 0.1
     3.5  
     3.6  fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
     3.7 -  | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
     3.8 +  | minimize_isar_step_dependencies
     3.9 +      {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
    3.10        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
    3.11      (case Lazy.force (preplay_outcome l meth) of
    3.12        Played time =>
    3.13 @@ -42,8 +43,12 @@
    3.14  
    3.15          val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
    3.16          val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
    3.17 +
    3.18 +        val step' = mk_step_lfs_gfs min_lfs min_gfs
    3.19        in
    3.20 -        set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
    3.21 +        reset_preplay_outcomes step';
    3.22 +        set_preplay_outcome l meth (Played time);
    3.23 +        step'
    3.24        end
    3.25      | _ => step (* don't touch steps that time out or fail *))
    3.26  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 19:15:25 2014 +0000
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     4.3 @@ -16,8 +16,9 @@
     4.4    val trace : bool Config.T
     4.5  
     4.6    type isar_preplay_data =
     4.7 -    {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
     4.8 +    {reset_preplay_outcomes: isar_step -> unit,
     4.9       set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    4.10 +     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    4.11       preplay_quietly: Time.time -> isar_step -> play_outcome,
    4.12       overall_preplay_outcome: isar_proof -> play_outcome}
    4.13  
    4.14 @@ -146,8 +147,9 @@
    4.15      end
    4.16  
    4.17  type isar_preplay_data =
    4.18 -  {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    4.19 +  {reset_preplay_outcomes: isar_step -> unit,
    4.20     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    4.21 +   preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    4.22     preplay_quietly: Time.time -> isar_step -> play_outcome,
    4.23     overall_preplay_outcome: isar_proof -> play_outcome}
    4.24  
    4.25 @@ -186,8 +188,9 @@
    4.26  fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    4.27    if not do_preplay then
    4.28      (* the "dont_preplay" option pretends that everything works just fine *)
    4.29 -    {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
    4.30 +    {reset_preplay_outcomes = K (),
    4.31       set_preplay_outcome = K (K (K ())),
    4.32 +     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
    4.33       preplay_quietly = K (K (Played Time.zeroTime)),
    4.34       overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
    4.35    else
    4.36 @@ -211,16 +214,17 @@
    4.37            preplay true timeout meth step
    4.38          | preplay_quietly _ _ = Played Time.zeroTime
    4.39  
    4.40 -      fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
    4.41 -          Canonical_Label_Tab.update_new
    4.42 -            (l, maps (map (fn meth =>
    4.43 -               (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
    4.44 -        | add_step_to_tab _ = I
    4.45 +      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
    4.46  
    4.47 -      val preplay_tab =
    4.48 -        Canonical_Label_Tab.empty
    4.49 -        |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
    4.50 -        |> Unsynchronized.ref
    4.51 +      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
    4.52 +          preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
    4.53 +              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
    4.54 +            (!preplay_tab)
    4.55 +        | reset_preplay_outcomes _ = ()
    4.56 +
    4.57 +      fun set_preplay_outcome l meth result =
    4.58 +        preplay_tab := Canonical_Label_Tab.map_entry l
    4.59 +          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
    4.60  
    4.61        fun preplay_outcome l meth =
    4.62          (case Canonical_Label_Tab.lookup (!preplay_tab) l of
    4.63 @@ -230,9 +234,7 @@
    4.64            | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
    4.65          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
    4.66  
    4.67 -      fun set_preplay_outcome l meth result =
    4.68 -        preplay_tab := Canonical_Label_Tab.map_entry l
    4.69 -          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
    4.70 +      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
    4.71  
    4.72        fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
    4.73            Lazy.force (preplay_outcome l meth)
    4.74 @@ -241,8 +243,9 @@
    4.75        fun overall_preplay_outcome (Proof (_, _, steps)) =
    4.76          fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
    4.77      in
    4.78 -      {preplay_outcome = preplay_outcome,
    4.79 +      {reset_preplay_outcomes = reset_preplay_outcomes,
    4.80         set_preplay_outcome = set_preplay_outcome,
    4.81 +       preplay_outcome = preplay_outcome,
    4.82         preplay_quietly = preplay_quietly,
    4.83         overall_preplay_outcome = overall_preplay_outcome}
    4.84      end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 19:15:25 2014 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
     5.3 @@ -43,6 +43,7 @@
     5.4            result as Played _ => SOME (variant, result)
     5.5          | _ => NONE)
     5.6      in
     5.7 +      (* FIXME: create variant after success *)
     5.8        (case Par_List.get_some try_variant (variants_of_step step) of
     5.9          SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
    5.10          (set_preplay_outcome l meth' result; step')