diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic_monad.ml | 318 | ||||
| -rw-r--r-- | proofs/logic_monad.mli | 157 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.mli | 9 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 270 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 144 |
7 files changed, 10 insertions, 892 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml deleted file mode 100644 index cb3e5a186..000000000 --- a/proofs/logic_monad.ml +++ /dev/null @@ -1,318 +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. 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 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..1bd701cb9 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -4,8 +4,6 @@ Evar_refiner Proof_using Proof_type Proof_errors -Logic_monad -Proofview_monad Logic Proofview Proof diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6e653806b..64ea5aea0 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -887,7 +887,7 @@ module Unsafe = struct end - +module UnsafeRepr = Proof.Unsafe (** {7 Notations} *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5a9e7f39f..98e1477ff 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -405,6 +405,15 @@ module Unsafe : sig val mark_as_goal : proofview -> Evar.t -> proofview end +(** This module gives access to the innards of the monad. Its use is + restricted to very specific cases. *) +module UnsafeRepr : +sig + type state = Proofview_monad.Logical.Unsafe.state + val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t + val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic +end + (** {7 Notations} *) module Notations : sig diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml deleted file mode 100644 index 6e68cd2e4..000000000 --- a/proofs/proofview_monad.ml +++ /dev/null @@ -1,270 +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 datatypes used as internal states by the - tactic monad, and specialises the [Logic_monad] to these type. *) - -(** {6 Trees/forest for traces} *) - -module Trace = struct - - (** The intent is that an ['a forest] is a list of messages of type - ['a]. But messages can stand for a list of more precise - messages, hence the structure is organised as a tree. *) - type 'a forest = 'a tree list - and 'a tree = Seq of 'a * 'a forest - - (** To build a trace incrementally, we use an intermediary data - structure on which we can define an S-expression like language - (like a simplified xml except the closing tags do not carry a - name). Note that nodes are built from right to left in ['a - incr], the result is mirrored when returning so that in the - exposed interface, the forest is read from left to right. - - Concretely, we want to add a new tree to a forest: and we are - building it by adding new trees to the left of its left-most - subtrees which is built the same way. *) - type 'a incr = { head:'a forest ; opened: 'a tree list } - - (** S-expression like language as ['a incr] transformers. It is the - responsibility of the library builder not to use [close] when no - tag is open. *) - let empty_incr = { head=[] ; opened=[] } - let opn a { head ; opened } = { head ; opened = Seq(a,[])::opened } - let close { head ; opened } = - match opened with - | [a] -> { head = a::head ; opened=[] } - | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened } - | [] -> assert false - let leaf a s = close (opn a s) - - (** Returning a forest. It is the responsibility of the library - builder to close all the tags. *) - (* spiwack: I may want to close the tags instead, to deal with - interruptions. *) - let rec mirror f = List.rev_map mirror_tree f - and mirror_tree (Seq(a,f)) = Seq(a,mirror f) - - let to_tree = function - | { head ; opened=[] } -> mirror head - | { head ; opened=_::_} -> assert false - -end - - - -(** {6 State types} *) - -(** We typically label nodes of [Trace.tree] with messages to - print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds -let pr_lazy_msg msg = msg () - -(** Info trace. *) -module Info = struct - - (** The type of the tags for [info]. *) - type tag = - | Msg of lazy_msg (** A simple message *) - | Tactic of lazy_msg (** A tactic call *) - | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *) - | DBranch (** A special marker to delimit individual branch of a dispatch. *) - - type state = tag Trace.incr - type tree = tag Trace.forest - - - - let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)") - - let unbranch = function - | Trace.Seq (DBranch,brs) -> brs - | _ -> assert false - - - let is_empty_branch = let open Trace in function - | Seq(DBranch,[]) -> true - | _ -> false - - (** Dispatch with empty branches are (supposed to be) equivalent to - [idtac] which need not appear, so they are removed from the - trace. *) - let dispatch brs = - let open Trace in - if CList.for_all is_empty_branch brs then None - else Some (Seq(Dispatch,brs)) - - let constr = let open Trace in function - | Dispatch -> dispatch - | t -> fun br -> Some (Seq(t,br)) - - let rec compress_tree = let open Trace in function - | Seq(t,f) -> constr t (compress f) - and compress f = - CList.map_filter compress_tree f - - let rec is_empty = let open Trace in function - | Seq(Dispatch,brs) -> List.for_all is_empty brs - | Seq(DBranch,br) -> List.for_all is_empty br - | _ -> false - - (** [with_sep] is [true] when [Tactic m] must be printed with a - trailing semi-colon. *) - let rec pr_tree with_sep = let open Trace in function - | Seq (Msg m,[]) -> pr_in_comments m - | Seq (Tactic m,_) -> - let tail = if with_sep then Pp.str";" else Pp.mt () in - Pp.(pr_lazy_msg m ++ tail) - | Seq (Dispatch,brs) -> - let tail = if with_sep then Pp.str";" else Pp.mt () in - Pp.(pr_dispatch brs++tail) - | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false - and pr_dispatch brs = - let open Pp in - let brs = List.map unbranch brs in - match brs with - | [br] -> pr_forest br - | _ -> - let sep () = spc()++str"|"++spc() in - let branches = prlist_with_sep sep pr_forest brs in - str"[>"++spc()++branches++spc()++str"]" - and pr_forest = function - | [] -> Pp.mt () - | [tr] -> pr_tree false tr - | tr::l -> Pp.(pr_tree true tr ++ pr_forest l) - - let print f = - pr_forest (compress f) - - let rec collapse_tree n t = - let open Trace in - match n , t with - | 0 , t -> [t] - | _ , (Seq(Tactic _,[]) as t) -> [t] - | n , Seq(Tactic _,f) -> collapse (pred n) f - | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))] - | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))] - | _ , (Seq(Msg _,_) as t) -> [t] - and collapse n f = - CList.map_append (collapse_tree n) f -end - - -(** Type of proof views: current [evar_map] together with the list of - focused goals. *) -type proofview = { solution : Evd.evar_map; comb : Goal.goal list } - - -(** {6 Instantiation of the logic monad} *) - -(** Parameters of the logic monads *) -module P = struct - - type s = proofview * Environ.env - - (** Recording info trace (true) or not. *) - type e = bool - - (** 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 - - type u = Info.state - - let uunit = Trace.empty_incr - -end - -module Logical = Logic_monad.Logical(P) - - -(** {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 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 - -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 - -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 - -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 - -module Status : Writer with type t := bool = struct - let put s = Logical.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 = Logical.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 = Logical.put (true,[],gs) -end - -(** Lens and utilies pertaining to the info trace *) -module InfoL = struct - let recording = Logical.current - let if_recording t = - let open Logical in - recording >>= fun r -> - if r then t else return () - - let record_trace t = Logical.local true t - - let raw_update = Logical.update - let update f = if_recording (raw_update f) - let opn a = update (Trace.opn a) - let close = update Trace.close - let leaf a = update (Trace.leaf a) - - let tag a t = - let open Logical in - recording >>= fun r -> - if r then begin - raw_update (Trace.opn a) >> - t >>= fun a -> - raw_update Trace.close >> - return a - end else - t -end diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli deleted file mode 100644 index d2a2e55fb..000000000 --- a/proofs/proofview_monad.mli +++ /dev/null @@ -1,144 +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 datatypes used as internal states by the - tactic monad, and specialises the [Logic_monad] to these type. *) - -(** {6 Traces} *) - -module Trace : sig - - (** The intent is that an ['a forest] is a list of messages of type - ['a]. But messages can stand for a list of more precise - messages, hence the structure is organised as a tree. *) - type 'a forest = 'a tree list - and 'a tree = Seq of 'a * 'a forest - - (** To build a trace incrementally, we use an intermediary data - structure on which we can define an S-expression like language - (like a simplified xml except the closing tags do not carry a - name). *) - type 'a incr - val to_tree : 'a incr -> 'a forest - - (** [open a] opens a tag with name [a]. *) - val opn : 'a -> 'a incr -> 'a incr - - (** [close] closes the last open tag. It is the responsibility of - the user to close all the tags. *) - val close : 'a incr -> 'a incr - - (** [leaf] creates an empty tag with name [a]. *) - val leaf : 'a -> 'a incr -> 'a incr - -end - -(** {6 State types} *) - -(** We typically label nodes of [Trace.tree] with messages to - print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds - -(** Info trace. *) -module Info : sig - - (** The type of the tags for [info]. *) - type tag = - | Msg of lazy_msg (** A simple message *) - | Tactic of lazy_msg (** A tactic call *) - | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *) - | DBranch (** A special marker to delimit individual branch of a dispatch. *) - - type state = tag Trace.incr - type tree = tag Trace.forest - - val print : tree -> Pp.std_ppcmds - - (** [collapse n t] flattens the first [n] levels of [Tactic] in an - info trace, effectively forgetting about the [n] top level of - names (if there are fewer, the last name is kept). *) - val collapse : int -> tree -> tree - -end - -(** Type of proof views: current [evar_map] together with the list of - focused goals. *) -type proofview = { solution : Evd.evar_map; comb : Goal.goal list } - -(** {6 Instantiation of the logic monad} *) - -module P : sig - type s = proofview * Environ.env - - (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list * Evar.t list - - val wunit : w - val wprod : w -> w -> w - - (** Recording info trace (true) or not. *) - type e = bool - - type u = Info.state - - val uunit : u -end - -module Logical : module type of Logic_monad.Logical(P) - - -(** {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 - -(** Lens to the [proofview]. *) -module Pv : State with type t := proofview - -(** Lens to the [evar_map] of the proofview. *) -module Solution : State with type t := Evd.evar_map - -(** Lens to the list of focused goals. *) -module Comb : State with type t = Evar.t list - -(** Lens to the global environment. *) -module Env : State with type t := Environ.env - -(** Lens to the tactic status ([true] if safe, [false] if unsafe) *) -module Status : Writer with type t := bool - -(** 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 - -(** 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 - -(** Lens and utilies pertaining to the info trace *) -module InfoL : sig - (** [record_trace t] behaves like [t] and compute its [info] trace. *) - val record_trace : 'a Logical.t -> 'a Logical.t - - val update : (Info.state -> Info.state) -> unit Logical.t - val opn : Info.tag -> unit Logical.t - val close : unit Logical.t - val leaf : Info.tag -> unit Logical.t - - (** [tag a t] opens tag [a] runs [t] then closes the tag. *) - val tag : Info.tag -> 'a Logical.t -> 'a Logical.t -end |