diff options
79 files changed, 874 insertions, 713 deletions
diff --git a/default.nix b/default.nix index d5c6cdb8ad..10c5f6be47 100644 --- a/default.nix +++ b/default.nix @@ -41,7 +41,7 @@ stdenv.mkDerivation rec { buildInputs = [ hostname - python2 time # coq-makefile timing tools + python3 time # coq-makefile timing tools dune ] ++ (with ocamlPackages; [ ocaml findlib num ]) diff --git a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh new file mode 100644 index 0000000000..0ec0c3673a --- /dev/null +++ b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "10419" ] || [ "$CI_BRANCH" = "heads+test" ]; then + + elpi_CI_REF=heads+test + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + equations_CI_REF=heads+test + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=heads+test + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=heads+test + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + quickchick_CI_REF=heads+test + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh new file mode 100644 index 0000000000..3a2f4e1001 --- /dev/null +++ b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "10434" ] || [ "$CI_BRANCH" = "proof+hook_record" ]; then + + equations_CI_REF=proof+hook_record + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=proof+hook_record + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=proof+hook_record + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + +fi diff --git a/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst new file mode 100644 index 0000000000..151c400b2c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10336-ambiguous-paths.rst @@ -0,0 +1,5 @@ +- Improve the ambiguous paths warning to indicate which path is ambiguous with + new one + (`#10336 <https://github.com/coq/coq/pull/10336>`_, + closes `#3219 <https://github.com/coq/coq/issues/3219>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 68ae5628db..9dd4700db5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] + ~kind:Decls.Definition ~opaque:false sigma udecl body None [] diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index d5523e8561..7fee62179b 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -145,19 +145,25 @@ Declaring Coercions .. exn:: Cannot recognize @class as a source class of @qualid. :undocumented: - .. exn:: @qualid does not respect the uniform inheritance condition. + .. warn:: @qualid does not respect the uniform inheritance condition. :undocumented: .. exn:: Found target class ... instead of ... :undocumented: - .. warn:: Ambiguous path. + .. warn:: New coercion path ... is ambiguous with existing ... - When the coercion :token:`qualid` is added to the inheritance graph, - invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check - that they are convertible with existing ones on the same classes. - The paths for which this check fails are displayed by a warning in the form - :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, new + coercion paths which have the same classes as existing ones are ignored. + The :cmd:`Coercion` command tries to check the convertibility of new ones and + existing ones. The paths for which this check fails are displayed by a warning + in the form :g:`[f₁;..;fₙ] : C >-> D`. + + The convertibility checking procedure for coercion paths is complete for + paths consisting of coercions satisfying the uniform inheritance condition, + but some coercion paths could be reported as ambiguous even if they are + convertible with existing ones when they have coercions that don't satisfy + the uniform inheritance condition. .. cmdv:: Local Coercion @qualid : @class >-> @class diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 0cff987a27..03b30d5d97 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -600,6 +600,14 @@ Requesting information its normalized form at the current stage of the proof, useful for debugging universe inconsistencies. + .. cmdv:: Show Goal @num at @num + :name: Show Goal + + This command is only available in coqtop. Displays a goal at a + proof state using the goal ID number and the proof state ID number. + It is primarily for use by tools such as Prooftree that need to fetch + goal history in this way. Prooftree is a tool for visualizing a proof + as a tree that runs in Proof General. .. cmd:: Guarded diff --git a/ide/idetop.ml b/ide/idetop.ml index c38b8fa820..c6a8fdaa55 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -429,6 +429,11 @@ let quit = ref false (** Disabled *) let print_ast id = Xml_datatype.PCData "ERROR" +let idetop_make_cases iname = + let qualified_iname = Libnames.qualid_of_string iname in + let iref = Nametab.global_inductive qualified_iname in + ComInductive.make_cases iref + (** Grouping all call handlers together + error handling *) let eval_call c = let interruptible f x = @@ -449,7 +454,7 @@ let eval_call c = Interface.search = interruptible search; Interface.get_options = interruptible get_options; Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.mkcases = interruptible idetop_make_cases; Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; diff --git a/library/decls.ml b/interp/decls.ml index 5cb35323dd..b802dbe9c3 100644 --- a/library/decls.ml +++ b/interp/decls.ml @@ -12,18 +12,60 @@ associated declarations *) open Names -open Decl_kinds open Libnames -(** Datas associated to section variables and local definitions *) +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary -type variable_data = { - path:DirPath.t; - opaque:bool; - univs:Univ.ContextSet.t; - poly:bool; - kind:logical_kind; -} +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural | Context + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) + +(** Kinds *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + +(** Data associated to section variables and local definitions *) + +type variable_data = + { path:DirPath.t + ; opaque:bool + ; univs:Univ.ContextSet.t + ; poly:bool + ; kind:logical_kind + } let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" @@ -41,11 +83,3 @@ let variable_secpath id = make_qualid dir id let variable_exists id = Id.Map.mem id !vartab - -(** Datas associated to global parameters and constants *) - -let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT" - -let add_constant_kind kn k = csttab := Cmap.add kn k !csttab - -let constant_kind kn = Cmap.find kn !csttab diff --git a/library/decls.mli b/interp/decls.mli index f88958bb04..05e4be0de6 100644 --- a/library/decls.mli +++ b/interp/decls.mli @@ -10,7 +10,49 @@ open Names open Libnames -open Decl_kinds + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + +type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + +type assumption_object_kind = Definitional | Logical | Conjectural | Context + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom + +*) + +(** Kinds used in library *) + +type logical_kind = + | IsPrimitive + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind (** This module manages non-kernel informations about declarations. It is either non-logical informations or logical informations that @@ -18,24 +60,27 @@ open Decl_kinds (** Registration and access to the table of variable *) -type variable_data = { - path:DirPath.t; - opaque:bool; - univs:Univ.ContextSet.t; - poly:bool; - kind:logical_kind; -} +type variable_data = + { path:DirPath.t + ; opaque:bool + ; univs:Univ.ContextSet.t + ; poly:bool + ; kind:logical_kind + } val add_variable_data : variable -> variable_data -> unit + +(* Not used *) val variable_path : variable -> DirPath.t + +(* Only used in dumpglob *) val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind + +(* User in Lemma, Very dubious *) val variable_opacity : variable -> bool + +(* Used in declare, very dubious *) val variable_context : variable -> Univ.ContextSet.t val variable_polymorphic : variable -> bool val variable_exists : variable -> bool - -(** Registration and access to the table of constants *) - -val add_constant_kind : Constant.t -> logical_kind -> unit -val constant_kind : Constant.t -> logical_kind diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index e1269025a4..482303d935 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -69,7 +69,7 @@ let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state -open Decl_kinds +open Decls open Declarations let type_of_logical_kind = function @@ -104,13 +104,20 @@ let type_of_logical_kind = function | Corollary -> "thm") | IsPrimitive -> "prim" + +(** Data associated to global parameters and constants *) + +let csttab = Summary.ref (Names.Cmap.empty : logical_kind Names.Cmap.t) ~name:"CONSTANT" +let add_constant_kind kn k = csttab := Names.Cmap.add kn k !csttab +let constant_kind kn = Names.Cmap.find kn !csttab + let type_of_global_ref gr = if Typeclasses.is_class gr then "class" else match gr with | Globnames.ConstRef cst -> - type_of_logical_kind (Decls.constant_kind cst) + type_of_logical_kind (constant_kind cst) | Globnames.VarRef v -> "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 18955985a0..e0308b8afc 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -45,3 +45,6 @@ val dump_constraint : Names.lname -> bool -> string -> unit val dump_string : string -> unit val type_of_global_ref : Names.GlobRef.t -> string + +(** Registration of constant information *) +val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit diff --git a/interp/interp.mllib b/interp/interp.mllib index 33573edcce..cb6c527c83 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -10,6 +10,7 @@ Notation Syntax_def Smartlocate Constrexpr_ops +Decls Dumpglob Reserve Impargs diff --git a/kernel/entries.ml b/kernel/entries.ml index ca08ba485e..bc389e9fcf 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -57,17 +57,15 @@ type mutual_inductive_entry = { } (** {6 Constants (Definition/Axiom) } *) -type 'a proof_output = constr Univ.in_universe_context_set * 'a -type 'a const_entry_body = 'a proof_output Future.computation type definition_entry = { - const_entry_body : constr Univ.in_universe_context_set; + const_entry_body : constr; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; - const_entry_type : types option; - const_entry_universes : universes_entry; + const_entry_type : types option; + const_entry_universes : universes_entry; const_entry_inline_code : bool } type section_def_entry = { @@ -98,6 +96,9 @@ type primitive_entry = { prim_entry_content : CPrimitives.op_or_type; } +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation + type 'a constant_entry = | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7526508c4e..2c434d4edf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff = } else DefinitionEntry { - const_entry_body = (p, Univ.ContextSet.empty); + const_entry_body = p; const_entry_secctx = Some cb.const_hyps; const_entry_feedback = None; const_entry_type = Some cb.const_type; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b3c3dcbf45..5844bd89f8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -194,14 +194,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in - let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let () = match trust with | Pure -> () | SideEffects _ -> assert false in let env, usubst, univs = match c.const_entry_universes with - | Monomorphic_entry univs -> - let ctx = Univ.ContextSet.union univs ctx in + | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> @@ -210,10 +209,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - let () = - if not (Univ.ContextSet.is_empty ctx) then - CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") - in env, sbst, Polymorphic auctx in let j = Typeops.infer env body in @@ -347,9 +342,8 @@ let translate_recipe env _kn r = let translate_local_def env _id centry = let open Cooking in - let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { - const_entry_body = body; + const_entry_body = centry.secdef_body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; diff --git a/lib/cErrors.ml b/lib/cErrors.ml index a42504701f..8406adfe18 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -39,9 +39,6 @@ let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) -exception AlreadyDeclared of Pp.t (* for already declared Schemes *) -let alreadydeclared pps = raise (AlreadyDeclared(pps)) - exception Timeout let handle_stack = ref [] diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 51ec5c907a..8580622095 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -41,9 +41,6 @@ val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an error [pp] with optional header and location [hdr] [loc] *) -exception AlreadyDeclared of Pp.t -val alreadydeclared : Pp.t -> 'a - val invalid_arg : ?loc:Loc.t -> string -> 'a (** [todo] is for running of an incomplete code its implementation is diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 6eb582baef..17746645ee 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -8,58 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Informal mathematical status of declarations *) - type binding_kind = Explicit | Implicit - -type private_flag = bool - -type cumulative_inductive_flag = bool - -type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - -type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - -type assumption_object_kind = Definitional | Logical | Conjectural | Context - -(* [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -(** Kinds used in library *) - -type logical_kind = - | IsPrimitive - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind diff --git a/library/kindops.ml b/library/kindops.ml deleted file mode 100644 index 0bf55c62a9..0000000000 --- a/library/kindops.ml +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* * 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 Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -let logical_kind_of_goal_kind = function - | DefinitionBody d -> IsDefinition d - | Proof s -> IsProof s - -let string_of_theorem_kind = function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | Corollary -> "Corollary" - -let string_of_definition_object_kind = function - | Definition -> "Definition" - | Example -> "Example" - | Coercion -> "Coercion" - | SubClass -> "SubClass" - | CanonicalStructure -> "Canonical Structure" - | Instance -> "Instance" - | Let -> "Let" - | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli deleted file mode 100644 index 3c9f2bb7c3..0000000000 --- a/library/kindops.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* * 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 Decl_kinds - -(** Operations about types defined in [Decl_kinds] *) - -val logical_kind_of_goal_kind : goal_object_kind -> logical_kind -val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_object_kind : definition_object_kind -> string diff --git a/library/library.mllib b/library/library.mllib index ef53471377..35af5fa43b 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,16 +1,15 @@ +Decl_kinds Libnames Globnames Libobject Summary Nametab Global -Decl_kinds Lib Declaremods Library States Kindops Goptions -Decls Keys Coqlib diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e34150f2b3..ead78f70a1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in let poly = false in - let kind = Decl_kinds.(DefinitionBody Definition) in + let kind = Decls.(IsDefinition Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 69e5c4231f..ca1520594d 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -648,7 +648,6 @@ let separate_extraction lr = is \verb!Extraction! [qualid]. *) let simple_extraction r = - Vernacentries.dump_global CAst.(make (Constrexpr.AN r)); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f773b2c39e..bf2b4c9122 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(IsProof Theorem)) () in let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index edda2f2eef..cb7a509829 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -354,7 +354,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) in let names = ref [new_princ_name] in let hook = - fun new_principle_type _ _ _ _ -> + fun new_principle_type _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) @@ -369,9 +369,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant - name - (Declare.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme)) + ~name + ~kind:Decls.(IsDefinition Scheme) + (Declare.DefinitionEntry ce) ); Declare.definition_message name; names := name :: !names @@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem) + save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -526,7 +526,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro this_block_funs 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) - (fun _ _ _ _ _ -> ()) + (fun _ _ -> ()) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -588,7 +588,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro this_block_funs !i (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) - (fun _ _ _ _ _ -> ()) + (fun _ _ -> ()) in const with Found_type i -> @@ -637,8 +637,9 @@ let build_scheme fas = (fun (princ_id,_,_) def_entry -> ignore (Declare.declare_constant - princ_id - (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + ~name:princ_id + ~kind:Decls.(IsProof Theorem) + (Declare.DefinitionEntry def_entry)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bb4e745fe9..bcad6cedf1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1506,7 +1506,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds ~cumulative:false ~poly:false ~private_ind:false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d305a58ccc..9a9e0b9692 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~name:fname ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition pl + ~kind:Decls.Definition pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 254760cb50..58b0ead130 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -123,21 +123,19 @@ open DeclareDef let definition_message = Declare.definition_message -let save id const ?hook uctx locality kind = +let save name const ?hook uctx scope kind = let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in - let r = match locality with + let r = match scope with | Discharge -> - let k = Kindops.logical_kind_of_goal_kind kind in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - VarRef id + let c = SectionLocalDef const in + let _ = declare_variable ~name ~kind (Lib.cwd(), c) in + VarRef name | Global local -> - let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in - ConstRef kn + let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in + ConstRef kn in - DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; - definition_message id + DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); + definition_message name let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 45d332031f..a95b1242ac 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -48,7 +48,7 @@ val save -> ?hook:DeclareDef.Hook.t -> UState.t -> DeclareDef.locality - -> Decl_kinds.goal_object_kind + -> Decls.logical_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 86defb2f2f..549f6d42c9 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(IsProof Theorem)) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false @@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.(Proof Theorem) () in + ~kind:Decls.(IsProof Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b68b31c93b..8d6b85f94d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,6 @@ open Tacmach open Tactics open Nametab open Declare -open Decl_kinds open Tacred open Goal open Glob_term @@ -66,9 +65,9 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?univs value = +let declare_fun name kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in - ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; + ConstRef(declare_constant ~name ~kind (DefinitionEntry ce)) let defined lemma = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None @@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = +let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -1308,7 +1307,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); - let hook _ _ _ _ = + let hook _ = let opacity = let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in @@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma)) () in let lemma = Lemmas.start_lemma ~name:na @@ -1411,7 +1410,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in + let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~sign:(Environ.named_context_val env) @@ -1535,7 +1534,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type let term_id = add_suffix function_name "_terminate" in let functional_ref = let univs = Evd.univ_entry ~poly:false evd in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res + declare_fun functional_id Decls.(IsDefinition Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evd = Evd.from_env (Global.env ()) in @@ -1547,9 +1546,9 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook uctx _ _ _ = + let hook { DeclareDef.Hook.S.uctx ; _ } = let term_ref = Nametab.locate (qualid_of_ident term_id) in - let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in + let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 8acb29ba74..13844c2707 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1898,11 +1898,11 @@ let declare_projection n instance_id r = let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in - let cst = - Declare.definition_entry ~types:typ ~univs term - in - ignore(Declare.declare_constant n - (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + let cst = Declare.definition_entry ~types:typ ~univs term in + let _ : Constant.t = + Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition) + (Declare.DefinitionEntry cst) + in () let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1978,10 +1978,9 @@ let add_morphism_as_parameter atts m n : unit = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in - let cst = Declare.declare_constant instance_id - (Declare.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) + let cst = Declare.declare_constant ~name:instance_id + ~kind:Decls.(IsAssumption Logical) + (Declare.ParameterEntry (None,(instance,uctx),None)) in Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); @@ -1995,9 +1994,9 @@ let add_morphism_interactive atts m n : Lemmas.t = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let poly = atts.polymorphic in - let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook _ _ _ = function + let hook { DeclareDef.Hook.S.dref; _ } = dref |> function | Globnames.ConstRef cst -> Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 33798c43c8..9973f2ec1d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -29,7 +29,6 @@ open Tacinterp open Libobject open Printer open Declare -open Decl_kinds open Entries open Newring_ast open Proofview.Notations @@ -156,9 +155,9 @@ let decl_constant na univs c = let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in - mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c), - IsProof Lemma)) + mkConst(declare_constant ~name:(Id.of_string na) + ~kind:Decls.(IsProof Lemma) + (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c))) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = diff --git a/pretyping/classops.ml b/pretyping/classops.ml index f5fffc4c1c..afb546b2d2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -313,7 +313,9 @@ let compare_path p q = !path_comparator p q let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" - (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l) + (fun l -> prlist_with_sep fnl (fun (c,p,q) -> + str"New coercion path " ++ print_path (c,p) ++ + str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -330,13 +332,13 @@ let different_class_params env i = let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = - (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in + (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in let try_add_new_path (i,j as ij) p = if not (Bijint.Index.equal i j) || different_class_params env i then match lookup_path_between_class ij with | q -> if not (compare_path env sigma p q) then - ambig_paths := (ij,p)::!ambig_paths; + ambig_paths := (ij,p,q)::!ambig_paths; false | exception Not_found -> (add_new_path ij p; true) else diff --git a/pretyping/heads.ml b/pretyping/heads.ml index d65faecd19..870df62500 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -41,8 +41,7 @@ let rec compute_head env = function | Some c -> kind_of_head env c) | EvalVarRef id -> (match lookup_named id env with - | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> - kind_of_head env c + | LocalDef (_,c,_) -> kind_of_head env c | _ -> RigidHead RigidOther) and kind_of_head env t = diff --git a/printing/printer.ml b/printing/printer.ml index 0bcea3b01c..1f68018678 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -831,6 +831,22 @@ let pr_goal_by_id ~proof id = pr_selected_subgoal (pr_id id) sigma g) with Not_found -> user_err Pp.(str "No such goal.") +(** print a goal identified by the goal id as it appears in -emacs mode. + sid should be the Stm state id corresponding to proof. Used to support + the Prooftree tool in Proof General. (https://askra.de/software/prooftree/). +*) +let pr_goal_emacs ~proof gid sid = + match proof with + | None -> user_err Pp.(str "No proof for that state.") + | Some proof -> + let pr gs = + v 0 ((str "goal ID " ++ (int gid) ++ str " at state " ++ (int sid)) ++ cut () + ++ pr_goal gs) + in + try + Proof.in_proof proof (fun sigma -> pr {it=(Evar.unsafe_of_int gid);sigma=sigma;}) + with Not_found -> user_err Pp.(str "No such goal.") + (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) diff --git a/printing/printer.mli b/printing/printer.mli index 4923e9ec0e..a72f319636 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -206,4 +206,4 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t - +val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t diff --git a/stm/stm.ml b/stm/stm.ml index 91397950f6..ceb62582cd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1114,6 +1114,7 @@ module Backtrack : sig (* Returns the state that the command should backtract to *) val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option + val get_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1259,6 +1260,7 @@ end = struct (* {{{ *) end (* }}} *) let get_prev_proof = Backtrack.get_prev_proof +let get_proof = Backtrack.get_proof let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = @@ -2421,8 +2423,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* State resulting from reach *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x) - ); - if eff then update_global_env () + ) ), eff || cache, true | `Cmd { cast = x; ceff = eff } -> (fun () -> (match !cur_opt.async_proofs_mode with @@ -2430,8 +2431,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = resilient_command reach view.next | APoff -> reach view.next); let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - if eff then update_global_env () + ignore(stm_vernac_interp id st x) ), eff || cache, true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; @@ -2560,8 +2560,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - update_global_env () + ignore(stm_vernac_interp id st x) ), cache, true | `Sideff (CherryPickEnv, origin) -> (fun () -> reach view.next; diff --git a/stm/stm.mli b/stm/stm.mli index f1bef2dc4d..92a782d965 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -119,6 +119,8 @@ the specified state AND that has differences in the underlying proof (i.e., ignoring proofview-only changes). Used to compute proof diffs. *) val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option +val get_proof : doc:doc -> Stateid.t -> Proof.t option + (* [query at ?report_with cmd] Executes [cmd] at a given state [at], throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 662a2fc22c..09d7e0278a 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -13,7 +13,6 @@ module CVars = Vars open Util open Termops open EConstr -open Decl_kinds open Evarutil module RelDecl = Context.Rel.Declaration @@ -153,12 +152,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in - let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) 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 decl + Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Proof_global.proof_entry_universes with diff --git a/tactics/declare.ml b/tactics/declare.ml index 74196bb875..e550e06471 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -11,21 +11,23 @@ (** This module is about the low-level declaration of logical objects *) open Pp -open CErrors open Util open Names -open Libnames -open Globnames -open Constr open Declarations open Entries +open Safe_typing open Libobject open Lib -open Impargs -open Safe_typing -open Cooking -open Decls -open Decl_kinds + +(* object_kind , id *) +exception AlreadyDeclared of (string option * Id.t) + +let _ = CErrors.register_handler (function + | AlreadyDeclared (kind, id) -> + seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind + ; Id.print id; str " already exists."] + | _ -> + raise CErrors.Unhandled) module NamedDecl = Context.Named.Declaration @@ -36,7 +38,7 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified type constant_obj = { cst_decl : Cooking.recipe option; (** Non-empty only when rebuilding a constant after a section *) - cst_kind : logical_kind; + cst_kind : Decls.logical_kind; cst_locl : import_status; } @@ -45,16 +47,14 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type constant_declaration = Evd.side_effects constant_entry * logical_kind - (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then - alreadydeclared (Id.print (basename sp) ++ str " already exists"); + raise (AlreadyDeclared (None, Libnames.basename sp)); let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con obj.cst_kind + Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con); + Dumpglob.add_constant_kind con obj.cst_kind let cooking_info segment = let modlist = replacement_context () in @@ -70,32 +70,33 @@ let open_constant i ((sp,kn), obj) = | ImportNeedQualified -> () | ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con) + Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) + Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) let check_exists id = - if exists_name id then alreadydeclared (Id.print id ++ str " already exists") + if exists_name id then + raise (AlreadyDeclared (None, id)) let cache_constant ((sp,kn), obj) = (* Invariant: the constant must exist in the logical environment, except when redefining it when exiting a section. See [discharge_constant]. *) - let id = basename sp in + let id = Libnames.basename sp in let kn' = match obj.cst_decl with | None -> - if Global.exists_objlabel (Label.of_id (basename sp)) + if Global.exists_objlabel (Label.of_id (Libnames.basename sp)) then Constant.make1 kn - else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".") + else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".") | Some r -> Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r in assert (Constant.equal kn' (Constant.make1 kn)); - Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); + Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - add_constant_kind (Constant.make1 kn) obj.cst_kind + Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in @@ -103,7 +104,7 @@ let discharge_constant ((sp, kn), obj) = let info = cooking_info (section_segment_of_constant con) in (* This is a hack: when leaving a section, we lose the constant definition, so we have to store it in the libobject to be able to retrieve it after. *) - Some { obj with cst_decl = Some { from; info } } + Some { obj with cst_decl = Some { Cooking.from; info } } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { @@ -127,8 +128,8 @@ let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f let update_tables c = - declare_constant_implicits c; - Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) + Impargs.declare_constant_implicits c; + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) let register_constant kn kind local = let o = inConstant { @@ -141,7 +142,7 @@ let register_constant kn kind local = update_tables kn let register_side_effect (c, role) = - let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in + let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in match role with | None -> () | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] @@ -173,12 +174,21 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types let cast_proof_entry e = let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in + let univs = + if Univ.ContextSet.is_empty ctx then e.proof_entry_universes + else match e.proof_entry_universes with + | Monomorphic_entry ctx' -> + (* This can actually happen, try compiling EqdepFacts for instance *) + Monomorphic_entry (Univ.ContextSet.union ctx' ctx) + | Polymorphic_entry _ -> + CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition."); + in { - const_entry_body = (body, ctx); + const_entry_body = body; const_entry_secctx = e.proof_entry_secctx; const_entry_feedback = e.proof_entry_feedback; const_entry_type = e.proof_entry_type; - const_entry_universes = e.proof_entry_universes; + const_entry_universes = univs; const_entry_inline_code = e.proof_entry_inline_code; } @@ -227,7 +237,7 @@ let get_roles export eff = in List.map map export -let define_constant ~side_effect id cd = +let define_constant ~side_effect ~name cd = let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let is_poly de = match de.proof_entry_universes with @@ -262,20 +272,20 @@ let define_constant ~side_effect id cd = | PrimitiveEntry e -> [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) in - let kn, eff = Global.add_constant ~side_effect ~in_section id decl in + let kn, eff = Global.add_constant ~side_effect ~in_section name decl in kn, eff, export -let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) = - let () = check_exists id in - let kn, (), export = define_constant ~side_effect:PureEntry id cd in +let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = + let () = check_exists name in + let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) = - let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in - let () = assert (List.is_empty export) in +let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd = + let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in + let () = assert (CList.is_empty export) in let () = register_constant kn kind local in let seff_roles = match role with | None -> Cmap.empty @@ -284,34 +294,25 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) - id ?types (body,univs) = - let cb = - definition_entry ?types ~univs ~opaque body - in - declare_constant ~local id - (DefinitionEntry cb, Decl_kinds.IsDefinition kind) - (** Declaration of section variables and local definitions *) type section_variable_entry = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } -type variable_declaration = DirPath.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry let cache_variable ((sp,_),o) = match o with | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(path,d,kind)) -> + | Inr (id,(path,d),kind) -> (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); + if Decls.variable_exists id then + raise (AlreadyDeclared (None, id)); let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;univs;poly;impl} -> let () = Global.push_named_assum ((id,typ,poly),univs) in - let impl = if impl then Implicit else Explicit in + let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in impl, true, poly, univs | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a @@ -336,20 +337,20 @@ let cache_variable ((sp,_),o) = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (id, se) in - Explicit, de.proof_entry_opaque, + Decl_kinds.Explicit, de.proof_entry_opaque, poly, univs in - Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + Nametab.push (Nametab.Until 1) (Libnames.restrict_path 0 sp) (GlobRef.VarRef id); add_section_variable ~name:id ~kind:impl ~poly univs; - add_variable_data id {path;opaque;univs;poly;kind} + Decls.(add_variable_data id {path;opaque;univs;poly;kind}) let discharge_variable (_,o) = match o with - | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) + | Inr (id,_,_) -> + if Decls.variable_polymorphic id then None + else Some (Inl (Decls.variable_context id)) | Inl _ -> Some o type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union + (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union let inVariable : variable_obj -> obj = declare_object { (default_object "VARIABLE") with @@ -358,22 +359,22 @@ let inVariable : variable_obj -> obj = classify_function = (fun _ -> Dispose) } (* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope Evd.empty (VarRef id); +let declare_variable ~name ~kind obj = + let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in + Impargs.declare_var_implicits name; + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name); oname (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i)); for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j)); done) mie.mind_entry_inds let inductive_names sp kn mie = - let (dp,_) = repr_path sp in + let (dp,_) = Libnames.repr_path sp in let kn = Global.mind_of_delta_kn kn in let names, _ = List.fold_left @@ -385,11 +386,11 @@ let inductive_names sp kn mie = let sp = Libnames.make_path dp l in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) + ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1)) (names, 1) ind.mind_entry_consnames in let sp = Libnames.make_path dp ind.mind_entry_typename in - ((sp, IndRef ind_p) :: names, n+1)) + ((sp, GlobRef.IndRef ind_p) :: names, n+1)) ([], 0) mie.mind_entry_inds in names @@ -403,8 +404,8 @@ let open_inductive i ((sp,kn),mie) = let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in - List.iter check_exists (List.map (fun p -> basename (fst p)) names); - let id = basename sp in + List.iter check_exists (List.map (fun p -> Libnames.basename (fst p)) names); + let id = Libnames.basename sp in let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in @@ -419,7 +420,7 @@ let discharge_inductive ((sp,kn),mie) = let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; - mind_entry_arity = mkProp; + mind_entry_arity = Constr.mkProp; mind_entry_template = false; mind_entry_consnames = mie.mind_entry_consnames; mind_entry_lc = [] @@ -471,7 +472,7 @@ let inPrim : (Projection.Repr.t * Constant.t) -> obj = let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let id = Label.to_id label in + let name = Label.to_id label in let univs, u = match univs with | Monomorphic_entry _ -> (* Global constraints already defined through the inductive *) @@ -482,11 +483,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let term = Vars.subst_instance_constr u term in let types = Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in - let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in declare_primitive_projection p cst - let declare_projections univs mind = let env = Global.env () in let mib = Environ.lookup_mind mind env in @@ -506,11 +506,11 @@ let declare_projections univs mind = let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename - | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in + | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive mie) in let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in - declare_mib_implicits mind; + Impargs.declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim @@ -520,7 +520,7 @@ let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "no recursive definition.") + | [] -> CErrors.anomaly (Pp.str "no recursive definition.") | [id] -> Id.print id ++ str " is recursively defined" ++ (match indexes with | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" @@ -535,7 +535,7 @@ let fixpoint_message indexes l = let cofixpoint_message l = Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "No corecursive definition.") + | [] -> CErrors.anomaly (Pp.str "No corecursive definition.") | [id] -> Id.print id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are corecursively defined")) @@ -577,9 +577,9 @@ type universe_source = type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list -let check_exists sp = +let check_exists_universe sp = if Nametab.exists_universe sp then - alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") + raise (AlreadyDeclared (Some "Universe", Libnames.basename sp)) else () let qualify_univ i dp src id = @@ -592,19 +592,19 @@ let qualify_univ i dp src id = let do_univ_name ~check i dp src (id,univ) = let i, sp = qualify_univ i dp src id in - if check then check_exists sp; + if check then check_exists_universe sp; Nametab.push_universe i sp univ let cache_univ_names ((sp, _), (src, univs)) = let depth = sections_depth () in - let dp = pop_dirpath_n depth (dirpath sp) in + let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs + List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs let discharge_univ_names = function | _, (BoundUniv, _) -> None @@ -624,12 +624,13 @@ let declare_univ_binders gr pl = if Global.is_polymorphic gr then () else - let l = match gr with + let l = let open GlobRef in match gr with | ConstRef c -> Label.to_id @@ Constant.label c | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | VarRef id -> + CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> - anomaly ~label:"declare_univ_binders" + CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on an constructor reference") in let univs = Id.Map.fold (fun id univ univs -> @@ -643,7 +644,7 @@ let do_universe ~poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err ~hdr:"Constraint" + CErrors.user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in @@ -663,13 +664,13 @@ let do_constraint ~poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err ~hdr:"Constraint" + CErrors.user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in let check_poly p p' = if poly then () else if p || p' then - user_err ~hdr:"Constraint" + CErrors.user_err ~hdr:"Constraint" (str "Cannot declare a global constraint on " ++ str "a polymorphic universe, use " ++ str "Polymorphic Constraint instead") diff --git a/tactics/declare.mli b/tactics/declare.mli index 1f72fff30e..f2d23fb319 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -11,7 +11,6 @@ open Names open Constr open Entries -open Decl_kinds (** This module provides the official functions to declare new variables, parameters, constants and inductive types. Using the following functions @@ -31,15 +30,17 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type variable_declaration = DirPath.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry -val declare_variable : variable -> variable_declaration -> Libobject.object_name +val declare_variable + : name:variable + -> kind:Decls.logical_kind + -> variable_declaration + -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = Evd.side_effects constant_entry * logical_kind - (* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> @@ -54,16 +55,20 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) -val declare_constant : - ?local:import_status -> Id.t -> constant_declaration -> Constant.t - -val declare_private_constant : - ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects - -val declare_definition : - ?opaque:bool -> ?kind:definition_object_kind -> - ?local:import_status -> Id.t -> ?types:constr -> - constr Entries.in_universes_entry -> Constant.t +val declare_constant + : ?local:import_status + -> name:Id.t + -> kind:Decls.logical_kind + -> Evd.side_effects constant_entry + -> Constant.t + +val declare_private_constant + : ?role:Evd.side_effect_role + -> ?local:import_status + -> name:Id.t + -> kind:Decls.logical_kind + -> Evd.side_effects constant_entry + -> Constant.t * Evd.side_effects (** Since transparent constants' side effects are globally declared, we * need that *) @@ -93,3 +98,6 @@ val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit val do_universe : poly:bool -> lident list -> unit val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit + +(* Used outside this module only in indschemes *) +exception AlreadyDeclared of (string option * Id.t) diff --git a/tactics/hints.ml b/tactics/hints.ml index 3a3a6b94dc..8d1c536db6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1315,12 +1315,16 @@ let project_hint ~poly pri l2r r = let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in - let id = + let name = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition id (c,ctx) in + let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in + let c = Declare.declare_constant + ~local:Declare.ImportDefaultBehavior + ~name ~kind:Decls.(IsDefinition Definition) cb + in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e01f3ab961..e2ef05461b 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -22,7 +22,6 @@ open Declarations open Constr open CErrors open Util -open Decl_kinds open Pp (**********************************************************************) @@ -136,7 +135,7 @@ let define internal role id c poly univs = proof_entry_inline_code = false; proof_entry_feedback = None; } in - let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in let () = match internal with | InternalTacticRequest -> () | _-> Declare.definition_message id diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e242b10d33..2af3947dd1 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -27,7 +27,6 @@ open Tacmach.New open Clenv open Tacticals.New open Tactics -open Decl_kinds open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -236,7 +235,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.univ_entry ~poly sigma in let entry = Declare.definition_entry ~univs invProof in - let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in + let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in () (* inv_op = Inv (derives de complete inv. lemma) diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 8447cf10db..8c4808a755 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -1,17 +1,16 @@ open Names -let evil t f = +let evil name name_f = let open Univ in let open Entries in - let open Decl_kinds in let open Constr in - let k = IsDefinition Definition in + let kind = Decls.(IsDefinition Definition) in let u = Level.var 0 in let tu = mkType (Universe.make u) in let te = Declare.definition_entry ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in - let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in + let tc = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry te) in let tc = mkConst tc in let fe = Declare.definition_entry @@ -19,4 +18,5 @@ let evil t f = ~types:(Term.mkArrowR tc tu) (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1)) in - ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k)) + let _ : Constant.t = Declare.declare_constant ~name:name_f ~kind (Declare.DefinitionEntry fe) in + () diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out new file mode 100644 index 0000000000..2eadd22db8 --- /dev/null +++ b/test-suite/output-coqtop/ShowGoal.out @@ -0,0 +1,73 @@ +
+Coq < 1 subgoal
+
+ ============================
+ forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
+
+x <
+x < 1 focused subgoal
+(shelved: 1)
+
+ i : nat
+ ============================
+ exists k : nat, i = ?j /\ ?j = k /\ i = k
+
+x < 1 focused subgoal
+(shelved: 2)
+
+ i : nat
+ ============================
+ i = ?j /\ ?j = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 2)
+
+ i : nat
+ ============================
+ i = ?j
+
+subgoal 2 is:
+ ?j = ?k /\ i = ?k
+
+x < 1 focused subgoal
+(shelved: 1)
+
+ i : nat
+ ============================
+ i = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 1)
+
+ i : nat
+ ============================
+ i = ?k
+
+subgoal 2 is:
+ i = ?k
+
+x < 1 subgoal
+
+ i : nat
+ ============================
+ i = i
+
+x < goal ID 16 at state 5
+
+ i : nat
+ ============================
+ i = ?j /\ ?j = ?k /\ i = ?k
+
+x < goal ID 16 at state 7
+
+ i : nat
+ ============================
+ i = i /\ i = ?k /\ i = ?k
+
+x < goal ID 16 at state 9
+
+ i : nat
+ ============================
+ i = i /\ i = i /\ i = i
+
+x <
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v new file mode 100644 index 0000000000..9545254770 --- /dev/null +++ b/test-suite/output-coqtop/ShowGoal.v @@ -0,0 +1,11 @@ +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. + eexists. + split. + trivial. + split. + trivial. +Show Goal 16 at 5. +Show Goal 16 at 7. +Show Goal 16 at 9. diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index 2a7ce806d7..dc793598a9 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -1,5 +1,7 @@ File "stdin", line 10, characters 0-28: -Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker] +Warning: +New coercion path [ac; cd] : A >-> D is ambiguous with existing +[ab; bd] : A >-> D. [ambiguous-paths,typechecker] [ab] : A >-> B [ab; bd] : A >-> D [ac] : A >-> C @@ -20,8 +22,9 @@ Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker] [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 103, characters 0-86: -Warning: Ambiguous paths: [D_C; C_A'] : D >-> A' -[ambiguous-paths,typechecker] +Warning: +New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing +[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] [A'_A] : A' >-> A [B_A'] : B >-> A' [B_A'; A'_A] : B >-> A diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4077c02604..4bcde566e3 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -403,6 +403,11 @@ let rec vernac_loop ~state = top_goal_print ~doc:state.doc c state.proof nstate.proof; vernac_loop ~state:nstate + | Some (VernacShowGoal {gid; sid}) -> + let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in + Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid); + vernac_loop ~state + | None -> top_stderr (fnl ()); exit 0 diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index cddcd5faa7..fed337ab03 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -11,6 +11,8 @@ { open Pcoq open Pcoq.Prim +open Tok +open Util open Vernacexpr (* Vernaculars specific to the toplevel *) @@ -19,6 +21,7 @@ type vernac_toplevel = | VernacDrop | VernacQuit | VernacControl of vernac_control + | VernacShowGoal of { gid : int; sid: int } module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -29,6 +32,21 @@ end open Toplevel_ +let err () = raise Stream.Failure + +let test_show_goal = + Pcoq.Entry.of_parser "test_show_goal" + (fun strm -> + match stream_nth 0 strm with + | IDENT "Show" -> + (match stream_nth 1 strm with + | IDENT "Goal" -> + (match stream_nth 2 strm with + | NUMERAL _ -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + } GRAMMAR EXTEND Gram @@ -38,6 +56,9 @@ GRAMMAR EXTEND Gram | IDENT "Quit"; "." -> { Some VernacQuit } | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> { Some (VernacBacktrack (n,m,p)) } + (* 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}) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None diff --git a/vernac/class.ml b/vernac/class.ml index febe8e34e4..f79e459f43 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Decl_kinds open Libobject let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -208,7 +207,7 @@ let build_id_coercion idf_opt source poly = user_err (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") in - let idf = + let name = match idf_opt with | Some idf -> idf | None -> @@ -222,8 +221,8 @@ let build_id_coercion idf_opt source poly = (definition_entry ~types:typ_f ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in - let decl = (constr_entry, IsDefinition IdentityCoercion) in - let kn = declare_constant idf decl in + let kind = Decls.(IsDefinition IdentityCoercion) in + let kn = declare_constant ~name ~kind constr_entry in ConstRef kn let check_source = function @@ -355,27 +354,27 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target = let try_add_new_coercion_with_source ref ~local ~poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false -let add_coercion_hook poly _uctx _trans local ref = +let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = let open DeclareDef in - let local = match local with + let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in - let () = try_add_new_coercion ref ~local ~poly in - let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let () = try_add_new_coercion dref ~local ~poly in + let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) -let add_subclass_hook ~poly _uctx _trans local ref = +let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = let open DeclareDef in - let stre = match local with + let stre = match scope with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in - let cl = class_of_global ref in + let cl = class_of_global dref in try_add_new_coercion_subclass cl ~local:stre ~poly let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) diff --git a/vernac/classes.ml b/vernac/classes.ml index 35108744cd..24f4f7fe70 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,23 +313,22 @@ let instance_hook info global imps ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook id decl poly sigma term termtype = +let declare_instance_constant info global imps ?hook name decl poly sigma term termtype = (* XXX: Duplication of the declare_constant path *) - let kind = IsDefinition Instance in let sigma = let levels = Univ.LSet.union (CVars.universes_of_constr termtype) (CVars.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in + let kind = Decls.(IsDefinition Instance) in let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in - let cdecl = (Declare.DefinitionEntry entry, kind) in - let kn = Declare.declare_constant id cdecl in - Declare.definition_message id; + let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in + Declare.definition_message name; Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (ConstRef kn) -let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id = +let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) @@ -337,15 +336,15 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in - let cst = Declare.declare_constant id - (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in + let cst = Declare.declare_constant ~name + ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (ConstRef cst) let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = - let hook _ _ vis gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr imps; + let hook { DeclareDef.Hook.S.scope; dref; _ } = + let cst = match dref with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false dref imps; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in @@ -363,7 +362,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition ~name:id ?term:constr - ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls) + ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Decls.Instance ~hook typ ctx obls) let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -373,8 +372,8 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in - let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in + let kind = Decls.(IsDefinition Instance) in + let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in let info = Lemmas.Info.make ~hook ~scope ~kind () in let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e91d8b9d3e..60086a7861 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -18,7 +18,6 @@ open Globnames open Constrexpr_ops open Constrintern open Impargs -open Decl_kinds open Pretyping open Entries @@ -36,14 +35,14 @@ let () = optread = (fun _ -> !axiom_into_instance); optwrite = (:=) axiom_into_instance; } -let should_axiom_into_instance = function +let should_axiom_into_instance = let open Decls in function | Context -> (* The typeclass behaviour of Variable and Context doesn't depend on section status *) true | Definitional | Logical | Conjectural -> !axiom_into_instance -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=ident} = +let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} = let open DeclareDef in match scope with | Discharge -> @@ -51,10 +50,11 @@ match scope with | Monomorphic_entry univs -> univs | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs in - let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, IsAssumption kind) in - let _ = declare_variable ident decl in - let () = assumption_message ident in - let r = VarRef ident in + let kind = Decls.IsAssumption kind in + let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in + let _ = declare_variable ~name ~kind decl in + let () = assumption_message name in + let r = VarRef name in let () = maybe_declare_manual_implicits true r imps in let env = Global.env () in let sigma = Evd.from_env env in @@ -69,12 +69,13 @@ match scope with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let decl = (Declare.ParameterEntry (None,(typ,univs),inl), IsAssumption kind) in - let kn = declare_constant ident ~local decl in + let kind = Decls.IsAssumption kind in + let decl = Declare.ParameterEntry (None,(typ,univs),inl) in + let kn = declare_constant ~name ~local ~kind decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in - let () = assumption_message ident in + let () = assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in @@ -211,7 +212,8 @@ let do_primitive id prim typopt = prim_entry_content = prim; } in - let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in + let _kn : Names.Constant.t = + declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") let named_of_rel_context l = @@ -269,24 +271,25 @@ let context ~poly l = Monomorphic_entry Univ.ContextSet.empty end in - let fn status (id, b, t) = + let fn status (name, b, t) = let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) + let kind = Decls.(IsAssumption Logical) in let decl = match b with | None -> - (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical) + Declare.ParameterEntry (None,(t,univs),None) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in - (Declare.DefinitionEntry entry, IsAssumption Logical) + Declare.DefinitionEntry entry in - let cst = Declare.declare_constant id decl in + let cst = Declare.declare_constant ~name ~kind decl in let env = Global.env () in Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); status else let test x = match x.CAst.v with - | Some (Name id',_) -> Id.equal id id' + | Some (Name id',_) -> Id.equal name id' | _ -> false in let impl = List.exists test impls in @@ -294,13 +297,13 @@ let context ~poly l = if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in let nstatus = match b with | None -> - pi3 (declare_assumption false ~scope ~poly ~kind:Context t univs UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make id)) + pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl + Declaremods.NoInline (CAst.make name)) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in let _gr = DeclareDef.declare_definition - ~name:id ~scope:DeclareDef.Discharge - ~kind:Definition UnivNames.empty_binders entry [] in + ~name ~scope:DeclareDef.Discharge + ~kind:Decls.Definition UnivNames.empty_binders entry [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 57b4aea9e3..028ed39656 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -11,7 +11,6 @@ open Names open Vernacexpr open Constrexpr -open Decl_kinds (** {6 Parameters/Assumptions} *) @@ -19,7 +18,7 @@ val do_assumptions : program_mode:bool -> poly:bool -> scope:DeclareDef.locality - -> kind:assumption_object_kind + -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool @@ -30,7 +29,7 @@ val declare_assumption : coercion_flag -> poly:bool -> scope:DeclareDef.locality - -> kind:assumption_object_kind + -> kind:Decls.assumption_object_kind -> Constr.types -> Entries.universes_entry -> UnivNames.universe_binders diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 71926a9d23..db0c102e14 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Decl_kinds open Redexpr open Constrexpr @@ -21,7 +20,7 @@ val do_definition -> name:Id.t -> scope:DeclareDef.locality -> poly:bool - -> kind:definition_object_kind + -> kind:Decls.definition_object_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index e3428d6afc..3f13d772ab 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -20,7 +20,6 @@ open Names open Constrexpr open Constrexpr_ops open Constrintern -open Decl_kinds open Pretyping open Evarutil open Evarconv @@ -257,8 +256,8 @@ let interp_fixpoint ~cofix l ntns = let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = let fix_kind, cofix, indexes = match indexes with - | Some indexes -> Fixpoint, false, indexes - | None -> CoFixpoint, true, [] + | Some indexes -> Decls.Fixpoint, false, indexes + | None -> Decls.CoFixpoint, true, [] in let thms = List.map3 (fun name t (ctx,impargs,_) -> @@ -269,7 +268,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl + Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl evd (Some(cofix,indexes,init_tac)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; @@ -278,8 +277,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Fixpoint - | None -> [], true, CoFixpoint + | Some indexes -> indexes, false, Decls.Fixpoint + | None -> [], true, Decls.CoFixpoint in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index f530dad4fd..d99d3e65fd 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -349,7 +349,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum ~poly prv finite = +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = check_all_names_different indl; List.iter check_param paramsl; if not (List.is_empty uparamsl) && not (List.is_empty notations) @@ -453,24 +453,24 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ impls) cimpls) indimpls constructors in - let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in + let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; - mind_entry_private = if prv then Some false else None; + mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; mind_entry_variance = variance; } in - (if poly && cum then + (if poly && cumulative then InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum ~poly prv finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum ~poly prv finite +let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = + interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -564,11 +564,11 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite = +let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in - let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum ~poly prv finite in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) @@ -577,3 +577,43 @@ let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite = List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +(* + + HH notes in PR #679: + + The Show Match could also be made more robust, for instance in the + presence of let in the branch of a constructor. A + decompose_prod_assum would probably suffice for that, but then, it + is a Context.Rel.Declaration.t which needs to be matched and not + just a pair (name,type). + + Otherwise, this is OK. After all, the API on inductive types is not + so canonical in general, and in this simple case, working at the + low-level of mind_nf_lc seems reasonable (compared to working at the + higher-level of Inductiveops). + +*) + +let make_cases ind = + let open Declarations in + let mib, mip = Global.lookup_inductive ind in + Util.Array.fold_right_i + (fun i (ctx, _) l -> + let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in + let rec rename avoid = function + | [] -> [] + | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l + | RelDecl.LocalAssum (n, _)::l -> + let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in + Id.to_string n' :: rename (Id.Set.add n' avoid) l in + let al' = rename Id.Set.empty al in + let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in + (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) + mip.mind_nf_lc [] diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index a77cd66a33..97f930c0a1 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -13,7 +13,6 @@ open Entries open Libnames open Vernacexpr open Constrexpr -open Decl_kinds (** {6 Inductive and coinductive types} *) @@ -23,11 +22,16 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -val do_mutual_inductive : - template:bool option -> universe_decl_expr option -> - (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - poly:bool -> private_flag -> uniform:uniform_inductive_flag -> - Declarations.recursivity_kind -> unit +val do_mutual_inductive + : template:bool option + -> universe_decl_expr option + -> (one_inductive_expr * decl_notation list) list + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> uniform:uniform_inductive_flag + -> Declarations.recursivity_kind + -> unit (************************************************************************) (** Internal API *) @@ -71,9 +75,21 @@ val extract_mutual_inductive_declaration_components : structured_inductive_expr * (*coercions:*) qualid list * decl_notation list (** Typing mutual inductive definitions *) - -val interp_mutual_inductive : - template:bool option -> universe_decl_expr option -> structured_inductive_expr -> - decl_notation list -> cumulative_inductive_flag -> - poly:bool -> private_flag -> Declarations.recursivity_kind -> - mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list +val interp_mutual_inductive + : template:bool option + -> universe_decl_expr option + -> structured_inductive_expr + -> decl_notation list + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> Declarations.recursivity_kind + -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : Names.inductive -> string list list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index d804957917..4d663d6b0e 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Decl_kinds open Evarutil open Context.Rel.Declaration open ComFixpoint @@ -204,8 +203,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let name = add_suffix recname "_func" in (* XXX: Mutating the evar_map in the hook! *) (* XXX: Likely the sigma is out of date when the hook is called .... *) - let hook sigma _ _ l gr = - let sigma, h_body = Evarutil.new_global sigma gr in + let hook sigma { DeclareDef.Hook.S.dref; _ } = + let sigma, h_body = Evarutil.new_global sigma dref in let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in @@ -213,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = (*FIXME poly? *) let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in (* FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let c = Declare.declare_constant ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in let gr = ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr impls @@ -222,9 +221,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook sigma _ _ l gr = + let hook sigma { DeclareDef.Hook.S.dref; _ } = if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr impls + Impargs.declare_manual_implicits false dref impls in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) @@ -288,8 +287,8 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> Fixpoint - | DeclareObl.IsCoFixpoint -> CoFixpoint + | DeclareObl.IsFixpoint _ -> Decls.Fixpoint + | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index d74fdcab2c..4dcb3db63b 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Decl_kinds open Declare open Globnames open Impargs @@ -18,19 +17,26 @@ type locality = Discharge | Global of Declare.import_status (* Hooks naturally belong here as they apply to both definitions and lemmas *) module Hook = struct module S = struct - type t = UState.t - -> (Names.Id.t * Constr.t) list - -> locality - -> Names.GlobRef.t - -> unit + type t = + { uctx : UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + ; obls : (Names.Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + ; scope : locality + (** [locality]: Locality of the original declaration *) + ; dref : Names.GlobRef.t + (** [ref]: identifier of the original declaration *) + } end - type t = S.t CEphemeron.key + type t = (S.t -> unit) CEphemeron.key let make hook = CEphemeron.create hook - let call ?hook ?fix_exn uctx trans l c = - try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook + let call ?hook ?fix_exn x = + try Option.iter (fun hook -> CEphemeron.get hook x) hook with e when CErrors.noncritical e -> let e = CErrors.push e in let e = Option.cata (fun fix -> fix e) e fix_exn in @@ -42,10 +48,11 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in let gr = match scope with | Discharge -> - let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in + let _ : Libobject.object_name = + declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) in VarRef name | Global local -> - let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in + let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in let gr = ConstRef kn in let () = Declare.declare_univ_binders gr udecl in gr @@ -55,8 +62,8 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = begin match hook_data with | None -> () - | Some (hook, uctx, extra_defs) -> - Hook.call ~fix_exn ~hook uctx extra_defs scope gr + | Some (hook, uctx, obls) -> + Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref = gr } end; gr diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 3934a29413..606cfade46 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Decl_kinds type locality = Discharge | Global of Declare.import_status @@ -22,29 +21,28 @@ module Hook : sig as a Coercion, perform some cleanup, update the search database, etc... *) module S : sig - (** [S.t] passes to the client: *) - type t - = UState.t + type t = + { uctx : UState.t (** [ustate]: universe constraints obtained when the term was closed *) - -> (Id.t * Constr.t) list + ; obls : (Id.t * Constr.t) list (** [(n1,t1),...(nm,tm)]: association list between obligation name and the corresponding defined term (might be a constant, but also an arbitrary term in the Expand case of obligations) *) - -> locality - (** [locality]: Locality of the original declaration *) - -> GlobRef.t - (** [ref]: identifier of the original declaration *) - -> unit + ; scope : locality + (** [scope]: Locality of the original declaration *) + ; dref : GlobRef.t + (** [dref]: identifier of the original declaration *) + } end - val make : S.t -> t - val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t + val make : (S.t -> unit) -> t + val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit end val declare_definition : name:Id.t -> scope:locality - -> kind:definition_object_kind + -> kind:Decls.definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders -> Evd.side_effects Proof_global.proof_entry @@ -56,7 +54,7 @@ val declare_fix -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> name:Id.t -> scope:locality - -> kind:definition_object_kind + -> kind:Decls.definition_object_kind -> UnivNames.universe_binders -> Entries.universes_entry -> Evd.side_effects Entries.proof_output diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 759e907bc9..a947fa2668 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -14,7 +14,6 @@ open Environ open Context open Constr open Vars -open Decl_kinds open Entries type 'a obligation_body = DefinedObl of 'a | TermObl of constr @@ -50,7 +49,7 @@ type program_info = ; prg_notations : notations ; prg_poly : bool ; prg_scope : DeclareDef.locality - ; prg_kind : definition_object_kind + ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool @@ -167,8 +166,9 @@ let declare_obligation prg obl body ty uctx = in (* ppedrot: seems legit to have obligations as local *) let constant = - Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified - (Declare.DefinitionEntry ce, IsProof Property) + Declare.declare_constant ~name:obl.obl_name + ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property) + (Declare.DefinitionEntry ce) in if not opaque then add_hint (Locality.make_section_locality None) prg constant; @@ -423,7 +423,7 @@ let declare_mutual_definition l = let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in let fixnames = first.prg_deps in let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in + let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> @@ -455,10 +455,10 @@ let declare_mutual_definition l = (Metasyntax.add_notation_interpretation (Global.env ())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls scope gr; + let dref = List.hd kns in + DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; - gr + dref let update_obls prg obls rem = let prg' = {prg with prg_obligations = (obls, rem)} in diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index fae27e1cb3..7433888cec 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -44,7 +44,7 @@ type program_info = ; prg_notations : notations ; prg_poly : bool ; prg_scope : DeclareDef.locality - ; prg_kind : Decl_kinds.definition_object_kind + ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 5c5a4ffbcb..ba1191285a 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -85,8 +85,6 @@ let vernac_interp_error_handler = function str "Tactic failure" ++ (if Pp.ismt s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")." - | AlreadyDeclared msg -> - msg ++ str "." | _ -> raise CErrors.Unhandled diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 94876d2142..5cffa18511 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -55,7 +55,7 @@ GRAMMAR EXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> - { VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) } + { VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) } | IDENT "Proof" -> { VernacProof (None,None) } | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn } | IDENT "Proof"; c = lconstr -> { VernacExactProof c } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74bd552459..2b475f1ef9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -20,7 +20,7 @@ open Impargs open Constrexpr open Constrexpr_ops open Extend -open Decl_kinds +open Decls open Declaremods open Declarations open Namegen diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 9559edbea0..d9b839e857 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -24,7 +24,6 @@ open Declarations open Term open Constr open Inductive -open Decl_kinds open Indrec open Declare open Libnames @@ -100,11 +99,11 @@ let () = (* Util *) -let define ~poly id sigma c t = - let f = declare_constant in +let define ~poly name sigma c t = + let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in let open Proof_global in - let kn = f id + let kn = f ~name (DefinitionEntry { proof_entry_body = c; proof_entry_secctx = None; @@ -113,9 +112,8 @@ let define ~poly id sigma c t = proof_entry_opaque = false; proof_entry_inline_code = false; proof_entry_feedback = None; - }, - Decl_kinds.IsDefinition Scheme) in - definition_message id; + }) in + definition_message name; kn (* Boolean equality *) @@ -161,8 +159,9 @@ let try_declare_scheme what f internal names kn = | UndefinedCst s -> alarm what internal (strbrk "Required constant " ++ str s ++ str " undefined.") - | AlreadyDeclared msg -> - alarm what internal (msg ++ str ".") + | AlreadyDeclared (kind, id) as exn -> + let msg = CErrors.print exn in + alarm what internal msg | DecidabilityMutualNotSupported -> alarm what internal (str "Decidability lemma for mutual inductive types not supported.") diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 31407de4da..d0e2e0f935 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -21,9 +21,6 @@ open Declareops open Entries open Nameops open Globnames -open Decls -open Decl_kinds -open Declare open Pretyping open Termops open Reductionops @@ -75,10 +72,11 @@ module Info = struct (* This could be improved and the CEphemeron removed *) ; other_thms : Recthm.t list ; scope : DeclareDef.locality - ; kind : Decl_kinds.goal_object_kind + ; kind : Decls.logical_kind } - let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () = + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) + ?(kind=Decls.(IsProof Lemma)) () = { hook ; compute_guard = [] ; impargs = [] @@ -121,14 +119,15 @@ let by tac pf = let retrieve_first_recthm uctx = function | VarRef id -> - (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) + NamedDecl.get_value (Global.lookup_named id), + Decls.variable_opacity id | ConstRef cst -> - let cb = Global.lookup_constant cst in - (* we get the right order somehow but surely it could be enforced in a better way *) - let uctx = UState.context uctx in - let inst = Univ.UContext.instance uctx in - let map (c, _, _) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) + let cb = Global.lookup_constant cst in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in + let inst = Univ.UContext.instance uctx in + let map (c, _, _) = Vars.subst_instance_constr inst c in + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function @@ -253,27 +252,27 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = let t_i = norm typ in - let k = IsAssumption Conjectural in + let kind = Decls.(IsAssumption Conjectural) in match body with | None -> let open DeclareDef in (match scope with | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let c = SectionLocalAssum {typ=t_i;univs;poly;impl} in - let _ = declare_variable name (Lib.cwd(),c,k) in - (VarRef name,impargs) + let impl = false in (* copy values from Vernacentries *) + let univs = match univs with + | Polymorphic_entry (_, univs) -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_entry univs -> univs + in + let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let _ = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in + (VarRef name,impargs) | Global local -> - let k = IsAssumption Conjectural in - let decl = (ParameterEntry (None,(t_i,univs),None), k) in - let kn = declare_constant name ~local decl in - (ConstRef kn,impargs)) + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry (None,(t_i,univs),None) in + let kn = Declare.declare_constant ~name ~local ~kind decl in + (ConstRef kn,impargs)) | Some body -> let body = norm body in let rec body_i t = match Constr.kind t with @@ -288,15 +287,13 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i let open DeclareDef in match scope with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = SectionLocalDef const in - let _ = declare_variable name (Lib.cwd(), c, k) in - (VarRef name,impargs) + let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in + let c = Declare.SectionLocalDef const in + let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in + (VarRef name,impargs) | Global local -> - let const = - Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i - in - let kn = declare_constant name ~local (DefinitionEntry const, k) in + let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in + let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in (ConstRef kn,impargs) let initialize_named_context_for_proof () = @@ -304,7 +301,7 @@ let initialize_named_context_for_proof () = List.fold_right (fun d signv -> let id = NamedDecl.get_id d in - let d = if variable_opacity id then NamedDecl.drop_body d else d in + let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val (* Starting a goal *) @@ -421,19 +418,19 @@ let warn_let_as_axiom = (* This declares implicits and calls the hooks for all the theorems, including the main one *) -let process_recthms ?fix_exn ?hook env sigma ctx ~udecl ~poly ~scope ref imps other_thms = +let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ctx ref in - let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in + let body,opaq = retrieve_first_recthm uctx dref in + let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly ctx udecl in + let uctx = UState.check_univ_decl ~poly uctx udecl in List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in - let thms_data = (ref,imps)::other_thms_data in - List.iter (fun (ref,imps) -> - maybe_declare_manual_implicits false ref imps; - DeclareDef.Hook.call ?fix_exn ?hook ctx [] scope ref) thms_data + let thms_data = (dref,imps)::other_thms_data in + List.iter (fun (dref,imps) -> + maybe_declare_manual_implicits false dref imps; + DeclareDef.Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref})) thms_data let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref @@ -446,10 +443,10 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe let open DeclareDef in let local = match scope with | Global local -> local - | Discharge -> warn_let_as_axiom name; ImportNeedQualified + | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified in - let kn = declare_constant name ~local (ParameterEntry pe, IsAssumption Conjectural) in - let () = assumption_message name in + let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in + let () = Declare.assumption_message name in Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms; @@ -497,20 +494,19 @@ let finish_proved env sigma idopt po info = let fix_exn = Future.fix_exn_of const.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in - let k = Kindops.logical_kind_of_goal_kind kind in let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in let open DeclareDef in let r = match scope with | Discharge -> - let c = SectionLocalDef const in - let _ = declare_variable name (Lib.cwd(), c, k) in + let c = Declare.SectionLocalDef const in + let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in let () = if should_suggest then Proof_using.suggest_variable (Global.env ()) name in VarRef name | Global local -> let kn = - declare_constant name ~local (DefinitionEntry const, k) in + Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in @@ -518,7 +514,7 @@ let finish_proved env sigma idopt po info = Declare.declare_univ_binders gr (UState.universe_binders universes); gr in - definition_message name; + Declare.definition_message name; (* This takes care of the implicits and hook for the current constant*) process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms with e when CErrors.noncritical e -> @@ -543,8 +539,9 @@ let finish_derived ~f ~name ~idopt ~entries = (* 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 Proof_global.proof_entry_opaque = false } in - let f_def = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in - let f_kn = Declare.declare_constant f 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 let f_kn_term = mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by @@ -566,21 +563,13 @@ let finish_derived ~f ~name ~idopt ~entries = proof_entry_body = lemma_body; proof_entry_type = Some lemma_type } in - let lemma_def = - Declare.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) - in - let _ : Names.Constant.t = Declare.declare_constant name lemma_def in + let lemma_def = Declare.DefinitionEntry lemma_def in + let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = - let open Decl_kinds in let obls = ref 1 in - let kind = match kind with - | DefinitionBody d -> IsDefinition d - | Proof p -> IsProof p - in let sigma, recobls = CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry -> let id = @@ -589,7 +578,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = | 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 cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in + let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in let sigma, app = Evarutil.new_global sigma (ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index d156954c85..c513f39f2d 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Decl_kinds (** {4 Proofs attached to a constant} *) @@ -68,7 +67,7 @@ module Info : sig (** Info for special constants *) -> ?scope : DeclareDef.locality (** locality *) - -> ?kind:goal_object_kind + -> ?kind:Decls.logical_kind (** Theorem, etc... *) -> unit -> t @@ -101,7 +100,7 @@ val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t -> poly:bool -> scope:DeclareDef.locality - -> kind:goal_object_kind + -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option @@ -116,7 +115,7 @@ val start_lemma_com : program_mode:bool -> poly:bool -> scope:DeclareDef.locality - -> kind:goal_object_kind + -> kind:Decls.logical_kind -> ?inference_hook:Pretyping.inference_hook -> ?hook:DeclareDef.Hook.t -> Vernacexpr.proof_expr list diff --git a/vernac/obligations.ml b/vernac/obligations.ml index b7392a28ca..5d7e1ff9f6 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -9,7 +9,6 @@ (************************************************************************) open Printf -open Decl_kinds (** - Get types of existentials ; @@ -398,8 +397,8 @@ let deps_remaining obls deps = deps [] -let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, DefinitionBody Definition) -let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Proof Lemma) +let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsDefinition Definition)) +let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsProof Lemma)) let kind_of_obligation o = match o with @@ -441,9 +440,9 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_hook prg obl num auto ctx' _ _ gr = +let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = let obls, rem = prg.prg_obligations in - let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in + let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with (true, Evar_kinds.Expand) @@ -638,7 +637,7 @@ let show_term n = ++ Printer.pr_constr_env env sigma prg.prg_body) let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?tactic + ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print name ++ str " has type-checked" in @@ -658,7 +657,7 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) | _ -> res) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic - ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce) + ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in @@ -689,8 +688,8 @@ let admit_prog prg = | None -> let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in - let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified - (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) + let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified + (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 233739ee46..f97bc784c3 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -50,7 +50,7 @@ val add_definition -> ?implicits:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality - -> ?kind:Decl_kinds.definition_object_kind + -> ?kind:Decls.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t @@ -66,7 +66,7 @@ val add_mutual_definitions -> ?tactic:unit Proofview.tactic -> poly:bool -> ?scope:DeclareDef.locality - -> ?kind:Decl_kinds.definition_object_kind + -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool -> DeclareObl.notations diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 4f053b98ae..78112d9dc4 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -16,7 +16,6 @@ open Util open CAst open Extend -open Decl_kinds open Constrexpr open Constrexpr_ops open Vernacexpr @@ -348,18 +347,18 @@ open Pputils let pr_assumption_token many discharge kind = match discharge, kind with - | (NoDischarge,Logical) -> + | (NoDischarge,Decls.Logical) -> keyword (if many then "Axioms" else "Axiom") - | (NoDischarge,Definitional) -> + | (NoDischarge,Decls.Definitional) -> keyword (if many then "Parameters" else "Parameter") - | (NoDischarge,Conjectural) -> str"Conjecture" - | (DoDischarge,Logical) -> + | (NoDischarge,Decls.Conjectural) -> str"Conjecture" + | (DoDischarge,Decls.Logical) -> keyword (if many then "Hypotheses" else "Hypothesis") - | (DoDischarge,Definitional) -> + | (DoDischarge,Decls.Definitional) -> keyword (if many then "Variables" else "Variable") - | (DoDischarge,Conjectural) -> + | (DoDischarge,Decls.Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture.") - | (_,Context) -> + | (_,Decls.Context) -> anomaly (Pp.str "Context is used only internally.") let pr_params pr_c (xl,(c,t)) = @@ -388,7 +387,16 @@ open Pputils prlist_with_sep pr_semicolon (pr_params pr_c) *) - let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) +let string_of_theorem_kind = let open Decls in function + | Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | Corollary -> "Corollary" + + let pr_thm_token k = keyword (string_of_theorem_kind k) let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> @@ -588,6 +596,18 @@ open Pputils with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + +let string_of_definition_object_kind = let open Decls in function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + CErrors.anomaly (Pp.str "Internal definition kind.") + let pr_vernac_expr v = let return = tag_vernac v in let env = Global.env () in @@ -719,7 +739,7 @@ open Pputils keyword ( if Name.is_anonymous (fst id).v then "Goal" - else Kindops.string_of_definition_object_kind dk) + else string_of_definition_object_kind dk) in let pr_reduce = function | None -> mt() diff --git a/vernac/record.ml b/vernac/record.ml index cc4f02349d..fe89303d33 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -24,7 +24,6 @@ open Declarations open Entries open Declare open Constrintern -open Decl_kinds open Type_errors open Constrexpr open Constrexpr_ops @@ -282,7 +281,7 @@ type projection_flags = { } (* We build projections *) -let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields = +let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in @@ -352,8 +351,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f proof_entry_opaque = false; proof_entry_inline_code = false; proof_entry_feedback = None } in - let k = (Declare.DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant fid k in + let kind = Decls.IsDefinition kind in + let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) @@ -402,7 +401,7 @@ let inStruc : Recordops.struc_tuple -> obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = +let declare_structure ~cumulative finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data = let nparams = List.length params in let poly, ctx = match univs with @@ -411,7 +410,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki | Polymorphic_entry (nas, ctx) -> true, Polymorphic_entry (nas, ctx) in - let variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in + let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -480,8 +479,8 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cum ubinders univs id idbuild paramimpls params arity - template fieldimpls fields ?(kind=StructureComponent) coers priorities = +let declare_class def cumulative ubinders univs id idbuild paramimpls params arity + template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) let impls = implicits_of_context params in @@ -497,8 +496,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity let class_type = it_mkProd_or_LetIn arity params in let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in - let cst = Declare.declare_constant id - (DefinitionEntry class_entry, IsDefinition Definition) + let cst = Declare.declare_constant ~name:id + (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) in let inst, univs = match univs with | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs @@ -512,8 +511,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity let proj_body = it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) + let proj_cst = Declare.declare_constant ~name:proj_name + (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; @@ -527,8 +526,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity | _ -> let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in - let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls - params template ~kind:Method ~name:[|binder_name|] record_data + let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls + params template ~kind:Decls.Method ~name:[|binder_name|] record_data in let coers = List.map2 (fun coe pri -> Option.map (fun b -> @@ -680,7 +679,7 @@ let extract_record_data records = (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure udecl kind ~template cum ~poly finite records = +let definition_structure udecl kind ~template ~cumulative ~poly finite records = let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in @@ -696,7 +695,7 @@ let definition_structure udecl kind ~template cum ~poly finite records = in let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in - declare_class def cum ubinders univs id.CAst.v idbuild + declare_class def cumulative ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ [CAst.make None] @ impls in @@ -710,5 +709,5 @@ let definition_structure udecl kind ~template cum ~poly finite records = id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in - let inds = declare_structure ~cum finite ubinders univs implpars params template data in + let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index d0164572f3..571fd9536e 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,7 +22,7 @@ type projection_flags = { val declare_projections : inductive -> Entries.universes_entry -> - ?kind:Decl_kinds.definition_object_kind -> + ?kind:Decls.definition_object_kind -> Id.t -> projection_flags list -> Impargs.manual_implicits list -> @@ -35,7 +35,7 @@ val definition_structure : universe_decl_expr option -> inductive_kind -> template:bool option - -> Decl_kinds.cumulative_inductive_flag + -> cumulative:bool -> poly:bool -> Declarations.recursivity_kind -> (coercion_flag * diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e0183b941e..681605cc31 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -24,14 +24,12 @@ open Goptions open Libnames open Globnames open Vernacexpr -open Decl_kinds open Constrexpr open Redexpr open Lemmas open Locality open Attributes -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (** TODO: make this function independent of Ltac *) @@ -146,59 +144,11 @@ let show_intro ~proof all = else mt () end else mt () -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - a known inductive type. *) - -(* - - HH notes in PR #679: - - The Show Match could also be made more robust, for instance in the - presence of let in the branch of a constructor. A - decompose_prod_assum would probably suffice for that, but then, it - is a Context.Rel.Declaration.t which needs to be matched and not - just a pair (name,type). - - Otherwise, this is OK. After all, the API on inductive types is not - so canonical in general, and in this simple case, working at the - low-level of mind_nf_lc seems reasonable (compared to working at the - higher-level of Inductiveops). - -*) - -let make_cases_aux glob_ref = - let open Declarations in - match glob_ref with - | Globnames.IndRef ind -> - let mib, mip = Global.lookup_inductive ind in - Util.Array.fold_right_i - (fun i (ctx, _) l -> - let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in - let rec rename avoid = function - | [] -> [] - | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l - | RelDecl.LocalAssum (n, _)::l -> - let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in - Id.to_string n' :: rename (Id.Set.add n' avoid) l in - let al' = rename Id.Set.empty al in - let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in - (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) - mip.mind_nf_lc [] - | _ -> raise Not_found - -let make_cases s = - let qualified_name = Libnames.qualid_of_string s in - let glob_ref = Nametab.locate qualified_name in - make_cases_aux glob_ref - (** Textual display of a generic "match" template *) let show_match id = let patterns = - try make_cases_aux (Nametab.global id) + try ComInductive.make_cases (Nametab.global_inductive id) with Not_found -> user_err Pp.(str "Unknown inductive type.") in let pr_branch l = @@ -574,11 +524,11 @@ let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = in start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l -let vernac_definition_hook ~poly = function +let vernac_definition_hook ~poly = let open Decls in function | Coercion -> Some (Class.add_coercion_hook ~poly) | CanonicalStructure -> - Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure)) + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | SubClass -> Some (Class.add_subclass_hook ~poly) | _ -> None @@ -607,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:(DefinitionBody kind) ?hook [(name, pl), (bl, t)] + start_proof_and_print ~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 @@ -630,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:(Proof kind) l + start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> @@ -685,7 +635,7 @@ let should_treat_as_uniform () = else ComInductive.NonUniformParameters let vernac_record ~template udecl cum k poly finite records = - let is_cumulative = should_treat_as_cumulative cum poly in + let cumulative = should_treat_as_cumulative cum poly in let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with | None -> add_prefix "Build_" id.v @@ -706,7 +656,7 @@ let vernac_record ~template udecl cum k poly finite records = coe, id, binders, cfs, const, sort in let records = List.map map records in - ignore(Record.definition_structure ~template udecl k is_cumulative ~poly finite records) + ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records) let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = match indl with @@ -804,9 +754,9 @@ let vernac_inductive ~atts cum lo finite indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let is_cumulative = should_treat_as_cumulative cum poly in + let cumulative = should_treat_as_cumulative cum poly in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl is_cumulative ~poly lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -2339,7 +2289,7 @@ let interp_typed_vernac c ~stack = (* We interpret vernacular commands to a DSL that specifies their allowed actions on proof states *) -let translate_vernac ~atts v = let open Vernacextend in match v with +let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacAbortAll | VernacRestart | VernacUndo _ @@ -2348,8 +2298,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with | VernacResetInitial | VernacBack _ | VernacBackTo _ - | VernacAbort _ - | VernacLoad _ -> + | VernacAbort _ -> anomaly (str "type_vernac") (* Syntax *) | VernacSyntaxExtension (infix, sl) -> @@ -2653,6 +2602,11 @@ let translate_vernac ~atts v = let open Vernacextend in match v with | VernacEndProof pe -> VtCloseProof (vernac_end_proof pe) + | VernacLoad (verbosely,fname) -> + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_load ~verbosely fname) + (* Extensions *) | VernacExtend (opn,args) -> Vernacextend.type_vernac ~atts opn args @@ -2661,7 +2615,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -let rec interp_expr ?proof ~atts ~st c = +and interp_expr ?proof ~atts ~st c = let stack = st.Vernacstate.lemmas in vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with @@ -2681,12 +2635,6 @@ let rec interp_expr ?proof ~atts ~st c = (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - (* Loading a file requires access to the control interpreter so - [vernac_load] is mutually-recursive with [interp_expr] *) - | VernacLoad (verbosely,fname) -> - unsupported_attributes atts; - vernac_load ~verbosely ~st fname - | v -> let fv = translate_vernac ~atts v in interp_typed_vernac ~stack fv @@ -2696,13 +2644,10 @@ let rec interp_expr ?proof ~atts ~st c = the classifier. The proper fix is to move it to the STM, however, the way the proof mode is set there makes the task non trivial without a considerable amount of refactoring. - *) -and vernac_load ~verbosely ~st fname = - let there_are_pending_proofs ~stack = not Option.(is_empty stack) in - let stack = st.Vernacstate.lemmas in - if there_are_pending_proofs ~stack then - CErrors.user_err Pp.(str "Load is not supported inside proofs."); - (* Open the file *) +*) +and vernac_load ~verbosely fname = + (* Note that no proof should be open here, so the state here is just token for now *) + let st = Vernacstate.freeze_interp_state ~marshallable:false in let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in @@ -2713,10 +2658,10 @@ and vernac_load ~verbosely ~st fname = (* Parsing loop *) let v_mod = if verbosely then Flags.verbosely else Flags.silently in let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing - (fun po -> - match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with - | Some x -> x - | None -> raise End_of_input) in + (fun po -> + match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with + | Some x -> x + | None -> raise End_of_input) in let rec load_loop ~stack = try let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in @@ -2728,15 +2673,18 @@ and vernac_load ~verbosely ~st fname = End_of_input -> stack in - let stack = load_loop ~stack in + let stack = load_loop ~stack:st.Vernacstate.lemmas in (* If Load left a proof open, we fail too. *) - if there_are_pending_proofs ~stack then + if Option.has_some stack then CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - stack + () and interp_control ?proof ~st v = match v with | { v=VernacExpr (atts, cmd) } -> - interp_expr ?proof ~atts ~st cmd + let before_univs = Global.universes () in + let pstack = interp_expr ?proof ~atts ~st cmd in + if before_univs == Global.universes () then pstack + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack | { v=VernacFail v } -> with_fail ~st (fun () -> interp_control ?proof ~st v); st.Vernacstate.lemmas diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 3563e9984a..e618cdcefe 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,17 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit - -(** Default proof mode set by `start_proof` *) -val get_default_proof_mode : unit -> Pvernac.proof_mode - -val proof_mode_opt_name : string list - -(** Vernacular entries *) -val vernac_require : - Libnames.qualid option -> bool option -> Libnames.qualid list -> unit - (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t @@ -32,22 +21,25 @@ val interp_qed_delayed_proof -> Vernacexpr.proof_end -> Vernacstate.t -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - a known inductive type. *) - -val make_cases : string -> string list list - (** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit -val command_focus : unit Proof.focus_kind +(** Flag set when the test-suite is called. Its only effect to display + verbose information for [Fail] *) +val test_mode : bool ref + +(** Vernacular require command *) +val vernac_require : + Libnames.qualid option -> bool option -> Libnames.qualid list -> unit +(** Hook to dissappear when #8240 is fixed *) val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t -(* Flag set when the test-suite is called. Its only effect to display - verbose information for `Fail` *) -val test_mode : bool ref +(** Miscellaneous stuff *) +val command_focus : unit Proof.focus_kind + +(** Default proof mode set by `start_proof` *) +val get_default_proof_mode : unit -> Pvernac.proof_mode + +val proof_mode_opt_name : string list diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index dc5df5904e..ee1f839b8d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -276,13 +276,13 @@ type nonrec vernac_expr = | VernacDeclareCustomEntry of string (* Gallina *) - | VernacDefinition of (discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr - | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list + | VernacDefinition of (discharge * Decls.definition_object_kind) * name_decl * definition_expr + | VernacStartTheoremProof of Decls.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (discharge * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list |