aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/logic_monad.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/logic_monad.ml')
-rw-r--r--engine/logic_monad.ml219
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