--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 17 11:55:40 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 17 11:56:34 2013 +0100
@@ -2,16 +2,21 @@
Author: Jasmin Blanchette, TU Muenchen
Author: Steffen Juilf Smolka, TU Muenchen
-Preplaying of reconstructed isar proofs.
+Preplaying of isar proofs.
*)
signature SLEDGEHAMMER_PREPLAY =
sig
type isar_step = Sledgehammer_Proof.isar_step
+ eqtype preplay_time
+ val zero_preplay_time : preplay_time
+ val some_preplay_time : preplay_time
+ val add_preplay_time : preplay_time -> preplay_time -> preplay_time
+ val string_of_preplay_time : preplay_time -> string
val try_metis : bool -> string -> string -> Proof.context ->
- Time.time -> (isar_step option * isar_step) -> unit -> Time.time option
+ Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
val try_metis_quietly : bool -> string -> string -> Proof.context ->
- Time.time -> (isar_step option * isar_step) -> unit -> Time.time option
+ Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
end
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
@@ -20,13 +25,25 @@
open Sledgehammer_Util
open Sledgehammer_Proof
+(* The boolean flag encodes whether the time is exact (false) or an lower bound
+ (true) *)
+type preplay_time = bool * Time.time
+
+val zero_preplay_time = (false, Time.zeroTime)
+val some_preplay_time = (true, Time.zeroTime)
+
+fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
+
+val string_of_preplay_time = ATP_Util.string_from_ext_time
+
(* timing *)
fun take_time timeout tac arg =
let
val timing = Timing.start ()
in
- (TimeLimit.timeLimit timeout tac arg; Timing.result timing |> #cpu |> SOME)
- handle TimeLimit.TimeOut => NONE
+ (TimeLimit.timeLimit timeout tac arg;
+ Timing.result timing |> #cpu |> pair false)
+ handle TimeLimit.TimeOut => (true, timeout)
end
(* lookup facts in context *)
@@ -71,9 +88,9 @@
Assume (_, t) => make_thm t
| Obtain (_, _, _, t, _) => make_thm t
| Prove (_, _, t, _) => make_thm t
- | _ => error "Preplay error: unexpected succedent of case split")
+ | _ => error "preplay error: unexpected succedent of case split")
:: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
- | _ => error "Preplay error: malformed case split")
+ | _ => error "preplay error: malformed case split")
#> make_thm)
cases)
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
@@ -83,12 +100,13 @@
fun tac {context = ctxt, prems = _} =
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
in
- take_time timeout (fn () => goal tac)
+ take_time timeout
+ (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg))
end
- handle ZEROTIME => K (SOME Time.zeroTime)
+ handle ZEROTIME => K zero_preplay_time
-(* this version does not throw exceptions but returns NONE instead *)
-fun try_metis_quietly debug type_enc lam_trans ctxt =
- the_default NONE oo try oo try_metis debug type_enc lam_trans ctxt
+(* this version treats exceptions like timeouts *)
+fun try_metis_quietly debug type_enc lam_trans ctxt timeout =
+ the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout
end