1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Jul 12 18:16:50 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Jul 12 19:03:08 2013 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4  (* PRE CONDITION: the proof must be labeled canocially, see
     1.5     Slegehammer_Proof.relabel_proof_canonically *)
     1.6  fun compress_proof isar_compress isar_compress_degree merge_timeout_slack
     1.7 -  ({get_time, set_time, preplay_quietly, preplay_fail, ...} : preplay_interface)
     1.8 +  ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface)
     1.9    proof =
    1.10    if isar_compress <= 1.0 then
    1.11      proof
    1.12 @@ -176,7 +176,7 @@
    1.13  
    1.14      fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
    1.15        if null subs orelse not (compress_further ()) then
    1.16 -        (set_time l (false, time);
    1.17 +        (set_preplay_time l (false, time);
    1.18           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs),
    1.19                  By_Metis (lfs, gfs)) )
    1.20        else
    1.21 @@ -189,7 +189,7 @@
    1.22                  By ((lfs', gfs'), MetisM))) = (try the_single) sub_steps
    1.23  
    1.24                (* only touch proofs that can be preplayed sucessfully *)
    1.25 -              val (false, time') = get_time l'
    1.26 +              val (false, time') = get_preplay_time l'
    1.27  
    1.28                (* merge steps *)
    1.29                val subs'' = subs @ nontriv_subs
    1.30 @@ -205,9 +205,8 @@
    1.31                val (false, time'') = preplay_quietly timeout step''
    1.32  
    1.33              in
    1.34 -              set_time l' zero_preplay_time; (* l' successfully eliminated! *)
    1.35 +              decrement_step_count (); (* l' successfully eliminated! *)
    1.36                map (replace_successor l' [l]) lfs';
    1.37 -              decrement_step_count ();
    1.38                elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
    1.39              end
    1.40              handle Bind =>
    1.41 @@ -219,8 +218,8 @@
    1.42        | elim_subproofs
    1.43          (step as Prove (qs, fix, l, t, subproofs, By ((lfs, gfs), MetisM))) =
    1.44            if subproofs = [] then step else
    1.45 -            case get_time l of
    1.46 -              (true, _) => step (* timeout *)
    1.47 +            case get_preplay_time l of
    1.48 +              (true, _) => step (* timeout or fail *)
    1.49              | (false, time) =>
    1.50                  elim_subproofs' time qs fix l t lfs gfs subproofs []
    1.51  
    1.52 @@ -262,9 +261,10 @@
    1.53          fun try_eliminate (cand as (i, l, _)) succ_lbls steps =
    1.54            let
    1.55              (* only touch steps that can be preplayed successfully *)
    1.56 -            val (false, time) = get_time l
    1.57 +            val (false, time) = get_preplay_time l
    1.58  
    1.59 -            val succ_times = map (get_time #> (fn (false, t) => t)) succ_lbls
    1.60 +            val succ_times =
    1.61 +              map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
    1.62  
    1.63              val timeslice =
    1.64                time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
    1.65 @@ -296,9 +296,8 @@
    1.66              val steps2 = update_steps steps2 succs'
    1.67  
    1.68            in
    1.69 -            set_time l zero_preplay_time; (* candidate successfully eliminated *)
    1.70 -            decrement_step_count ();
    1.71 -            map (uncurry set_time) (succ_lbls ~~ preplay_times);
    1.72 +            decrement_step_count (); (* candidate successfully eliminated *)
    1.73 +            map (uncurry set_preplay_time) (succ_lbls ~~ preplay_times);
    1.74              map (replace_successor l succ_lbls) lfs;
    1.75              (* removing the step would mess up the indices
    1.76                 -> replace with dummy step instead *)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 18:16:50 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 19:03:08 2013 +0200
     2.3 @@ -24,11 +24,11 @@
     2.4  val slack = 1.3
     2.5  
     2.6  fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
     2.7 -  | min_deps_of_step {get_time, set_time, preplay_quietly, set_preplay_fail, ...}
     2.8 +  | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
     2.9        (step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
    2.10 -  (case get_time l of
    2.11 -    (* don't touch steps that time out *)
    2.12 -    (true, _) => (set_preplay_fail true; step)
    2.13 +  (case get_preplay_time l of
    2.14 +    (* don't touch steps that time out or fail; minimizing won't help *)
    2.15 +    (true, _) => step
    2.16    | (false, time) =>
    2.17      let
    2.18        fun mk_step_lfs_gfs lfs gfs =
    2.19 @@ -46,12 +46,11 @@
    2.20        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
    2.21  
    2.22      in
    2.23 -      set_time l (false, time);
    2.24 +      set_preplay_time l (false, time);
    2.25        mk_step_lfs_gfs min_lfs min_gfs
    2.26      end)
    2.27  
    2.28 -fun minimize_dependencies_and_remove_unrefed_steps (preplay_interface as
    2.29 -  {set_time, set_preplay_fail, ...} : preplay_interface) proof =
    2.30 +fun minimize_dependencies_and_remove_unrefed_steps preplay_interface proof =
    2.31    let
    2.32      fun cons_to xs x = x :: xs
    2.33  
    2.34 @@ -83,8 +82,7 @@
    2.35              |>> Ord_List.union label_ord refed
    2.36              ||> cons_to accu
    2.37            else
    2.38 -            (set_time l zero_preplay_time; (* remove unrefed step! *)
    2.39 -             (refed, accu))
    2.40 +            (refed, accu)
    2.41  
    2.42      and do_refed_step step =
    2.43        min_deps_of_step preplay_interface step
    2.44 @@ -104,7 +102,6 @@
    2.45          end
    2.46  
    2.47    in
    2.48 -    set_preplay_fail false; (* step(s) causing the failure may be removed *)
    2.49      snd (do_proof proof)
    2.50    end
    2.51  

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 18:16:50 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 19:03:08 2013 +0200
     3.3 @@ -12,20 +12,26 @@
     3.4    type label = Sledgehammer_Proof.label
     3.5  
     3.6    eqtype preplay_time
     3.7 +
     3.8 +  datatype preplay_result =
     3.9 +    PplFail of exn |
    3.10 +    PplSucc of preplay_time
    3.11 +
    3.12    val zero_preplay_time : preplay_time
    3.13    val some_preplay_time : preplay_time
    3.14    val add_preplay_time : preplay_time -> preplay_time -> preplay_time
    3.15    val string_of_preplay_time : preplay_time -> string
    3.16 -  val preplay : bool -> bool -> string -> string -> Proof.context ->
    3.17 -    Time.time -> isar_step -> preplay_time
    3.18 +  (*val preplay_raw : bool -> bool -> string -> string -> Proof.context ->
    3.19 +    Time.time -> isar_step -> preplay_time*)
    3.20  
    3.21    type preplay_interface =
    3.22 -  { get_time : label -> preplay_time,
    3.23 -    set_time : label -> preplay_time -> unit,
    3.24 +  { get_preplay_result : label -> preplay_result,
    3.25 +    set_preplay_result : label -> preplay_result -> unit,
    3.26 +    get_preplay_time : label -> preplay_time,
    3.27 +    set_preplay_time : label -> preplay_time -> unit,
    3.28      preplay_quietly : Time.time -> isar_step -> preplay_time,
    3.29 -    preplay_fail : unit -> bool,
    3.30 -    set_preplay_fail : bool -> unit,
    3.31 -    overall_preplay_stats : unit -> preplay_time * bool }
    3.32 +    (* the returned flag signals a preplay failure *)
    3.33 +    overall_preplay_stats : isar_proof -> preplay_time * bool }
    3.34  
    3.35    val proof_preplay_interface :
    3.36      bool -> Proof.context -> string -> string -> bool -> Time.time -> bool
    3.37 @@ -45,6 +51,10 @@
    3.38        (t, true)  = "> t ms" *)
    3.39  type preplay_time = bool * Time.time
    3.40  
    3.41 +datatype preplay_result =
    3.42 +  PplFail of exn |
    3.43 +  PplSucc of preplay_time
    3.44 +
    3.45  val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
    3.46  val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
    3.47  
    3.48 @@ -119,9 +129,9 @@
    3.49              | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt
    3.50  
    3.51  
    3.52 -(* main function for preplaying isar_steps *)
    3.53 -fun preplay _ _ _ _ _ _ (Let _) = zero_preplay_time
    3.54 -  | preplay debug trace type_enc lam_trans ctxt timeout
    3.55 +(* main function for preplaying isar_steps; may throw exceptions *)
    3.56 +fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time
    3.57 +  | preplay_raw debug trace type_enc lam_trans ctxt timeout
    3.58        (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) =
    3.59    let
    3.60      val (prop, obtain) =
    3.61 @@ -167,12 +177,13 @@
    3.62  (*** proof preplay interface ***)
    3.63  
    3.64  type preplay_interface =
    3.65 -  { get_time : label -> preplay_time,
    3.66 -    set_time : label -> preplay_time -> unit,
    3.67 -    preplay_quietly : Time.time -> isar_step -> preplay_time,
    3.68 -    preplay_fail : unit -> bool,
    3.69 -    set_preplay_fail : bool -> unit,
    3.70 -    overall_preplay_stats : unit -> preplay_time * bool }
    3.71 +{ get_preplay_result : label -> preplay_result,
    3.72 +  set_preplay_result : label -> preplay_result -> unit,
    3.73 +  get_preplay_time : label -> preplay_time,
    3.74 +  set_preplay_time : label -> preplay_time -> unit,
    3.75 +  preplay_quietly : Time.time -> isar_step -> preplay_time,
    3.76 +  (* the returned flag signals a preplay failure *)
    3.77 +  overall_preplay_stats : isar_proof -> preplay_time * bool }
    3.78  
    3.79  
    3.80  (* enriches context with local proof facts *)
    3.81 @@ -197,22 +208,25 @@
    3.82    end
    3.83  
    3.84  
    3.85 -(* Given a proof, produces an imperative preplay interface with a shared state.
    3.86 -   The preplay times are caluclated lazyly and cached to avoid repeated
    3.87 +(* Given a proof, produces an imperative preplay interface with a shared table
    3.88 +   mapping from labels to preplay results.
    3.89 +   The preplay results are caluclated lazyly and cached to avoid repeated
    3.90     calculation.
    3.91  
    3.92     PRE CONDITION: the proof must be labeled canocially, see
    3.93     Slegehammer_Proof.relabel_proof_canonically
    3.94  *)
    3.95 +
    3.96 +
    3.97  fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
    3.98        preplay_timeout preplay_trace proof : preplay_interface =
    3.99    if not do_preplay then
   3.100      (* the dont_preplay option pretends that everything works just fine *)
   3.101 -    { get_time = K zero_preplay_time,
   3.102 -      set_time = K (K ()),
   3.103 +    { get_preplay_result = K (PplSucc zero_preplay_time),
   3.104 +      set_preplay_result = K (K ()),
   3.105 +      get_preplay_time = K zero_preplay_time,
   3.106 +      set_preplay_time = K (K ()),
   3.107        preplay_quietly = K (K zero_preplay_time),
   3.108 -      preplay_fail = K false,
   3.109 -      set_preplay_fail = K (),
   3.110        overall_preplay_stats = K (zero_preplay_time, false)}
   3.111    else
   3.112      let
   3.113 @@ -220,20 +234,20 @@
   3.114        (* add local proof facts to context *)
   3.115        val ctxt = enrich_context proof ctxt
   3.116  
   3.117 -      val fail = Unsynchronized.ref false
   3.118 -      fun preplay_fail () = !fail
   3.119 +      fun preplay timeout step =
   3.120 +        preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step
   3.121 +        |> PplSucc
   3.122 +        handle exn =>
   3.123 +          if Exn.is_interrupt exn orelse debug then reraise exn
   3.124 +          else PplFail exn
   3.125  
   3.126 -      fun set_preplay_fail b = fail := b
   3.127 +      (* preplay steps treating exceptions like timeouts *)
   3.128 +      fun preplay_quietly timeout step =
   3.129 +        case preplay timeout step of
   3.130 +          PplSucc preplay_time => preplay_time
   3.131 +        | PplFail _ => (true, timeout)
   3.132  
   3.133 -      val preplay = preplay debug preplay_trace type_enc lam_trans ctxt
   3.134 -
   3.135 -      (* preplay steps without registering preplay_fails, treating exceptions
   3.136 -         like timeouts *)
   3.137 -      fun preplay_quietly timeout step =
   3.138 -        try (preplay timeout) step
   3.139 -        |> the_default (true, timeout)
   3.140 -
   3.141 -      val preplay_time_tab =
   3.142 +      val preplay_tab =
   3.143          let
   3.144            fun add_step_to_tab step tab =
   3.145              case label_of_step step of
   3.146 @@ -250,34 +264,42 @@
   3.147            |> Unsynchronized.ref
   3.148          end
   3.149  
   3.150 -      fun register_preplay_fail lazy_time = Lazy.force lazy_time
   3.151 -        handle exn =>
   3.152 -          if Exn.is_interrupt exn orelse debug then reraise exn
   3.153 -          else (fail := true; some_preplay_time)
   3.154 -
   3.155 -      fun get_time lbl =
   3.156 -        register_preplay_fail
   3.157 -          (Canonical_Lbl_Tab.lookup (!preplay_time_tab) lbl |> the)
   3.158 +      fun get_preplay_result lbl =
   3.159 +        Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
   3.160          handle
   3.161            Option.Option =>
   3.162              raise Fail "Sledgehammer_Preplay: preplay time table"
   3.163  
   3.164 -      fun set_time lbl time =
   3.165 -        preplay_time_tab :=
   3.166 -          Canonical_Lbl_Tab.update (lbl, Lazy.value time) (!preplay_time_tab)
   3.167 +      fun set_preplay_result lbl result =
   3.168 +        preplay_tab :=
   3.169 +          Canonical_Lbl_Tab.update (lbl, Lazy.value result) (!preplay_tab)
   3.170  
   3.171 -      fun total_preplay_time () =
   3.172 -        Canonical_Lbl_Tab.fold
   3.173 -          (snd #> register_preplay_fail #> add_preplay_time)
   3.174 -          (!preplay_time_tab) zero_preplay_time
   3.175 +      fun get_preplay_time lbl =
   3.176 +        case get_preplay_result lbl of
   3.177 +          PplSucc preplay_time => preplay_time
   3.178 +        | PplFail _ => some_preplay_time (* best approximation possible *)
   3.179  
   3.180 -      fun overall_preplay_stats () = (total_preplay_time (), preplay_fail ())
   3.181 +      fun set_preplay_time lbl time = set_preplay_result lbl (PplSucc time)
   3.182 +
   3.183 +      fun overall_preplay_stats (Proof(_, _, steps)) =
   3.184 +        let
   3.185 +          fun result_of_step step =
   3.186 +            try (label_of_step #> the #> get_preplay_result) step
   3.187 +            |> the_default (PplSucc zero_preplay_time)
   3.188 +          fun do_step step =
   3.189 +            case result_of_step step of
   3.190 +              PplSucc preplay_time => apfst (add_preplay_time preplay_time)
   3.191 +            | PplFail _ => apsnd (K true)
   3.192 +        in
   3.193 +          fold_isar_steps do_step steps (zero_preplay_time, false)
   3.194 +        end
   3.195 +
   3.196      in
   3.197 -      { get_time = get_time,
   3.198 -        set_time = set_time,
   3.199 +      { get_preplay_result = get_preplay_result,
   3.200 +        set_preplay_result = set_preplay_result,
   3.201 +        get_preplay_time = get_preplay_time,
   3.202 +        set_preplay_time = set_preplay_time,
   3.203          preplay_quietly = preplay_quietly,
   3.204 -        preplay_fail = preplay_fail,
   3.205 -        set_preplay_fail = set_preplay_fail,
   3.206          overall_preplay_stats = overall_preplay_stats}
   3.207      end
   3.208  

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 18:16:50 2013 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 19:03:08 2013 +0200
     4.3 @@ -372,7 +372,7 @@
     4.4            val (l, subst, next) =
     4.5              (l, subst, next) |> fresh_label depth have_prefix
     4.6            val sub = do_proofs subst depth sub
     4.7 -          val by = by |> do_byline subst depth
     4.8 +          val by = by |> do_byline subst
     4.9          in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
    4.10        | do_steps subst depth next (step :: steps) =
    4.11          step :: do_steps subst depth next steps
    4.12 @@ -380,7 +380,7 @@
    4.13        let val (assms, subst) = do_assms subst depth assms in
    4.14          Proof (fix, assms, do_steps subst depth 1 steps)
    4.15        end
    4.16 -    and do_byline subst depth byline =
    4.17 +    and do_byline subst byline =
    4.18        map_facts_of_byline (do_facts subst) byline
    4.19      and do_proofs subst depth = map (do_proof subst (depth + 1))
    4.20    in do_proof [] 0 end
    4.21 @@ -588,7 +588,7 @@
    4.22            |> relabel_proof_canonically
    4.23            |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
    4.24                 preplay_timeout preplay_trace)
    4.25 -        val isar_proof =
    4.26 +        val ((preplay_time, preplay_fail), isar_proof) =
    4.27            isar_proof
    4.28            |> compress_proof
    4.29                 (if isar_proofs = SOME true then isar_compress else 1000.0)
    4.30 @@ -596,11 +596,10 @@
    4.31                 merge_timeout_slack preplay_interface
    4.32            |> try0 preplay_timeout preplay_interface
    4.33            |> minimize_dependencies_and_remove_unrefed_steps preplay_interface
    4.34 -          |> clean_up_labels_in_proof
    4.35 -        val isar_text =
    4.36 -          string_of_proof ctxt type_enc lam_trans subgoal subgoal_count
    4.37 -                          isar_proof
    4.38 -        val (preplay_time, preplay_fail) = overall_preplay_stats ()
    4.39 +          |> `overall_preplay_stats
    4.40 +          ||> clean_up_labels_in_proof
    4.41 +        val isar_text = string_of_proof ctxt type_enc lam_trans subgoal
    4.42 +          subgoal_count isar_proof
    4.43        in
    4.44          case isar_text of
    4.45            "" =>

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 18:16:50 2013 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 19:03:08 2013 +0200
     5.3 @@ -35,15 +35,15 @@
     5.4        end
     5.5  
     5.6  fun try0_step _ _ (step as Let _) = step
     5.7 -  | try0_step preplay_timeout ({preplay_quietly, get_time, set_time,
     5.8 -    set_preplay_fail, ...} : preplay_interface)
     5.9 +  | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
    5.10 +    set_preplay_time, ...} : preplay_interface)
    5.11      (step as Prove (_, _, l, _, _, _)) =
    5.12        let
    5.13  
    5.14 -        val (preplay_fail, timeout) =
    5.15 -          case get_time l of
    5.16 -            (true, _) => (true, preplay_timeout)
    5.17 -          | (false, t) => (false, t)
    5.18 +        val timeout =
    5.19 +          case get_preplay_time l of
    5.20 +            (true, _) => preplay_timeout
    5.21 +          | (false, t) => t
    5.22  
    5.23          fun try_variant variant =
    5.24             case preplay_quietly timeout variant of
    5.25 @@ -52,13 +52,11 @@
    5.26  
    5.27        in
    5.28          case Par_List.get_some try_variant (variants step) of
    5.29 -          SOME (step, time) => (set_time l time; step)
    5.30 -        | NONE => (if preplay_fail then set_preplay_fail true else (); step)
    5.31 +          SOME (step, time) => (set_preplay_time l time; step)
    5.32 +        | NONE => step
    5.33        end
    5.34  
    5.35 -fun try0 preplay_timeout
    5.36 -  (preplay_interface as {set_preplay_fail, ...} : preplay_interface) proof =
    5.37 -    (set_preplay_fail false; (* failure might be fixed *)
    5.38 -     map_isar_steps (try0_step preplay_timeout preplay_interface) proof)
    5.39 +fun try0 preplay_timeout preplay_interface proof =
    5.40 +     map_isar_steps (try0_step preplay_timeout preplay_interface) proof
    5.41  
    5.42  end