Refactoring proofview: make the definition of the logic monad polymorphic.

Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad.

The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.

5 files changed, 216 insertions, 151 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 53b73097f..8d43513f2 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -318,7 +318,7 @@ let initial_goals p = Proofview.initial_goals p.entry
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in
+  let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in
   let shelf =
     Proofview.in_proofview tacticced_proofview begin fun sigma ->
       let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index dd1515918..34d53c3f2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -22,10 +22,86 @@
 
 open Pp
 open Util
+open Proofview_monad
 
 (* Type of proofviews. *)
-type proofview = Proofview_monad.proofview
-open Proofview_monad
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+
+(** Parameters of the logic monads *)
+module P = struct
+
+  type s = proofview * Environ.env
+
+  type e = unit
+  (* spiwack: nothing read-only anymore but it's free so I'll leave a place holder. *)
+
+  (** Status (safe/unsafe) * shelved goals * given up *)
+  type w = bool * Evar.t list * Evar.t list
+
+  let wunit = true , [] , []
+  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
+
+end
+
+(** Definition of the tactic monad *)
+module Proof = Logical(P)
+
+(** Lenses to access to components of the states *)
+module Pv = struct
+
+  type t = proofview
+
+  let get : t Proof.t = Proof.(map fst get)
+  let set (p:t) : unit Proof.t = Proof.modify (fun (_,e) -> (p,e))
+  let modify (f:t->t) : unit Proof.t = Proof.modify (fun (p,e) -> (f p,e))
+
+end
+
+module Comb = struct
+
+  type t = Evar.t list
+
+  let get : t Proof.t = Proof.map (fun {comb} -> comb) Pv.get
+  let set (c:Evar.t list) : unit Proof.t = Pv.modify (fun pv -> { pv with comb = c })
+  let modify (f:Evar.t list -> Evar.t list) : unit Proof.t =
+    Pv.modify (fun pv -> { pv with comb = f pv.comb })
+
+end
+
+module Env = struct
+
+  type t = Environ.env
+
+  let get : t Proof.t = Proof.(map snd get)
+  let set (e:t) : unit Proof.t = Proof.modify (fun (p,_) -> (p,e))
+  let modify (f:t->t) : unit Proof.t = Proof.modify (fun (p,e) -> (p,f e))
+
+end
+
+module Status = struct
+
+  type t = bool
+
+  let put (s:t) : unit Proof.t = Proof.put (s,[],[])
+
+end
+
+module Shelf = struct
+
+  type t = Evar.t list
+
+  let put (sh:t) : unit Proof.t = Proof.put (true,sh,[])
+
+end
+
+module Giveup = struct
+
+  type t = Evar.t list
+
+  let put (gs:t) : unit Proof.t = Proof.put (true,[],gs)
+
+end
+
 
 type entry = (Term.constr * Term.types) list
 
@@ -235,7 +311,6 @@ let unfocus c sp =
    - report unsafe status, shelved goals and given up goals
    - access and change the current [proofview]
    - backtrack on previous changes of the proofview *)
-module Proof = Proofview_monad.Logical
 type +'a tactic = 'a Proof.t
 
 type 'a case =
@@ -244,8 +319,10 @@ type 'a case =
 
 (* Applies a tactic to the current proofview. *)
 let apply env t sp =
-  let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in
-  next_r , next_state , status
+  let (next_r,(next_state,_),status) =
+    Proofview_monad.NonLogical.run (Proof.run t () (sp,env))
+  in
+  next_r,next_state,status
 
 (*** tacticals ***)
 
@@ -344,12 +421,12 @@ let tclFOCUS_gen nosuchgoal i j t =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   try
     let (focused,context) = focus i j initial in
-    Proof.set focused >>
+    Pv.set focused >>
     t >>= fun result ->
-    Proof.modify (fun next -> unfocus context next) >>
+    Pv.modify (fun next -> unfocus context next) >>
     Proof.ret result
   with IndexOutOfRange -> nosuchgoal
 
