diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /proofs/logic_monad.ml | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'proofs/logic_monad.ml')
-rw-r--r-- | proofs/logic_monad.ml | 321 |
1 files changed, 0 insertions, 321 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml deleted file mode 100644 index 68efa71e..00000000 --- a/proofs/logic_monad.ml +++ /dev/null @@ -1,321 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \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 - - 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) - - (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) - let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) - let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) - - 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 rationale 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. 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 } - - let (>>=) m f = - { iolist = fun s nil cons -> - m.iolist s nil (fun x s next -> (f x).iolist s next cons) } - - let (>>) m f = - { iolist = fun s nil cons -> - m.iolist s nil (fun () s next -> f.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) } - - end) - - let zero e = - { iolist = fun _ nil cons -> nil e } - - let plus m1 m2 = - { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons } - - let ignore m = - { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } - - let lift m = - { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } - - (** 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) } - - 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 } - - (** List observation *) - - let once m = - { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) } - - let break f m = - { iolist = fun s nil cons -> - m.iolist s nil (fun x s next -> cons x s (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 * state) reified) : 'a iolist = - { iolist = fun s0 nil cons -> - let next = function - | Nil e -> nil e - | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) - in - NonLogical.(m >>= next) - } - - let split m : ('a, rich_exn -> 'a t) 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 -> - let open NonLogical in - m.iolist s rnil rcons >>= begin function - | Nil e -> cons (Nil e) s nil - | Cons ((x, s), l) -> - let l e = 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 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 s rnil rcons - - let repr x = x - - end |