Cleaning of the new implementation of the tactic monad.

* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v

7 files changed, 192 insertions, 87 deletions

diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml
deleted file mode 100644
index e543b0c8fd..0000000000
--- a/proofs/proof_errors.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-exception Exception of exn
-exception Timeout
-exception TacticFailure of exn
-
-let _ = Errors.register_handler begin function
-  | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
-  | Exception e -> Errors.print e
-  | TacticFailure e -> Errors.print e
-  | _ -> Pervasives.raise Errors.Unhandled
-end
-
-
diff --git a/proofs/proof_errors.mli b/proofs/proof_errors.mli
deleted file mode 100644
index dd21d539c9..0000000000
--- a/proofs/proof_errors.mli
+++ /dev/null
@@ -1,18 +0,0 @@
-(** This small files declares the exceptions needed by Proofview_gen,
-    as Coq's extraction cannot produce exception declarations. *)
-
-(** To help distinguish between exceptions raised by the IO monad from
-    the one used natively by Coq, the former are wrapped in
-    [Exception].  It is only used internally so that [catch] blocks of
-    the IO monad would only catch exceptions raised by the [raise]
-    function of the IO monad, and not for instance, by system
-    interrupts. Also used in [Proofview] to avoid capturing exception
-    from the IO monad ([Proofview] catches errors in its compatibility
-    layer, and when lifting goal-level expressions). *)
-exception Exception of exn
-(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
-(** This exception is used by the tactics to signal failure by lack of
-    successes, rather than some other exceptions (like system
-    interrupts). *)
-exception TacticFailure of exn
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 08a736278e..d207a03825 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -224,7 +224,7 @@ let apply env t sp =
 
 
 let catchable_exception = function
-  | Proof_errors.Exception _ -> false
+  | Proofview_monad.Exception _ -> false
   | e -> Errors.noncritical e
 
 
@@ -578,8 +578,8 @@ let tclTIMEOUT n t =
           (fun r -> Proofview_monad.NonLogical.ret (Util.Inl r))
       end
       begin function
-        | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
-        | Proof_errors.TacticFailure e as src ->
+        | Proofview_monad.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
+        | Proofview_monad.TacticFailure e as src ->
           let e = Backtrace.app_backtrace ~src ~dst:e in
           Proofview_monad.NonLogical.ret (Util.Inr e)
         | e -> Proofview_monad.NonLogical.raise e
@@ -812,7 +812,7 @@ module V82 = struct
       let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
-    with Proof_errors.TacticFailure e as src ->
+    with Proofview_monad.TacticFailure e as src ->
       let src = Errors.push src in
       let e = Backtrace.app_backtrace ~src ~dst:e in
       raise e
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b60673ac96..165f7a9b52 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -465,8 +465,8 @@ module NonLogical : sig
      [()]. *)
   val seq : unit t -> 'a t -> 'a t
 
-  (* [new_ref x] creates a reference containing [x]. *)
-  val new_ref : 'a -> 'a ref t
+  (* [ref x] creates a reference containing [x]. *)
+  val ref : 'a -> 'a ref t
   (* [set r x] assigns [x] to [r]. *)
   val set : 'a ref -> 'a -> unit t
   (* [get r] returns the value of [r] *)
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 90b730198b..d3e2b8df79 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -1,73 +1,155 @@
-type ('a, 'b) list_view =
-| Nil of exn
-| Cons of 'a * 'b
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This file defines the low-level monadic operations used by the
+    tactic monad. The monad is divided into two layers: a non-logical
+    layer which consists in operations which will not (or cannot) be
+    backtracked in case of failure (input/output or persistent state)
+    and a logical layer which handles backtracking, proof
+    manipulation, and any other effect which needs to backtrack. *)
+
+(** {6 States of the logical monad} *)
+
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+(** Read/write *)
+type logicalState = proofview
 
-module IO =
- struct
+(** Write only. Must be a monoid.
+
+    Status (safe/unsafe) * ( shelved goals * given up ). *)
+type logicalMessageType = bool*(Goal.goal list*Goal.goal list)
+
+(** Read only *)
+type logicalEnvironment = Environ.env
+
+
+(** {6 Exceptions} *)
+
+
+(** To help distinguish between exceptions raised by the IO monad from
+    the one used natively by Coq, the former are wrapped in
+    [Exception].  It is only used internally so that [catch] blocks of
+    the IO monad would only catch exceptions raised by the [raise]
+    function of the IO monad, and not for instance, by system
+    interrupts. Also used in [Proofview] to avoid capturing exception
+    from the IO monad ([Proofview] catches errors in its compatibility
+    layer, and when lifting goal-level expressions). *)
+exception Exception of exn
+(** This exception is used to signal abortion in [timeout] functions. *)
+exception Timeout
+(** This exception is used by the tactics to signal failure by lack of
+    successes, rather than some other exceptions (like system
+    interrupts). *)
+exception TacticFailure of exn
+
+let _ = Errors.register_handler begin function
+  | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
+  | Exception e -> Errors.print e
+  | TacticFailure e -> Errors.print e
+  | _ -> Pervasives.raise Errors.Unhandled
+end
+
+(** {6 Non-logical layer} *)
+
+(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The
+    operations are simple wrappers around corresponding usual
+    operations and require little documentation. *)
+module NonLogical =
+struct
   type 'a t = unit -> 'a
 
