--- a/src/Doc/Nitpick/document/root.tex Thu Dec 19 10:15:12 2013 +0100
+++ b/src/Doc/Nitpick/document/root.tex Thu Dec 19 13:43:21 2013 +0100
@@ -1892,9 +1892,8 @@
\item[\labelitemi] \qtybf{int\_range}: An integer (e.g., 3) or a range
of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
\item[\labelitemi] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
-\item[\labelitemi] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
-(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
-($\infty$ seconds).
+\item[\labelitemi] \qtybf{float}: An floating-point number (e.g., 0.5 or 60)
+expressing a number of seconds.
\item[\labelitemi] \qtybf{const\/}: The name of a HOL constant.
\item[\labelitemi] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
\item[\labelitemi] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
@@ -2531,7 +2530,7 @@
\label{timeouts}
\begin{enum}
-\opdefault{timeout}{float\_or\_none}{\upshape 30}
+\opdefault{timeout}{float}{\upshape 30}
Specifies the maximum number of seconds that the \textbf{nitpick} command should
spend looking for a counterexample. Nitpick tries to honor this constraint as
well as it can but offers no guarantees. For automatic runs, the ``Auto Time
@@ -2541,7 +2540,7 @@
\nopagebreak
{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
-\opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
+\opdefault{tac\_timeout}{float}{\upshape 0.5}
Specifies the maximum number of seconds that should be used by internal
tactics---\textit{lexicographic\_order} and \textit{size\_change} when checking
whether a (co)in\-duc\-tive predicate is well-founded, \textit{auto} tactic when
--- a/src/Doc/Sledgehammer/document/root.tex Thu Dec 19 10:15:12 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Dec 19 13:43:21 2013 +0100
@@ -789,13 +789,11 @@
\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
\textit{smart}.
\item[\labelitemi] \qtybf{int\/}: An integer.
-%\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5).
+\item[\labelitemi] \qtybf{float}: A floating-point number (e.g., 2.5 or 60)
+expressing a number of seconds.
\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
(e.g., 0.6 0.95).
\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
-\item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or
-0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$
-seconds).
\end{enum}
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
@@ -1356,11 +1354,11 @@
\label{timeouts}
\begin{enum}
-\opdefault{timeout}{float\_or\_none}{\upshape 30}
+\opdefault{timeout}{float}{\upshape 30}
Specifies the maximum number of seconds that the automatic provers should spend
searching for a proof. This excludes problem preparation and is a soft limit.
-\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
+\opdefault{preplay\_timeout}{float}{\upshape 3}
Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
should spend trying to ``preplay'' the found proof. If this option is set to 0,
no preplaying takes place, and no timing information is displayed next to the
--- a/src/HOL/TPTP/mash_eval.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Dec 19 13:43:21 2013 +0100
@@ -176,7 +176,7 @@
"slice" |> not slice ? prefix "dont_",
"type_enc = " ^ the_default "smart" type_enc,
"lam_trans = " ^ the_default "smart" lam_trans,
- "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout),
+ "timeout = " ^ ATP_Util.string_of_time timeout,
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val _ = print " * * *";
val _ = print ("Options: " ^ commas options);
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 19 13:43:21 2013 +0100
@@ -172,7 +172,7 @@
val is_problem_trivially_false : problem -> bool
val problems_equivalent : problem * problem -> bool
val solve_any_problem :
- bool -> bool -> Time.time option -> int -> int -> problem list -> outcome
+ bool -> bool -> Time.time -> int -> int -> problem list -> outcome
end;
structure Kodkod : KODKOD =
@@ -983,10 +983,7 @@
val fudge_ms = 250
fun milliseconds_until_deadline deadline =
- case deadline of
- NONE => ~1
- | SOME time =>
- Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms)
+ Int.max (0, Time.toMilliseconds (Time.- (deadline, Time.now ())) - fudge_ms)
fun uncached_solve_any_problem overlord deadline max_threads max_solutions
problems =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 19 13:43:21 2013 +0100
@@ -43,8 +43,8 @@
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
- timeout: Time.time option,
- tac_timeout: Time.time option,
+ timeout: Time.time,
+ tac_timeout: Time.time,
max_threads: int,
show_datatypes: bool,
show_skolems: bool,
@@ -129,8 +129,8 @@
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
- timeout: Time.time option,
- tac_timeout: Time.time option,
+ timeout: Time.time,
+ tac_timeout: Time.time,
max_threads: int,
show_datatypes: bool,
show_skolems: bool,
@@ -193,14 +193,10 @@
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
-fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
- | unsound_delay_for_timeout (SOME timeout) =
- Int.max (0, Int.min (max_unsound_delay_ms,
- Time.toMilliseconds timeout
- * max_unsound_delay_percent div 100))
-
-fun passed_deadline NONE = false
- | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
+fun unsound_delay_for_timeout timeout =
+ Int.max (0, Int.min (max_unsound_delay_ms,
+ Time.toMilliseconds timeout
+ * max_unsound_delay_percent div 100))
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
@@ -258,7 +254,10 @@
val print_v = pprint_v o K o plazy
fun check_deadline () =
- if passed_deadline deadline then raise TimeLimit.TimeOut else ()
+ if Time.compare (Time.now (), deadline) <> LESS then
+ raise TimeLimit.TimeOut
+ else
+ ()
val (def_assm_ts, nondef_assm_ts) =
if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
@@ -385,8 +384,8 @@
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type ctxt T orelse is_bit_type T
fun is_type_actually_monotonic T =
- time_limit tac_timeout (formulas_monotonic hol_ctxt binarize T)
- (nondef_ts, def_ts)
+ TimeLimit.timeLimit tac_timeout (formulas_monotonic hol_ctxt binarize T)
+ (nondef_ts, def_ts)
handle TimeLimit.TimeOut => false
fun is_type_kind_of_monotonic T =
case triple_lookup (type_match thy) monos T of
@@ -579,8 +578,7 @@
val bit_width = if bits = 0 then 16 else bits + 1
val delay =
if unsound then
- Option.map (fn time => Time.- (time, Time.now ())) deadline
- |> unsound_delay_for_timeout
+ unsound_delay_for_timeout (Time.- (deadline, Time.now ()))
else
0
val settings = [("solver", commas_quote kodkod_sat_solver),
@@ -1075,10 +1073,9 @@
else
let
val unknown_outcome = (unknownN, state)
- val deadline = Option.map (curry Time.+ (Time.now ())) timeout
+ val deadline = Time.+ (Time.now (), timeout)
val outcome as (outcome_code, _) =
- time_limit (if debug orelse is_none timeout then NONE
- else SOME (Time.+ (the timeout, timeout_bonus)))
+ TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
(pick_them_nits_in_term deadline state params mode i n step subst
def_assm_ts nondef_assm_ts) orig_t
handle TOO_LARGE (_, details) =>
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 19 13:43:21 2013 +0100
@@ -29,7 +29,7 @@
star_linear_preds: bool,
total_consts: bool option,
needs: term list option,
- tac_timeout: Time.time option,
+ tac_timeout: Time.time,
evals: term list,
case_names: (string * int) list,
def_tables: const_table * const_table,
@@ -271,7 +271,7 @@
star_linear_preds: bool,
total_consts: bool option,
needs: term list option,
- tac_timeout: Time.time option,
+ tac_timeout: Time.time,
evals: term list,
case_names: (string * int) list,
def_tables: const_table * const_table,
@@ -2069,8 +2069,7 @@
#> the #> Goal.finish ctxt) goal
val max_cached_wfs = 50
-val cached_timeout =
- Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
+val cached_timeout = Synchronized.var "Nitpick_HOL.cached_timeout" Time.zeroTime
val cached_wf_props =
Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Dec 19 13:43:21 2013 +0100
@@ -226,8 +226,8 @@
lookup_assigns read prefix "" (space_explode " ")
fun lookup_time name =
case lookup name of
- SOME s => parse_time_option name s
- | NONE => NONE
+ SOME s => parse_time name s
+ | NONE => Time.zeroTime
val read_type_polymorphic =
Syntax.read_typ ctxt #> Logic.mk_type
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
@@ -269,7 +269,7 @@
val peephole_optim = lookup_bool "peephole_optim"
val datatype_sym_break = lookup_int "datatype_sym_break"
val kodkod_sym_break = lookup_int "kodkod_sym_break"
- val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
+ val timeout = lookup_time "timeout"
val tac_timeout = lookup_time "tac_timeout"
val max_threads =
if mode = Normal then Int.max (0, lookup_int "max_threads") else 1
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 19 13:43:21 2013 +0100
@@ -41,7 +41,7 @@
-> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
-> Pretty.T * bool
val prove_hol_model :
- scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
+ scope -> Time.time -> nut list -> nut list -> nut NameTable.table
-> Kodkod.raw_bound list -> term -> bool option
end;
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Dec 19 13:43:21 2013 +0100
@@ -533,9 +533,9 @@
string_for_vars ", " (sort int_ord xs))
|> space_implode "\n"))
-(* The ML solver timeout should correspond more or less to the overhead of
- invoking an external prover. *)
-val ml_solver_timeout = SOME (seconds 0.02)
+(* The ML solver timeout should correspond more or less to the overhead of invoking an external
+ prover. *)
+val ml_solver_timeout = seconds 0.02
fun solve tac_timeout max_var (comps, clauses) =
let
@@ -560,11 +560,12 @@
|> List.partition (member (op =) ["dptsat", "dpll"] o fst)
val res =
if null nonml_solvers then
- time_limit tac_timeout (snd (hd ml_solvers)) prop
+ TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop
else
- time_limit ml_solver_timeout (snd (hd ml_solvers)) prop
+ TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop
handle TimeLimit.TimeOut =>
- time_limit tac_timeout (SatSolver.invoke_solver "auto") prop
+ TimeLimit.timeLimit tac_timeout
+ (SatSolver.invoke_solver "auto") prop
in
case res of
SatSolver.SATISFIABLE assigns => do_assigns assigns
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Dec 19 13:43:21 2013 +0100
@@ -211,11 +211,11 @@
fun run_all_tests () =
let
- val {debug, overlord, ...} = Nitpick_Isar.default_params @{theory} []
+ val {debug, overlord, timeout, ...} = Nitpick_Isar.default_params @{theory} []
val max_threads = 1
val max_solutions = 1
in
- case Kodkod.solve_any_problem debug overlord NONE max_threads max_solutions
+ case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions
(map (problem_for_nut @{context}) tests) of
Kodkod.Normal ([], _, _) => ()
| _ => error "Tests failed."
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 19 13:43:21 2013 +0100
@@ -51,7 +51,7 @@
val serial_commas : string -> string list -> string list
val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
val parse_bool_option : bool -> string -> string -> bool option
- val parse_time_option : string -> string -> Time.time option
+ val parse_time : string -> string -> Time.time
val string_of_time : Time.time -> string
val nat_subscript : int -> string
val flip_polarity : polarity -> polarity
@@ -71,8 +71,7 @@
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> string * typ -> term -> term
val eta_expand : typ list -> term -> int -> term
- val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
- val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
+ val DETERM_TIMEOUT : Time.time -> tactic -> tactic
val indent_size : int
val pstrs : string -> Pretty.T list
val unyxml : string -> string
@@ -238,7 +237,7 @@
p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps
val parse_bool_option = Sledgehammer_Util.parse_bool_option
-val parse_time_option = Sledgehammer_Util.parse_time_option
+val parse_time = Sledgehammer_Util.parse_time
val string_of_time = ATP_Util.string_of_time
val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
@@ -296,10 +295,9 @@
val monomorphic_term = ATP_Util.monomorphic_term
val specialize_type = ATP_Util.specialize_type
val eta_expand = ATP_Util.eta_expand
-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) ()))
+ Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ()))
val indent_size = 2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 19 13:43:21 2013 +0100
@@ -120,8 +120,7 @@
("dont_try0_isar", "isar_try0")]
val params_not_for_minimize =
- ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice",
- "minimize"];
+ ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
val property_dependent_params = ["provers", "timeout"]
@@ -225,40 +224,40 @@
val lookup = Option.map implode_param o AList.lookup (op =) raw_params
val lookup_string = the_default "" o lookup
fun general_lookup_bool option default_value name =
- case lookup name of
+ (case lookup name of
SOME s => parse_bool_option option name s
- | NONE => default_value
+ | NONE => default_value)
val lookup_bool = the o general_lookup_bool false (SOME false)
fun lookup_time name =
- case lookup name of
- SOME s => parse_time_option name s
- | NONE => NONE
+ (case lookup name of
+ SOME s => parse_time name s
+ | NONE => Time.zeroTime)
fun lookup_int name =
- case lookup name of
+ (case lookup name of
NONE => 0
- | SOME s => case Int.fromString s of
- SOME n => n
- | NONE => error ("Parameter " ^ quote name ^
- " must be assigned an integer value.")
+ | SOME s =>
+ (case Int.fromString s of
+ SOME n => n
+ | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.")))
fun lookup_real name =
- case lookup name of
+ (case lookup name of
NONE => 0.0
- | SOME s => case Real.fromString s of
- SOME n => n
- | NONE => error ("Parameter " ^ quote name ^
- " must be assigned a real value.")
+ | SOME s =>
+ (case Real.fromString s of
+ SOME n => n
+ | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value.")))
fun lookup_real_pair name =
- case lookup name of
+ (case lookup name of
NONE => (0.0, 0.0)
- | SOME s => case s |> space_explode " " |> map Real.fromString of
- [SOME r1, SOME r2] => (r1, r2)
- | _ => error ("Parameter " ^ quote name ^
- " must be assigned a pair of floating-point \
- \values (e.g., \"0.6 0.95\")")
+ | SOME s =>
+ (case s |> space_explode " " |> map Real.fromString of
+ [SOME r1, SOME r2] => (r1, r2)
+ | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \
+ \values (e.g., \"0.6 0.95\")")))
fun lookup_option lookup' name =
- case lookup name of
+ (case lookup name of
SOME "smart" => NONE
- | _ => SOME (lookup' name)
+ | _ => SOME (lookup' name))
val debug = mode <> Auto_Try andalso lookup_bool "debug"
val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
@@ -291,9 +290,8 @@
val isar_try0 = lookup_bool "isar_try0"
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"
- val preplay_timeout =
- if mode = Auto_Try then SOME Time.zeroTime else lookup_time "preplay_timeout"
+ val timeout = lookup_time "timeout"
+ val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 19 13:43:21 2013 +0100
@@ -1070,7 +1070,7 @@
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths =
if is_mash_enabled () then
- launch_thread (timeout |> the_default one_day) (fn () =>
+ launch_thread timeout (fn () =>
let
val thy = Proof_Context.theory_of ctxt
val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t] |> map fst
@@ -1095,12 +1095,11 @@
val commit_timeout = seconds 30.0
(* The timeout is understood in a very relaxed fashion. *)
-fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
- save auto_level run_prover learn_timeout facts =
+fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover save auto_level
+ run_prover learn_timeout facts =
let
val timer = Timer.startRealTimer ()
- fun next_commit_time () =
- Time.+ (Timer.checkRealTimer timer, commit_timeout)
+ fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {access_G, ...} = peek_state ctxt overlord I
val is_in_access_G = is_fact_in_graph access_G o snd
val no_new_facts = forall is_in_access_G facts
@@ -1182,10 +1181,7 @@
(commit false learns [] []; ([], next_commit_time ()))
else
(learns, next_commit)
- val timed_out =
- case learn_timeout of
- SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
- | NONE => false
+ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
in (learns, (n, next_commit, timed_out)) end
val n =
if no_new_facts then
@@ -1215,10 +1211,7 @@
([], [], next_commit_time ()))
else
(relearns, flops, next_commit)
- val timed_out =
- case learn_timeout of
- SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
- | NONE => false
+ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
in ((relearns, flops), (n, next_commit, timed_out)) end
val n =
if not run_prover then
@@ -1267,15 +1260,13 @@
val num_facts = length facts
val prover = hd provers
fun learn auto_level run_prover =
- mash_learn_facts ctxt params prover true auto_level run_prover NONE facts
+ mash_learn_facts ctxt params prover true auto_level run_prover one_year 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 ^
- (case timeout of
- SOME timeout => " timeout: " ^ string_of_time timeout
- | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
+ ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+ " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^
+ ").\n\nCollecting Isar proofs first..."
|> Output.urgent_message;
learn 1 false;
"Now collecting automatic proofs. This may take several hours. You can \
@@ -1305,10 +1296,8 @@
Sledgehammer and Try. *)
val min_secs_for_learning = 15
-fun relevant_facts ctxt
- (params as {overlord, blocking, learn, fact_filter, timeout, ...})
- prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t
- facts =
+fun relevant_facts ctxt (params as {overlord, blocking, learn, fact_filter, timeout, ...}) prover
+ max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
if not (subset (op =) (the_list fact_filter, fact_filters)) then
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
else if only then
@@ -1320,16 +1309,11 @@
else
let
fun maybe_launch_thread () =
- if not blocking andalso
- not (Async_Manager.has_running_threads MaShN) andalso
- (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 true 2
- false timeout facts))
+ if not blocking 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
+ (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
end
else
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 19 13:43:21 2013 +0100
@@ -61,13 +61,8 @@
let
val _ =
print silent (fn () =>
- "Testing " ^ n_facts (map fst facts) ^
- (if verbose then
- case timeout of
- SOME timeout => " (timeout: " ^ string_of_time timeout ^ ")"
- | _ => ""
- else
- "") ^ "...")
+ "Testing " ^ n_facts (map fst facts) ^
+ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
val params =
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
@@ -103,11 +98,9 @@
part of the timeout. *)
val slack_msecs = 200
-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
+fun new_timeout timeout run_time =
+ Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds
(* The linear algorithm usually outperforms the binary algorithm when over 60%
of the facts are actually needed. The binary algorithm is much more
@@ -128,14 +121,15 @@
let
fun min _ [] p = p
| min timeout (x :: xs) (seen, result) =
- case test timeout (xs @ seen) of
- result as {outcome = NONE, used_facts, run_time, ...}
- : prover_result =>
+ (case test timeout (xs @ seen) of
+ result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
min (new_timeout timeout run_time)
(filter_used_facts true used_facts xs)
(filter_used_facts false used_facts seen, result)
- | _ => min timeout xs (x :: seen, result)
- in min timeout xs ([], result) end
+ | _ => min timeout xs (x :: seen, result))
+ in
+ min timeout xs ([], result)
+ end
fun binary_minimize test timeout result xs =
let
@@ -188,8 +182,8 @@
| p => p
end
-fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
- i n state goal preplay0 facts =
+fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
+ preplay0 facts =
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
@@ -222,24 +216,18 @@
message, message_tail))
end
| {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 |> the_default (seconds 60.0)) div 1000) ^
- "\").", ""))
+ (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) ^ "\").", ""))
| {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg => (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, ""))
end
fun adjust_reconstructor_params override_params
- ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict,
- lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
- fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
- isar_compress, isar_try0, slice, minimize, timeout, preplay_timeout,
- expect} : params) =
+ ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
+ uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
+ max_new_mono_instances, isar_proofs, isar_compress, isar_try0, slice, minimize, timeout,
+ preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -284,20 +272,18 @@
(case Lazy.force preplay of
Played (reconstr as Metis _, timeout) =>
if isar_proofs = SOME true then
- (* Cheat: Assume the selected ATP is as fast as "metis" for
- the goal it proved itself. *)
- (can_min_fast_enough timeout,
- (isar_proof_reconstructor ctxt name, params))
+ (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
+ itself. *)
+ (can_min_fast_enough timeout, (isar_proof_reconstructor ctxt name, params))
else if can_min_fast_enough timeout then
(true, extract_reconstructor params reconstr
||> (fn override_params =>
- adjust_reconstructor_params override_params
- params))
+ adjust_reconstructor_params override_params params))
else
(prover_fast_enough (), (name, params))
| Played (SMT, timeout) =>
- (* Cheat: Assume the original prover is as fast as "smt" for
- the goal it proved itself *)
+ (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
+ itself. *)
(can_min_fast_enough timeout, (name, params))
| _ => (prover_fast_enough (), (name, params)),
preplay)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Dec 19 13:43:21 2013 +0100
@@ -9,7 +9,7 @@
signature SLEDGEHAMMER_PROOF =
sig
type label = string * int
- type facts = label list * string list (* local & global facts *)
+ type facts = label list * string list (* local and global facts *)
datatype isar_qualifier = Show | Then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 13:43:21 2013 +0100
@@ -40,8 +40,8 @@
isar_try0 : bool,
slice : bool,
minimize : bool option,
- timeout : Time.time option,
- preplay_timeout : Time.time option,
+ timeout : Time.time,
+ preplay_timeout : Time.time,
expect : string}
type prover_problem =
@@ -281,8 +281,8 @@
isar_try0 : bool,
slice : bool,
minimize : bool option,
- timeout : Time.time option,
- preplay_timeout : Time.time option,
+ timeout : Time.time,
+ preplay_timeout : Time.time,
expect : string}
type prover_problem =
@@ -378,7 +378,9 @@
let
val {context = ctxt, facts, goal} = Proof.goal state
val full_tac = Method.insert_tac facts i THEN tac ctxt i
- in time_limit timeout (try (Seq.pull o full_tac)) goal end
+ in
+ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
+ end
fun tac_of_reconstructor (Metis (type_enc, lam_trans)) =
metis_tac [type_enc] lam_trans
@@ -401,24 +403,20 @@
if member (op =) reconstrs preferred then preferred
else List.last reconstrs
in
- if timeout = SOME Time.zeroTime then
+ if timeout = Time.zeroTime then
Play_Timed_Out (get_preferred reconstrs, Time.zeroTime)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
val ths = pairs |> sort_wrt (fst o fst) |> map snd
fun play [] [] = Play_Failed (get_preferred reconstrs)
- | play timed_outs [] =
- Play_Timed_Out (get_preferred timed_outs, timeout |> the_default Time.zeroTime (* wrong *))
+ | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout)
| play timed_out (reconstr :: reconstrs) =
let
val _ =
if verbose then
- "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
- (case timeout of
- SOME timeout => " for " ^ string_of_time timeout
- | NONE => "") ^ "..."
- |> Output.urgent_message
+ Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
+ "\" for " ^ string_of_time timeout ^ "...")
else
()
val timer = Timer.startRealTimer ()
@@ -664,27 +662,20 @@
val sound = is_type_enc_sound type_enc
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
- 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
+ (real_ms time_left
+ |> (if slice < num_actual_slices - 1 then
+ curry Real.min (time_frac * real_ms timeout)
+ else
+ I))
+ * 0.001
+ |> seconds
val generous_slice_timeout =
- if mode = MaSh then NONE
- else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
+ if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
val _ =
if debug then
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
" with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^
- (case slice_timeout of
- SOME timeout => " for " ^ string_of_time timeout
- | NONE => "") ^ "..."
+ plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
|> Output.urgent_message
else
()
@@ -715,8 +706,8 @@
val ord = effective_term_order ctxt name
val full_proof = isar_proofs |> the_default (mode = Minimize)
val args =
- arguments ctxt full_proof extra (slice_timeout |> the_default one_day)
- (File.shell_path prob_path) (ord, ord_info, sel_weights)
+ arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path)
+ (ord, ord_info, sel_weights)
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
|> enclose "TIMEFORMAT='%3R'; { time " " ; }"
@@ -726,7 +717,7 @@
|> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
|> File.write_list prob_path
val ((output, run_time), (atp_proof, outcome)) =
- time_limit generous_slice_timeout Isabelle_System.bash_output command
+ TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
|>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
|> fst |> split_time
|> (fn accum as (output, _) =>
@@ -734,7 +725,7 @@
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
|>> atp_proof_of_tstplike_proof atp_problem
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
- handle TimeLimit.TimeOut => (("", the slice_timeout), ([], SOME TimedOut))
+ handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
val outcome =
case outcome of
NONE =>
@@ -759,13 +750,9 @@
fun maybe_run_slice slice
(result as (cache, (_, run_time0, _, _, SOME _))) =
let
- val time_left =
- Option.map
- (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
- timeout
+ val time_left = Time.- (timeout, Timer.checkRealTimer timer)
in
- if time_left <> NONE andalso
- Time.<= (the time_left, Time.zeroTime) then
+ if Time.<= (time_left, Time.zeroTime) then
result
else
run_slice time_left cache slice
@@ -935,24 +922,21 @@
let
val timer = Timer.startRealTimer ()
val slice_timeout =
- if slice < max_slices andalso timeout <> NONE then
- let val ms = timeout |> the |> Time.toMilliseconds in
+ if slice < max_slices then
+ let val ms = Time.toMilliseconds timeout 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
+ |> Time.fromMilliseconds
end
else
timeout
val num_facts = length weighted_facts
val _ =
if debug then
- quote name ^ " slice " ^ string_of_int slice ^ " with " ^
- string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
- (case slice_timeout of
- SOME timeout => " for " ^ string_of_time timeout
- | NONE => "") ^ "..."
+ quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
+ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
|> Output.urgent_message
else
()
@@ -961,7 +945,7 @@
if debug then Output.urgent_message "Invoking SMT solver..." else ()
val (outcome, used_facts) =
SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
- |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
+ |> SMT_Solver.smt_filter_apply slice_timeout
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn => if Exn.is_interrupt exn then
reraise exn
@@ -979,18 +963,13 @@
| SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
| SOME SMT_Failure.Out_Of_Memory => true
| SOME (SMT_Failure.Other_Failure _) => true
- val timeout =
- Option.map
- (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
- timeout
+ val timeout = Time.- (timeout, Timer.checkRealTimer timer)
in
- if too_many_facts_perhaps andalso slice < max_slices andalso
- num_facts > 0 andalso
- (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
+ if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
+ Time.> (timeout, Time.zeroTime) then
let
val new_num_facts =
- Real.ceil (Config.get ctxt smt_slice_fact_frac
- * Real.fromInt num_facts)
+ Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
val weighted_factss as (new_fact_filter, _) :: _ =
weighted_factss
|> rotate_one
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 13:43:21 2013 +0100
@@ -14,8 +14,7 @@
type one_line_params = Sledgehammer_Reconstructor.one_line_params
type isar_params =
- bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
- thm
+ bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string
val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int ->
@@ -190,8 +189,7 @@
end
type isar_params =
- bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
- thm
+ bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
val arith_methodss =
[[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
@@ -214,7 +212,7 @@
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
|> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
val one_line_proof = one_line_proof_text 0 one_line_params
- val do_preplay = preplay_timeout <> SOME Time.zeroTime
+ val do_preplay = preplay_timeout <> Time.zeroTime
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
@@ -342,9 +340,6 @@
and isar_proof outer fix assms lems infs =
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
- (* 60 seconds seems like a reasonable interpreation of "no timeout" *)
- val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
-
val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
refute_graph
(*
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 19 13:43:21 2013 +0100
@@ -19,10 +19,9 @@
val timeoutN : string
val unknownN : string
val string_of_factss : (string * fact list) list -> string
- val run_sledgehammer :
- params -> mode -> (string -> unit) option -> int -> fact_override
- -> ((string * string list) list -> string -> minimize_command)
- -> Proof.state -> bool * (string * Proof.state)
+ val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
+ ((string * string list) list -> string -> minimize_command) -> Proof.state ->
+ bool * (string * Proof.state)
end;
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
@@ -65,13 +64,13 @@
(if blocking then "."
else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
-fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...})
- mode output_result minimize_command only learn
- {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
+fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
+ output_result minimize_command only learn
+ {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
let
val ctxt = Proof.context_of state
- val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
+ val hard_timeout = time_mult 3.0 timeout
val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, hard_timeout)
@@ -173,7 +172,7 @@
in (outcome_code, message) end
in
if mode = Auto_Try then
- let val (outcome_code, message) = time_limit timeout go () in
+ let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
(outcome_code,
state
|> outcome_code = someN
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 19 13:43:21 2013 +0100
@@ -17,15 +17,13 @@
val infinite_timeout : Time.time
val time_mult : real -> Time.time -> Time.time
val parse_bool_option : bool -> string -> string -> bool option
- val parse_time_option : string -> string -> Time.time option
+ val parse_time : string -> string -> Time.time
val subgoal_count : Proof.state -> int
val reserved_isar_keyword_table : unit -> unit Symtab.table
- val thms_in_proof :
- (string Symtab.table * string Symtab.table) option -> thm -> string list
+ val thms_in_proof : (string Symtab.table * 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
val hackish_string_of_term : Proof.context -> term -> string
val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
@@ -86,15 +84,14 @@
val has_junk =
exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
-fun parse_time_option _ "none" = NONE
- | parse_time_option name s =
- let val secs = if has_junk s then NONE else Real.fromString s in
- if is_none secs orelse Real.< (the secs, 0.0) then
- error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
- \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
- else
- SOME (seconds (the secs))
- end
+fun parse_time name s =
+ let val secs = if has_junk s then NONE else Real.fromString s in
+ if is_none secs orelse Real.< (the secs, 0.0) then
+ error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
+ \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
+ else
+ seconds (the secs)
+ end
val subgoal_count = Try.subgoal_count
@@ -144,9 +141,6 @@
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