From 00a09f2cc4a8f4b6baeca0a474e5ab4062ff0f97 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Sun, 22 Nov 2020 11:22:52 +0100
Subject: Add support for high resolution timeout functions.

---
 engine/logic_monad.mli | 2 +-
 engine/proofview.ml    | 4 +++-
 engine/proofview.mli   | 3 ++-
 3 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 7784b38c80..5208469082 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -74,7 +74,7 @@ module NonLogical : sig
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val timeout : int -> 'a t -> 'a option t
+  val timeout : float -> 'a t -> 'a option t
 
   (** Construct a monadified side-effect. Exceptions raised by the argument are
       wrapped with {!Exception}. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 22863f451d..a4d96a7e8f 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -926,7 +926,7 @@ let _ = CErrors.register_handler begin function
   | _ -> None
 end
 
-let tclTIMEOUT n t =
+let tclTIMEOUTF n t =
   let open Proof in
   (* spiwack: as one of the monad is a continuation passing monad, it
      doesn't force the computation to be threaded inside the underlying
@@ -951,6 +951,8 @@ let tclTIMEOUT n t =
         return res
     | Util.Inr (e, info) -> tclZERO ~info e
 
+let tclTIMEOUT n t = tclTIMEOUTF (float_of_int n) t
+
 let tclTIME s t =
   let pr_time t1 t2 n msg =
     let msg =
diff --git a/engine/proofview.mli b/engine/proofview.mli
index fe0d7ae51e..bf6021b1b6 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -418,7 +418,8 @@ val tclCHECKINTERRUPT : unit tactic
 
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout it fails with [tclZERO Tac_Timeout]. *)
-val tclTIMEOUT : int -> 'a tactic -> 'a tactic
+val tclTIMEOUTF : float -> 'a tactic -> 'a tactic
+val tclTIMEOUT  : int   -> 'a tactic -> 'a tactic
 
 (** [tclTIME s t] displays time for each atomic call to t, using s as an
     identifying annotation if present *)
-- 
cgit v1.2.3