--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 02 23:29:05 2016 +0200
@@ -541,7 +541,7 @@
val facts = named_thms |> map (ref_of_str o fst o fst)
val fact_override = {add = facts, del = [], only = true}
fun my_timeout time_slice =
- timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
+ timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal
fun sledge_tac time_slice prover type_enc =
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
(override_params prover type_enc (my_timeout time_slice)) fact_override []
--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Apr 02 23:29:05 2016 +0200
@@ -989,7 +989,7 @@
val fudge_ms = 250
fun milliseconds_until_deadline deadline =
- Int.max (0, Time.toMilliseconds (Time.- (deadline, Time.now ())) - fudge_ms)
+ Int.max (0, Time.toMilliseconds (deadline - Time.now ()) - fudge_ms)
fun uncached_solve_any_problem overlord deadline max_threads max_solutions
problems =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 02 23:29:05 2016 +0200
@@ -251,7 +251,7 @@
fun check_deadline () =
let val t = Time.now () in
if Time.compare (t, deadline) <> LESS
- then raise Timeout.TIMEOUT (Time.- (t, time_start))
+ then raise Timeout.TIMEOUT (t - time_start)
else ()
end
@@ -540,7 +540,7 @@
val bit_width = if bits = 0 then 16 else bits + 1
val delay =
if unsound then
- unsound_delay_for_timeout (Time.- (deadline, Time.now ()))
+ unsound_delay_for_timeout (deadline - Time.now ())
else
0
val settings = [("solver", commas_quote kodkod_sat_solver),
@@ -986,9 +986,9 @@
else
let
val unknown_outcome = (unknownN, [])
- val deadline = Time.+ (Time.now (), timeout)
+ val deadline = Time.now () + timeout
val outcome as (outcome_code, _) =
- Timeout.apply (Time.+ (timeout, timeout_bonus))
+ Timeout.apply (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/Sledgehammer/async_manager_legacy.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sat Apr 02 23:29:05 2016 +0200
@@ -96,7 +96,7 @@
let
fun time_limit timeout_heap =
(case try Thread_Heap.min timeout_heap of
- NONE => Time.+ (Time.now (), max_wait_time)
+ NONE => Time.now () + max_wait_time
| SOME (time, _) => time)
(*action: find threads whose timeout is reached, and interrupt canceling threads*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 02 23:29:05 2016 +0200
@@ -460,7 +460,7 @@
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
- | Play_Timed_Out time => Time.> (time, Time.zeroTime)
+ | Play_Timed_Out time => time > Time.zeroTime
| Play_Failed => true)
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Sat Apr 02 23:29:05 2016 +0200
@@ -103,8 +103,8 @@
val merge_slack_factor = 1.5
fun adjust_merge_timeout max time =
- let val timeout = time_mult merge_slack_factor (Time.+ (merge_slack_time, time)) in
- if Time.< (max, timeout) then max else timeout
+ let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in
+ if max < timeout then max else timeout
end
val compress_degree = 2
@@ -171,7 +171,7 @@
val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
(* check if the modified step can be preplayed fast enough *)
- val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
+ val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l')
in
(case preplay_isar_step ctxt [] timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
@@ -215,7 +215,7 @@
| SOME times0 =>
let
val n = length labels
- val total_time = Library.foldl Time.+ (reference_time l, times0)
+ val total_time = Library.foldl (op +) (reference_time l, times0)
val timeout = adjust_merge_timeout preplay_timeout
(Time.fromReal (Time.toReal total_time / Real.fromInt n))
val meths_outcomess =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sat Apr 02 23:29:05 2016 +0200
@@ -45,7 +45,7 @@
fun minimize_half _ min_facts [] time = (min_facts, time)
| minimize_half mk_step min_facts (fact :: facts) time =
- (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth
+ (case preplay_isar_step_for_method ctxt [] (time + slack) meth
(mk_step (min_facts @ facts)) of
Played time' => minimize_half mk_step min_facts facts time'
| _ => minimize_half mk_step (fact :: min_facts) facts time)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Apr 02 23:29:05 2016 +0200
@@ -52,7 +52,7 @@
fun apply_f x =
let val timeout = !next_timeout in
- if Time.<= (timeout, min_timeout) then
+ if timeout <= min_timeout then
NONE
else
let val y = f timeout x in
@@ -188,7 +188,7 @@
fun add_preplay_outcomes Play_Failed _ = Play_Failed
| add_preplay_outcomes _ Play_Failed = Play_Failed
- | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
+ | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2)
| add_preplay_outcomes play1 play2 =
Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Apr 02 23:29:05 2016 +0200
@@ -168,7 +168,7 @@
fun normalize_scores _ [] = []
| normalize_scores max_facts xs =
- map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
+ map (apsnd (curry (op *) (1.0 / avg (map snd (take max_facts xs))))) xs
fun mesh_facts maybe_distinct _ max_facts [(_, (sels, unks))] =
map fst (take max_facts sels) @ take (max_facts - length sels) unks
@@ -655,7 +655,7 @@
(case try OS.FileSys.modTime (File.platform_path path) of
NONE => time_state
| SOME disk_time =>
- if Time.>= (memory_time, disk_time) then
+ if memory_time >= disk_time then
time_state
else
(disk_time,
@@ -700,7 +700,7 @@
val dirty_facts' =
(case try OS.FileSys.modTime (File.platform_path path) of
NONE => NONE
- | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
+ | SOME disk_time => if disk_time <= memory_time then dirty_facts else NONE)
val (banner, entries) =
(case dirty_facts' of
SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
@@ -1278,7 +1278,7 @@
let
val hard_timeout = time_mult learn_timeout_slack timeout
val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, hard_timeout)
+ val death_time = birth_time + hard_timeout
val desc = ("Machine learner for Sledgehammer", "")
in
Async_Manager_Legacy.thread MaShN birth_time death_time desc task
@@ -1328,7 +1328,7 @@
learn_timeout facts =
let
val timer = Timer.startRealTimer ()
- fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
+ fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout
val {access_G, ...} = peek_state ctxt
val is_in_access_G = is_fact_in_graph access_G o snd
@@ -1408,11 +1408,11 @@
val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
val learns = (name, parents, feats, deps) :: learns
val (learns, next_commit) =
- if Time.> (Timer.checkRealTimer timer, next_commit) then
+ if Timer.checkRealTimer timer > next_commit then
(commit false learns [] []; ([], next_commit_time ()))
else
(learns, next_commit)
- val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ val timed_out = Timer.checkRealTimer timer > learn_timeout
in
(learns, (num_nontrivial, next_commit, timed_out))
end
@@ -1443,11 +1443,11 @@
SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
| NONE => (num_nontrivial, relearns, name :: flops))
val (relearns, flops, next_commit) =
- if Time.> (Timer.checkRealTimer timer, next_commit) then
+ if Timer.checkRealTimer timer > next_commit then
(commit false [] relearns flops; ([], [], next_commit_time ()))
else
(relearns, flops, next_commit)
- val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+ val timed_out = Timer.checkRealTimer timer > learn_timeout
in
((relearns, flops), (num_nontrivial, next_commit, timed_out))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Apr 02 23:29:05 2016 +0200
@@ -250,7 +250,7 @@
* 0.001
|> seconds
val generous_slice_timeout =
- if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
+ if mode = MaSh then one_day else slice_timeout + atp_timeout_slack
val _ =
if debug then
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
@@ -328,14 +328,14 @@
val timer = Timer.startRealTimer ()
fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
- let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
- if Time.<= (time_left, Time.zeroTime) then
+ let val time_left = timeout - Timer.checkRealTimer timer in
+ if time_left <= Time.zeroTime then
result
else
run_slice time_left cache slice
|> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
format_type_enc) =>
- (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome),
+ (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome),
format_type_enc))
end
| maybe_run_slice _ result = result
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sat Apr 02 23:29:05 2016 +0200
@@ -130,8 +130,8 @@
val death = Timer.checkRealTimer timer
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
- val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
- val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+ val time_so_far = time_so_far + (death - birth)
+ val timeout = timeout - Timer.checkRealTimer timer
val too_many_facts_perhaps =
(case outcome of
@@ -143,7 +143,7 @@
| SOME (SMT_Failure.Other_Failure _) => true)
in
if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
- Time.> (timeout, Time.zeroTime) then
+ timeout > Time.zeroTime then
let
val new_num_facts =
Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Apr 02 23:29:05 2016 +0200
@@ -69,7 +69,7 @@
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
+ if is_none secs orelse 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
--- a/src/Pure/Concurrent/event_timer.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Sat Apr 02 23:29:05 2016 +0200
@@ -52,7 +52,7 @@
(case Requests.min requests of
NONE => NONE
| SOME (time, entries) =>
- if Time.< (t0, time) then NONE
+ if t0 < time then NONE
else
let
val (rest, (_, event)) = split_last entries;
--- a/src/Pure/Concurrent/future.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/future.ML Sat Apr 02 23:29:05 2016 +0200
@@ -126,7 +126,7 @@
Multithreading.sync_wait NONE NONE cond lock;
fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
- Multithreading.sync_wait NONE (SOME (Time.+ (Time.now (), timeout))) cond lock;
+ Multithreading.sync_wait NONE (SOME (Time.now () + timeout)) cond lock;
fun signal cond = (*requires SYNCHRONIZED*)
ConditionVar.signal cond;
@@ -280,7 +280,7 @@
fun scheduler_next () = (*requires SYNCHRONIZED*)
let
val now = Time.now ();
- val tick = Time.<= (Time.+ (! last_round, next_round), now);
+ val tick = ! last_round + next_round <= now;
val _ = if tick then last_round := now else ();
--- a/src/Pure/Concurrent/mailbox.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/mailbox.ML Sat Apr 02 23:29:05 2016 +0200
@@ -25,7 +25,7 @@
fun receive timeout (Mailbox mailbox) =
Synchronized.timed_access mailbox
- (fn _ => Option.map (fn t => (Time.+ (Time.now (), t))) timeout)
+ (fn _ => Option.map (fn t => Time.now () + t) timeout)
(fn [] => NONE | msgs => SOME (msgs, []))
|> these |> rev;
--- a/src/Pure/Concurrent/multithreading.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Sat Apr 02 23:29:05 2016 +0200
@@ -127,10 +127,10 @@
fun tracing_time detailed time =
tracing
(if not detailed then 5
- else if Time.>= (time, seconds 1.0) then 1
- else if Time.>= (time, seconds 0.1) then 2
- else if Time.>= (time, seconds 0.01) then 3
- else if Time.>= (time, seconds 0.001) then 4 else 5);
+ else if time >= seconds 1.0 then 1
+ else if time >= seconds 0.1 then 2
+ else if time >= seconds 0.01 then 3
+ else if time >= seconds 0.001 then 4 else 5);
fun real_time f x =
let
--- a/src/Pure/Concurrent/task_queue.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Sat Apr 02 23:29:05 2016 +0200
@@ -139,7 +139,7 @@
let
val start = Time.now ();
val result = Exn.capture (restore_attributes e) ();
- val t = Time.- (Time.now (), start);
+ val t = Time.now () - start;
val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
in Exn.release result end) ();
@@ -167,14 +167,14 @@
(* timing *)
fun running task =
- update_timing (fn t => fn (a, b, ds) => (Time.+ (a, t), b, ds)) task;
+ update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task;
fun joining task =
- update_timing (fn t => fn (a, b, ds) => (Time.- (a, t), b, ds)) task;
+ update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task;
fun waiting task deps =
update_timing (fn t => fn (a, b, ds) =>
- (Time.- (a, t), Time.+ (b, t),
+ (a - t, b + t,
if ! Multithreading.trace > 0
then fold (insert (op =) o name_of_task) deps ds else ds)) task;
--- a/src/Pure/Concurrent/timeout.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/timeout.ML Sat Apr 02 23:29:05 2016 +0200
@@ -23,7 +23,7 @@
val start = Time.now ();
val request =
- Event_Timer.request (Time.+ (start, timeout))
+ Event_Timer.request (start + timeout)
(fn () => Standard_Thread.interrupt_unsynchronized self);
val result =
Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
@@ -33,7 +33,7 @@
val test = Exn.capture Multithreading.interrupted ();
in
if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
- then raise TIMEOUT (Time.- (stop, start))
+ then raise TIMEOUT (stop - start)
else (Exn.release test; Exn.release result)
end);
--- a/src/Pure/General/timing.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/General/timing.ML Sat Apr 02 23:29:05 2016 +0200
@@ -76,7 +76,7 @@
val min_time = Time.fromMilliseconds 1;
-fun is_relevant_time time = Time.>= (time, min_time);
+fun is_relevant_time time = time >= min_time;
fun is_relevant {elapsed, cpu, gc} =
is_relevant_time elapsed orelse
--- a/src/Pure/Isar/toplevel.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Apr 02 23:29:05 2016 +0200
@@ -651,7 +651,7 @@
val timings = map get_timing trs;
in
if forall is_some timings then
- SOME (fold (curry Time.+ o the) timings Time.zeroTime)
+ SOME (fold (curry (op +) o the) timings Time.zeroTime)
else NONE
end;
--- a/src/Pure/PIDE/command.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/PIDE/command.ML Sat Apr 02 23:29:05 2016 +0200
@@ -417,7 +417,7 @@
in
(case delay of
NONE => fork ()
- | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
+ | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
end
else run_process execution_id exec_id print_process;
--- a/src/Pure/PIDE/document.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/PIDE/document.ML Sat Apr 02 23:29:05 2016 +0200
@@ -464,7 +464,7 @@
val delay = seconds (Options.default_real "editor_execution_delay");
val _ = Future.cancel delay_request;
- val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
+ val delay_request' = Event_Timer.future (Time.now () + delay);
fun finished_import (name, (node, _)) =
finished_result node orelse is_some (loaded_theory name);
--- a/src/Pure/Tools/build.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Tools/build.ML Sat Apr 02 23:29:05 2016 +0200
@@ -22,7 +22,7 @@
(case Markup.parse_command_timing_properties props of
SOME ({file, offset, name}, time) =>
Symtab.map_default (file, Inttab.empty)
- (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
+ (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
| NONE => I);
fun approximative_id name pos =
@@ -83,7 +83,7 @@
val {elapsed, ...} = Markup.parse_timing_properties args;
val is_significant =
Timing.is_relevant_time elapsed andalso
- Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
+ elapsed >= Options.default_seconds "command_timing_threshold";
in
if is_significant then
(case approximative_id name pos of