-  type 'a coq_Ref = 'a Pervasives.ref
+  type 'a ref = 'a Pervasives.ref
+
+  (* The functions in this module follow the pattern that they are
+     defined with the form [(); fun ()->...]. This is an optimisation
+     which signals to the compiler that the function is usually partially
+     applied up to the [();]. Without this annotation, partial
+     applications can be significantly slower.
+
+     Documentation of this behaviour can be found at:
+     https://ocaml.janestreet.com/?q=node/30 *)
 
-  let ret = fun a -> (); fun () -> a
+  let ret a = (); fun () -> a
 
-  let bind = fun a k -> (); fun () -> k (a ()) ()
+  let bind a k = (); fun () -> k (a ()) ()
 
-  let ignore = fun a -> (); fun () -> ignore (a ())
+  let ignore a = (); fun () -> ignore (a ())
 
-  let seq = fun a k -> (); fun () -> a (); k ()
+  let seq a k = (); fun () -> a (); k ()
 
-  let map = fun f a -> (); fun () -> f (a ())
+  let map f a = (); fun () -> f (a ())
 
-  let ref = fun a -> (); fun () -> Pervasives.ref a
+  let ref a = (); fun () -> Pervasives.ref a
 
-  let set = fun r a -> (); fun () -> Pervasives.(:=) r a
+  (** [Pervasives.(:=)] *)
+  let set r a = (); fun () -> r := a
 
-  let get = fun r -> (); fun () -> Pervasives.(!) r
+  (** [Pervasives.(!)] *)
+  let get = fun r -> (); fun () -> ! r
 
-  let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
+  (** [Pervasives.raise]. Except that exceptions are wrapped with
+      {!Exception}. *)
+  let raise = fun e -> (); fun () -> raise (Exception e)
 
+  (** [try ... with ...] but restricted to {!Exception}. *)
   let catch = fun s h -> ();
-  fun () -> try s ()
-  with Proof_errors.Exception e as src ->
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    h e ()
+    fun () -> try s ()
+      with Exception e as src ->
+        let src = Errors.push src in
+        let e = Backtrace.app_backtrace ~src ~dst:e in
+        h e ()
 
   let read_line = fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()
 
   let print_char = fun c -> (); fun () -> print_char c
 
+  (** {!Pp.pp}. The buffer is also flushed. *)
   let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()
 
   let timeout = fun n t -> (); fun () ->
-    Control.timeout n t (Proof_errors.Exception Proof_errors.Timeout)
+    Control.timeout n t (Exception Timeout)
 
+  let run = fun x ->
+    try x () with Exception e as src ->
+      let src = Errors.push src in
+      let e = Backtrace.app_backtrace ~src ~dst:e in
+      Pervasives.raise e
 end
 
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+(** {6 Logical layer} *)
 
-type logicalState = proofview
+(** The logical monad is a backtracking monad on top of which is
+    layered a state monad (which is used to implement all of read/write,
+    read only, and write only effects). The state monad being layered on
+    top of the backtracking monad makes it so that the state is
+    backtracked on failure.
 
-type logicalMessageType = bool*(Goal.goal list*Goal.goal list)
+    Backtracking differs from regular exception in that, writing (+)
+    for exception catching and (>>=) for bind, we require the
+    following extra distributivity laws:
 
-type logicalEnvironment = Environ.env
+    x+(y+z) = (x+y)+z
 
-module NonLogical =
- struct
-  include IO
-  type 'a ref = 'a IO.coq_Ref
+    zero+x = x
 
-  let new_ref = ref
+    x+zero = x
 
-  let run = fun x ->
-  try x () with Proof_errors.Exception e as src ->
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    Pervasives.raise e
- end
+    (x+y)>>=k = (x>>=k)+(y>>=k) *)
+
+(** A view type for the logical monad, which is a form of list, hence
+    we can decompose it with as a list. *)
+type ('a, 'b) list_view =
+  | Nil of exn
+  | Cons of 'a * 'b
 
 module Logical =
- struct
+struct
 
   type rt = logicalEnvironment
   type wt = logicalMessageType
@@ -83,8 +165,40 @@ module Logical =
 
   let merge (b1, (l1, k1)) (b2, (l2, k2)) = (b1 && b2, (l1 @ l2, k1 @ k2))
 
+  (** Double-continuation backtracking monads are reasonable folklore
+      for "search" implementations (including the Tac interactive
+      prover's tactics). Yet it's quite hard to wrap your head around
+      these.  I recommand reading a few times the "Backtracking,
+      Interleaving, and Terminating Monad Transformers" paper by
+      O. Kiselyov, C. Shan, D. Friedman, and A. Sabry.  The peculiar
+      shape of the monadic type is reminiscent of that of the
+      continuation monad transformer.
+
+      The paper also contains the rational for the [split] abstraction.
+
+      An explanation of how to derive such a monad from mathematical
+      principles can be found in "Kan Extensions for Program
+      Optimisation" by Ralf Hinze.
+
+      A somewhat concrete view is that the type ['a iolist] is, in fact
+      the impredicative encoding of the following stream type:
+
+      [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist'
+       and 'a iolist = 'a _iolist NonLogical.t]
+
+      Using impredicative encoding avoids intermediate allocation and
+      is, empirically, very efficient in Ocaml. It also has the
+      practical benefit that the monadic operation are independent of
+      the underlying monad, which simplifies the code and side-steps
+      the limited inlining of Ocaml.
+
+      In that vision, [bind] is simply [concat_map] (though the cps
+      version is significantly simpler), [plus] is concatenation, and
+      [split] is pattern-matching. *)
   type 'a iolist =
-    { iolist : 'r. (exn -> 'r IO.t) -> ('a -> (exn -> 'r IO.t) -> 'r IO.t) -> 'r IO.t }
+      { iolist : 'r. (exn -> 'r NonLogical.t) ->
+                     ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+                     'r NonLogical.t }
 
   type 'a tactic = state -> ('a * state) iolist
 
@@ -116,8 +230,8 @@ module Logical =
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) }
 
