Bases tactics on an IO monad.

It allowed to restore the timeout tactics. It also prepares for the debugging
mechanism to be restored.

['a IO.t] is just [unit -> 'a].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16970 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 189 insertions, 48 deletions

diff --git a/proofs/monads.ml b/proofs/monads.ml
index db1df19ef5..a6aa98b2b4 100644
--- a/proofs/monads.ml
+++ b/proofs/monads.ml
@@ -22,13 +22,77 @@ module type State = sig
   val get : s t
 end
 
-module Id : S with type 'a t = 'a = struct
-  type 'a t = 'a
+module type IO = sig
+  include S
+
+  type 'a ref
+
+  val ref : 'a -> 'a ref
+  val (:=) : 'a ref -> 'a -> unit t
+  val (!) : 'a ref -> 'a t
 
-  let return x = x
-  let bind x k = k x
-  let ignore x = Pervasives.ignore x
-  let seq () x = x
+  val raise : exn -> 'a t
+  val catch : 'a t -> (exn -> 'a t) -> 'a t
+
+  (** In the basic IO monad, [timeout n x] acts as [x] unless it runs for more than [n]
+      seconds in which case it raises [IO.Timeout]. *)
+  val timeout : int -> 'a t -> 'a t
+end
+
+module IO : sig
+  include IO
+
+  (** To help distinguish between exceptions raised by the [IO] monad
+      from the one used natively by Coq, the former are wrapped in
+      [Exception]. *)
+  exception Exception of exn
+  (** This exception is used to signal abortion in [timeout] functions. *)
+  exception Timeout
+  (** runs the suspension for its effects *)
+  val run : 'a t -> 'a
+end = struct
+  type 'a t = unit -> 'a
+
+  let run x = x ()
+
+  let return x () = x
+  let bind x k () = k (x ()) ()
+  let seq x k () = x (); k ()
+  let ignore x () = ignore (x ())
+
+  type 'a ref = 'a Pervasives.ref
+
+  let ref = Pervasives.ref
+  let (:=) r x () = Pervasives.(:=) r x
+  let (!) r () = Pervasives.(!) r
+
+  exception Exception of exn
+  let raise e () = raise (Exception e)
+  let catch s h () =
+    try s ()
+    with Exception e -> h e ()
+
+  exception Timeout
+  let timeout n t () =
+    let timeout_handler _ = Pervasives.raise (Exception Timeout) in
+    let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+    Pervasives.ignore (Unix.alarm n);
+    let restore_timeout () =
+      Pervasives.ignore (Unix.alarm 0);
+      Sys.set_signal Sys.sigalrm psh
+    in
+    try
+      let res = t () in
+      restore_timeout ();
+      res
+    with
+    | e -> restore_timeout (); Pervasives.raise e
+
+  let _ = Errors.register_handler begin function
+    | Timeout -> Errors.errorlabstrm "Monads.IO.timeout" (Pp.str"Timeout!")
+    | Exception e -> Errors.print e
+    | _ -> Pervasives.raise Errors.Unhandled
+  end
 end
 
 (* State monad transformer, adapted from Haskell's StateT *)
@@ -82,8 +146,15 @@ end
    An explanation of how to derive such a monad from mathematical
    principle can be found in "Kan Extensions for Program Optimisation" by
    Ralf Hinze. *)
+(* arnaud: ajouter commentaire sur la vision "liste" *)
+(* spiwack: I added the primitives from [IO] directly in the [Logic]
+   signature for convenience. It doesn't really make sense, strictly
+   speaking, as they are somewhat deconnected from the semantics of
+   [Logic], but without an appropriate language for composition (some
+   kind of mixins?) I would be going nowhere with a gazillion
+   functors. *)
 module type Logic = sig
-  include S
+  include IO
 
   (* [zero] is usually argument free, but Coq likes to explain errors,
      hence error messages should be carried around. *)
@@ -91,6 +162,8 @@ module type Logic = sig
   val plus : 'a t -> (exn -> 'a t) -> 'a t
 (** Writing (+) for plus and (>>=) for bind, we shall require that
 
+    x+(y+z) = (x+y)+z
+
     zero+x = x
 
     x+zero = x
@@ -111,7 +184,7 @@ end
    no immediate use for [T]. We might, however, consider instantiating it
    with a "writer" monad around [Pp] to implement [idtac "msg"] for
    instance. *)
