--- a/src/HOL/TPTP/mash_eval.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 15 19:57:12 2012 +0100
@@ -16,8 +16,12 @@
structure MaSh_Eval : MASH_EVAL =
struct
+open Sledgehammer_Util
open Sledgehammer_Fact
+open Sledgehammer_MePo
open Sledgehammer_MaSh
+open Sledgehammer_Provers
+open Sledgehammer_Isar
val MePoN = "MePo"
val MaShN = "MaSh"
@@ -31,12 +35,12 @@
val _ = File.write report_path ""
fun print s = (tracing s; File.append report_path (s ^ "\n"))
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
- Sledgehammer_Isar.default_params ctxt []
+ default_params ctxt []
val prover = hd provers
val slack_max_facts = generous_max_facts (the max_facts)
val sugg_path = sugg_file_name |> Path.explode
val lines = sugg_path |> File.read_lines
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+ val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
val all_names = build_all_names nickname_of facts
val mepo_ok = Unsynchronized.ref 0
@@ -46,7 +50,7 @@
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
fun index_string (j, s) = s ^ "@" ^ string_of_int j
fun str_of_res label facts ({outcome, run_time, used_facts, ...}
- : Sledgehammer_Provers.prover_result) =
+ : prover_result) =
let val facts = facts |> map (fn ((name, _), _) => name ()) in
" " ^ label ^ ": " ^
(if is_none outcome then
@@ -77,9 +81,9 @@
val isar_deps = isar_dependencies_of all_names th |> these
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
val mepo_facts =
- Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
- slack_max_facts NONE hyp_ts concl_t facts
- |> Sledgehammer_MePo.weight_mepo_facts
+ mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
+ concl_t facts
+ |> weight_mepo_facts
val (mash_facts, mash_unks) =
find_mash_suggestions slack_max_facts suggs facts [] []
|>> weight_mash_facts
@@ -93,9 +97,8 @@
"goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
heading
in
- Config.put Sledgehammer_Provers.dest_dir dir
- #> Config.put Sledgehammer_Provers.problem_prefix
- (prob_prefix ^ "__")
+ Config.put dest_dir dir
+ #> Config.put problem_prefix (prob_prefix ^ "__")
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
end
| set_file_name _ NONE = I
@@ -105,7 +108,7 @@
val facts =
facts
|> map get
- |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
+ |> maybe_instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
|> map nickify
val ctxt = ctxt |> set_file_name heading prob_dir_name
@@ -128,11 +131,12 @@
" " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
Real.fmt (StringCvt.FIX (SOME 1))
(100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
- val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
+ val inst_inducts = Config.get ctxt instantiate_inducts
val options =
[prover, string_of_int (the max_facts) ^ " facts",
"slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
- the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
+ the_default "smart" lam_trans,
+ ATP_Util.string_from_time (timeout |> the_default one_year),
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val n = length lines
in
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Dec 15 19:57:12 2012 +0100
@@ -283,9 +283,7 @@
val monomorphic_term = ATP_Util.monomorphic_term
val specialize_type = ATP_Util.specialize_type
val eta_expand = ATP_Util.eta_expand
-
-fun time_limit NONE = I
- | time_limit (SOME delay) = TimeLimit.timeLimit delay
+val time_limit = Sledgehammer_Util.time_limit
fun DETERM_TIMEOUT delay tac st =
Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 15 19:57:12 2012 +0100
@@ -249,8 +249,6 @@
end)]
end
-val the_timeout = the_default infinite_timeout
-
fun extract_params mode default_params override_params =
let
val raw_params = rev override_params @ rev default_params
@@ -320,11 +318,10 @@
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
- val timeout =
- (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
+ val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
val preplay_timeout =
- if mode = Auto_Try then Time.zeroTime
- else lookup_time "preplay_timeout" |> the_timeout
+ if mode = Auto_Try then SOME Time.zeroTime
+ else lookup_time "preplay_timeout"
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 15 19:57:12 2012 +0100
@@ -818,7 +818,7 @@
if is_smt_prover ctxt prover then
()
else
- launch_thread timeout (fn () =>
+ launch_thread (timeout |> the_default one_day) (fn () =>
let
val thy = Proof_Context.theory_of ctxt
val name = freshish_name ()
@@ -920,7 +920,10 @@
(commit false adds [] []; ([], next_commit_time ()))
else
(adds, next_commit)
- val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ val timed_out =
+ case learn_timeout of
+ SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
+ | NONE => false
in (adds, ([name], n, next_commit, timed_out)) end
val n =
if null new_facts then
@@ -951,7 +954,10 @@
(commit false [] reps flops; ([], [], next_commit_time ()))
else
(reps, flops, next_commit)
- val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ val timed_out =
+ case learn_timeout of
+ SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
+ | NONE => false
in ((reps, flops), (n, next_commit, timed_out)) end
val n =
if not run_prover orelse null old_facts then
@@ -1003,15 +1009,15 @@
val num_facts = length facts
val prover = hd provers
fun learn auto_level run_prover =
- mash_learn_facts ctxt params prover auto_level run_prover infinite_timeout
- facts
+ mash_learn_facts ctxt params prover auto_level run_prover NONE facts
|> Output.urgent_message
in
if run_prover then
("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
- " timeout: " ^ string_from_time timeout ^
- ").\n\nCollecting Isar proofs first..."
+ (case timeout of
+ SOME timeout => " timeout: " ^ string_from_time timeout
+ | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
|> Output.urgent_message;
learn 1 false;
"Now collecting automatic proofs. This may take several hours. You can \
@@ -1048,9 +1054,12 @@
let
fun maybe_learn () =
if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
- Time.toSeconds timeout >= min_secs_for_learning then
- let val timeout = time_mult learn_timeout_slack timeout in
- launch_thread timeout
+ (timeout = NONE orelse
+ Time.toSeconds (the timeout) >= min_secs_for_learning) then
+ let
+ val timeout = Option.map (time_mult learn_timeout_slack) timeout
+ in
+ launch_thread (timeout |> the_default one_day)
(fn () => (true, mash_learn_facts ctxt params prover 2 false
timeout facts))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 19:57:12 2012 +0100
@@ -61,8 +61,12 @@
val _ =
print silent (fn () =>
"Testing " ^ n_facts (map fst facts) ^
- (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
- else "") ^ "...")
+ (if verbose then
+ case timeout of
+ SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+ | _ => ""
+ else
+ "") ^ "...")
val {goal, ...} = Proof.goal state
val facts =
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
@@ -101,10 +105,11 @@
part of the timeout. *)
val slack_msecs = 200
-fun new_timeout timeout run_time =
- Int.min (Time.toMilliseconds timeout,
- Time.toMilliseconds run_time + slack_msecs)
- |> Time.fromMilliseconds
+fun new_timeout NONE _ = NONE
+ | new_timeout (SOME timeout) run_time =
+ Int.min (Time.toMilliseconds timeout,
+ Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds |> SOME
(* The linear algorithm usually outperforms the binary algorithm when over 60%
of the facts are actually needed. The binary algorithm is much more
@@ -222,11 +227,12 @@
| {outcome = SOME TimedOut, preplay, ...} =>
(NONE,
(preplay,
- fn _ => "Timeout: You can increase the time limit using the \
- \\"timeout\" option (e.g., \"timeout = " ^
- string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
- "\").",
- ""))
+ fn _ =>
+ "Timeout: You can increase the time limit using the \"timeout\" \
+ \option (e.g., \"timeout = " ^
+ string_of_int (10 + Time.toMilliseconds
+ (timeout |> the_default (seconds 60.0)) div 1000) ^
+ "\").", ""))
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Dec 15 19:57:12 2012 +0100
@@ -37,8 +37,8 @@
isar_shrink : real,
slice : bool,
minimize : bool option,
- timeout : Time.time,
- preplay_timeout : Time.time,
+ timeout : Time.time option,
+ preplay_timeout : Time.time option,
expect : string}
type relevance_fudge =
@@ -330,8 +330,8 @@
isar_shrink : real,
slice : bool,
minimize : bool option,
- timeout : Time.time,
- preplay_timeout : Time.time,
+ timeout : Time.time option,
+ preplay_timeout : Time.time option,
expect : string}
type relevance_fudge =
@@ -479,7 +479,7 @@
let
val {context = ctxt, facts, goal} = Proof.goal state
val full_tac = Method.insert_tac facts i THEN tac ctxt i
- in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
+ in time_limit timeout (try (Seq.pull o full_tac)) goal end
fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
metis_tac [type_enc] lam_trans
@@ -500,39 +500,40 @@
fun play_one_line_proof mode debug verbose timeout pairs state i preferred
reconstrs =
let
- val _ =
- if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
- Output.urgent_message "Preplaying proof..."
- else
- ()
- val ths = pairs |> sort_wrt (fst o fst) |> map snd
fun get_preferred reconstrs =
if member (op =) reconstrs preferred then preferred
else List.last reconstrs
- fun play [] [] = Failed_to_Play (get_preferred reconstrs)
- | play timed_outs [] =
- Trust_Playable (get_preferred timed_outs, SOME timeout)
- | play timed_out (reconstr :: reconstrs) =
- let
- val _ =
- if verbose then
- "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^
- string_from_time timeout ^ "..."
- |> Output.urgent_message
- else
- ()
- val timer = Timer.startRealTimer ()
- in
- case timed_reconstructor reconstr debug timeout ths state i of
- SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
- | _ => play timed_out reconstrs
- end
- handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
in
- if timeout = Time.zeroTime then
+ if timeout = SOME Time.zeroTime then
Trust_Playable (get_preferred reconstrs, NONE)
else
- play [] reconstrs
+ let
+ val _ =
+ if mode = Minimize then Output.urgent_message "Preplaying proof..."
+ else ()
+ val ths = pairs |> sort_wrt (fst o fst) |> map snd
+ fun play [] [] = Failed_to_Play (get_preferred reconstrs)
+ | play timed_outs [] =
+ Trust_Playable (get_preferred timed_outs, timeout)
+ | play timed_out (reconstr :: reconstrs) =
+ let
+ val _ =
+ if verbose then
+ "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^
+ (case timeout of
+ SOME timeout => " for " ^ string_from_time timeout
+ | NONE => "") ^ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val timer = Timer.startRealTimer ()
+ in
+ case timed_reconstructor reconstr debug timeout ths state i of
+ SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+ | _ => play timed_out reconstrs
+ end
+ handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+ in play [] reconstrs end
end
@@ -734,20 +735,26 @@
val sound = is_type_enc_sound type_enc
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
- ((real_ms time_left
- |> (if slice < num_actual_slices - 1 then
- curry Real.min (time_frac * real_ms timeout)
- else
- I))
- * 0.001) |> seconds
+ case time_left of
+ SOME time_left =>
+ ((real_ms time_left
+ |> (if slice < num_actual_slices - 1 then
+ curry Real.min (time_frac * real_ms (the timeout))
+ else
+ I))
+ * 0.001)
+ |> seconds |> SOME
+ | NONE => NONE
val generous_slice_timeout =
- Time.+ (slice_timeout, atp_timeout_slack)
+ Option.map (curry Time.+ atp_timeout_slack) slice_timeout
val _ =
if debug then
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
" with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^
- string_from_time slice_timeout ^ "..."
+ plural_s num_facts ^
+ (case slice_timeout of
+ SOME timeout => " for " ^ string_from_time timeout
+ | NONE => "") ^ "..."
|> Output.urgent_message
else
()
@@ -778,7 +785,8 @@
fun ord_info () = atp_problem_term_order_info atp_problem
val ord = effective_term_order ctxt name
val full_proof = debug orelse isar_proofs
- val args = arguments ctxt full_proof extra slice_timeout
+ val args = arguments ctxt full_proof extra
+ (slice_timeout |> the_default one_day)
(ord, ord_info, sel_weights)
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
@@ -790,8 +798,8 @@
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_path
val ((output, run_time), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout
- Isabelle_System.bash_output command
+ time_limit generous_slice_timeout Isabelle_System.bash_output
+ command
|>> (if overlord then
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
@@ -805,7 +813,7 @@
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut =>
- (("", slice_timeout), ([], SOME TimedOut))
+ (("", the slice_timeout), ([], SOME TimedOut))
val outcome =
case outcome of
NONE =>
@@ -826,9 +834,13 @@
fun maybe_run_slice slice
(result as (cache, (_, run_time0, _, SOME _))) =
let
- val time_left = Time.- (timeout, Timer.checkRealTimer timer)
+ val time_left =
+ Option.map
+ (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+ timeout
in
- if Time.<= (time_left, Time.zeroTime) then
+ if time_left <> NONE andalso
+ Time.<= (the time_left, Time.zeroTime) then
result
else
run_slice time_left cache slice
@@ -979,22 +991,25 @@
(repair_monomorph_context max_mono_iters
default_max_mono_iters max_new_mono_instances
default_max_new_mono_instances)
- val ms = timeout |> Time.toMilliseconds
val slice_timeout =
- if slice < max_slices then
- Int.min (ms,
- Int.max (1000 * Config.get ctxt smt_slice_min_secs,
- Real.ceil (Config.get ctxt smt_slice_time_frac
- * Real.fromInt ms)))
- |> Time.fromMilliseconds
+ if slice < max_slices andalso timeout <> NONE then
+ let val ms = timeout |> the |> Time.toMilliseconds in
+ Int.min (ms,
+ Int.max (1000 * Config.get ctxt smt_slice_min_secs,
+ Real.ceil (Config.get ctxt smt_slice_time_frac
+ * Real.fromInt ms)))
+ |> Time.fromMilliseconds |> SOME
+ end
else
timeout
val num_facts = length facts
val _ =
if debug then
quote name ^ " slice " ^ string_of_int slice ^ " with " ^
- string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
- string_from_time slice_timeout ^ "..."
+ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+ (case slice_timeout of
+ SOME timeout => " for " ^ string_from_time timeout
+ | NONE => "") ^ "..."
|> Output.urgent_message
else
()
@@ -1004,7 +1019,7 @@
val state_facts = these (try (#facts o Proof.goal) state)
val (outcome, used_facts) =
SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
- |> SMT_Solver.smt_filter_apply slice_timeout
+ |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn => if Exn.is_interrupt exn then
reraise exn
@@ -1022,10 +1037,14 @@
| SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
| SOME SMT_Failure.Out_Of_Memory => true
| SOME (SMT_Failure.Other_Failure _) => true
- val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+ val timeout =
+ Option.map
+ (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+ timeout
in
if too_many_facts_perhaps andalso slice < max_slices andalso
- num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
+ num_facts > 0 andalso
+ (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
let
val new_num_facts =
Real.ceil (Config.get ctxt smt_slice_fact_frac
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 15 19:57:12 2012 +0100
@@ -23,7 +23,7 @@
type one_line_params =
play * string * (string * stature) list * minimize_command * int * int
type isar_params =
- bool * bool * Time.time * real * string Symtab.table
+ bool * bool * Time.time option * real * string Symtab.table
* (string * stature) list vector * int Symtab.table * string proof * thm
val smtN : string
@@ -592,7 +592,7 @@
in chain_proof NONE end
type isar_params =
- bool * bool * Time.time * real * string Symtab.table
+ bool * bool * Time.time option * real * string Symtab.table
* (string * stature) list vector * int Symtab.table * string proof * thm
fun isar_proof_text ctxt isar_proofs
@@ -607,7 +607,7 @@
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
- val preplay = preplay_timeout <> seconds 0.0
+ val preplay = preplay_timeout <> SOME Time.zeroTime
fun isar_proof_of () =
let
@@ -693,10 +693,12 @@
|> redirect_graph axioms tainted
|> map (do_inf true)
|> append assms
- |> (if not preplay andalso isar_shrink <= 1.0
- then pair (false, (true, seconds 0.0)) #> swap
- else shrink_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout (if isar_proofs then isar_shrink else 1000.0))
+ |> (if not preplay andalso isar_shrink <= 1.0 then
+ pair (false, (true, seconds 0.0)) #> swap
+ else
+ shrink_proof debug ctxt type_enc lam_trans preplay
+ preplay_timeout
+ (if isar_proofs then isar_shrink else 1000.0))
(* |>> reorder_proof_to_minimize_jumps (* ? *) *)
|>> chain_direct_proof
|>> kill_useless_labels_in_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 19:57:12 2012 +0100
@@ -68,7 +68,7 @@
{state, goal, subgoal, subgoal_count, facts} name =
let
val ctxt = Proof.context_of state
- val hard_timeout = Time.+ (timeout, timeout)
+ val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
val max_facts =
@@ -131,7 +131,7 @@
in (outcome_code, message) end
in
if mode = Auto_Try then
- let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+ let val (outcome_code, message) = time_limit timeout go () in
(outcome_code,
state
|> outcome_code = someN
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Sat Dec 15 19:57:12 2012 +0100
@@ -9,8 +9,8 @@
sig
type isar_step = Sledgehammer_Proof.isar_step
val shrink_proof :
- bool -> Proof.context -> string -> string -> bool -> Time.time -> real
- -> isar_step list -> isar_step list * (bool * (bool * Time.time))
+ bool -> Proof.context -> string -> string -> bool -> Time.time option
+ -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
end
structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
@@ -46,7 +46,7 @@
(* Timing *)
fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val no_time = (false, seconds 0.0)
+val no_time = (false, Time.zeroTime)
fun take_time timeout tac arg =
let val timing = Timing.start () in
(TimeLimit.timeLimit timeout tac arg;
@@ -59,15 +59,18 @@
fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
isar_shrink proof =
let
+ (* 60 seconds seems like a good interpreation of "no timeout" *)
+ val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+
(* handle metis preplay fail *)
local
open Unsynchronized
val metis_fail = ref false
in
fun handle_metis_fail try_metis () =
- try_metis () handle _ => (metis_fail := true ; SOME (seconds 0.0))
+ try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime)
fun get_time lazy_time =
- if !metis_fail then SOME (seconds 0.0) else Lazy.force lazy_time
+ if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
val metis_fail = fn () => !metis_fail
end
@@ -120,7 +123,7 @@
|> maps (thms_of_name ctxt)
fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
- if not preplay then (fn () => SOME (seconds 0.0)) else
+ if not preplay then (fn () => SOME Time.zeroTime) else
(case byline of
By_Metis fact_names =>
let
@@ -154,7 +157,7 @@
in
take_time timeout (fn () => goal tac)
end)
- | try_metis _ _ = (fn () => SOME (seconds 0.0) )
+ | try_metis _ _ = (fn () => SOME Time.zeroTime)
val try_metis_quietly = the_default NONE oo try oo try_metis
@@ -195,7 +198,7 @@
NONE => (NONE, metis_time)
| some_t12 =>
(SOME s12, metis_time
- |> replace (seconds 0.0 |> SOME |> Lazy.value) i
+ |> replace (Time.zeroTime |> SOME |> Lazy.value) i
|> replace (Lazy.value some_t12) j)
end))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Dec 15 18:48:58 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Dec 15 19:57:12 2012 +0100
@@ -19,6 +19,9 @@
val reserved_isar_keyword_table : unit -> unit Symtab.table
val thms_in_proof : string Symtab.table option -> thm -> string list
val thms_of_name : Proof.context -> string -> thm list
+ val one_day : Time.time
+ val one_year : Time.time
+ val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
end;
@@ -119,6 +122,12 @@
|> Source.exhaust
end
+val one_day = seconds (24.0 * 60.0 * 60.0)
+val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
+
+fun time_limit NONE = I
+ | time_limit (SOME delay) = TimeLimit.timeLimit delay
+
fun with_vanilla_print_mode f x =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f x