-  let lift (m : 'a IO.t) : 'a tactic = (); fun s ->
-    { iolist = fun nil cons -> IO.bind m (fun x -> cons (x, s) nil) }
+  let lift (m : 'a NonLogical.t) : 'a tactic = (); fun s ->
+    { iolist = fun nil cons -> NonLogical.bind m (fun x -> cons (x, s) nil) }
 
   (** State related *)
 
@@ -148,7 +262,9 @@ module Logical =
       m.iolist nil (fun x next -> cons x (fun e -> if f e then nil e else next e))
     }
 
-  type 'a reified = ('a, exn -> 'a reified) list_view IO.t
+  (** For [reflect] and [split] see the "Backtracking, Interleaving,
+      and Terminating Monad Transformers" paper.  *)
+  type 'a reified = ('a, exn -> 'a reified) list_view NonLogical.t
 
   let rec reflect (m : 'a reified) : 'a iolist =
     { iolist = fun nil cons ->
@@ -156,15 +272,15 @@ module Logical =
       | Nil e -> nil e
       | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
       in
-      IO.bind m next
+      NonLogical.bind m next
     }
 
   let split (m : 'a tactic) : ('a, exn -> 'a t) list_view tactic = (); fun s ->
     let m = m s in
-    let rnil e = IO.ret (Nil e) in
-    let rcons p l = IO.ret (Cons (p, l)) in
+    let rnil e = NonLogical.ret (Nil e) in
+    let rcons p l = NonLogical.ret (Cons (p, l)) in
     { iolist = fun nil cons ->
-      IO.bind (m.iolist rnil rcons) begin function
+      NonLogical.bind (m.iolist rnil rcons) begin function
       | Nil e -> cons (Nil e, s) nil
       | Cons ((x, s), l) ->
         let l e = (); fun _ -> reflect (l e) in
@@ -174,8 +290,8 @@ module Logical =
   let run m r s =
     let s = { wstate = empty; rstate = r; sstate = s } in
     let m = m s in
-    let nil e = IO.raise (Proof_errors.TacticFailure e) in
-    let cons (x, s) _ = IO.ret ((x, s.sstate), s.wstate) in
+    let nil e = NonLogical.raise (TacticFailure e) in
+    let cons (x, s) _ = NonLogical.ret ((x, s.sstate), s.wstate) in
     m.iolist nil cons
 
  end
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 6b6f216b0a..27aea3ae95 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -15,6 +15,25 @@ type logicalEnvironment = Environ.env
 type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )
 
 
+(** {6 Exceptions} *)
+
+
+(** To help distinguish between exceptions raised by the IO monad from
+    the one used natively by Coq, the former are wrapped in
+    [Exception].  It is only used internally so that [catch] blocks of
+    the IO monad would only catch exceptions raised by the [raise]
+    function of the IO monad, and not for instance, by system
+    interrupts. Also used in [Proofview] to avoid capturing exception
+    from the IO monad ([Proofview] catches errors in its compatibility
+    layer, and when lifting goal-level expressions). *)
+exception Exception of exn
+(** This exception is used to signal abortion in [timeout] functions. *)
+exception Timeout
+(** This exception is used by the tactics to signal failure by lack of
+    successes, rather than some other exceptions (like system
+    interrupts). *)
+exception TacticFailure of exn
+
 
 module NonLogical : sig
 
@@ -27,7 +46,7 @@ module NonLogical : sig
   val ignore : 'a t -> unit t
   val seq : unit t -> 'a t -> 'a t
 
-  val new_ref : 'a -> 'a ref t
+  val ref : 'a -> 'a ref t
   val set : 'a ref -> 'a -> unit t
   val get : 'a ref -> 'a t
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1cc08fa49b..62b157307a 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -76,9 +76,9 @@ let goal_com tac =
 (* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
    expressions. It avoids parametrizing everything over a
    reference. *)
-let skipped = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
-let skip = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
-let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.new_ref None)
+let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
 
 let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)