Exposing the minimal amount of internal of the Logic monad in order to

allow reusability of the implementation throughout the Coq codebase.

We effectively feature a generalized version of the logical monad where the
input state, the output state and the inner exception can be arbitrarily chosen.
This will allow for more efficient implementations of close variants of the
monad.

1 files changed, 137 insertions, 82 deletions

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index cb3e5a186..79bf48acd 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -135,46 +135,13 @@ end
 
 (** 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 Exninfo.iexn
-  | Cons of 'a * 'b
+type ('a, 'b, 'e) list_view =
+  | Nil of 'e
+  | Cons of 'a * ('e -> '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
-
-  (** Update-only. Essentially a writer on [u->u]. *)
-  type u
-
-  (** [u] must be pointed. *)
-  val uunit : u
-
-end
-
-
-module Logical (P:Param) =
+module BackState =
 struct
 
-  (** All three of environment, writer and state are coded as a single
-      state-passing-style monad.*)
-  type state = {
-    rstate : P.e;
-    ustate : P.u;
-    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
@@ -205,32 +172,25 @@ struct
       In that vision, [bind] is simply [concat_map] (though the cps
       version is significantly simpler), [plus] is concatenation, and
       [split] is pattern-matching. *)
-  type rich_exn = Exninfo.iexn
-
-  type 'a iolist =
-    { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) ->
-      ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-      'r NonLogical.t }
-
-  include Monad.Make(struct
-
-    type 'a t = 'a iolist
 
-    let return x =
-      { iolist = fun s nil cons -> cons x s nil }
+  type ('a, 'i, 'o, 'e) t =
+      { iolist : 'r. 'i -> ('e -> 'r NonLogical.t) ->
+                     ('a -> 'o -> ('e -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+                     'r NonLogical.t }
 
-    let (>>=) m f =
-      { iolist = fun s nil cons ->
-        m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
+  let return x =
+    { iolist = fun s nil cons -> cons x s nil }
 
-    let (>>) m f =
-      { iolist = fun s nil cons ->
-        m.iolist s nil (fun () s next -> f.iolist s next cons) }
+  let (>>=) m f =
+    { iolist = fun s nil cons ->
+      m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
 
-    let map f m =
-      { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
+  let (>>) m f =
+    { iolist = fun s nil cons ->
+      m.iolist s nil (fun () s next -> f.iolist s next cons) }
 
-  end)
+  let map f m =
+    { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
 
   let zero e =
     { iolist = fun _ nil cons -> nil e }
@@ -247,27 +207,13 @@ struct
   (** State related *)
 
   let get =
-    { iolist = fun s nil cons -> cons s.sstate s nil }
-
-  let set (sstate : P.s) =
-    { iolist = fun s nil cons -> cons () { s with sstate } nil }
-
-  let modify (f : P.s -> P.s) =
-    { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
-
-  let current =
-    { iolist = fun s nil cons -> cons s.rstate s nil }
-
-  let local e m =
-    { iolist = fun s nil cons ->
-      m.iolist { s with rstate = e } nil
-        (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
+    { iolist = fun s nil cons -> cons s s nil }
 
-  let put w =
-    { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
+  let set s =
+    { iolist = fun _ nil cons -> cons () s nil }
 
-  let update (f : P.u -> P.u) =
-    { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
+  let modify f =
+    { iolist = fun s nil cons -> cons () (f s) nil }
 
   (** List observation *)
 
@@ -281,9 +227,9 @@ struct
 
   (** For [reflect] and [split] see the "Backtracking, Interleaving,
       and Terminating Monad Transformers" paper.  *)
-  type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t
+  type ('a, 'e) reified = ('a, ('a, 'e) reified, 'e) list_view NonLogical.t
 
-  let rec reflect (m : ('a * state) reified) : 'a iolist =
+  let rec reflect (m : ('a * 'o, 'e) reified) =
     { iolist = fun s0 nil cons ->
       let next = function
       | Nil e -> nil e
@@ -292,7 +238,7 @@ struct
       NonLogical.(m >>= next)
     }
 
-  let split m : ('a, rich_exn -> 'a t) list_view t =
+  let split m : ((_, _, _) list_view, _, _, _) t =
     let rnil e = NonLogical.return (Nil e) in
     let rcons p s l = NonLogical.return (Cons ((p, s), l)) in
     { iolist = fun s nil cons ->
@@ -304,6 +250,117 @@ struct
         cons (Cons (x, l)) s nil
       end }
 
+  let run m s =
+    let rnil e = NonLogical.return (Nil e) in
+    let rcons x s l =
+      let p = (x, s) in
+      NonLogical.return (Cons (p, l))
+    in
+    m.iolist s rnil rcons
+
+  let repr x = x
+end
+
+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
+
+  (** Update-only. Essentially a writer on [u->u]. *)
+  type u
+
+  (** [u] must be pointed. *)
+  val uunit : u
+
+end
+
+
+module Logical (P:Param) =
+struct
+
+  module Unsafe =
+  struct
+    (** All three of environment, writer and state are coded as a single
+        state-passing-style monad.*)
+    type state = {
+      rstate : P.e;
+      ustate : P.u;
+      wstate : P.w;
+      sstate : P.s;
+    }
+
+    let make m = m
+    let repr m = m
+  end
+
+  open Unsafe
+
+  type state = Unsafe.state
+
+  type iexn = Exninfo.iexn
+
+  type 'a reified = ('a, iexn) BackState.reified
+
+  (** Inherited from Backstate *)
+
+  open BackState
+
+  include Monad.Make(struct
+    type 'a t = ('a, state, state, iexn) BackState.t
+    let return = BackState.return
+    let (>>=) = BackState.(>>=)
+    let (>>) = BackState.(>>)
+    let map = BackState.map
+  end)
+
+  let zero = BackState.zero
+  let plus = BackState.plus
+  let ignore = BackState.ignore
+  let lift = BackState.lift
+  let once = BackState.once
+  let break = BackState.break
+  let reflect = BackState.reflect
+  let split = BackState.split
+  let repr = BackState.repr
+
+  (** State related. We specialize them here to ensure soundness (for reader and
+      writer) and efficiency. *)
+
+  let get =
+    { iolist = fun s nil cons -> cons s.sstate s nil }
+
+  let set (sstate : P.s) =
+    { iolist = fun s nil cons -> cons () { s with sstate } nil }
+
+  let modify (f : P.s -> P.s) =
+    { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
+
+  let current =
+    { iolist = fun s nil cons -> cons s.rstate s nil }
+
+  let local e m =
+    { iolist = fun s nil cons ->
+      m.iolist { s with rstate = e } nil
+        (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
+
+  let put w =
+    { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
+
+  let update (f : P.u -> P.u) =
+    { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
+
+  (** Monadic run is specialized to handle reader / writer *)
+
   let run m r s =
     let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
     let rnil e = NonLogical.return (Nil e) in
@@ -313,6 +370,4 @@ struct
     in
     m.iolist s rnil rcons
 
-  let repr x = x
-
  end