-module Logic (T:S) : sig
+module Logic (T:IO) : sig
   include Logic
 
   (** [run x] raises [e] if [x] is [zero e]. *)
@@ -162,10 +235,51 @@ end = struct
     | Util.Inr e -> zero e
     | Util.Inl (a,x) -> plus (return a) x
 
-  let split x =
+  let lower x =
     let fk e = T.return (Util.Inr e) in
     let sk a fk = T.return (Util.Inl (a,fun e -> bind (lift (fk e)) reflect)) in
-    lift (x.go sk fk)
+    x.go sk fk  
+
+  let split x =
+    lift (lower x)
+
+  (*** IO ***)
+
+  type 'a ref = 'a T.ref
+  let ref = T.ref
+  let (:=) r x = lift (T.(:=) r x)
+  let (!) r = lift (T.(!) r)
+
+  let raise e = lift (T.raise e)
+  let catch t h =
+    let h' e = lower (h e) in
+    bind (lift (T.catch (lower t) h')) reflect
+
+  (** [timeout n x] can have several success. It succeeds as long as,
+      individually, each of the past successes run in less than [n]
+      seconds.
+      In case of timeout if fails with [zero Timeout]. *)
+  let rec timeout n x =
+    (* spiwack: adds a [T.return] in front of [x] in order to force
+       [lower] to go into [T] before running [x]. The problem is that
+       in a continuation-passing monad transformer, the monadic
+       operations don't make use of the underlying ones. Hence, when
+       going back to a lower monad, much computation can be done
+       before returning (and running the lower monad). It is
+       undesirable for timeout, obviously. *)
+    let x = seq (lift (T.return ())) x in
+    let x' =
+      (* spiwack: this could be a [T.map] if provided *)
+      T.bind (lower x) begin function
+        | Util.Inr _ as e -> T.return e
+        | Util.Inl (a,h) -> T.return (Util.Inl (a, fun e -> timeout n (h e)))
+      end
+    in
+    (* spiwack: we report timeouts as resumable failures. *)
+    bind (catch (lift (T.timeout n x')) begin function
+      | IO.Timeout -> zero IO.Timeout
+      | e -> raise e
+    end) reflect
 end
 
 
@@ -218,6 +332,45 @@ end = struct
           in
           set a.state >>
           return (Util.Inl(a.result,y'))
+
+
+  (*** IO ***)
+
+  type 'a ref = 'a T.ref
+  let ref = T.ref
+  let (:=) r x = lift (T.(:=) r x)
+  let (!) r = lift (T.(!) r)
+
+  let raise e = lift (T.raise e)
+  let catch t h =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    get >>= fun initial ->
+    let h' e = run (h e) initial in
+    lift (T.catch (run t initial) h') >>= fun a ->
+    set a.state >>
+    return a.result
+
+  exception Timeout
+  let timeout n t =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    get >>= fun initial ->
+    lift (T.timeout n (run t initial)) >>= fun a ->
+    set a.state >>
+    return a.result
 end
 
 
+
+
+
+
+
+
+
+
+
+
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 1fbce62dfa..bac4c22cd6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -193,14 +193,14 @@ let unfocus c sp =
 module LocalState = struct
   type t = proofview
 end
-module Backtrack = Monads.Logic(Monads.Id)
+module Backtrack = Monads.Logic(Monads.IO)
 module Inner = Monads.StateLogic(LocalState)(Backtrack)
 
 type +'a tactic = Environ.env -> 'a Inner.t
 
 (* Applies a tactic to the current proofview. *)
 let apply env t sp =
-  let next = Backtrack.run (Inner.run (t env) sp) in
+  let next = Monads.IO.run (Backtrack.run (Inner.run (t env) sp)) in
   next.Inner.result , next.Inner.state
 
 (*** tacticals ***)
@@ -224,10 +224,10 @@ let tclTHEN t1 t2 env =
 let tclIGNORE tac env = Inner.ignore (tac env)
 
 (* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
-   of [t1] have been depleted, then it behaves as [t2].  No
-   interleaving at this point. *)
+   of [t1] have been depleted and it failed with [e], then it behaves
+   as [t2 e].  No interleaving at this point. *)
 let tclOR t1 t2 env =
-  Inner.plus (t1 env) (fun _ -> t2 env)
+  Inner.plus (t1 env) (fun e -> t2 e env)
 
 (* [tclZERO e] always fails with error message [e]*)
 let tclZERO e _ = Inner.zero e
@@ -393,30 +393,7 @@ let tclEVARMAP _ =
 let tclENV env =
   Inner.return env
 
-let tclTIMEOUT n t = t
-(* arnaud: todo: restore
-(* Fails if a tactic hasn't finished after a certain amount of time *)
-
-exception TacTimeout
-
-let tclTIMEOUT n t g =
-  let timeout_handler _ = raise TacTimeout in
-  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
-  ignore (Unix.alarm n);
-  let restore_timeout () =
-    ignore (Unix.alarm 0);
-    Sys.set_signal Sys.sigalrm psh
-  in
-  try
-    let res = t g in
-    restore_timeout ();
-    res
-  with
-    | TacTimeout | Loc.Exc_located(_,TacTimeout) ->
-      restore_timeout ();
-      errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
-    | e -> restore_timeout (); raise e
-*)
+let tclTIMEOUT n t env = Inner.timeout n (t env)
 
 (*** Commands ***)
 
@@ -454,7 +431,7 @@ module Notations = struct
   let (>>=) = (>>-)
   let (>>==) = (>>--)
   let (<*>) = tclTHEN
-  let (<+>) = tclOR
+  let (<+>) t1 t2 = tclOR t2 (fun _ -> t2)
 end
 
 open Notations
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 93d1f2bb6b..2613115924 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -138,9 +138,9 @@ val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
 val tclIGNORE : 'a tactic -> unit tactic
 
 (* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
-   of [t1] have been depleted, then it behaves as [t2].  No
-   interleaving at this point. *)
-val tclOR : 'a tactic -> 'a tactic -> 'a tactic
+   of [t1] have been depleted and it failed with [e], then it behaves
+   as [t2 e].  No interleaving at this point. *)
+val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
 
 (* [tclZERO] always fails *)
 val tclZERO : exn -> 'a tactic
@@ -191,10 +191,11 @@ val tclEVARMAP : Evd.evar_map tactic
    environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
-(* [tclTIMEOUT n t] runs [t] for at most [n] seconds, succeeds if [t]
-   succeeds in the meantime, fails otherwise. *)
-(* arnaud: behaves as the identity for now *)
-val tclTIMEOUT : int -> unit tactic -> unit tactic
+(** [tclTIMEOUT n t] can have several success. It succeeds as long as,
+      individually, each of the past successes run in less than [n]
+      seconds.
+      In case of timeout if fails with [tclZERO Timeout]. *)
+val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 
 val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 45ece0ba4a..d788ade4d0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1118,7 +1118,7 @@ and eval_tactic ist = function
 	(Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
   | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
   | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
-  | TacTimeout (n,tac) -> Proofview.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
+  | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac)
   | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac)
   | TacOrelse (tac1,tac2) ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b9a104b64a..ef6a0b19a0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -508,6 +508,14 @@ module New = struct
         in
         Proofview.V82.tactic (Refiner.tclEVARS sigma) <*> tac x <*> check_evars_if
 
+  let tclTIMEOUT n t =
+    Proofview.tclOR
+      (Proofview.tclTIMEOUT n t)
+      begin function
+        | Monads.IO.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
+        | e -> Proofview.tclZERO e
+      end
+
   let nthDecl m =
     Proofview.Goal.hyps >>== fun hyps ->
     try
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index d32a0dab7b..d0dae09932 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -223,6 +223,8 @@ module New : sig
   val tclSOLVE : unit tactic list -> unit tactic
   val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic
 
+  val tclTIMEOUT : int -> unit tactic -> unit tactic
+
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->