Split [Proofview] into a file where the basic operations on the state are defined and the file providing the primitives.

The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.

7 files changed, 573 insertions, 476 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
new file mode 100644
index 000000000..9ac7faaf2
--- /dev/null
+++ b/proofs/logic_monad.ml
@@ -0,0 +1,304 @@
+(************************************************************************)
+(*  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 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
+
+  (* 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 *)
+
+  include Monad.Make(struct
+    type 'a t = unit -> 'a
+
+    let return a = (); fun () -> a
+    let (>>=) a k = (); fun () -> k (a ()) ()
+    let (>>) a k = (); fun () -> a (); k ()
+    let map f a = (); fun () -> f (a ())
+  end)
+
+  type 'a ref = 'a Pervasives.ref
+
+  let ignore a = (); fun () -> ignore (a ())
+
+  let ref a = (); fun () -> Pervasives.ref a
+
+  (** [Pervasives.(:=)] *)
+  let (:=) r a = (); fun () -> r := a
+
+  (** [Pervasives.(!)] *)
+  let (!) = fun r -> (); fun () -> ! r
+
+  (** [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 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 (Exception Timeout)
+
+  let make f = (); fun () ->
+    try f ()
+    with e when Errors.noncritical e ->
+      let e = Errors.push e in
+      Pervasives.raise (Exception e)
+
+  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
+
+(** {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 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) =
+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
+      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 NonLogical.t) ->
+                     ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+                     'r NonLogical.t }
+
+  include Monad.Make(struct
+    type 'a t = state -> ('a * state) iolist
+
+    let return x : 'a t = (); fun s ->
+      { iolist = fun nil cons -> cons (x, s) nil }
+
+    let (>>=) (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 (>>) (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 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) }
+
+  end)
+
+  let zero e : 'a t = (); fun s ->
+    { iolist = fun nil cons -> nil e }
+
+  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 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 t = (); fun s ->
+    { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) }
+
+  (** State related *)
+
+  let get : P.s t = (); fun s ->
+    { iolist = fun nil cons -> cons (s.sstate, s) nil }
+
+  let set (sstate : P.s) : unit t = (); fun s ->
+    { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
+
+  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 : P.e t = (); fun s ->
+    { iolist = fun nil cons -> cons (s.rstate, s) 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 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 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))
+    }
+
+  (** 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 ->
+      let next = function
+      | Nil e -> nil e
+      | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
+      in
+      NonLogical.(m >>= next)
+    }
+
+  let split (m : 'a t) : ('a, exn -> 'a t) list_view t = (); fun s ->
+    let m = m s in
+    let rnil e = NonLogical.return (Nil e) in
+    let rcons p l = NonLogical.return (Cons (p, l)) in
+    { iolist = fun nil cons ->
+      let open NonLogical in
+      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
+        cons (Cons (x, l), s) nil
+      end }
+
+  let run m r s =
+    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.return (x, s.sstate, s.wstate) in
+    m.iolist nil cons
+
+ end
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
new file mode 100644
index 000000000..c1315e9f5
--- /dev/null
+++ b/proofs/logic_monad.mli
@@ -0,0 +1,144 @@
+(************************************************************************)
+(*  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 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
+
+
+(** {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
+
+  include Monad.S
+
+  val ignore : 'a t -> unit t
+
+  type 'a ref
+
+  val ref : 'a -> 'a ref t
+  (** [Pervasives.(:=)] *)
+  val (:=) : 'a ref -> 'a -> unit t
+  (** [Pervasives.(!)] *)
+  val (!) : '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
+
+  (** Construct a monadified side-effect. Exceptions raised by the argument are
+      wrapped with {!Exception}. *)
+  val make : (unit -> 'a) -> 'a t
+
+  (** [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
+
+(** 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
+
+  include Monad.S
+
+  val ignore : 'a t -> 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
+  val split : 'a t -> (('a,(exn->'a t)) list_view) t
+  val once : 'a t -> 'a t
+  val break : (exn -> bool) -> 'a t -> 'a t
+
+  val lift : 'a NonLogical.t -> 'a t
+
+  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w) NonLogical.t
+end
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index bfb36824d..32bf5576f 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -4,7 +4,7 @@ Evar_refiner
 Proof_using
 Proof_type
 Proof_errors
-Proofview_gen
+Logic_monad
 Proofview_monad
 Logic
 Proofview
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index db498caea..4b46417e9 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -24,82 +24,8 @@ open Pp
 open Util
 open Proofview_monad
 
-(* Type of proofviews. *)
-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 type State = sig
-  type t
-  val get : t Proof.t
-  val set : t -> unit Proof.t
-  val modify : (t->t) -> unit Proof.t
-end
-
-module type Writer = sig
-  type t
-  val put : t -> unit Proof.t
-end
-
-module Pv : State with type t := proofview = struct
-  let get = Proof.(map fst get)
-  let set p = Proof.modify (fun (_,e) -> (p,e))
-  let modify f= Proof.modify (fun (p,e) -> (f p,e))
-end
-
-module Solution : State with type t := Evd.evar_map = struct
-  let get = Proof.map (fun {solution} -> solution) Pv.get
-  let set s = Pv.modify (fun pv -> { pv with solution = s })
-  let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
-end
-
-module Comb : State with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let get = Proof.map (fun {comb} -> comb) Pv.get
-  let set c = Pv.modify (fun pv -> { pv with comb = c })
-  let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
-end
-
-module Env : State with type t := Environ.env = struct
-  let get = Proof.(map snd get)
-  let set e = Proof.modify (fun (p,_) -> (p,e))
-  let modify f = Proof.modify (fun (p,e) -> (p,f e))
-end
-
-module Status : Writer with type t := bool = struct
-  let put s = Proof.put (s,[],[])
-end
-
-module Shelf : Writer with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let put sh = Proof.put (true,sh,[])
-end
-
-module Giveup : Writer with type t = Evar.t list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
-  let put gs = Proof.put (true,[],gs)
-end
+(** Main state of tactics *)
+type proofview = Proofview_monad.proofview
 
 type entry = (Term.constr * Term.types) list
 
@@ -260,6 +186,8 @@ let unfocus c sp =
      bind on unit-returning tactics).
 *)
 
+module Proof = Logical
+
 (* type of tactics:
 
    tactics can
@@ -276,7 +204,7 @@ 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 () (sp,env))
+    Logic_monad.NonLogical.run (Proof.run t () (sp,env))
   in
   next_r,next_state,status
 
@@ -284,7 +212,7 @@ let apply env t sp =
 
 
 let catchable_exception = function
-  | Proofview_monad.Exception _ -> false
+  | Logic_monad.Exception _ -> false
   | e -> Errors.noncritical e
 
 
@@ -313,6 +241,7 @@ let tclZERO = Proof.zero
 
 (* [tclCASE t] observes the head of the tactic and returns it as a value *)
 let tclCASE t =
+  let open Logic_monad in
   let map = function
   | Nil e -> Fail e
   | Cons (x, t) -> Next (x, t)
@@ -322,6 +251,7 @@ let tclCASE t =
 (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
    or [t2] if [t1] fails. *)
 let tclORELSE t1 t2 =
+  let open Logic_monad in
   let open Proof in
   split t1 >>= function
     | Nil e -> t2 e
@@ -331,6 +261,7 @@ let tclORELSE t1 t2 =
    succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
    fails with [e], then it behaves as [f e]. *)
 let tclIFCATCH a s f =
+  let open Logic_monad in
   let open Proof in
   split a >>= function
     | Nil e -> f e
@@ -354,6 +285,7 @@ end
    does not have a second success. Moreover the second success may be
    conditional on the error recieved: [e] is used. *)
 let tclEXACTLY_ONCE e t =
+  let open Logic_monad in
   let open Proof in
   split t >>= function
     | Nil e -> tclZERO e
@@ -588,21 +520,21 @@ let tclTIMEOUT n t =
      (IO) monad. Hence I force it myself by asking for the evaluation of
      a dummy value first, lest [timeout] be called when everything has
      already been computed. *)
-  let t = Proof.lift (Proofview_monad.NonLogical.return ()) >> t in
+  let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in
   Proof.get >>= fun initial ->
   Proof.lift begin
-    Proofview_monad.NonLogical.catch
+    Logic_monad.NonLogical.catch
       begin
-        let open Proofview_monad.NonLogical in
+        let open Logic_monad.NonLogical in
         timeout n (Proof.run t () initial) >>= fun r ->
         return (Util.Inl r)
       end
-      begin let open Proofview_monad.NonLogical in function
-        | Proofview_monad.Timeout -> return (Util.Inr Timeout)
-        | Proofview_monad.TacticFailure e as src ->
+      begin let open Logic_monad.NonLogical in function
+        | Logic_monad.Timeout -> return (Util.Inr Timeout)
+        | Logic_monad.TacticFailure e as src ->
           let e = Backtrace.app_backtrace ~src ~dst:e in
           return (Util.Inr e)
-        | e -> Proofview_monad.NonLogical.raise e
+        | e -> Logic_monad.NonLogical.raise e
       end
   end >>= function
     | Util.Inl (res,s,m) ->
@@ -625,7 +557,7 @@ let tclTIME s t =
     let open Proof in
     tclUNIT () >>= fun () ->
     let tstart = System.get_time() in
-    Proof.split t >>= function
+    Proof.split t >>= let open Logic_monad in function
     | Nil e ->
       begin
         let tend = System.get_time() in
@@ -941,7 +873,7 @@ struct
   end
 end
 
-module NonLogical = Proofview_monad.NonLogical
+module NonLogical = Logic_monad.NonLogical
 
 let tclLIFT = Proof.lift
 
@@ -1036,7 +968,7 @@ module V82 = struct
       let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
-    with Proofview_monad.TacticFailure e as src ->
+    with Logic_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 a32ceb59e..914af982d 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -404,7 +404,7 @@ end
 
 (* The [NonLogical] module allows the execution of side effects in tactics
    (non-logical side-effects are not discarded at failures). *)
-module NonLogical : module type of Proofview_monad.NonLogical
+module NonLogical : module type of Logic_monad.NonLogical
 
 (* [tclLIFT c] includes the non-logical command [c] in a tactic. *)
 val tclLIFT : 'a NonLogical.t -> 'a tactic
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index 9ac7faaf2..b04d053f5 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -6,299 +6,89 @@
 (*         *       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. *)
+(** This file defines the datatypes used as internal states by the
+    tactic monad, and specialises the [Logic_monad] to these type. *)
 
+(** {6 State types} *)
 
-(** {6 Exceptions} *)
+(** Type of proof views: current [evar_map] together with the list of
+    focused goals. *)
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
 
 
-(** 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
+(** {6 Instantiation of the logic monad} *)
 
-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
-
-  (* 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 *)
-
-  include Monad.Make(struct
-    type 'a t = unit -> 'a
-
-    let return a = (); fun () -> a
-    let (>>=) a k = (); fun () -> k (a ()) ()
-    let (>>) a k = (); fun () -> a (); k ()
-    let map f a = (); fun () -> f (a ())
-  end)
-
-  type 'a ref = 'a Pervasives.ref
-
-  let ignore a = (); fun () -> ignore (a ())
-
-  let ref a = (); fun () -> Pervasives.ref a
-
-  (** [Pervasives.(:=)] *)
-  let (:=) r a = (); fun () -> r := a
-
-  (** [Pervasives.(!)] *)
-  let (!) = fun r -> (); fun () -> ! r
-
-  (** [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 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 ()
+(** Parameters of the logic monads *)
+module P = struct
 
-  let print_char = fun c -> (); fun () -> print_char c
+  type s = proofview * Environ.env
 
-  (** {!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 ()
+  type e = unit
+  (* spiwack: nothing read-only anymore but it's free so I'll leave a place holder. *)
 
-  let timeout = fun n t -> (); fun () ->
-    Control.timeout n t (Exception Timeout)
+  (** Status (safe/unsafe) * shelved goals * given up *)
+  type w = bool * Evar.t list * Evar.t list
 
-  let make f = (); fun () ->
-    try f ()
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in
-      Pervasives.raise (Exception e)
+  let wunit = true , [] , []
+  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
 
-  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
 
-(** {6 Logical layer} *)
+module Logical = Logic_monad.Logical(P)
 
-(** 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 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
+(** {6 Lenses to access to components of the states} *)
 
+module type State = sig
+  type t
+  val get : t Logical.t
+  val set : t -> unit Logical.t
+  val modify : (t->t) -> unit Logical.t
 end
 
+module type Writer = sig
+  type t
+  val put : t -> unit Logical.t
+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
-      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 NonLogical.t) ->
-                     ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-                     'r NonLogical.t }
-
-  include Monad.Make(struct
-    type 'a t = state -> ('a * state) iolist
-
-    let return x : 'a t = (); fun s ->
-      { iolist = fun nil cons -> cons (x, s) nil }
-
-    let (>>=) (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 (>>) (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 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) }
-
-  end)
-
-  let zero e : 'a t = (); fun s ->
-    { iolist = fun nil cons -> nil e }
-
-  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 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 t = (); fun s ->
-    { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) }
-
-  (** State related *)
-
-  let get : P.s t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.sstate, s) nil }
-
-  let set (sstate : P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
-
-  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 : P.e t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.rstate, s) 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 t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
+module Pv : State with type t := proofview = struct
+  let get = Logical.(map fst get)
+  let set p = Logical.modify (fun (_,e) -> (p,e))
+  let modify f= Logical.modify (fun (p,e) -> (f p,e))
+end
 
-  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))
-    }
+module Solution : State with type t := Evd.evar_map = struct
+  let get = Logical.map (fun {solution} -> solution) Pv.get
+  let set s = Pv.modify (fun pv -> { pv with solution = s })
+  let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
+end
 
-  (** For [reflect] and [split] see the "Backtracking, Interleaving,
-      and Terminating Monad Transformers" paper.  *)
-  type 'a reified = ('a, exn -> 'a reified) list_view NonLogical.t
+module Comb : State with type t = Evar.t list = struct
+    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+  type t = Evar.t list
+  let get = Logical.map (fun {comb} -> comb) Pv.get
+  let set c = Pv.modify (fun pv -> { pv with comb = c })
+  let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
+end
 
-  let rec reflect (m : 'a reified) : 'a iolist =
-    { iolist = fun nil cons ->
-      let next = function
-      | Nil e -> nil e
-      | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
-      in
-      NonLogical.(m >>= next)
-    }
+module Env : State with type t := Environ.env = struct
+  let get = Logical.(map snd get)
+  let set e = Logical.modify (fun (p,_) -> (p,e))
+  let modify f = Logical.modify (fun (p,e) -> (p,f e))
+end
 
-  let split (m : 'a t) : ('a, exn -> 'a t) list_view t = (); fun s ->
-    let m = m s in
-    let rnil e = NonLogical.return (Nil e) in
-    let rcons p l = NonLogical.return (Cons (p, l)) in
-    { iolist = fun nil cons ->
-      let open NonLogical in
-      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
-        cons (Cons (x, l), s) nil
-      end }
+module Status : Writer with type t := bool = struct
+  let put s = Logical.put (s,[],[])
+end
 
-  let run m r s =
-    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.return (x, s.sstate, s.wstate) in
-    m.iolist nil cons
+module Shelf : Writer with type t = Evar.t list = struct
+    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+  type t = Evar.t list
+  let put sh = Logical.put (true,sh,[])
+end
 
- end
+module Giveup : Writer with type t = Evar.t list = struct
+    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
+  type t = Evar.t list
+  let put gs = Logical.put (true,[],gs)
+end
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index c1315e9f5..43d1f6d80 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -6,139 +6,66 @@
 (*         *       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. *)
+(** This file defines the datatypes used as internal states by the
+    tactic monad, and specialises the [Logic_monad] to these type. *)
 
+(** {6 State types} *)
 
-(** {6 Exceptions} *)
+(** Type of proof views: current [evar_map] together with the list of
+    focused goals. *)
+type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
 
 
-(** 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
+(** {6 Instantiation of the logic monad} *)
 
+module P : sig
+  type s = proofview * Environ.env
 
-(** {6 Non-logical layer} *)
+  (** Status (safe/unsafe) * shelved goals * given up *)
+  type w = bool * Evar.t list * Evar.t list
 
-(** 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
-
-  include Monad.S
-
-  val ignore : 'a t -> unit t
-
-  type 'a ref
-
-  val ref : 'a -> 'a ref t
-  (** [Pervasives.(:=)] *)
-  val (:=) : 'a ref -> 'a -> unit t
-  (** [Pervasives.(!)] *)
-  val (!) : '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
-
-  (** Construct a monadified side-effect. Exceptions raised by the argument are
-      wrapped with {!Exception}. *)
-  val make : (unit -> 'a) -> 'a t
-
-  (** [run] performs effects. *)
-  val run : 'a t -> 'a
+  val wunit : w
+  val wprod : w -> w -> w
 
+  type e = unit
 end
 
+module Logical : module type of Logic_monad.Logical(P)
 
-(** {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
+(** {6 Lenses to access to components of the states} *)
 
-    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
-
-(** 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
+module type State = sig
+  type t
+  val get : t Logical.t
+  val set : t -> unit Logical.t
+  val modify : (t->t) -> unit Logical.t
+end
 
+module type Writer = sig
+  type t
+  val put : t -> unit Logical.t
 end
 
-module Logical (P:Param) : sig
+(** Lens to the [proofview]. *)
+module Pv : State with type t := proofview
 
-  include Monad.S
+(** Lens to the [evar_map] of the proofview. *)
+module Solution : State with type t := Evd.evar_map
 
-  val ignore : 'a t -> unit t
+(** Lens to the list of focused goals. *)
+module Comb : State with type t = Evar.t list
 
-  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
+(** Lens to the global environment. *)
+module Env : State with type t := Environ.env
 
-  val zero : exn -> 'a t
-  val plus : 'a t -> (exn -> 'a t) -> 'a t
-  val split : 'a t -> (('a,(exn->'a t)) list_view) t
-  val once : 'a t -> 'a t
-  val break : (exn -> bool) -> 'a t -> 'a t
+(** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
+module Status : Writer with type t := bool
 
-  val lift : 'a NonLogical.t -> 'a t
+(** Lens to the list of goals which have been shelved during the
+    execution of the tactic. *)
+module Shelf : Writer with type t = Evar.t list
 
-  val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w) NonLogical.t
-end
+(** Lens to the list of goals which were given up during the execution
+    of the tactic. *)
+module Giveup : Writer with type t = Evar.t list