diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/logic_monad.ml | 326 | ||||
-rw-r--r-- | proofs/logic_monad.mli | 157 | ||||
-rw-r--r-- | proofs/proofs.mllib | 1 |
3 files changed, 0 insertions, 484 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml deleted file mode 100644 index d509670ec..000000000 --- a/proofs/logic_monad.ml +++ /dev/null @@ -1,326 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * 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. *) - - -(** {6 Exceptions} *) - - -(** 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 - -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 ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) - - (** [try ... with ...] but restricted to {!Exception}. *) - let catch = fun s h -> (); - fun () -> try s () - with Exception e as src -> - let (src, info) = Errors.push src in - h (e, info) () - - let read_line = fun () -> try Pervasives.read_line () with e -> - let (e, info) = Errors.push e in raise ~info e () - - let print_char = fun c -> (); fun () -> print_char c - - (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> - let (e, info) = Errors.push e in raise ~info 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, info) = Errors.push e in - Util.iraise (Exception e, info) - - let run = fun x -> - try x () with Exception e as src -> - let (src, info) = Errors.push src in - Util.iraise (e, info) -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 Exninfo.iexn - | 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 - - (** Update-only. Essentially a writer on [u->u]. *) - type u - - (** [u] must be pointed. *) - val uunit : u - -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; - 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 - 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 rich_exn = Exninfo.iexn - - type 'a iolist = - { iolist : 'r. (rich_exn -> 'r NonLogical.t) -> - ('a -> (rich_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 local (type a) (e:P.e) (m:a t) : a t = (); fun s -> - let m = m { s with rstate = e } in - { iolist = fun nil cons -> - m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) } - - let put (w : P.w) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil } - - let update (f : P.u -> P.u) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) 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 : rich_exn -> rich_exn option) (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 -> match f e with None -> next e | Some e -> nil e)) - } - - (** 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 - - 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, rich_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; ustate = P.uunit; rstate = r; sstate = s } in - let m = m s in - let rnil e = NonLogical.return (Nil e) in - let rcons (x, s) l = - let p = (x, s.sstate, s.wstate, s.ustate) in - NonLogical.return (Cons (p, l)) - in - m.iolist rnil rcons - - let repr x = x - - end diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli deleted file mode 100644 index ab729aff7..000000000 --- a/proofs/logic_monad.mli +++ /dev/null @@ -1,157 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * 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. *) - - -(** {6 Exceptions} *) - - -(** 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 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 : 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 : ?info:Exninfo.info -> exn -> 'a t - (** [try ... with ...] but restricted to {!Exception}. *) - val catch : 'a t -> (Exninfo.iexn -> '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 Exninfo.iexn -| 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 - - (** Update-only. Essentially a writer on [u->u]. *) - type u - - (** [u] must be pointed. *) - val uunit : u - -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 local : P.e -> 'a t -> 'a t - val update : (P.u -> P.u) -> unit t - - 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 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 - - val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t - - val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified - -end diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 32bf5576f..de0879127 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -4,7 +4,6 @@ Evar_refiner Proof_using Proof_type Proof_errors -Logic_monad Proofview_monad Logic Proofview |