@@ -359,15 +436,15 @@ let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
 let tclFOCUSID id t =
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   let rec aux n = function
     | [] -> tclZERO (NoSuchGoals 1)
     | g::l ->
         if Names.Id.equal (Evd.evar_ident g initial.solution) id then
           let (focused,context) = focus n n initial in
-          Proof.set focused >>
+          Pv.set focused >>
             t >>= fun result ->
-          Proof.modify (fun next -> unfocus context next) >>
+          Pv.modify (fun next -> unfocus context next) >>
             Proof.ret result
         else
           aux (n+1) l in
@@ -430,15 +507,10 @@ let list_iter2 l1 l2 s i =
       | reraise -> tclZERO reraise
     end
 
-(* A variant of [Proof.set] specialized on the comb. Doesn't change
-   the underlying "solution" (i.e. [evar_map]) *)
-let set_comb c =
-  Proof.modify (fun step -> { step with comb = c })
-
 let on_advance g ~solved ~adv =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun step ->
+  Pv.get >>= fun step ->
   match advance step.solution g with
   | None -> solved (* If [first] has been solved by side effect: do nothing. *)
   | Some g -> adv g
@@ -452,17 +524,17 @@ let list_iter_goal s i =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   list_iter initial.comb (s,[]) begin fun goal ((r,subgoals) as cur) ->
     on_advance goal
       ~solved: ( Proof.ret cur )
       ~adv: begin fun goal ->
-        set_comb [goal] >>
+        Comb.set [goal] >>
         i goal r >>= fun r ->
-        Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get
+        Proof.map (fun step -> (r, step.comb :: subgoals)) Pv.get
       end
   end >>= fun (r,subgoals) ->
-  set_comb (List.flatten (List.rev subgoals)) >>
+  Comb.set (List.flatten (List.rev subgoals)) >>
   Proof.ret r
 
 (* spiwack: essentially a copy/paste of the above… *)
@@ -471,17 +543,17 @@ let list_iter_goal2 l s i =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   list_iter2 initial.comb l (s,[]) begin fun goal a ((r,subgoals) as cur) ->
     on_advance goal
       ~solved: ( Proof.ret cur )
       ~adv: begin fun goal ->
-        set_comb [goal] >>
+        Comb.set [goal] >>
         i goal a r >>= fun r ->
-        Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get
+        Proof.map (fun step -> (r, step.comb :: subgoals)) Pv.get
       end
   end >>= fun (r,subgoals) ->
-  set_comb (List.flatten (List.rev subgoals)) >>
+  Comb.set (List.flatten (List.rev subgoals)) >>
   Proof.ret r
 
 (* spiwack: we use an parametrised function to generate the dispatch
@@ -493,14 +565,14 @@ let tclDISPATCHGEN f join tacs =
   match tacs with
   | [] ->
       begin 
-        Proof.get >>= fun initial ->
+        Pv.get >>= fun initial ->
         match initial.comb with
         | [] -> tclUNIT (join [])
         | _ -> tclZERO (SizeMismatch (List.length initial.comb,0))
       end
   | [tac] ->
       begin
-        Proof.get >>= fun initial ->
+        Pv.get >>= fun initial ->
         match initial.comb with
         | [goal] ->
             on_advance goal
@@ -543,7 +615,7 @@ let extend_to_list startxs rx endxs l =
 let tclEXTEND tacs1 rtac tacs2 =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun step ->
+  Pv.get >>= fun step ->
   try
     let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
     tclDISPATCH tacs
@@ -558,14 +630,14 @@ let tclEXTEND tacs1 rtac tacs2 =
 let tclINDEPENDENT tac =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   match initial.comb with
   | [] -> tclUNIT ()
   | [_] -> tac
   | _ -> list_iter_goal () (fun _ () -> tac)
 
 let tclNEWGOALS gls =
-  Proof.modify begin fun step ->
+  Pv.modify begin fun step ->
   let map gl = advance step.solution gl in
   let gls = List.map_filter map gls in
   { step with comb = step.comb @ gls }
@@ -580,9 +652,9 @@ let goal_equal evars1 gl1 evars2 gl2 =
 let tclPROGRESS t =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   t >>= fun res ->
-  Proof.get >>= fun final ->
+  Pv.get >>= fun final ->
   let test =
     Evd.progress_evar_map initial.solution final.solution &&
     not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb)
