From 87c8236de9a8141ea6925cf4390a971f0a941ae8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 19 Apr 2015 12:25:50 +0200
Subject: 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.
---
 engine/logic_monad.mli | 58 ++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 52 insertions(+), 6 deletions(-)

(limited to 'engine/logic_monad.mli')

diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index ab729aff7..42e49d5a7 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -97,9 +97,41 @@ 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 BackState : sig
+
+  type (+'a, -'i, +'o, 'e) t
+  val return : 'a -> ('a, 's, 's, 'e) t
+  val (>>=) : ('a, 'i, 'm, 'e) t -> ('a -> ('b, 'm, 'o, 'e) t) -> ('b, 'i, 'o, 'e) t
+  val (>>) : (unit, 'i, 'm, 'e) t -> ('b, 'm, 'o, 'e) t -> ('b, 'i, 'o, 'e) t
+  val map : ('a -> 'b) -> ('a, 'i, 'o, 'e) t -> ('b, 'i, 'o, 'e) t
+
+  val ignore : ('a, 'i, 'o, 'e) t -> (unit, 'i, 'o, 'e) t
+
+  val set : 'o -> (unit, 'i, 'o, 'e) t
+  val get : ('s, 's, 's, 'e) t
+  val modify : ('i -> 'o) -> (unit, 'i, 'o, 'e) t
+
+  val zero : 'e -> ('a, 'i, 'o, 'e) t
+  val plus : ('a, 'i, 'o, 'e) t -> ('e -> ('a, 'i, 'o, 'e) t) -> ('a, 'i, 'o, 'e) t
+
+  val split : ('a, 's, 's, 'e) t ->
+    (('a, ('a, 'i, 's, 'e) t, 'e) list_view, 's, 's, 'e) t
+
+  val once : ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t
+  val break : ('e -> 'e option) -> ('a, 'i, 'o, 'e) t -> ('a, 'i, 'o, 'e) t
+  val lift : 'a NonLogical.t -> ('a, 's, 's, 'e) t
+
+  type ('a, 'e) reified
+
+  val repr : ('a, 'e) reified -> ('a, ('a, 'e) reified, 'e) list_view NonLogical.t
+
+  val run : ('a, 'i, 'o, 'e) t -> 'i -> ('a * 'o, 'e) reified
+
+end
 
 (** The monad is parametrised in the types of state, environment and
     writer. *)
@@ -142,16 +174,30 @@ module Logical (P:Param) : sig
 
   val zero : Exninfo.iexn -> 'a t
   val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t
+  val split : 'a t -> ('a, 'a t, Exninfo.iexn) list_view t
   val once : 'a t -> 'a t
   val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t
 
   val lift : 'a NonLogical.t -> 'a t
 
-  type 'a reified
+  type 'a reified = ('a, Exninfo.iexn) BackState.reified
 
-  val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t
+  val repr : 'a reified -> ('a, 'a reified, Exninfo.iexn) list_view NonLogical.t
 
   val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified
 
+  module Unsafe :
+  sig
+    type state = {
+      rstate : P.e;
+      ustate : P.u;
+      wstate : P.w;
+      sstate : P.s;
+    }
+
+    val make : ('a, state, state, Exninfo.iexn) BackState.t -> 'a t
+    val repr : 'a t -> ('a, state, state, Exninfo.iexn) BackState.t
+
+  end
+
 end
-- 
cgit v1.2.3