Some comments in the interface of Proofview_monad.

1 files changed, 59 insertions, 8 deletions

diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 27aea3ae95..ab92a57fcd 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -1,17 +1,31 @@
-(* This is an interface for the code extracted from bootstrap/Monad.v.
-   The relevant comments are overthere. *)
-
-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
 
+(** Read only *)
 type logicalEnvironment = Environ.env
 
-(** status (safe/unsafe) * ( shelved goals * given up ) *)
+(** Write only. Must be a monoid.
+
+    Status (safe/unsafe) * ( shelved goals * given up ). *)
 type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )
 
 
@@ -35,6 +49,11 @@ exception Timeout
 exception TacticFailure of exn
 
 
+(** {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 : sig
 
   type +'a t
@@ -47,24 +66,56 @@ module NonLogical : sig
   val seq : unit t -> 'a t -> 'a t
 
   val ref : 'a -> 'a ref t
+  (** [Pervasives.(:=)] *)
   val set : 'a ref -> 'a -> unit t
+  (** [Pervasives.(!)] *)
   val get : 'a ref -> 'a t
 
   val read_line : string t
   val print_char : char -> unit t
+  (** {!Pp.pp}. The buffer is also flushed. *)
   val print : Pp.std_ppcmds -> unit t
 
+  (** [Pervasives.raise]. Except that exceptions are wrapped with
+      {!Exception}. *)
   val raise : exn -> 'a t
+  (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (exn -> 'a t) -> 'a t
   val timeout : int -> 'a t -> 'a t
 
 
-  (* [run] performs effects. *)
+  (** [run] performs effects. *)
   val run : 'a t -> 'a
 
 end
 
 
+(** {6 Logical layer} *)
+
+(** 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.
+
+    Backtracking differs from regular exception in that, writing (+)
+    for exception catching and (>>=) for bind, we require the
+    following extra distributivity laws:
+
+    x+(y+z) = (x+y)+z
+
+    zero+x = x
+
+    x+zero = x
+
+    (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 : sig
 
   type +'a t