@@ -593,16 +665,16 @@ let tclPROGRESS t =
     tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
 let tclEVARMAP =
-  Proof.map (fun initial -> initial.solution) Proof.get
+  Proof.map (fun initial -> initial.solution) Pv.get
 
-let tclENV = Proof.current
+let tclENV = Env.get
 
 let tclEFFECTS eff =
   Proof.bind (Proof.ret ())
     (fun () -> (* The Global.env should be taken at exec time *)
        Proof.seq
-         (Proof.update (Global.env ()))
-         (Proof.modify (fun initial -> emit_side_effects eff initial)))
+         (Env.set (Global.env ()))
+         (Pv.modify (fun initial -> emit_side_effects eff initial)))
 
 exception Timeout
 let _ = Errors.register_handler begin function
@@ -620,13 +692,12 @@ let tclTIMEOUT n t =
      a dummy value first, lest [timeout] be called when everything has
      already been computed. *)
   let t = Proof.lift (Proofview_monad.NonLogical.ret ()) >> t in
-  Proof.current >>= fun env ->
   Proof.get >>= fun initial ->
   Proof.lift begin
     Proofview_monad.NonLogical.catch
       begin
         Proofview_monad.NonLogical.bind
-          (Proofview_monad.NonLogical.timeout n (Proof.run t env initial))
+          (Proofview_monad.NonLogical.timeout n (Proof.run t () initial))
           (fun r -> Proofview_monad.NonLogical.ret (Util.Inl r))
       end
       begin function
@@ -637,7 +708,7 @@ let tclTIMEOUT n t =
         | e -> Proofview_monad.NonLogical.raise e
       end
   end >>= function
-    | Util.Inl ((res,s),m) ->
+    | Util.Inl (res,s,m) ->
         Proof.set s >>
         Proof.put m >>
         Proof.ret res
@@ -670,17 +741,16 @@ let tclTIME s t =
         tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
   in aux 0 t
 
-let mark_as_unsafe =
-  Proof.put (false,([],[]))
+let mark_as_unsafe = Status.put false
 
 (* Shelves all the goals under focus. *)
 let shelve =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
-  Proof.set {initial with comb=[]} >>
-  Proof.put (true,(initial.comb,[]))
+  Pv.get >>= fun initial ->
+  Pv.set {initial with comb=[]} >>
+  Shelf.put initial.comb
 
 
 (* [contained_in_info e evi] checks whether the evar [e] appears in
@@ -716,14 +786,14 @@ let shelve_unifiable =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   let (u,n) = partition_unifiable initial.solution initial.comb in
-  Proof.set {initial with comb=n} >>
-  Proof.put (true,(u,[]))
+  Pv.set {initial with comb=n} >>
+  Shelf.put u
 
 let check_no_dependencies =
   let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   let (u,n) = partition_unifiable initial.solution initial.comb in
   match u with
   | [] -> tclUNIT ()
@@ -745,9 +815,10 @@ let give_up =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
-  Proof.get >>= fun initial ->
-  Proof.set {initial with comb=[]} >>
-  Proof.put (false,([],initial.comb))
+  Pv.get >>= fun initial ->
+  Pv.set {initial with comb=[]} >>
+  mark_as_unsafe >>
+  Giveup.put initial.comb
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -761,16 +832,16 @@ let goodmod p m =
 let cycle n =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   let l = List.length initial.comb in
   let n' = goodmod n l in
   let (front,rear) = List.chop n' initial.comb in
-  Proof.set {initial with comb=rear@front}
+  Pv.set {initial with comb=rear@front}
 
 let swap i j =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
+  Pv.get >>= fun initial ->
   let l = List.length initial.comb in
   let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
   let i = goodmod i l and j = goodmod j l in
@@ -782,18 +853,18 @@ let swap i j =
       | _ -> x
     end 0 initial.comb
   in
-  Proof.set {initial with comb}
+  Pv.set {initial with comb}
 
 let revgoals =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun initial ->
-  Proof.set {initial with comb=List.rev initial.comb}
+  Pv.get >>= fun initial ->
+  Pv.set {initial with comb=List.rev initial.comb}
 
 let numgoals =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
-  Proof.get >>= fun { comb } ->
+  Pv.get >>= fun { comb } ->
   Proof.ret (List.length comb)
 
 (*** Commands ***)
@@ -826,7 +897,7 @@ module V82 = struct
        expectingly preserving the semantics of <= 8.2 tactics *)
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
     let (>>=) = Proof.bind in
