# HG changeset patch
# User wenzelm
# Date 1614956982 -3600
# Node ID 6b104dc069de5cc6d8c4550216a368e713627783
# Parent  2b1b7b58d0e76d5263e8ba3f1b4aba7a638046c4
clarified signature --- augment existing structure Time;

diff -r 2b1b7b58d0e7 -r 6b104dc069de src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 05 13:48:23 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -123,7 +123,7 @@
   let
     val ctxt = Proof.context_of state
 
-    val hard_timeout = time_mult 5.0 timeout
+    val hard_timeout = Time.scale 5.0 timeout
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length facts |> not only ? Integer.min max_facts
diff -r 2b1b7b58d0e7 -r 6b104dc069de src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Mar 05 13:48:23 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -129,7 +129,7 @@
 val merge_slack_factor = 1.5
 
 fun adjust_merge_timeout max time =
-  let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in
+  let val timeout = Time.scale merge_slack_factor (merge_slack_time + time) in
     if max < timeout then max else timeout
   end
 
diff -r 2b1b7b58d0e7 -r 6b104dc069de src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Mar 05 13:48:23 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -57,7 +57,7 @@
           else
             let val y = f timeout x in
               (case get_time y of
-                SOME time => next_timeout := time_min (time, !next_timeout)
+                SOME time => next_timeout := Time.min (time, !next_timeout)
               | _ => ());
               SOME y
             end
diff -r 2b1b7b58d0e7 -r 6b104dc069de src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Mar 05 13:48:23 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -1264,7 +1264,7 @@
 
 fun launch_thread timeout task =
   let
-    val hard_timeout = time_mult learn_timeout_slack timeout
+    val hard_timeout = Time.scale learn_timeout_slack timeout
     val birth_time = Time.now ()
     val death_time = birth_time + hard_timeout
     val desc = ("Machine learner for Sledgehammer", "")
@@ -1546,7 +1546,7 @@
       fun maybe_launch_thread exact min_num_facts_to_learn =
         if not (Async_Manager_Legacy.has_running_threads MaShN) andalso
            Time.toSeconds timeout >= min_secs_for_learning then
-          let val timeout = time_mult learn_timeout_slack timeout in
+          let val timeout = Time.scale learn_timeout_slack timeout in
             (if verbose then
                writeln ("Started MaShing through " ^
                  (if exact then "" else "up to ") ^ string_of_int min_num_facts_to_learn ^
diff -r 2b1b7b58d0e7 -r 6b104dc069de src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Mar 05 13:48:23 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -13,8 +13,6 @@
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
   val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
-  val time_mult : real -> Time.time -> Time.time
-  val time_min : Time.time * Time.time -> Time.time
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time : string -> string -> Time.time
   val subgoal_count : Proof.state -> int
@@ -49,9 +47,6 @@
   |> tap (fn _ => clean_up x)
   |> Exn.release
 
-fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
-fun time_min (x, y) = if x < y then x else y
-
 fun parse_bool_option option name s =
   (case s of
      "smart" => if option then NONE else raise Option.Option
diff -r 2b1b7b58d0e7 -r 6b104dc069de src/Pure/General/time.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/time.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -0,0 +1,25 @@
+(*  Title:      Pure/General/time.scala
+    Author:     Makarius
+
+Time based on nanoseconds (idealized).
+*)
+
+signature TIME =
+sig
+  include TIME
+  val min: time * time -> time
+  val max: time * time -> time
+  val scale: real -> time -> time
+end;
+
+structure Time: TIME =
+struct
+
+open Time;
+
+fun min (t1, t2) = if t1 < t2 then t1 else t2;
+fun max (t1, t2) = if t1 > t2 then t1 else t2;
+
+fun scale s t = Time.fromNanoseconds (Real.ceil (s * Real.fromInt (Time.toNanoseconds t)));
+
+end;
diff -r 2b1b7b58d0e7 -r 6b104dc069de src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Mar 05 13:48:23 2021 +0100
+++ b/src/Pure/ROOT.ML	Fri Mar 05 16:09:42 2021 +0100
@@ -85,6 +85,7 @@
 ML_file "General/binding.ML";
 ML_file "General/socket_io.ML";
 ML_file "General/seq.ML";
+ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";