diff options
Diffstat (limited to 'proofs/logic_monad.mli')
-rw-r--r-- | proofs/logic_monad.mli | 157 |
1 files changed, 157 insertions, 0 deletions
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli new file mode 100644 index 00000000..ab729aff --- /dev/null +++ b/proofs/logic_monad.mli @@ -0,0 +1,157 @@ +(************************************************************************) +(* 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 |