-    Proof.get >>= fun ps ->
+    Pv.get >>= fun ps ->
     try
       let tac gl evd = 
         let glsigma  =
@@ -841,7 +912,7 @@ module V82 = struct
       in
       let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Proof.set { solution = evd; comb = sgs; }
+      Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let e = Errors.push e in
       tclZERO e
@@ -850,7 +921,7 @@ module V82 = struct
   (* normalises the evars in the goals, and stores the result in
      solution. *)
   let nf_evar_goals =
-    Proof.modify begin fun ps ->
+    Pv.modify begin fun ps ->
     let map g s = Goal.V82.nf_evar s g in
     let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
     { solution = evd; comb = goals; }
@@ -858,13 +929,13 @@ module V82 = struct
 
   (* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
   let tclEVARS evd =
-    Proof.modify (fun ps -> { ps with solution = evd })
+    Pv.modify (fun ps -> { ps with solution = evd })
 
   let tclEVARSADVANCE evd =
-    Proof.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
+    Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx = 
-    Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
+    Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
       
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
@@ -916,8 +987,7 @@ module V82 = struct
       let e = Backtrace.app_backtrace ~src ~dst:e in
       raise e
 
-  let put_status b =
-    Proof.put (b,([],[]))
+  let put_status = Status.put
 
   let catchable_exception = catchable_exception
 
@@ -959,7 +1029,7 @@ module Goal = struct
 
   let nf_enter f =
     list_iter_goal () begin fun goal () ->
-      Proof.current >>= fun env ->
+      Env.get >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
@@ -970,7 +1040,7 @@ module Goal = struct
     end
 
   let normalize { self } =
-    Proof.current >>= fun env ->
+    Env.get >>= fun env ->
     tclEVARMAP >>= fun sigma ->
     let (gl,sigma) = nf_gmake env sigma self in
     tclTHEN (V82.tclEVARS sigma) (tclUNIT gl)
@@ -981,7 +1051,7 @@ module Goal = struct
 
   let enter f =
     list_iter_goal () begin fun goal () ->
-      Proof.current >>= fun env ->
+      Env.get >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try f (gmake env sigma goal)
       with e when catchable_exception e ->
@@ -990,8 +1060,8 @@ module Goal = struct
     end
 
   let goals =
-    Proof.current >>= fun env ->
-    Proof.get >>= fun step ->
+    Env.get >>= fun env ->
+    Pv.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
       match advance sigma goal with
@@ -1062,7 +1132,7 @@ struct
     (** Select the goals *)
     let comb = undefined sigma (List.rev evs) in
     let sigma = List.fold_left mark_as_goal sigma comb in
-    Proof.set { solution = Evd.reset_future_goals sigma; comb; }
+    Pv.set { solution = Evd.reset_future_goals sigma; comb; }
   end
 
   (** Useful definitions *)
@@ -1085,7 +1155,7 @@ end
 
 module NonLogical = Proofview_monad.NonLogical
 
-let tclLIFT = Proofview_monad.Logical.lift
+let tclLIFT = Proof.lift
 
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index d822f933b..45a0c9484 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -133,7 +133,7 @@ type 'a case =
    case it is [false]. *)
 val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                    * proofview
