From 038819807ba7cab0bc451dfd1f6772eae110826b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 21 Oct 2014 16:50:47 +0200 Subject: 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. --- proofs/logic_monad.ml | 304 +++++++++++++++++++++++++++++++++++++++++ proofs/logic_monad.mli | 144 +++++++++++++++++++ proofs/proofs.mllib | 2 +- proofs/proofview.ml | 108 +++------------ proofs/proofview.mli | 2 +- proofs/proofview_monad.ml | 334 +++++++++------------------------------------ proofs/proofview_monad.mli | 155 ++++++--------------- 7 files changed, 573 insertions(+), 476 deletions(-) create mode 100644 proofs/logic_monad.ml create mode 100644 proofs/logic_monad.mli (limited to 'proofs') 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 *) +(* 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 *) +(* '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 -- cgit v1.2.3