1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 17 11:55:40 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 17 11:56:34 2013 +0100
     1.3 @@ -2,16 +2,21 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Author:     Steffen Juilf Smolka, TU Muenchen
     1.6  
     1.7 -Preplaying of reconstructed isar proofs.
     1.8 +Preplaying of isar proofs.
     1.9  *)
    1.10  
    1.11  signature SLEDGEHAMMER_PREPLAY =
    1.12  sig
    1.13    type isar_step = Sledgehammer_Proof.isar_step
    1.14 +  eqtype preplay_time
    1.15 +  val zero_preplay_time : preplay_time
    1.16 +  val some_preplay_time : preplay_time
    1.17 +  val add_preplay_time : preplay_time -> preplay_time -> preplay_time
    1.18 +  val string_of_preplay_time : preplay_time -> string
    1.19    val try_metis : bool -> string -> string -> Proof.context ->
    1.20 -    Time.time -> (isar_step option * isar_step) -> unit -> Time.time option
    1.21 +    Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
    1.22    val try_metis_quietly : bool -> string -> string -> Proof.context ->
    1.23 -    Time.time -> (isar_step option * isar_step) -> unit -> Time.time option
    1.24 +    Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
    1.25  end
    1.26  
    1.27  structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
    1.28 @@ -20,13 +25,25 @@
    1.29  open Sledgehammer_Util
    1.30  open Sledgehammer_Proof
    1.31  
    1.32 +(* The boolean flag encodes whether the time is exact (false) or an lower bound
    1.33 +     (true) *)
    1.34 +type preplay_time = bool * Time.time
    1.35 +
    1.36 +val zero_preplay_time = (false, Time.zeroTime)
    1.37 +val some_preplay_time = (true, Time.zeroTime)
    1.38 +
    1.39 +fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
    1.40 +
    1.41 +val string_of_preplay_time = ATP_Util.string_from_ext_time
    1.42 +
    1.43  (* timing *)
    1.44  fun take_time timeout tac arg =
    1.45    let
    1.46      val timing = Timing.start ()
    1.47    in
    1.48 -    (TimeLimit.timeLimit timeout tac arg; Timing.result timing |> #cpu |> SOME)
    1.49 -    handle TimeLimit.TimeOut => NONE
    1.50 +    (TimeLimit.timeLimit timeout tac arg;
    1.51 +      Timing.result timing |> #cpu |> pair false)
    1.52 +    handle TimeLimit.TimeOut => (true, timeout)
    1.53    end
    1.54  
    1.55  (* lookup facts in context *)
    1.56 @@ -71,9 +88,9 @@
    1.57                Assume (_, t) => make_thm t
    1.58              | Obtain (_, _, _, t, _) => make_thm t
    1.59              | Prove (_, _, t, _) => make_thm t
    1.60 -            | _ => error "Preplay error: unexpected succedent of case split")
    1.61 +            | _ => error "preplay error: unexpected succedent of case split")
    1.62            :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
    1.63 -                          | _ => error "Preplay error: malformed case split")
    1.64 +                          | _ => error "preplay error: malformed case split")
    1.65                       #> make_thm)
    1.66                 cases)
    1.67      val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
    1.68 @@ -83,12 +100,13 @@
    1.69      fun tac {context = ctxt, prems = _} =
    1.70        Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
    1.71    in
    1.72 -    take_time timeout (fn () => goal tac)
    1.73 +    take_time timeout
    1.74 +      (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg))
    1.75    end
    1.76 -  handle ZEROTIME => K (SOME Time.zeroTime)
    1.77 +  handle ZEROTIME => K zero_preplay_time
    1.78  
    1.79 -(* this version does not throw exceptions but returns NONE instead *)
    1.80 -fun try_metis_quietly debug type_enc lam_trans ctxt =
    1.81 -   the_default NONE oo try oo try_metis debug type_enc lam_trans ctxt
    1.82 +(* this version treats exceptions like timeouts *)
    1.83 +fun try_metis_quietly debug type_enc lam_trans ctxt timeout =
    1.84 +   the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout
    1.85  
    1.86  end

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 17 11:55:40 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 17 11:56:34 2013 +0100
     2.3 @@ -741,7 +741,7 @@
     2.4          and do_case outer (c, infs) =
     2.5            Assume (label_of_clause c, prop_of_clause c) ::
     2.6            map (isar_step_of_direct_inf outer) infs
     2.7 -        val (isar_proof, (preplay_fail, ext_time)) =
     2.8 +        val (isar_proof, (preplay_fail, preplay_time)) =
     2.9            ref_graph
    2.10            |> redirect_graph axioms tainted
    2.11            |> map (isar_step_of_direct_inf true)
    2.12 @@ -771,8 +771,8 @@
    2.13            let
    2.14              val msg =
    2.15                (if preplay then
    2.16 -                [if preplay_fail then "may fail"
    2.17 -                 else string_from_ext_time ext_time]
    2.18 +                [(if preplay_fail then "may fail, " else "") ^
    2.19 +                   Sledgehammer_Preplay.string_of_preplay_time preplay_time]
    2.20                 else
    2.21                   []) @
    2.22                (if verbose then

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 17 11:55:40 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 17 11:56:34 2013 +0100
     3.3 @@ -8,9 +8,10 @@
     3.4  signature SLEDGEHAMMER_SHRINK =
     3.5  sig
     3.6    type isar_step = Sledgehammer_Proof.isar_step
     3.7 +  type preplay_time = Sledgehammer_Preplay.preplay_time
     3.8    val shrink_proof :
     3.9      bool -> Proof.context -> string -> string -> bool -> Time.time option
    3.10 -    -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
    3.11 +    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
    3.12  end
    3.13  
    3.14  structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
    3.15 @@ -45,10 +46,6 @@
    3.16  fun pop_max tab = pop tab (the (Inttab.max_key tab))
    3.17  fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
    3.18  
    3.19 -(* Timing *)
    3.20 -fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
    3.21 -val no_time = (false, Time.zeroTime)
    3.22 -
    3.23  (* Main function for shrinking proofs *)
    3.24  fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
    3.25                   isar_shrink proof =
    3.26 @@ -64,9 +61,11 @@
    3.27        fun handle_metis_fail try_metis () =
    3.28          try_metis () handle exn =>
    3.29            (if Exn.is_interrupt exn orelse debug then reraise exn
    3.30 -           else metis_fail := true; SOME Time.zeroTime)
    3.31 +           else metis_fail := true; some_preplay_time)
    3.32        fun get_time lazy_time =
    3.33 -        if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
    3.34 +        if !metis_fail andalso not (Lazy.is_finished lazy_time)
    3.35 +          then some_preplay_time
    3.36 +          else Lazy.force lazy_time
    3.37        val metis_fail = fn () => !metis_fail
    3.38      end
    3.39  
    3.40 @@ -115,10 +114,10 @@
    3.41        (* cache metis preplay times in lazy time vector *)
    3.42        val metis_time =
    3.43          v_map_index
    3.44 -          (if not preplay then K (SOME Time.zeroTime) #> Lazy.value
    3.45 +          (if not preplay then K (zero_preplay_time) #> Lazy.value
    3.46             else
    3.47 -             apsnd the
    3.48 -             #> apfst (fn i => try (get (i-1) #> the) proof_vect)
    3.49 +             apsnd the (* step *)
    3.50 +             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
    3.51               #> try_metis debug type_enc lam_trans ctxt preplay_timeout
    3.52               #> handle_metis_fail
    3.53               #> Lazy.lazy)
    3.54 @@ -126,47 +125,46 @@
    3.55  
    3.56        fun sum_up_time lazy_time_vector =
    3.57          Vector.foldl
    3.58 -          ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
    3.59 -             | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout)))
    3.60 -            o apfst get_time)
    3.61 -          no_time lazy_time_vector
    3.62 +          (apfst get_time #> uncurry add_preplay_time)
    3.63 +          zero_preplay_time lazy_time_vector
    3.64  
    3.65        (* Merging *)
    3.66 -      (* TODO: consider adding "Obtain" cases *)
    3.67        fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
    3.68            let
    3.69              val (step_constructor, lfs2, gfs2) =
    3.70                (case step2 of
    3.71                  (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
    3.72                    (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
    3.73 -              | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
    3.74 +              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
    3.75                    (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
    3.76 -              | _ => error "Internal error: unmergeable Isar steps" )
    3.77 +              | _ => error "sledgehammer_shrink: unmergeable Isar steps" )
    3.78              val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
    3.79              val gfs = union (op =) gfs1 gfs2
    3.80            in step_constructor (By_Metis (lfs, gfs)) end
    3.81 -        | merge _ _ = error "Internal error: unmergeable Isar steps"
    3.82 +        | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps"
    3.83  
    3.84        fun try_merge metis_time (s1, i) (s2, j) =
    3.85 -        (case get i metis_time |> Lazy.force of
    3.86 -          NONE => (NONE, metis_time)
    3.87 -        | SOME t1 =>
    3.88 -          (case get j metis_time |> Lazy.force of
    3.89 -            NONE => (NONE, metis_time)
    3.90 -          | SOME t2 =>
    3.91 -            let
    3.92 -              val s12 = merge s1 s2
    3.93 -              val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
    3.94 -            in
    3.95 -              case try_metis_quietly debug type_enc lam_trans ctxt timeout
    3.96 -              (NONE, s12) () of
    3.97 -                NONE => (NONE, metis_time)
    3.98 -              | some_t12 =>
    3.99 -                (SOME s12, metis_time
   3.100 -                           |> replace (Time.zeroTime |> SOME |> Lazy.value) i
   3.101 -                           |> replace (Lazy.value some_t12) j)
   3.102 +        if not preplay then (merge s1 s2 |> SOME, metis_time)
   3.103 +        else
   3.104 +          (case get i metis_time |> Lazy.force of
   3.105 +            (true, _) => (NONE, metis_time)
   3.106 +          | (_, t1) =>
   3.107 +            (case get j metis_time |> Lazy.force of
   3.108 +              (true, _) => (NONE, metis_time)
   3.109 +            | (_, t2) =>
   3.110 +              let
   3.111 +                val s12 = merge s1 s2
   3.112 +                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
   3.113 +              in
   3.114 +                case try_metis_quietly debug type_enc lam_trans ctxt timeout
   3.115 +                (NONE, s12) () of
   3.116 +                  (true, _) => (NONE, metis_time)
   3.117 +                | exact_time =>
   3.118 +                  (SOME s12, metis_time
   3.119 +                             |> replace (zero_preplay_time |> Lazy.value) i
   3.120 +                             |> replace (Lazy.value exact_time) j)
   3.121  
   3.122 -            end))
   3.123 +              end))
   3.124  
   3.125        fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
   3.126          if Inttab.is_empty cand_tab
   3.127 @@ -225,20 +223,20 @@
   3.128            proof |> do_case_splits rich_ctxt
   3.129                  |>> shrink_top_level on_top_level rich_ctxt
   3.130        in
   3.131 -        (proof, ext_time_add lower_level_time top_level_time)
   3.132 +        (proof, add_preplay_time lower_level_time top_level_time)
   3.133        end
   3.134  
   3.135      and do_case_splits ctxt proof =
   3.136        let
   3.137          fun shrink_each_and_collect_time shrink candidates =
   3.138 -          let fun f_m cand time = shrink cand ||> ext_time_add time
   3.139 -          in fold_map f_m candidates no_time end
   3.140 +          let fun f_m cand time = shrink cand ||> add_preplay_time time
   3.141 +          in fold_map f_m candidates zero_preplay_time end
   3.142          val shrink_case_split =
   3.143            shrink_each_and_collect_time (do_proof false ctxt)
   3.144          fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) =
   3.145              let val (cases, time) = shrink_case_split cases
   3.146              in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
   3.147 -          | shrink step = (step, no_time)
   3.148 +          | shrink step = (step, zero_preplay_time)
   3.149        in
   3.150          shrink_each_and_collect_time shrink proof
   3.151        end