-                                                   * (bool*(Goal.goal list*Goal.goal list))
+                                                   * (bool*Goal.goal list*Goal.goal list)
 
 (*** tacticals ***)
 
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index 9be26ab2b..784b7d7f3 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -13,21 +13,6 @@
     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
-
-(** 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} *)
 
@@ -154,22 +139,34 @@ type ('a, 'b) list_view =
   | Nil of exn
   | Cons of 'a * 'b
 
-module Logical =
-struct
+module type Param = sig
 
-  type rt = logicalEnvironment
-  type wt = logicalMessageType
-  type st = logicalState
+  (** Read only *)
+  type e
 
-  type state = {
-    rstate : rt;
-    wstate : wt;
-    sstate : st;
-  }
+  (** Write only *)
+  type w
 
-  let empty = (true, ([], []))
+  (** [w] must be a monoid *)
+  val wunit : w
+  val wprod : w -> w -> w
 
-  let merge (b1, (l1, k1)) (b2, (l2, k2)) = (b1 && b2, (l1 @ l2, k1 @ k2))
+  (** Read-write *)
+  type s
+
+end
+
+
+module Logical (P:Param) =
+struct
+
+  (** All three of environment, writer and state are coded as a single
+      state-passing-style monad.*)
+  type state = {
+    rstate : P.e;
+    wstate : P.w;
+    sstate : P.s;
+  }
 
   (** Double-continuation backtracking monads are reasonable folklore
       for "search" implementations (including the Tac interactive
@@ -190,7 +187,7 @@ struct
       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]
+      and 'a iolist = 'a _iolist NonLogical.t]
 
       Using impredicative encoding avoids intermediate allocation and
       is, empirically, very efficient in Ocaml. It also has the
@@ -206,66 +203,61 @@ struct
                      ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
                      'r NonLogical.t }
 
-  type 'a tactic = state -> ('a * state) iolist
+  type 'a t = state -> ('a * state) iolist
 
-  type 'a t = 'a tactic
-
-  let zero e : 'a tactic = (); fun s ->
+  let zero e : 'a t = (); fun s ->
     { iolist = fun nil cons -> nil e }
 
-  let plus m1 m2 : 'a tactic = (); fun s ->
+  let plus m1 m2 : 'a t = (); fun s ->
     let m1 = m1 s in
     { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons }
 
-  let ret x : 'a tactic = (); fun s ->
+  let ret x : 'a t = (); fun s ->
     { iolist = fun nil cons -> cons (x, s) nil }
 
-  let bind (m : 'a tactic) (f : 'a -> 'b tactic) : 'b tactic = (); fun s ->
+  let bind (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) }
 
-  let seq (m : unit tactic) (f : 'a tactic) : 'a tactic = (); fun s ->
+  let seq (m : unit t) (f : 'a t) : 'a t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun ((), s) next -> (f s).iolist next cons) }
 
-  let map (f : 'a -> 'b) (m : 'a tactic) : 'b tactic = (); fun s ->
+  let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) }
 
