diff options
Diffstat (limited to 'proofs/proofview_monad.mli')
| -rw-r--r-- | proofs/proofview_monad.mli | 155 |
1 files changed, 41 insertions, 114 deletions
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 |