--- a/doc-src/IsarImplementation/Thy/ML.thy Tue Nov 02 20:32:33 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Nov 02 21:24:07 2010 +0100
@@ -1274,6 +1274,30 @@
*}
+subsection {* Time *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type Time.time} \\
+ @{index_ML seconds: "real -> Time.time"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type @{ML_type Time.time} represents time abstractly according
+ to the SML97 basis library definition. This is adequate for
+ internal ML operations, but awkward in concrete time specifications.
+
+ \item @{ML seconds}~@{text "s"} turns the concrete scalar @{text
+ "s"} (measured in seconds) into an abstract time value. Floating
+ point numbers are easy to use as context parameters (e.g.\ via
+ configuration options, see \secref{sec:config-options}) or
+ preferences that are maintained by external tools as well.
+
+ \end{description}
+*}
+
+
subsection {* Options *}
text %mlref {*
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Nov 02 20:32:33 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Nov 02 21:24:07 2010 +0100
@@ -1643,6 +1643,44 @@
%
\endisadelimmlref
%
+\isamarkupsubsection{Time%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{Time.time}\verb|type Time.time| \\
+ \indexdef{}{ML}{seconds}\verb|seconds: real -> Time.time| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type \verb|Time.time| represents time abstractly according
+ to the SML97 basis library definition. This is adequate for
+ internal ML operations, but awkward in concrete time specifications.
+
+ \item \verb|seconds|~\isa{s} turns the concrete scalar \isa{s} (measured in seconds) into an abstract time value. Floating
+ point numbers are easy to use as context parameters (e.g.\ via
+ configuration options, see \secref{sec:config-options}) or
+ preferences that are maintained by external tools as well.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsubsection{Options%
}
\isamarkuptrue%
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 02 21:24:07 2010 +0100
@@ -497,8 +497,8 @@
|> snd
end
-val try_inner_timeout = Time.fromSeconds 5
-val try_outer_timeout = Time.fromSeconds 30
+val try_inner_timeout = seconds 5.0
+val try_outer_timeout = seconds 30.0
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Nov 02 21:24:07 2010 +0100
@@ -248,7 +248,7 @@
end
fun is_executable_term thy t =
- can (TimeLimit.timeLimit (Time.fromMilliseconds 2000)
+ can (TimeLimit.timeLimit (seconds 2.0)
(Quickcheck.test_term
(Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
(SOME "SML"))) (preprocess thy [] t)
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Nov 02 21:24:07 2010 +0100
@@ -125,7 +125,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
- timeout = Time.fromSeconds 10,
+ timeout = seconds 10.0,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Nov 02 21:24:07 2010 +0100
@@ -120,7 +120,7 @@
structure System_Config = Generic_Data
(
type T = system_configuration
- val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
+ val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
val extend = I;
fun merge ({timeout = timeout1, prolog_system = prolog_system1},
{timeout = timeout2, prolog_system = prolog_system2}) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Nov 02 21:24:07 2010 +0100
@@ -1809,7 +1809,7 @@
let
val [nrandom, size, depth] = arguments
in
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
t' [] nrandom size
@@ -1817,14 +1817,14 @@
depth true)) ())
end
| DSeq =>
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
thy NONE DSequence.map t' []) (the_single arguments) true)) ())
| Pos_Generator_DSeq =>
let
val depth = (the_single arguments)
in
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
t' [] depth))) ())
@@ -1835,7 +1835,7 @@
val seed = Random_Engine.next_seed ()
in
if stats then
- apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+ apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (seconds 20.0)
(fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
@@ -1844,7 +1844,7 @@
|> Lazy_Sequence.mapa (apfst proc))
t' [] nrandom size seed depth))) ()))
else rpair NONE
- (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+ (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
thy NONE
@@ -1853,7 +1853,7 @@
t' [] nrandom size seed depth))) ())
end
| _ =>
- rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
+ rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Predicate.yieldn k
(Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
thy NONE Predicate.map t' []))) ()))
handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
--- a/src/HOL/Tools/async_manager.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Tools/async_manager.ML Tue Nov 02 21:24:07 2010 +0100
@@ -80,8 +80,8 @@
(* main manager thread -- only one may exist *)
-val min_wait_time = Time.fromMilliseconds 300;
-val max_wait_time = Time.fromSeconds 10;
+val min_wait_time = seconds 0.3;
+val max_wait_time = seconds 10.0;
fun replace_all bef aft =
let
--- a/src/HOL/Tools/try.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/HOL/Tools/try.ML Tue Nov 02 21:24:07 2010 +0100
@@ -20,7 +20,7 @@
ProofGeneralPgip.add_preference Preferences.category_tracing
(Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
-val default_timeout = Time.fromSeconds 5
+val default_timeout = seconds 5.0
fun can_apply timeout_opt pre post tac st =
let val {goal, ...} = Proof.goal st in
--- a/src/Pure/Concurrent/future.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/Pure/Concurrent/future.ML Tue Nov 02 21:24:07 2010 +0100
@@ -253,7 +253,7 @@
val status_ticks = Unsynchronized.ref 0;
val last_round = Unsynchronized.ref Time.zeroTime;
-val next_round = Time.fromMilliseconds 50;
+val next_round = seconds 0.05;
fun scheduler_next () = (*requires SYNCHRONIZED*)
let
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Nov 02 21:24:07 2010 +0100
@@ -120,10 +120,10 @@
fun tracing_time detailed time =
tracing
(if not detailed then 5
- else if Time.>= (time, Time.fromMilliseconds 1000) then 1
- else if Time.>= (time, Time.fromMilliseconds 100) then 2
- else if Time.>= (time, Time.fromMilliseconds 10) then 3
- else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 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);
fun real_time f x =
let
@@ -202,13 +202,13 @@
Posix.Signal.int)
| NONE => ())
handle OS.SysErr _ => () | IO.Io _ =>
- (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
+ (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
val _ =
while ! result = Wait do
let val res =
sync_wait (SOME orig_atts)
- (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
+ (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
in if Exn.is_interrupt_exn res then kill 10 else () end;
(*cleanup*)
--- a/src/Pure/ML-Systems/timing.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/Pure/ML-Systems/timing.ML Tue Nov 02 21:24:07 2010 +0100
@@ -1,9 +1,11 @@
(* Title: Pure/ML-Systems/timing.ML
Author: Makarius
-Compiler-independent timing functions.
+Basic support for timing.
*)
+fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+
fun start_timing () =
let
val real_timer = Timer.startRealTimer ();
--- a/src/Pure/System/isabelle_process.ML Tue Nov 02 20:32:33 2010 +0100
+++ b/src/Pure/System/isabelle_process.ML Tue Nov 02 21:24:07 2010 +0100
@@ -81,7 +81,7 @@
(case receive mbox of
SOME msg =>
(List.app (fn s => TextIO.output (out_stream, s)) msg;
- loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
+ loop (Mailbox.receive_timeout (seconds 0.02)))
| NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
in fn () => loop (SOME o Mailbox.receive) end;
@@ -165,7 +165,7 @@
fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
let
- val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
+ val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
val _ = Output.raw_stdout Symbol.STX;
val _ = quick_and_dirty := true; (* FIXME !? *)