diff options
53 files changed, 687 insertions, 367 deletions
diff --git a/clib/cMap.ml b/clib/cMap.ml index baac892b9e..8d822667c3 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -58,6 +58,7 @@ module MapExt (M : Map.OrderedType) : sig type 'a map = 'a Map.Make(M).t val set : M.t -> 'a -> 'a map -> 'a map + val get : M.t -> 'a map -> 'a val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map val domain : 'a map -> Set.Make(M).t val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map @@ -124,6 +125,14 @@ struct if r == r' then s else map_inj (MNode {l; v=k'; d=v'; r=r'; h}) + let rec get k (s:'a map) : 'a = match map_prj s with + | MEmpty -> assert false + | MNode {l; v=k'; d=v; r; h} -> + let c = M.compare k k' in + if c < 0 then get k l + else if c = 0 then v + else get k r + let rec modify k f (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found | MNode {l; v; d; r; h} -> @@ -324,5 +333,4 @@ module Make(M : Map.OrderedType) = struct include Map.Make(M) include MapExt(M) - let get k m = try find k m with Not_found -> assert false end diff --git a/clib/hMap.ml b/clib/hMap.ml index f77068b477..9858477489 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -367,7 +367,10 @@ struct | None -> None | Some m -> Map.find_opt k m - let get k s = try find k s with Not_found -> assert false + let get k s = + let h = M.hash k in + let m = Int.Map.get h s in + Map.get k m let split k s = assert false (** Cannot be implemented efficiently *) diff --git a/clib/int.ml b/clib/int.ml index ee4b3128d5..e0dbfb5274 100644 --- a/clib/int.ml +++ b/clib/int.ml @@ -42,6 +42,13 @@ struct else if i = k then v else find i r + let rec get i s = match map_prj s with + | MEmpty -> assert false + | MNode (l, k, v, r, h) -> + if i < k then get i l + else if i = k then v + else get i r + let rec find_opt i s = match map_prj s with | MEmpty -> None | MNode (l, k, v, r, h) -> diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh new file mode 100644 index 0000000000..f4840c2a83 --- /dev/null +++ b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then + + equations_CI_REF=proof+private_entry + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index ab9df12766..8ab00c6fd8 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,8 @@ ### ML API +- Function UnivGen.global_of_constr has been removed. + - Functions and types deprecated in 8.10 have been removed in Coq 8.11. diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh index ea96de970a..ec59a6047f 100755 --- a/dev/tools/make-changelog.sh +++ b/dev/tools/make-changelog.sh @@ -7,7 +7,8 @@ echo "Where? (type a prefix)" (cd doc/changelog && ls -d */) read -r where -where=$(echo doc/changelog/"$where"*) +where="doc/changelog/$where" +if ! [ -d "$where" ]; then where=$(echo "$where"*); fi where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst" # shellcheck disable=SC2016 diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst new file mode 100644 index 0000000000..09bef82c80 --- /dev/null +++ b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst @@ -0,0 +1,11 @@ +- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + only run their tactic argument once, even if it has multiple + successes. This prevents blow-up and looping from using + multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 + <https://github.com/coq/coq/issues/10965>`_, by Jason Gross). + +- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + behave correctly when their tactic fully solves the goal. (`#10966 + <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 + <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst new file mode 100644 index 0000000000..c1df728c5c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -0,0 +1,6 @@ +- Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 <https://github.com/coq/coq/pull/10494>`_, + by Jim Fehrle). diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index c08a9ed0e6..6410620b40 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1046,6 +1046,67 @@ between universes for inductive types in the Type hierarchy. exT_intro : forall X:Type, P X -> exType P. +.. example:: Negative occurrence (first example) + + The following inductive definition is rejected because it does not + satisfy the positivity condition: + + .. coqtop:: all + + Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I. + + If we were to accept such definition, we could derive a + contradiction from it (we can test this by disabling the + :flag:`Positivity Checking` flag): + + .. coqtop:: none + + Unset Positivity Checking. + Inductive I : Prop := not_I_I (not_I : I -> False) : I. + Set Positivity Checking. + + .. coqtop:: all + + Definition I_not_I : I -> ~ I := fun i => + match i with not_I_I not_I => not_I end. + + .. coqtop:: in + + Lemma contradiction : False. + Proof. + enough (I /\ ~ I) as [] by contradiction. + split. + - apply not_I_I. + intro. + now apply I_not_I. + - intro. + now apply I_not_I. + Qed. + +.. example:: Negative occurrence (second example) + + Here is another example of an inductive definition which is + rejected because it does not satify the positivity condition: + + .. coqtop:: all + + Fail Inductive Lam := lam (_ : Lam -> Lam). + + Again, if we were to accept it, we could derive a contradiction + (this time through a non-terminating recursive function): + + .. coqtop:: none + + Unset Positivity Checking. + Inductive Lam := lam (_ : Lam -> Lam). + Set Positivity Checking. + + .. coqtop:: all + + Fixpoint infinite_loop l : False := + match l with lam x => infinite_loop (x l) end. + + Check infinite_loop (lam (@id Lam)) : False. .. _Template-polymorphism: diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 79eddbd3b5..6efc634087 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. + This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and + behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr` + has at least one success. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -528,7 +530,7 @@ success: :name: assert_succeeds This behaves like - :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. + :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`. Solving ~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 57a54bc0ad..00f8269dc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. + Experimental: Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + .. cmdv:: Show Conjectures :name: Show Conjectures @@ -624,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added diff --git a/engine/univGen.ml b/engine/univGen.ml index b1ed3b2694..1fe09270ba 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -82,14 +82,6 @@ let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty | IsGlobal gr -> fresh_global_instance env gr -let global_of_constr c = - match kind c with - | Const (c, u) -> GlobRef.ConstRef c, u - | Ind (i, u) -> GlobRef.IndRef i, u - | Construct (c, u) -> GlobRef.ConstructRef c, u - | Var id -> GlobRef.VarRef id, Instance.empty - | _ -> raise Not_found - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty diff --git a/engine/univGen.mli b/engine/univGen.mli index 1c8735bfa8..1b351c61c4 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -54,9 +54,6 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const val fresh_universe_context_set_instance : ContextSet.t -> universe_level_subst * ContextSet.t -(** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> GlobRef.t puniverses - (** Create a fresh global in the global environment, without side effects. BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. diff --git a/kernel/environ.ml b/kernel/environ.ml index 98d66cafa1..2bee2f7a8e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -231,22 +231,26 @@ let fold_inductives f env acc = (* Global constants *) let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.Globals.constants + Cmap_env.get kn env.env_globals.Globals.constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.Globals.constants) + fst (lookup_constant_key kn env) + +let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants (* Mutual Inductives *) +let lookup_mind_key kn env = + Mindmap_env.get kn env.env_globals.Globals.inductives + let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.Globals.inductives) + fst (lookup_mind_key kn env) + +let mem_mind kn env = Mindmap_env.mem kn env.env_globals.Globals.inductives let mind_context env mind = let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.Globals.inductives - let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in diff --git a/kernel/environ.mli b/kernel/environ.mli index 5af2a7288b..782ea1c666 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -201,10 +201,12 @@ val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_in val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body val evaluable_constant : Constant.t -> env -> bool +val mem_constant : Constant.t -> env -> bool + (** New-style polymorphism *) val polymorphic_constant : Constant.t -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool @@ -215,7 +217,7 @@ val type_in_type_constant : Constant.t -> env -> bool [c] is opaque, [NotEvaluableConst NoBody] if it has no body, [NotEvaluableConst IsProj] if [c] is a projection, [NotEvaluableConst (IsPrimitive p)] if [c] is primitive [p] - and [Not_found] if it does not exist in [env] *) + and an anomaly if it does not exist in [env] *) type const_evaluation_result = | NoBody @@ -254,9 +256,11 @@ val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names - raises [Not_found] if the required path is not found *) + raises an anomaly if the required path is not found *) val lookup_mind : MutInd.t -> env -> mutual_inductive_body +val mem_mind : MutInd.t -> env -> bool + (** The universe context associated to the inductive, empty if not polymorphic *) val mind_context : env -> MutInd.t -> Univ.AUContext.t diff --git a/kernel/names.ml b/kernel/names.ml index 9802d4f531..b755ff0e08 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -675,6 +675,7 @@ module InductiveOrdered_env = struct end module Indset = Set.Make(InductiveOrdered) +module Indset_env = Set.Make(InductiveOrdered_env) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) @@ -688,6 +689,8 @@ module ConstructorOrdered_env = struct let compare = constructor_user_ord end +module Constrset = Set.Make(ConstructorOrdered) +module Constrset_env = Set.Make(ConstructorOrdered_env) module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 78eb9295d4..0c92a2f2bc 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -471,7 +471,7 @@ end module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset -module Mindmap_env : CSig.MapS with type key = MutInd.t +module Mindmap_env : CMap.ExtS with type key = MutInd.t (** Designation of a (particular) inductive type. *) type inductive = MutInd.t (* the name of the inductive type *) @@ -484,11 +484,14 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) -module Indset : CSig.SetS with type elt = inductive -module Indmap : CSig.MapS with type key = inductive -module Constrmap : CSig.MapS with type key = constructor -module Indmap_env : CSig.MapS with type key = inductive -module Constrmap_env : CSig.MapS with type key = constructor +module Indset : CSet.S with type elt = inductive +module Constrset : CSet.S with type elt = constructor +module Indset_env : CSet.S with type elt = inductive +module Constrset_env : CSet.S with type elt = constructor +module Indmap : CMap.ExtS with type key = inductive and module Set := Indset +module Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset +module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset_env +module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env val ind_modpath : inductive -> ModPath.t val constr_modpath : constructor -> ModPath.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 00559206ee..e846b17aa0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -302,8 +302,8 @@ let lift_constant c = let push_private_constants env eff = let eff = side_effects_of_private_constants eff in let add_if_undefined env eff = - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + if Environ.mem_constant eff.seff_constant env then env + else Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env in List.fold_left add_if_undefined env eff @@ -598,8 +598,8 @@ let inline_side_effects env body side_eff = (** First step: remove the constants that are still in the environment *) let filter e = let cb = (e.seff_constant, e.seff_body) in - try ignore (Environ.lookup_constant e.seff_constant env); None - with Not_found -> Some (cb, e.from_env) + if Environ.mem_constant e.seff_constant env then None + else Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) let side_eff = List.map_filter filter (SideEffects.repr side_eff) in @@ -750,9 +750,7 @@ let translate_direct_opaque env kn ce = { cb with const_body = OpaqueDef c } let export_side_effects mb env (b_ctx, eff) = - let not_exists e = - try ignore(Environ.lookup_constant e.seff_constant env); false - with Not_found -> true in + let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl else e :: acc, e.from_env :: sl in diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 87b9a8eea3..470782a7dc 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -263,7 +263,7 @@ GRAMMAR EXTEND Gram { mkProdCN ~loc bl c } | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> { mkLambdaCN ~loc bl c } - | "let"; id=name; bl = binders; ty = type_cstr; ":="; + | "let"; id=name; bl = binders; ty = let_type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { let ty,c1 = match ty, c1 with | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) @@ -353,7 +353,7 @@ GRAMMAR EXTEND Gram | "cofix" -> { false } ] ] ; fix_decl: - [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; + [ [ id=identref; bl=binders_fixannot; ty=let_type_cstr; ":="; c=operconstr LEVEL "200" -> { (id,fst bl,snd bl,c,ty) } ] ] ; @@ -525,7 +525,7 @@ GRAMMAR EXTEND Gram ] ] ; - type_cstr: + let_type_cstr: [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ] ; END diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a43549f6c3..0a6c3afd0d 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -620,18 +620,16 @@ let lookup_eliminator env ind_sp s = let knc = KerName.make mpc l in (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) - try - let cst = Constant.make knu knc in - let _ = lookup_constant cst env in - GlobRef.ConstRef cst - with Not_found -> - (* Then try to get a user-defined eliminator in some other places *) - (* using short name (e.g. for "eq_rec") *) - try Nametab.locate (qualid_of_ident id) - with Not_found -> - user_err ~hdr:"default_elim" - (strbrk "Cannot find the elimination combinator " ++ - Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++ - strbrk " on sort " ++ Sorts.pr_sort_family s ++ - strbrk " is probably not allowed.") + let cst = Constant.make knu knc in + if mem_constant cst env then GlobRef.ConstRef cst + else + (* Then try to get a user-defined eliminator in some other places *) + (* using short name (e.g. for "eq_rec") *) + try Nametab.locate (qualid_of_ident id) + with Not_found -> + user_err ~hdr:"default_elim" + (strbrk "Cannot find the elimination combinator " ++ + Id.print id ++ strbrk ", the elimination of the inductive definition " ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++ + strbrk " on sort " ++ Sorts.pr_sort_family s ++ + strbrk " is probably not allowed.") diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 866c0da555..e8a2189611 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -241,8 +241,10 @@ let invert_name labs l {binder_name=na0} env sigma ref na = let refi = match ref with | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) - | EvalConst kn -> - Some (EvalConst (Constant.change_label kn (Label.of_id id))) in + | EvalConst kn -> + let kn = Constant.change_label kn (Label.of_id id) in + if Environ.mem_constant kn env then Some (EvalConst kn) else None + in match refi with | None -> None | Some ref -> diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index f6fca91eea..a806ab7123 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,6 +16,9 @@ val write_diffs_option : string -> unit (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool +(** Returns true if the diffs option is "removed" *) +val show_removed : unit -> bool + (** controls whether color output is enabled *) val write_color_enabled : bool -> unit diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 03ab0a1c13..1e18028e7b 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -8,14 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Util open Termops open EConstr open Evarutil -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* tactical to save as name a subproof such that the generalisation of @@ -23,67 +20,21 @@ module NamedDecl = Context.Named.Declaration is solved by tac *) (** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl env evd d1 d2 = +let interpretable_as_section_decl env sigma d1 d2 = let open Context.Named.Declaration in - let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with - | None -> false - | Some cstr -> - try ignore (Evd.add_universe_constraints !sigma cstr); true - with UState.UniversesDiffer -> false + let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env sigma c1 c2 with + | None -> false + | Some cstr -> + try + let _sigma = Evd.add_universe_constraints sigma cstr in + true + with UState.UniversesDiffer -> false in match d2, d1 with | LocalDef _, LocalAssum _ -> false | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> - e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) - -let rec decompose len c t accu = - let open Constr in - let open Context.Rel.Declaration in - if len = 0 then (c, t, accu) - else match kind c, kind t with - | Lambda (na, u, c), Prod (_, _, t) -> - decompose (pred len) c t (LocalAssum (na, u) :: accu) - | LetIn (na, b, u, c), LetIn (_, _, _, t) -> - decompose (pred len) c t (LocalDef (na, b, u) :: accu) - | _ -> assert false - -let rec shrink ctx sign c t accu = - let open Constr in - let open CVars in - match ctx, sign with - | [], [] -> (c, t, accu) - | p :: ctx, decl :: sign -> - if noccurn 1 c && noccurn 1 t then - let c = subst1 mkProp c in - let t = subst1 mkProp t in - shrink ctx sign c t accu - else - let c = Term.mkLambda_or_LetIn p c in - let t = Term.mkProd_or_LetIn p t in - let accu = if RelDecl.is_local_assum p - then mkVar (NamedDecl.get_id decl) :: accu - else accu - in - shrink ctx sign c t accu -| _ -> assert false - -let shrink_entry sign const = - let open Declare in - let typ = match const.proof_entry_type with - | None -> assert false - | Some t -> t - in - (* The body has been forced by the call to [build_constant_by_tactic] *) - let () = assert (Future.is_over const.proof_entry_body) in - let ((body, uctx), eff) = Future.force const.proof_entry_body in - let (body, typ, ctx) = decompose (List.length sign) body typ [] in - let (body, typ, args) = shrink ctx sign body typ [] in - let const = { const with - proof_entry_body = Future.from_val ((body, uctx), eff); - proof_entry_type = Some typ; - } in - (const, args) + e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2 + | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma t1 (NamedDecl.get_type d2) let name_op_to_name ~name_op ~name suffix = match name_op with @@ -101,22 +52,22 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) - let suffix = if opaque - then "_subproof" - else "_subterm" in + let suffix, kind = if opaque + then "_subproof", Decls.(IsProof Lemma) + else "_subterm", Decls.(IsDefinition Definition) + in let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in - let evdref = ref sigma in let sign,secsign = List.fold_right (fun d (s1,s2) -> let id = NamedDecl.get_id d in if mem_named_context_val id current_sign && - interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d + interpretable_as_section_decl env sigma (lookup_named_val id current_sign) d then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, Environ.empty_named_context_val) in @@ -126,21 +77,21 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = | Some ty -> ty in let concl = it_mkNamedProd_or_LetIn concl sign in let concl = - try flush_and_check_evars !evdref concl + try flush_and_check_evars sigma concl with Uninstantiated_evar _ -> CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in - let evd, ctx, concl = + let sigma, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd = Evd.minimize_universes !evdref in - let ctx = Evd.universe_context_set evd in - evd, ctx, Evarutil.nf_evars_universes evd concl + let sigma = Evd.minimize_universes sigma in + let ctx = Evd.universe_context_set sigma in + sigma, ctx, Evarutil.nf_evars_universes sigma concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in - let ectx = Evd.evar_universe_context evd in + let ectx = Evd.evar_universe_context sigma in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -151,16 +102,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let body, effs = Future.force const.Declare.proof_entry_body in (* We drop the side-effects from the entry, they already exist in the ambient environment *) - let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in - let const, args = shrink_entry sign const in + let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in + (* EJGA: Hack related to the above call to + `build_constant_by_tactic` with `~opaque:Transparent`. Even if + the abstracted term is destined to be opaque, if we trigger the + `if poly && opaque && private_poly_univs ()` in `Proof_global` + kernel will boom. This deserves more investigation. *) + let const = Declare.Internal.set_opacity ~opaque const in + let const, args = Declare.Internal.shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = { const with Declare.proof_entry_opaque = opaque } in - let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd + Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Declare.proof_entry_universes with @@ -174,14 +129,14 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in - let evd = Evd.set_universe_context evd ectx in + let sigma = Evd.set_universe_context sigma ectx in let effs = Evd.concat_side_effects eff effs in let solve = Proofview.tclEFFECTS effs <*> tacK lem args in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac end let abstract_subproof ~opaque tac = diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 96ddbea7b2..779e46cd49 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -20,11 +20,3 @@ val cache_term_by_tactic_then -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic - -(* Internal but used in a few places; should likely be made intro a - proper library function, or incorporated into the generic constant - save path *) -val shrink_entry - : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Declare.proof_entry - -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index 57eeddb847..fb06bb8a4f 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -139,9 +139,6 @@ let (inConstant : constant_obj -> obj) = subst_function = ident_subst_function; discharge_function = discharge_constant } -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f - let update_tables c = Impargs.declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) @@ -159,7 +156,7 @@ let register_side_effect (c, role) = let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in match role with | None -> () - | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] + | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] let record_aux env s_ty s_bo = let open Environ in @@ -174,6 +171,7 @@ let record_aux env s_ty s_bo = Aux_file.record_in_aux "context_used" v let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty + let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); @@ -184,6 +182,26 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_feedback = None; proof_entry_inline_code = inline} +let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types + ?(univs=default_univ_entry) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ()); + proof_entry_secctx = None; + proof_entry_type = types; + proof_entry_universes = univs; + proof_entry_opaque = opaque; + proof_entry_feedback = None; + proof_entry_inline_code = inline} + +let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body = + { proof_entry_body = body + ; proof_entry_secctx = section_vars + ; proof_entry_type = types + ; proof_entry_universes = univs + ; proof_entry_opaque = opaque + ; proof_entry_feedback = feedback_id + ; proof_entry_inline_code = inline + } + let cast_proof_entry e = let (body, ctx), () = Future.force e.proof_entry_body in let univs = @@ -326,6 +344,12 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff +let inline_private_constants ~univs env ce = + let body, eff = Future.force ce.proof_entry_body in + let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in + cb, univs + (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry @@ -413,3 +437,64 @@ let assumption_message id = the type of the object than to the name of the object (see discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") + +module Internal = struct + + let map_entry_body ~f entry = + { entry with proof_entry_body = Future.chain entry.proof_entry_body f } + + let map_entry_type ~f entry = + { entry with proof_entry_type = f entry.proof_entry_type } + + let set_opacity ~opaque entry = + { entry with proof_entry_opaque = opaque } + + let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body + + let rec decompose len c t accu = + let open Constr in + let open Context.Rel.Declaration in + if len = 0 then (c, t, accu) + else match kind c, kind t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t (LocalAssum (na, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t (LocalDef (na, b, u) :: accu) + | _ -> assert false + + let rec shrink ctx sign c t accu = + let open Constr in + let open Vars in + match ctx, sign with + | [], [] -> (c, t, accu) + | p :: ctx, decl :: sign -> + if noccurn 1 c && noccurn 1 t then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = Term.mkLambda_or_LetIn p c in + let t = Term.mkProd_or_LetIn p t in + let accu = if Context.Rel.Declaration.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu + in + shrink ctx sign c t accu + | _ -> assert false + + let shrink_entry sign const = + let typ = match const.proof_entry_type with + | None -> assert false + | Some t -> t + in + (* The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.proof_entry_body) in + let ((body, uctx), eff) = Future.force const.proof_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + { const with + proof_entry_body = Future.from_val ((body, uctx), eff) + ; proof_entry_type = Some typ + }, args + +end diff --git a/tactics/declare.mli b/tactics/declare.mli index 1a037ef937..c646d2f85b 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -20,7 +20,7 @@ open Entries [Nametab] and [Impargs]. *) (** Proof entries *) -type 'a proof_entry = { +type 'a proof_entry = private { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) proof_entry_secctx : Id.Set.t option; @@ -55,10 +55,35 @@ val declare_variable i.e. Definition/Theorem/Axiom/Parameter/... *) (* Default definition entries, transparent with no secctx or proj information *) -val definition_entry : ?fix_exn:Future.fix_exn -> - ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry +val definition_entry + : ?fix_exn:Future.fix_exn + -> ?opaque:bool + -> ?inline:bool + -> ?types:types + -> ?univs:Entries.universes_entry + -> ?eff:Evd.side_effects + -> constr + -> Evd.side_effects proof_entry + +val pure_definition_entry + : ?fix_exn:Future.fix_exn + -> ?opaque:bool + -> ?inline:bool + -> ?types:types + -> ?univs:Entries.universes_entry + -> constr + -> unit proof_entry + +(* Delayed definition entries *) +val delayed_definition_entry + : ?opaque:bool + -> ?inline:bool + -> ?feedback_id:Stateid.t + -> ?section_vars:Id.Set.t + -> ?univs:Entries.universes_entry + -> ?types:types + -> 'a Entries.const_entry_body + -> 'a proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified @@ -83,10 +108,14 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects -(** Since transparent constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * Constant.t) array -> unit) -> unit +(** [inline_private_constants ~sideff ~univs env ce] will inline the + constants in [ce]'s body and return the body plus the updated + [UState.t]. *) +val inline_private_constants + : univs:UState.t + -> Environ.env + -> Evd.side_effects proof_entry + -> Constr.t * UState.t (** Declaration messages *) @@ -101,3 +130,19 @@ val check_exists : Id.t -> unit (* Used outside this module only in indschemes *) exception AlreadyDeclared of (string option * Id.t) + +(* For legacy support, do not use *) +module Internal : sig + + val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry + val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry + (* Overriding opacity is indeed really hacky *) + val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry + + (* TODO: This is only used in DeclareDef to forward the fix to + hooks, should eventually go away *) + val get_fix_exn : 'a proof_entry -> Future.fix_exn + + val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list + +end diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml new file mode 100644 index 0000000000..5f4626fcb2 --- /dev/null +++ b/tactics/declareScheme.ml @@ -0,0 +1,42 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" + +let cache_one_scheme kind (ind,const) = + let map = try Indmap.find ind !scheme_map with Not_found -> CString.Map.empty in + scheme_map := Indmap.add ind (CString.Map.add kind const map) !scheme_map + +let cache_scheme (_,(kind,l)) = + Array.iter (cache_one_scheme kind) l + +let subst_one_scheme subst (ind,const) = + (* Remark: const is a def: the result of substitution is a constant *) + (Mod_subst.subst_ind subst ind, Mod_subst.subst_constant subst const) + +let subst_scheme (subst,(kind,l)) = + (kind, CArray.Smart.map (subst_one_scheme subst) l) + +let discharge_scheme (_,(kind,l)) = + Some (kind, l) + +let inScheme : string * (inductive * Constant.t) array -> Libobject.obj = + let open Libobject in + declare_object @@ superglobal_object "SCHEME" + ~cache:cache_scheme + ~subst:(Some subst_scheme) + ~discharge:discharge_scheme + +let declare_scheme kind indcl = + Lib.add_anonymous_leaf (inScheme (kind,indcl)) + +let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map) diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli new file mode 100644 index 0000000000..f2ae5e41c8 --- /dev/null +++ b/tactics/declareScheme.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val declare_scheme : string -> (Names.inductive * Names.Constant.t) array -> unit +val lookup_scheme : string -> Names.inductive -> Names.Constant.t diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 3f824a94bf..9c94f3c319 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -15,8 +15,6 @@ declaring schemes and generating schemes on demand *) open Names -open Mod_subst -open Libobject open Nameops open Declarations open Constr @@ -40,33 +38,8 @@ type individual_scheme_object_function = type 'a scheme_kind = string -let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" - let pr_scheme_kind = Pp.str -let cache_one_scheme kind (ind,const) = - let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in - scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map - -let cache_scheme (_,(kind,l)) = - Array.iter (cache_one_scheme kind) l - -let subst_one_scheme subst (ind,const) = - (* Remark: const is a def: the result of substitution is a constant *) - (subst_ind subst ind,subst_constant subst const) - -let subst_scheme (subst,(kind,l)) = - (kind,Array.Smart.map (subst_one_scheme subst) l) - -let discharge_scheme (_,(kind,l)) = - Some (kind, l) - -let inScheme : string * (inductive * Constant.t) array -> obj = - declare_object @@ superglobal_object "SCHEME" - ~cache:cache_scheme - ~subst:(Some subst_scheme) - ~discharge:discharge_scheme - (**********************************************************************) (* The table of scheme building functions *) @@ -104,11 +77,6 @@ let declare_individual_scheme_object s ?(aux="") f = (**********************************************************************) (* Defining/retrieving schemes *) -let declare_scheme kind indcl = - Lib.add_anonymous_leaf (inScheme (kind,indcl)) - -let () = Declare.set_declare_scheme declare_scheme - let is_visible_name id = try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true with Not_found -> false @@ -124,16 +92,7 @@ let define internal role id c poly univs = let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = { - Declare.proof_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), ()); - proof_entry_secctx = None; - proof_entry_type = None; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - } in + let entry = Declare.pure_definition_entry ~univs c in let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in let () = match internal with | InternalTacticRequest -> () @@ -149,7 +108,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let role = Evd.Schema (ind, kind) in let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in - declare_scheme kind [|ind,const|]; + DeclareScheme.declare_scheme kind [|ind,const|]; const, Evd.concat_side_effects neff eff let define_individual_scheme kind mode names (mind,i as ind) = @@ -171,7 +130,7 @@ let define_mutual_scheme_base kind suff f mode names mind = in let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in - declare_scheme kind schemes; + DeclareScheme.declare_scheme kind schemes; consts, eff let define_mutual_scheme kind mode names mind = @@ -181,7 +140,7 @@ let define_mutual_scheme kind mode names mind = define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = - let s = String.Map.find kind (Indmap.find ind !scheme_map) in + let s = DeclareScheme.lookup_scheme kind ind in s, Evd.empty_side_effects let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 17e9c7ef42..e9a792c264 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -30,7 +30,9 @@ type mutual_scheme_object_function = type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects -(** Main functions to register a scheme builder *) +(** Main functions to register a scheme builder. Note these functions + are not safe to be used by plugins as their effects won't be undone + on backtracking *) val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 413c6540a3..3c9803432a 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -55,8 +55,7 @@ let get_current_goal_context pf = let env = Global.env () in Evd.from_env env, env -let get_current_context pf = - let p = Proof_global.get_proof pf in +let get_proof_context p = try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -64,6 +63,10 @@ let get_current_context pf = let { Proof.sigma } = Proof.data p in sigma, Global.env () +let get_current_context pf = + let p = Proof_global.get_proof pf in + get_proof_context p + let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac @@ -114,14 +117,14 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic ~name ctx sign ~poly typ tac = +let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac = let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in try let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> entry, status, universes @@ -135,12 +138,13 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Declare.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body + let cb, univs = + if side_eff then Declare.inline_private_constants ~univs env ce + else + (* GG: side effects won't get reset: no need to treat their universes specially *) + let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in + cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx in - let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 30514191fa..a2e742c0d7 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : Proof.t -> Evd.evar_map * env + (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. @@ -59,6 +63,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : name:Id.t + -> ?opaque:Proof_global.opacity_flag -> UState.t -> named_context_val -> poly:bool diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b723922642..b1fd34e43c 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -238,18 +238,10 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - let open Declare in - { - proof_entry_body = body; - proof_entry_secctx = section_vars; - proof_entry_feedback = feedback_id; - proof_entry_type = Some typ; - proof_entry_inline_code = false; - proof_entry_opaque = opaque; - proof_entry_universes = univs; } + Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in - let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { name; entries = entries; poly; universes; udecl } + let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in + { name; entries; poly; universes; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index c5c7969a09..0c4e496650 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +DeclareScheme Declare Proof_global Pfedit diff --git a/test-suite/bugs/closed/bug_4502.v b/test-suite/bugs/closed/bug_4502.v new file mode 100644 index 0000000000..f1dcae9773 --- /dev/null +++ b/test-suite/bugs/closed/bug_4502.v @@ -0,0 +1,17 @@ +Require Import FunInd. + +Set Universe Polymorphism. +Set Primitive Projections. +Set Implicit Arguments. +Set Strongly Strict Implicit. + +Function first_false (n : nat) (f : nat -> bool) : option nat := + match n with + | O => None + | S m => + match first_false m f with + | (Some _) as s => s + | None => if f m then None else Some m + end + end. +(* undefined universe *) diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v new file mode 100644 index 0000000000..2cf91c1c2b --- /dev/null +++ b/test-suite/bugs/closed/bug_9114.v @@ -0,0 +1,5 @@ +Goal True. + assert_succeeds (exact I). + idtac. + (* Error: No such goal. *) +Abort. diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out new file mode 100644 index 0000000000..285a3bcd89 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.out @@ -0,0 +1,42 @@ +
+Coq < Coq < 1 subgoal
+
+ ============================
+ [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x <
+x < 1 focused subgoal
+(shelved: 1)
+ [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+ ============================
+ [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+ i : nat
+ ============================
+ [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?j[49m
+ [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+ [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x <
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v new file mode 100644 index 0000000000..4251c52cb4 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.v @@ -0,0 +1,6 @@ +(* coq-prog-args: ("-color" "on" "-diffs" "on") *) +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. Show Proof Diffs. + eexists. Show Proof Diffs. + split. Show Proof Diffs. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 19c9fc4423..70427220ed 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -6,3 +6,4 @@ The command has indeed failed with message: H is already used. The command has indeed failed with message: H is already used. +a diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index fa12f09a46..96b6d652c9 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -22,3 +22,11 @@ intros H. Fail intros [H%myid ?]. Fail destruct 1 as [H%myid ?]. Abort. + + +(* Test that assert_succeeds only runs a tactic once *) +Ltac should_not_loop := idtac + should_not_loop. +Goal True. + assert_succeeds should_not_loop. + assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) +Abort. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 81c9763ccd..6c333121da 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -96,10 +96,25 @@ Section visibility. Let Fixpoint by_proof (n:nat) : True. Proof. exact I. Defined. + + Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool. + Proof. + - destruct n as [|n]. + + exact true. + + exact (bar n). + - destruct n as [|n]. + + exact false. + + exact (foo n). + Qed. + + Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool. + Admitted. + End visibility. Fail Check imm. Fail Check by_proof. +Check bla. Check bli. Module Import mod_local. Fixpoint imm_importable (n:nat) : True := I. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index ad6f1765a3..6de9f8f88d 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -325,9 +325,9 @@ Ltac time_constr tac := (** Useful combinators *) Ltac assert_fails tac := - tryif tac then fail 0 tac "succeeds" else idtac. + tryif (once tac) then gfail 0 tac "succeeds" else idtac. Ltac assert_succeeds tac := - tryif (assert_fails tac) then fail 0 tac "fails" else idtac. + tryif (assert_fails tac) then gfail 0 tac "fails" else idtac. Tactic Notation "assert_succeeds" tactic3(tac) := assert_succeeds tac. Tactic Notation "assert_fails" tactic3(tac) := diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1f319d2bfd..97f0e57d2e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -418,6 +418,50 @@ let rec vernac_loop ~state = Feedback.msg_notice (v 0 (goal ++ evars)); vernac_loop ~state + | Some VernacShowProofDiffs removed -> + (* extension of Vernacentries.show_proof *) + let to_pp pstate = + let p = Option.get pstate in + let sigma, env = Pfedit.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf + (* We print nothing if there are no goals left *) + in + + if not (Proof_diffs.color_enabled ()) then + CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") + else begin + let out = + try + let n_pp = to_pp state.proof in + if true (*Proof_diffs.show_diffs ()*) then + let doc = state.doc in + let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in + try + let o_pp = to_pp oproof in + let tokenize_string = Proof_diffs.tokenize_string in + let show_removed = Some removed in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> n_pp + | Pp_diff.Diff_Failure msg -> begin + (* todo: print the unparsable string (if we know it) *) + Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() + ++ str "Showing results without diff highlighting" ); + n_pp + end + else + n_pp + with + | Pfedit.NoSuchGoal + | Option.IsNone -> + CErrors.user_err (str "No goals to show.") + in + Feedback.msg_notice out; + end; + vernac_loop ~state + | None -> top_stderr (fnl ()); exit 0 diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index e180d9e750..56fda58a25 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -22,6 +22,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } + | VernacShowProofDiffs of bool module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -59,6 +60,8 @@ GRAMMAR EXTEND Gram (* show a goal for the specified proof state *) | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } + | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." -> + { Some (VernacShowProofDiffs (removed <> None)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index cb034bdff6..dacef1cb18 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -135,11 +135,13 @@ let lookup_constant_in_impl cst fallback = | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".") let lookup_constant cst = - try - let cb = Global.lookup_constant cst in + let env = Global.env() in + if not (Environ.mem_constant cst env) + then lookup_constant_in_impl cst None + else + let cb = Environ.lookup_constant cst env in if Declareops.constant_has_body cb then cb else lookup_constant_in_impl cst (Some cb) - with Not_found -> lookup_constant_in_impl cst None let lookup_mind_in_impl mind = try @@ -150,8 +152,9 @@ let lookup_mind_in_impl mind = anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".") let lookup_mind mind = - try Global.lookup_mind mind - with Not_found -> lookup_mind_in_impl mind + let env = Global.env() in + if Environ.mem_mind mind env then Environ.lookup_mind mind env + else lookup_mind_in_impl mind (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index f044c025d8..e57c324c9a 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.proof_entry_body in + let fix_exn = Declare.Internal.get_fix_exn ce in let gr = match scope with | Discharge -> let () = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index d6001f5970..1bb6620886 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -62,11 +62,16 @@ val declare_fix -> Impargs.manual_implicits -> GlobRef.t -val prepare_definition : allow_evars:bool -> - ?opaque:bool -> ?inline:bool -> poly:bool -> - Evd.evar_map -> UState.universe_decl -> - types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_definition + : allow_evars:bool + -> ?opaque:bool + -> ?inline:bool + -> poly:bool + -> Evd.evar_map + -> UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 2c56f707f1..b56b9c8ce2 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -490,10 +490,8 @@ let obligation_terminator entries uctx { name; num; auto } = | [entry] -> let env = Global.env () in let ty = entry.Declare.proof_entry_type in - let body, eff = Future.force entry.Declare.proof_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) let prg = CEphemeron.get (ProgMap.find name !from_prg) in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index efcb2635be..1387ca4675 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -418,19 +418,19 @@ GRAMMAR EXTEND Gram rec_definition: [ [ id_decl = ident_decl; bl = binders_fixannot; - rtype = type_cstr; + rtype = rec_type_cstr; body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> { let binders, rec_order = bl in {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; corec_definition: - [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + [ [ id_decl = ident_decl; binders = binders; rtype = rec_type_cstr; body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} } ]] ; - type_cstr: + rec_type_cstr: [ [ ":"; c=lconstr -> { c } | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ] ; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 5ace8b917c..cf322c52d0 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -17,15 +17,10 @@ open Pp open Names open Constr open Declareops -open Entries open Nameops open Pretyping -open Termops -open Reductionops -open Constrintern open Impargs -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* Support for terminators and proofs with an associated constant @@ -113,13 +108,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -let check_name_freshness locality {CAst.loc;v=id} : unit = - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err ?loc (Id.print id ++ str " already exists.") - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -193,41 +181,6 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua | None -> p | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma -let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms = - let env0 = Global.env () in - let decl = fst (List.hd thms) in - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in - let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in - let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in - let flags = { all_and_fail_flags with program_mode } in - let hook = inference_hook in - let evd = solve_remaining_evars ?hook flags env evd in - let ids = List.map RelDecl.get_name ctx in - check_name_freshness scope id; - (* XXX: The nf_evar is critical !! *) - evd, (id.CAst.v, - (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), - (ids, imps @ imps')))) - evd thms in - let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in - let evd = Evd.minimize_universes evd in - (* XXX: This nf_evar is critical too!! We are normalizing twice if - you look at the previous lines... *) - let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in - let () = - let open UState in - if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl ~poly evd udecl) - in - let evd = - if poly then evd - else (* We fix the variables to ensure they won't be lowered to Set *) - Evd.fix_undefined_variables evd - in - start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl - (************************************************************************) (* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) @@ -258,17 +211,9 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect let open DeclareDef in (match scope with | Discharge -> - let impl = Glob_term.Explicit in - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let () = Declare.declare_universe_context ~poly univs in - let c = Declare.SectionLocalAssum {typ=t_i; impl} in - let () = Declare.declare_variable ~name ~kind c in - GlobRef.VarRef name, impargs + (* Let Fixpoint + Admitted gets turned into axiom so scope is Global, + see finish_admitted *) + assert false | Global local -> let kind = Decls.(IsAssumption Conjectural) in let decl = Declare.ParameterEntry (None,(t_i,univs),None) in @@ -384,17 +329,14 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with - Declare.proof_entry_body = - Future.chain const.Declare.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) - } + Declare.Internal.map_entry_body const + ~f:(fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) let finish_proved env sigma idopt po info = let open Proof_global in @@ -404,7 +346,7 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in + let fix_exn = Declare.Internal.get_fix_exn const in let () = try let const = adjust_guardness_conditions const compute_guard in let should_suggest = const.Declare.proof_entry_opaque && @@ -452,7 +394,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Declare.proof_entry_opaque = false } in + let f_def = Declare.Internal.set_opacity ~opaque:false f_def in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,20 +405,15 @@ let finish_derived ~f ~name ~idopt ~entries = performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match lemma_def.Declare.proof_entry_type with - | Some t -> t + let lemma_pretype typ = + match typ with + | Some t -> Some (substf t) | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in + let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = - { lemma_def with - Declare.proof_entry_body = lemma_body; - proof_entry_type = Some lemma_type } - in + let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = Declare.DefinitionEntry lemma_def in let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () @@ -491,7 +428,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = | Some id -> id | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in - let entry, args = Abstract.shrink_entry local_context entry in + let entry, args = Declare.Internal.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index fbf91b3ad4..e790c39022 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -110,17 +110,6 @@ val start_lemma_with_initialization val default_thm_id : Names.Id.t -(** Main [Lemma foo args : type.] command *) -val start_lemma_com - : program_mode:bool - -> poly:bool - -> scope:DeclareDef.locality - -> kind:Decls.logical_kind - -> ?inference_hook:Pretyping.inference_hook - -> ?hook:DeclareDef.Hook.t - -> Vernacexpr.proof_expr list - -> t - (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c8cede1f84..4ea34e2b60 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,9 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Declare.proof_entry_body in - let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') + let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in + Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body); + Some (body, entry.Declare.proof_entry_type, ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4ecd815dd2..684d8a3d90 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -465,29 +465,64 @@ let vernac_custom_entry ~module_local s = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = - let inference_hook = - if program_mode then - let hook env sigma ev = - let tac = !Obligations.default_tactic in - let evi = Evd.find sigma ev in - let evi = Evarutil.nf_evar_info sigma evi in - let env = Evd.evar_filtered_env evi in - try - let concl = evi.Evd.evar_concl in - if not (Evarutil.is_ground_env sigma env && - Evarutil.is_ground_term sigma concl) - then raise Exit; - let c, _, ctx = - Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac - in Evd.set_universe_context sigma ctx, EConstr.of_constr c - with Logic_monad.TacticFailure e when Logic.catchable_exception e -> - user_err Pp.(str "The statement obligations could not be resolved \ - automatically, write a statement definition first.") - in Some hook - else None +let check_name_freshness locality {CAst.loc;v=id} : unit = + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id || + locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + then + user_err ?loc (Id.print id ++ str " already exists.") + +let program_inference_hook env sigma ev = + let tac = !Obligations.default_tactic in + let evi = Evd.find sigma ev in + let evi = Evarutil.nf_evar_info sigma evi in + let env = Evd.evar_filtered_env evi in + try + let concl = evi.Evd.evar_concl in + if not (Evarutil.is_ground_env sigma env && + Evarutil.is_ground_term sigma concl) + then raise Exit; + let c, _, ctx = + Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac + in Evd.set_universe_context sigma ctx, EConstr.of_constr c + with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + user_err Pp.(str "The statement obligations could not be resolved \ + automatically, write a statement definition first.") + +let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = + let env0 = Global.env () in + let decl = fst (List.hd thms) in + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in + let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> + let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in + let flags = Pretyping.{ all_and_fail_flags with program_mode } in + let inference_hook = if program_mode then Some program_inference_hook else None in + let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in + let ids = List.map Context.Rel.Declaration.get_name ctx in + check_name_freshness scope id; + (* XXX: The nf_evar is critical !! *) + evd, (id.CAst.v, + (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), + (ids, imps @ imps')))) + evd thms in + let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in + let evd = Evd.minimize_universes evd in + (* XXX: This nf_evar is critical too!! We are normalizing twice if + you look at the previous lines... *) + let thms = List.map (fun (name, (typ, (args, impargs))) -> + { Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in + let () = + let open UState in + if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl ~poly evd udecl) + in + let evd = + if poly then evd + else (* We fix the variables to ensure they won't be lowered to Set *) + Evd.fix_undefined_variables evd in - start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l + start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl let vernac_definition_hook ~poly = let open Decls in function | Coercion -> @@ -522,7 +557,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] + start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -545,7 +580,7 @@ let vernac_start_proof ~atts kind l = let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l + start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> |