diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 58 | ||||
| -rw-r--r-- | proofs/clenv.mli | 1 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 12 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/logic_monad.ml | 321 | ||||
| -rw-r--r-- | proofs/logic_monad.mli | 162 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 46 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 9 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 107 | ||||
| -rw-r--r-- | proofs/proofview.mli | 104 | ||||
| -rw-r--r-- | proofs/proofview_monad.ml | 275 | ||||
| -rw-r--r-- | proofs/proofview_monad.mli | 148 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.mli | 3 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 18 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 53 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 5 |
22 files changed, 283 insertions, 1062 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 88e1bce95..1ef0b087b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -24,6 +24,7 @@ open Pretype_errors open Evarutil open Unification open Misctypes +open Sigma.Notations (* Abbreviations *) @@ -119,7 +120,7 @@ let clenv_environments evd bound t = clrec (evd,[]) bound t let mk_clenv_from_env env sigma n (c,cty) = - let evd = create_goal_evar_defs sigma in + let evd = clear_metas sigma in let (evd,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; @@ -335,22 +336,15 @@ let clenv_pose_metas_as_evars clenv dep_mvs = else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in - let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in + let evd = Sigma.Unsafe.of_evar_map clenv.evd in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs (******************************************************************) -let connect_clenv gls clenv = - let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in - { clenv with - evd = evd ; - env = Goal.V82.env evd (sig_it gls) } - -(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *) -(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *) - (* [clenv_fchain mv clenv clenv'] * * Resolves the value of "mv" (which must be undefined) in clenv to be @@ -432,6 +426,44 @@ let check_bindings bl = str " occurs more than once in binding list.") | [] -> () +let explain_no_such_bound_variable evd id = + let fold l (n, clb) = + let na = match clb with + | Cltyp (na, _) -> na + | Clval (na, _, _) -> na + in + if na != Anonymous then out_name na :: l else l + in + let mvl = List.fold_left fold [] (Evd.meta_list evd) in + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id ++ + (if mvl == [] then str " (no bound variables at all in the expression)." + else + (str" (possible name" ++ + str (if List.length mvl == 1 then " is: " else "s are: ") ++ + pr_enum pr_id mvl ++ str")."))) + +let meta_with_name evd id = + let na = Name id in + let fold (l1, l2 as l) (n, clb) = + let (na',def) = match clb with + | Cltyp (na, _) -> (na, false) + | Clval (na, _, _) -> (na, true) + in + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l + in + let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in + match mvnodef, mvl with + | _,[] -> + explain_no_such_bound_variable evd id + | ([n],_|_,[n]) -> + n + | _ -> + errorlabstrm "Evd.meta_with_name" + (str "Binder name \"" ++ pr_id id ++ + strbrk "\" occurs more than once in clause.") + let meta_of_binder clause loc mvs = function | NamedHyp s -> meta_with_name clause.evd s | AnonHyp n -> @@ -576,7 +608,9 @@ let make_evar_clause env sigma ?len t = | Cast (t, _, _) -> clrec (sigma, holes) n t | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in - let sigma, ev = new_evar ~store env sigma t1 in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let sigma = Sigma.to_evar_map sigma in let dep = dependent (mkRel 1) t2 in let hole = { hole_evar = ev; diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 7ecc26ec9..59b166ea0 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -49,7 +49,6 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst (** {6 linking of clenvs } *) -val connect_clenv : Goal.goal sigma -> clausenv -> clausenv val clenv_fchain : ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8e9225992..08e6c91de 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -16,7 +16,7 @@ open Logic open Reduction open Tacmach open Clenv - +open Proofview.Notations (* This function put casts around metavariables whose type could not be * infered by the refiner, that is head of applications, predicates and @@ -83,10 +83,10 @@ open Unification let dft = default_unify_flags let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let clenv gl = clenv_unique_resolver ~flags clenv gl in clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) - end + end } (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en particulier ne semblent pas vérifier que des instances différentes @@ -118,12 +118,12 @@ let fail_quick_unif_flags = { (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unify ?(flags=fail_quick_unif_flags) m = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in let n = Tacmach.New.pf_nf_concl gl in - let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in + let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' with e when Errors.noncritical e -> Proofview.tclZERO e - end + end } diff --git a/proofs/goal.mli b/proofs/goal.mli index 6152826ca..8a3d6e815 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -67,7 +67,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index ed3a1df1a..99e32db04 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -95,12 +95,12 @@ let check_typability env sigma c = forces the user to give them in order). *) let clear_hyps env sigma ids sign cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in (hyps, cl, !evdref) let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in (hyps, t, cl, !evdref) @@ -532,7 +532,7 @@ let prim_refiner r sigma goal = push_named_context_val (id,None,t) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in + let oterm = Term.mkNamedLetIn id ev1 t ev2 in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) diff --git a/proofs/logic.mli b/proofs/logic.mli index ed99d3a38..9aa4ac207 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -53,4 +53,4 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.named_declaration -> Environ.named_context_val + Context.Named.Declaration.t -> Environ.named_context_val diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml deleted file mode 100644 index 68efa71e8..000000000 --- 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 diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli deleted file mode 100644 index 96655d538..000000000 --- a/proofs/logic_monad.mli +++ /dev/null @@ -1,162 +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 - - -(** {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 - - (** Loggers. The buffer is also flushed. *) - val print_debug : Pp.std_ppcmds -> unit t - val print_warning : Pp.std_ppcmds -> unit t - val print_notice : Pp.std_ppcmds -> unit t - val print_info : Pp.std_ppcmds -> unit t - val print_error : 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/pfedit.ml b/proofs/pfedit.ml index b635cc963..20d696fd9 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -138,7 +138,8 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - start_proof id goal_kind evd sign typ (fun _ -> ()); + let terminator = Proof_global.make_terminator (fun _ -> ()) in + start_proof id goal_kind evd sign typ terminator; try let status = by tac in let _,(const,univs,_) = cook_proof () in @@ -214,7 +215,7 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f22cdbcc8..fc33e9a65 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -92,6 +92,9 @@ type pstate = { universe_binders: universe_binders option; } +let make_terminator f = f +let apply_terminator f = f + (* The head of [!pstates] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) @@ -299,6 +302,11 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf +let constrain_variables init uctx = + let levels = Univ.Instance.levels (Univ.UContext.instance init) in + let cstrs = UState.constrain_variables levels uctx in + Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) + let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in @@ -329,7 +337,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) @@ -338,7 +346,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* Since the proof is computed now, we can simply have 1 set of * constraints in which we merge the ones for the body and the ones * for the typ *) @@ -353,7 +361,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let initunivs = Evd.evar_context_universe_context initial_euctx in Future.from_val (initunivs, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff) + (pt,constrain_variables initunivs (Future.force univs)),eff) in let entries = Future.map2 (fun p (_, t) -> @@ -458,7 +466,7 @@ module Bullet = struct type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> std_ppcmds } let behaviors = Hashtbl.create 4 @@ -468,7 +476,7 @@ module Bullet = struct let none = { name = "None"; put = (fun x _ -> x); - suggest = (fun _ -> None) + suggest = (fun _ -> mt ()) } let _ = register_behavior none @@ -484,26 +492,20 @@ module Bullet = struct (* give a message only if more informative than the standard coq message *) let suggest_on_solved_goal sugg = match sugg with - | NeedClosingBrace -> Some "Try unfocusing with \"}\"." - | NoBulletInUse -> None - | ProofFinished -> None - | Suggest b -> Some ("Focus next goal with bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^".") - | Unfinished b -> Some ("The current bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is unfinished.") + | NeedClosingBrace -> str"Try unfocusing with \"}\"." + | NoBulletInUse -> mt () + | ProofFinished -> mt () + | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"." + | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished." (* give always a message. *) let suggest_on_error sugg = match sugg with - | NeedClosingBrace -> "Try unfocusing with \"}\"." + | NeedClosingBrace -> str"Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> "No more subgoals." - | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is mandatory here.") - | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is not finished.") + | ProofFinished -> str"No more subgoals." + | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here." + | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." exception FailedBullet of t * suggestion @@ -511,8 +513,8 @@ module Bullet = struct Errors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in - Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) + let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in + Errors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg) | _ -> raise Errors.Unhandled) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 7fbd183e6..ebe7f6d6f 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -70,9 +70,12 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object -type proof_terminator = proof_ending -> unit +type proof_terminator type closed_proof = proof_object * proof_terminator +val make_terminator : (proof_ending -> unit) -> proof_terminator +val apply_terminator : proof_terminator -> proof_ending -> unit + (** [start_proof id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -169,7 +172,7 @@ module Bullet : sig type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> Pp.std_ppcmds } (** A registered behavior can then be accessed in Coq @@ -186,7 +189,7 @@ module Bullet : sig (** Handles focusing/defocusing with bullets: *) val put : Proof.proof -> t -> Proof.proof - val suggest : Proof.proof -> string option + val suggest : Proof.proof -> Pp.std_ppcmds 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 49228c93a..8008b0025 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -16,6 +16,7 @@ open Pp open Util open Proofview_monad +open Sigma.Notations (** Main state of tactics *) type proofview = Proofview_monad.proofview @@ -64,7 +65,9 @@ let dependent_init = let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in @@ -350,7 +353,7 @@ exception NoSuchGoals of int (* This hook returns a string to be appended to the usual message. Primarily used to add a suggestion about the right bullet to use to focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> string option) ref = ref ((fun n -> None)) +let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ()) let set_nosuchgoals_hook f = nosuchgoals_hook := f @@ -358,10 +361,9 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f (* This uses the hook above *) let _ = Errors.register_handler begin function | NoSuchGoals n -> - let suffix:string option = (!nosuchgoals_hook) n in + let suffix = !nosuchgoals_hook n in Errors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." - ++ pr_opt str suffix) + (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) | _ -> raise Errors.Unhandled end @@ -907,19 +909,11 @@ module Unsafe = struct end +module UnsafeRepr = Proof.Unsafe - -(** {7 Notations} *) - -module Notations = struct - let (>>=) = tclBIND - let (<*>) = tclTHEN - let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) -end - -open Notations - - +let (>>=) = tclBIND +let (<*>) = tclTHEN +let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) (** {6 Goal-dependent tactics} *) @@ -933,17 +927,20 @@ let catchable_exception = function module Goal = struct - type 'a t = { + type ('a, 'r) t = { env : Environ.env; sigma : Evd.evar_map; concl : Term.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } - let assume (gl : 'a t) = (gl :> [ `NF ] t) + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } + + let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) let env { env=env } = env - let sigma { sigma=sigma } = sigma + let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma let hyps { env=env } = Environ.named_context env let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self @@ -969,7 +966,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f.enter gl)) with e when catchable_exception e -> let (e, info) = Errors.push e in tclZERO ~info e @@ -987,7 +984,7 @@ module Goal = struct gmake_with info env sigma goal let enter f = - let f gl = InfoL.tag (Info.DBranch) (f gl) in + let f gl = InfoL.tag (Info.DBranch) (f.enter gl) in InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> Env.get >>= fun env -> @@ -999,6 +996,41 @@ module Goal = struct end end + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } + + let s_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let gl = gmake env sigma goal in + let Sigma (tac, sigma, _) = f.s_enter gl in + let sigma = Sigma.to_evar_map sigma in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + + let nf_s_enter f = + InfoL.tag (Info.Dispatch) begin + iter_goal begin fun goal -> + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + let (gl, sigma) = nf_gmake env sigma goal in + let Sigma (tac, sigma, _) = f.s_enter gl in + let sigma = Sigma.to_evar_map sigma in + tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac) + with e when catchable_exception e -> + let (e, info) = Errors.push e in + tclZERO ~info e + end + end + let goals = Env.get >>= fun env -> Pv.get >>= fun step -> @@ -1018,6 +1050,8 @@ module Goal = struct (* compatibility *) let goal { self=self } = self + let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) + end @@ -1066,8 +1100,9 @@ struct let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () - let refine ?(unsafe = true) f = Goal.enter begin fun gl -> + let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl -> let sigma = Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in let env = Goal.env gl in let concl = Goal.concl gl in (** Save the [future_goals] state to restore them after the @@ -1075,7 +1110,7 @@ struct let prev_future_goals = Evd.future_goals sigma in let prev_principal_goal = Evd.principal_future_goal sigma in (** Create the refinement term *) - let (sigma, c) = f (Evd.reset_future_goals sigma) in + let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in (** Check that the introduced evars are well-typed *) @@ -1106,7 +1141,7 @@ struct let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.modify (fun ps -> { ps with solution = sigma; comb; }) - end + end } (** Useful definitions *) @@ -1118,12 +1153,16 @@ struct in evd , j'.Environ.uj_val - let refine_casted ?unsafe f = Goal.enter begin fun gl -> + let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl -> let concl = Goal.concl gl in let env = Goal.env gl in - let f h = let (h, c) = f h in with_type env h c concl in + let f = { run = fun h -> + let Sigma (c, h, p) = f.run h in + let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) + } in refine ?unsafe f - end + end } end @@ -1258,3 +1297,15 @@ module V82 = struct let (e, info) = Errors.push e in tclZERO ~info e end + +(** {7 Notations} *) + +module Notations = struct + let (>>=) = tclBIND + let (<*>) = tclTHEN + let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } +end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2157459f4..dc97e44b6 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -235,7 +235,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic This hook is used to add a suggestion about bullets when applicable. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> string option) -> unit +val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic @@ -409,65 +409,84 @@ module Unsafe : sig val mark_as_goal : proofview -> Evar.t -> proofview end -(** {7 Notations} *) - -module Notations : sig - - (** {!tclBIND} *) - val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - (** {!tclTHEN} *) - val (<*>) : unit tactic -> 'a tactic -> 'a tactic - (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) - val (<+>) : 'a tactic -> 'a tactic -> 'a tactic - +(** 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 - (** {6 Goal-dependent tactics} *) module Goal : sig - (** The type of goals. The parameter type is a phantom argument indicating - whether the data contained in the goal has been normalized w.r.t. the - current sigma. If it is the case, it is flagged [ `NF ]. You may still - access the un-normalized data using {!assume} if you known you do not rely - on the assumption of being normalized, at your own risk. *) - type 'a t + (** Type of goals. + + The first parameter type is a phantom argument indicating whether the data + contained in the goal has been normalized w.r.t. the current sigma. If it + is the case, it is flagged [ `NF ]. You may still access the un-normalized + data using {!assume} if you known you do not rely on the assumption of + being normalized, at your own risk. + + The second parameter is a stage indicating where the goal belongs. See + module {!Sigma}. + *) + type ('a, 'r) t (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t + val assume : ('a, 'r) t -> ([ `NF ], 'r) t (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic + val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : [ `NF ] t -> Term.constr - val hyps : [ `NF ] t -> Context.named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t + val concl : ([ `NF ], 'r) t -> Term.constr + val hyps : ([ `NF ], 'r) t -> Context.Named.t + val env : ('a, 'r) t -> Environ.env + val sigma : ('a, 'r) t -> 'r Sigma.t + val extra : ('a, 'r) t -> Evd.Store.t (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : 'a t -> Term.constr + val raw_concl : ('a, 'r) t -> Term.constr + + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic + val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic + val enter : ([ `LZ ], unit tactic) enter -> unit tactic + + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } - (** Recover the list of current goals under focus, without evar-normalization *) - val goals : [ `LZ ] t tactic list tactic + (** A variant of {!enter} allows to work with a monotonic state. The evarmap + returned by the argument is put back into the current state before firing + the returned tactic. *) + val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic + + (** Like {!s_enter}, but normalizes the goal beforehand. *) + val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic + + (** Recover the list of current goals under focus, without evar-normalization. + FIXME: encapsulate the level in an existential type. *) + val goals : ([ `LZ ], 'r) t tactic list tactic (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t + val goal : ([ `NF ], 'r) t -> Evar.t + + (** Every goal is valid at a later stage. FIXME: take a later evarmap *) + val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t end @@ -482,7 +501,7 @@ module Refine : sig (** {7 Refinement primitives} *) - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic + val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic (** In [refine ?unsafe t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the @@ -498,7 +517,7 @@ module Refine : sig (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) - val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic + val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) @@ -578,3 +597,20 @@ module V82 : sig the monad. *) val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic end + +(** {7 Notations} *) + +module Notations : sig + + (** {!tclBIND} *) + val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic + (** {!tclTHEN} *) + val (<*>) : unit tactic -> 'a tactic -> 'a tactic + (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) + val (<+>) : 'a tactic -> 'a tactic -> 'a tactic + + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } +end diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml deleted file mode 100644 index e9bc7761e..000000000 --- a/proofs/proofview_monad.ml +++ /dev/null @@ -1,275 +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 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; - shelf : 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 - - let wunit = true , [] - let wprod (b1, g1) (b2, g2) = b1 && b2 , 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 : 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 {shelf} -> shelf) Pv.get - let set c = Pv.modify (fun pv -> { pv with shelf = c }) - let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) -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 7a6ea10fe..000000000 --- a/proofs/proofview_monad.mli +++ /dev/null @@ -1,148 +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 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; - shelf : Goal.goal list; -} - -(** {6 Instantiation of the logic monad} *) - -module P : sig - type s = proofview * Environ.env - - (** Status (safe/unsafe) * given up *) - type w = bool * 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 : State 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 diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ea21917ac..818805a56 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -158,8 +158,6 @@ let make_flag env f = f.rConst red in red -let is_reference = function PRef _ | PVar _ -> true | _ -> false - (* table of custom reductino fonctions, not synchronized, filled via ML calls to [declare_reduction] *) let reduction_tab = ref String.Map.empty diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458c..8d6bdf6ae 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -197,10 +197,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.named_context = pf_hyps goal in + let oldhyps:Context.Named.t = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.named_context list = + let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in let newhyps = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 13a9be59e..dd9153a02 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Evd open Proof_type @@ -16,7 +15,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a75b6fa0f..a1ebacea8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -48,7 +48,7 @@ let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = try - Context.lookup_named id (pf_hyps gls) + Context.Named.lookup id (pf_hyps gls) with Not_found -> raise (RefinerError (NoSuchHyp id)) @@ -158,11 +158,15 @@ let pr_glls glls = (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct + let project gl = + let sigma = Proofview.Goal.sigma gl in + Sigma.to_evar_map sigma + let pf_apply f gl = - f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + f (Proofview.Goal.env gl) (project gl) let of_old f gl = - f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl } + f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } let pf_global id gl = (** We only check for the existence of an [id] in [hyps] *) @@ -194,7 +198,7 @@ module New = struct let pf_get_hyp id gl = let hyps = Proofview.Goal.hyps gl in let sign = - try Context.lookup_named id hyps + try Context.Named.lookup id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign @@ -212,11 +216,11 @@ module New = struct let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) = (** We normalize the conclusion just after *) let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = project gl in nf_evar sigma concl let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t @@ -235,6 +239,6 @@ module New = struct let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t + let pf_nf_evar gl t = nf_evar (project gl) t end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7e943cb18..f786b5f21 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Evd open Proof_type @@ -34,18 +33,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t (*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration +val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types -val pf_get_hyp : goal sigma -> Id.t -> named_declaration +val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -106,36 +105,38 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : identifier -> 'a Proofview.Goal.t -> constr - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + (** FIXME: encapsulate the level in an existential type. *) + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : [ `NF ] Proofview.Goal.t -> types + val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map + val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types - val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool - val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list + val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> [ `NF ] Proofview.Goal.t -> types - val pf_last_hyp : [ `NF ] Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr end diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index a4a447e88..d33278ff8 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -12,6 +12,7 @@ open Pp open Tacexpr open Termops open Nameops +open Proofview.Notations let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -47,10 +48,10 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) - end + end } (* Prints the commands *) |