diff options
-rw-r--r-- | engine/logic_monad.ml | 219 | ||||
-rw-r--r-- | engine/logic_monad.mli | 58 | ||||
-rw-r--r-- | proofs/proofview.ml | 2 | ||||
-rw-r--r-- | proofs/proofview.mli | 9 |
4 files changed, 199 insertions, 89 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 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 diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6e653806b..64ea5aea0 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -887,7 +887,7 @@ module Unsafe = struct end - +module UnsafeRepr = Proof.Unsafe (** {7 Notations} *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5a9e7f39f..98e1477ff 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -405,6 +405,15 @@ module Unsafe : sig val mark_as_goal : proofview -> Evar.t -> proofview end +(** This module gives access to the innards of the monad. Its use is + restricted to very specific cases. *) +module UnsafeRepr : +sig + type state = Proofview_monad.Logical.Unsafe.state + val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t + val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic +end + (** {7 Notations} *) module Notations : sig |