-  let ignore (m : 'a tactic) : unit tactic = (); fun s ->
+  let ignore (m : 'a t) : unit t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) }
 
-  let lift (m : 'a NonLogical.t) : 'a tactic = (); fun s ->
+  let lift (m : 'a NonLogical.t) : 'a t = (); fun s ->
     { iolist = fun nil cons -> NonLogical.bind m (fun x -> cons (x, s) nil) }
 
   (** State related *)
 
-  let get : st tactic = (); fun s ->
+  let get : P.s t = (); fun s ->
     { iolist = fun nil cons -> cons (s.sstate, s) nil }
 
-  let set (sstate : st) : unit tactic = (); fun s ->
+  let set (sstate : P.s) : unit t = (); fun s ->
     { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
 
-  let modify (f : st -> st) : unit tactic = (); fun s ->
+  let modify (f : P.s -> P.s) : unit t = (); fun s ->
     { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil }
 
-  let current : rt tactic = (); fun s ->
+  let current : P.e t = (); fun s ->
     { iolist = fun nil cons -> cons (s.rstate, s) nil }
 
-  let update (rstate : rt) : unit tactic = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with rstate }) nil }
-
-  let put (w : wt) : unit tactic = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with wstate = merge w s.wstate }) nil }
+  let put (w : P.w) : unit t = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil }
 
   (** List observation *)
 
-  let once (m : 'a tactic) : 'a tactic = (); fun s ->
+  let once (m : 'a t) : 'a t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
 
-  let break (f : exn -> bool) (m : 'a tactic) : 'a tactic = (); fun s ->
+  let break (f : exn -> bool) (m : 'a t) : 'a t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons ->
       m.iolist nil (fun x next -> cons x (fun e -> if f e then nil e else next e))
@@ -284,7 +276,7 @@ struct
       NonLogical.bind m next
     }
 
-  let split (m : 'a tactic) : ('a, exn -> 'a t) list_view tactic = (); fun s ->
+  let split (m : 'a t) : ('a, exn -> 'a t) list_view t = (); fun s ->
     let m = m s in
     let rnil e = NonLogical.ret (Nil e) in
     let rcons p l = NonLogical.ret (Cons (p, l)) in
@@ -297,10 +289,10 @@ struct
       end }
 
   let run m r s =
-    let s = { wstate = empty; rstate = r; sstate = s } in
+    let s = { wstate = P.wunit; rstate = r; sstate = s } in
     let m = m s in
     let nil e = NonLogical.raise (TacticFailure e) in
-    let cons (x, s) _ = NonLogical.ret ((x, s.sstate), s.wstate) 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 e1d9b4fa1..675b4c768 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -13,21 +13,6 @@
     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
-
-(** Write only. Must be a monoid.
-
-    Status (safe/unsafe) * ( shelved goals * given up ). *)
-type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )
-
 
 (** {6 Exceptions} *)
 
@@ -119,7 +104,26 @@ type ('a, 'b) list_view =
 | Nil of exn
 | Cons of 'a * 'b
 
-module Logical : sig
+(** The monad is parametrised in the types of state, environment and
+    writer. *)
+module type Param = sig
+
+  (** Read only *)
+  type e
+
+  (** Write only *)
+  type w
+
+  (** [w] must be a monoid *)
+  val wunit : w
+  val wprod : w -> w -> w
+
+  (** Read-write *)
+  type s
+
+end
+
+module Logical (P:Param) : sig
 
   type +'a t
 
@@ -129,12 +133,11 @@ module Logical : sig
   val ignore : 'a t -> unit t
   val seq : unit t -> 'a t -> 'a t
 
-  val set : logicalState -> unit t
-  val get : logicalState t
-  val modify : (logicalState -> logicalState) -> unit t
-  val put : logicalMessageType -> unit t
-  val current : logicalEnvironment t
-  val update : logicalEnvironment -> unit t
+  val set : P.s -> unit t
+  val get : P.s t
+  val modify : (P.s -> P.s) -> unit t
+  val put : P.w -> unit t
+  val current : P.e t
 
   val zero : exn -> 'a t
   val plus : 'a t -> (exn -> 'a t) -> 'a t
@@ -144,5 +147,5 @@ module Logical : sig
 
   val lift : 'a NonLogical.t -> 'a t
 
-  val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t
+  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w) NonLogical.t
 end