diff options
92 files changed, 1807 insertions, 788 deletions
diff --git a/coq-doc.opam b/coq-doc.opam index 2f4072955f..67cdbd8bf0 100644 --- a/coq-doc.opam +++ b/coq-doc.opam @@ -1,3 +1,6 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" synopsis: "The Coq Proof Assistant --- Reference Manual" description: """ Coq is a formal proof management system. It provides @@ -5,37 +8,29 @@ a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. -This package provides the Coq Reference Manual. -""" -opam-version: "2.0" -maintainer: "The Coq development team <coqdev@inria.fr>" -authors: "The Coq development team, INRIA, CNRS, and contributors." +This package provides the Coq Reference Manual.""" +maintainer: ["The Coq development team <coqdev@inria.fr>"] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "OPL-1.0" homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" -license: "Open Publication License" - -version: "dev" - depends: [ - "dune" { build } - "coq" { build & = version } + "dune" {build & >= "2.5.0"} + "coq" {build & = version} ] - -build-env: [ - [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] -] - build: [ - [ "dune" "build" "-p" name "-j" jobs ] -] - -# Would be better to have a *-conf package? -depexts: [ - [ "sphinx" ] - [ "sphinx_rtd_theme" ] - [ "beautifulsoup4" ] - [ "antlr4-python3-runtime"] - [ "pexpect" ] - [ "sphinxcontrib-bibtex" ] + ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] ] +dev-repo: "git+https://github.com/coq/coq.git" @@ -1,33 +1,45 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" synopsis: "The Coq Proof Assistant" description: """ Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for -semi-interactive development of machine-checked proofs. Typical -applications include the certification of properties of programming -languages (e.g. the CompCert compiler certification project, or the -Bedrock verified low-level programming library), the formalization of -mathematics (e.g. the full formalization of the Feit-Thompson theorem -or homotopy type theory) and teaching. -""" -opam-version: "2.0" -maintainer: "The Coq development team <coqdev@inria.fr>" -authors: "The Coq development team, INRIA, CNRS, and contributors." +semi-interactive development of machine-checked proofs. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching.""" +maintainer: ["The Coq development team <coqdev@inria.fr>"] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "git+https://github.com/coq/coq.git" -license: "LGPL-2.1" - -version: "dev" - depends: [ - "ocaml" { >= "4.05.0" } - "dune" { >= "2.5.0" } - "ocamlfind" { build } - "zarith" { >= "1.10" } + "ocaml" {>= "4.05.0"} + "dune" {>= "2.5.0"} + "ocamlfind" {>= "1.8.1"} + "zarith" {>= "1.10"} ] - build: [ - [ "./configure" "-prefix" prefix "-native-compiler" "no" ] - [ "dune" "build" "-p" name "-j" jobs ] + ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] ] diff --git a/coq.opam.template b/coq.opam.template new file mode 100644 index 0000000000..c0efccdc0f --- /dev/null +++ b/coq.opam.template @@ -0,0 +1,3 @@ +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] diff --git a/coqide-server.opam b/coqide-server.opam index 4cec409f78..101cd4ad78 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -1,4 +1,7 @@ -synopsis: "The Coq Proof Assistant" +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +synopsis: "The Coq Proof Assistant, XML protocol server" description: """ Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable @@ -8,21 +11,29 @@ semi-interactive development of machine-checked proofs. This package provides the `coqidetop` language server, an implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md) which allows clients, such as CoqIDE, to interact with Coq in a -structured way. -""" -opam-version: "2.0" -maintainer: "The Coq development team <coqdev@inria.fr>" -authors: "The Coq development team, INRIA, CNRS, and contributors." +structured way.""" +maintainer: ["The Coq development team <coqdev@inria.fr>"] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "git+https://github.com/coq/coq.git" -license: "LGPL-2.1" - -version: "dev" - depends: [ - "dune" { >= "2.0.0" } - "coq" { = version } + "dune" {>= "2.5.0"} + "coq" {= version} ] - -build: [ [ "dune" "build" "-p" name "-j" jobs ] ] +build: [ + ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" diff --git a/coqide.opam b/coqide.opam index 54b8dca98b..3007200fe5 100644 --- a/coqide.opam +++ b/coqide.opam @@ -1,4 +1,7 @@ -synopsis: "The Coq Proof Assistant" +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +synopsis: "The Coq Proof Assistant --- GTK3 IDE" description: """ Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable @@ -6,26 +9,29 @@ algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. This package provides the CoqIDE, a graphical user interface for the -development of interactive proofs. -""" -opam-version: "2.0" -maintainer: "The Coq development team <coqdev@inria.fr>" -authors: "The Coq development team, INRIA, CNRS, and contributors." +development of interactive proofs.""" +maintainer: ["The Coq development team <coqdev@inria.fr>"] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "git+https://github.com/coq/coq.git" -license: "LGPL-2.1" - -version: "dev" - depends: [ - "dune" { >= "2.0.0" } - "coqide-server" { = version } - "lablgtk3" { >= "3.0.beta5" } - "lablgtk3-sourceview3" { >= "3.0.beta5" } + "dune" {>= "2.5.0"} + "coqide-server" {= version} ] - -build-env: [ - [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +build: [ + ["dune" "subst"] {pinned} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] ] -build: [ [ "dune" "build" "-p" name "-j" jobs ] ] +dev-repo: "git+https://github.com/coq/coq.git" diff --git a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh new file mode 100644 index 0000000000..b7d21ed59c --- /dev/null +++ b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then + + elpi_CI_REF=record+refactor + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +# mtac2_CI_REF=record+refactor +# mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 8b0bf216e3..de3d5a3d15 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -175,6 +175,12 @@ local copy of Coq. For this purpose, Dune supports the `-p` option, so version of Coq libs, and use a "release" profile that for example enables stronger compiler optimizations. +## OPAM file generation + +`.opam` files are automatically generated by Dune from the package +descriptions in the `dune-project` file; see Dune's manual for more +details. + ## Stanzas `dune` files contain the so-called "stanzas", that may declare: diff --git a/doc/changelog/01-kernel/13356-primarray-cumul.rst b/doc/changelog/01-kernel/13356-primarray-cumul.rst new file mode 100644 index 0000000000..978ca325bf --- /dev/null +++ b/doc/changelog/01-kernel/13356-primarray-cumul.rst @@ -0,0 +1,5 @@ +- **Changed:** Primitive arrays are now irrelevant in their single + polymorphic universe (same as a polymorphic cumulative list + inductive would be) (`#13356 + <https://github.com/coq/coq/pull/13356>`_, fixes `#13354 + <https://github.com/coq/coq/issues/13354>`_, by GaĆ«tan Gilbert). diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst new file mode 100644 index 0000000000..6a431f85ed --- /dev/null +++ b/doc/changelog/02-specification-language/13188-instance-gen.rst @@ -0,0 +1,6 @@ +- **Removed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. + Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 + <https://github.com/coq/coq/issues/6042>`_, by GaĆ«tan Gilbert). diff --git a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst new file mode 100644 index 0000000000..bf792fda6d --- /dev/null +++ b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst @@ -0,0 +1,6 @@ +- **Added:** + Inference of return predicate of a :g:`match` by inversion takes + sort elimination constraints into account + (`#13290 <https://github.com/coq/coq/pull/13290>`_, + grants `#13278 <https://github.com/coq/coq/issues/13278>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst new file mode 100644 index 0000000000..5758f35c3d --- /dev/null +++ b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst @@ -0,0 +1,5 @@ +- **Fixed:** + A case of unification raising an anomaly IllTypedInstance + (`#13376 <https://github.com/coq/coq/pull/13376>`_, + fixes `#13266 <https://github.com/coq/coq/issues/13266>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst b/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst new file mode 100644 index 0000000000..c0e5a81641 --- /dev/null +++ b/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly + (`#13383 <https://github.com/coq/coq/pull/13383>`_, + fixes `#11816 <https://github.com/coq/coq/issues/11816>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst new file mode 100644 index 0000000000..eaf049dc97 --- /dev/null +++ b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst @@ -0,0 +1,6 @@ +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 <https://github.com/coq/coq/pull/13387>`_, + fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst new file mode 100644 index 0000000000..048835a0e9 --- /dev/null +++ b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst @@ -0,0 +1,6 @@ +- **Changed:** + Scope information is propagated in indirect applications to a + reference prefixed with :g:`@@`; this covers for instance the case + :g:`r.(@@p) t` where scope information from :g:`p` is now taken into + account for interpreting :g:`t` (`#12685 + <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst new file mode 100644 index 0000000000..a51f96d0a2 --- /dev/null +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -0,0 +1,6 @@ +- **Deprecated:** + Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``. + Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``; + replacement TBD. + (`#13381 <https://github.com/coq/coq/pull/13381>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst new file mode 100644 index 0000000000..1c7c3102a3 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 <https://github.com/coq/coq/pull/12516>`_, + by Maxime DĆ©nĆØs). diff --git a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst new file mode 100644 index 0000000000..9ae759be56 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst @@ -0,0 +1,5 @@ +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 <https://github.com/coq/coq/pull/13339>`_, + by ThĆ©o Zimmermann). diff --git a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst new file mode 100644 index 0000000000..df2bdfeabb --- /dev/null +++ b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst @@ -0,0 +1,6 @@ +- **Changed:** + The :attr:`export` locality can now be used for all Hint commands, + including Hint Cut, Hint Mode, Hint Transparent / Opaque and + Remove Hints + (`#13388 <https://github.com/coq/coq/pull/13388>`_, + by Pierre-Marie PĆ©drot). diff --git a/doc/changelog/10-standard-library/12420-decidable.rst b/doc/changelog/10-standard-library/12420-decidable.rst new file mode 100644 index 0000000000..6a4da91fa3 --- /dev/null +++ b/doc/changelog/10-standard-library/12420-decidable.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Decidable`` instance for negation + (`#12420 <https://github.com/coq/coq/pull/12420>`_, + by Yishuai Li). diff --git a/doc/changelog/10-standard-library/13365-axiom-free-wf.rst b/doc/changelog/10-standard-library/13365-axiom-free-wf.rst new file mode 100644 index 0000000000..1fc40894eb --- /dev/null +++ b/doc/changelog/10-standard-library/13365-axiom-free-wf.rst @@ -0,0 +1,4 @@ +- **Fixed:** + `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. + (`#13365 <https://github.com/coq/coq/pull/13365>`_, + by Li-yao Xia). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index cdd31fcb86..2474c784b8 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -336,20 +336,23 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info hint_info + .. insertprodn hint_info one_pattern .. prodn:: - hint_info ::= %| {? @natural } {? @one_term } + hint_info ::= %| {? @natural } {? @one_pattern } + one_pattern ::= @one_term Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of the class. - Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info` - specifies the hint priority, where 0 is the highest priority as for + Adds one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info` + may be used to specify the hint priority, where 0 is the highest priority as for :tacn:`auto` hints. If the priority is not specified, the default is the number - of non-dependent binders of the instance. + of non-dependent binders of the instance. If :token:`one_pattern` is given, terms + matching that pattern will trigger use of the instance. Otherwise, + use is triggered based on the conclusion of the type. This command supports the :attr:`global` attribute that can be used on instances declared in a section so that their @@ -388,6 +391,16 @@ Summary of the commands equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. + .. flag:: Instance Generalized Output + + .. deprecated:: 8.13 + + Disabled by default, this provides compatibility with Coq + version 8.12 and earlier. + + When enabled, the type of the instance is implicitly generalized + over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``. + .. cmd:: Print Instances @reference Shows the list of instances associated with the typeclass :token:`reference`. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 4ea3ea5e6d..79489c85f6 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -13,15 +13,18 @@ Let-in definitions .. prodn:: term_let ::= let @name {? : @type } := @term in @term | let @name {+ @binder } {? : @type } := @term in @term - | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term - | let ' @pattern := @term {? return @term100 } in @term - | let ' @pattern in @pattern := @term return @term100 in @term - -:n:`let @ident := @term in @termā` -denotes the local binding of :n:`@term` to the variable -:n:`@ident` in :n:`@term`ā. There is a syntactic sugar for let-in -definition of functions: :n:`let @ident {+ @binder} := @term in @termā` -stands for :n:`let @ident := fun {+ @binder} => @term in @termā`. + | @destructuring_let + +:n:`let @ident := @term__1 in @term__2` represents the local binding of +the variable :n:`@ident` to the value :n:`@term__1` in :n:`@term__2`. + +:n:`let @ident {+ @binder} := @term__1 in @term__2` is an abbreviation +for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`. + +.. seealso:: + + Extensions of the `let ... in ...` syntax are described in + :ref:`irrefutable-patterns`. .. index:: single: ... : ... (type cast) diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 23389eba3b..8e62c2af13 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -86,6 +86,13 @@ Pattern-matching on terms inhabiting inductive type having only one constructor can be alternatively written using :g:`let ā¦ in ā¦` constructions. There are two variants of them. +.. insertprodn destructuring_let destructuring_let + +.. prodn:: + destructuring_let ::= let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term + | let ' @pattern := @term {? return @term100 } in @term + | let ' @pattern in @pattern := @term return @term100 in @term + First destructuring let syntax ++++++++++++++++++++++++++++++ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7baf193266..86d1d25745 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -133,7 +133,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. prodn:: search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key } - | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term + | {? {| head | hyp | concl | headhyp | headconcl } : } @one_pattern | is : @logical_kind Searched objects can be filtered by patterns, by the constants they @@ -141,9 +141,9 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). names. The location of the pattern or constant within a term - :n:`@one_term` + :n:`@one_pattern` Search for objects whose type contains a subterm matching the - pattern :n:`@one_term`. Holes of the pattern are indicated by + pattern :n:`@one_pattern`. Holes of the pattern are indicated by `_` or :n:`?@ident`. If the same :n:`?@ident` occurs more than once in the pattern, all occurrences in the subterm must be identical. See :ref:`this example <search-pattern>`. @@ -312,7 +312,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Search is:Instance [ Reflexive | Symmetric ]. -.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } } .. deprecated:: 8.12 @@ -320,8 +320,8 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term` - matches a subterm of `C` in head position. For example, a :n:`@one_term` of `f _ b` + form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern` + matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b` matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -337,12 +337,12 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchHead le. SearchHead (@eq bool). -.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern - :n:`@one_term`. + :n:`@one_pattern`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -362,11 +362,11 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchPattern (?X1 + _ = _ + ?X1). -.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchRewrite @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the form - :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term` + :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_pattern` matches either `LHS` or `RHS`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index e6dc6f6c51..485b92342d 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -280,9 +280,7 @@ automatically created. sections. + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. This attribute is only effective for - the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and - :cmd:`Hint Extern` variants of the command. + module. Requiring it is not enough. + :attr:`global` hints are made available by merely requiring the current module. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index fd8a0329d6..40d032543f 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -288,12 +288,18 @@ Name a set of section hypotheses for ``Proof using`` existential variables remain. To instantiate existential variables during proof edition, you should use the tactic :tacn:`instantiate`. + .. deprecated:: 8.13 + .. cmd:: Grab Existential Variables This command can be run when a proof has no more goal to be solved but has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. + .. deprecated:: 8.13 + + Use :cmd:`Unshelve` instead. + Proof modes ``````````` diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index 7ab8f9d763..b68b2ed2a7 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -200,6 +200,14 @@ at the beginning of a line. if n <= 1 then 1 else n * fact (n-1) >> +Verbatim material on a single line is also possible (assuming that +``>>`` is not part of the text to be presented as verbatim). + +.. example:: + + :: + + Here is the corresponding caml expression: << fact (n-1) >> Hyperlinks diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4ad32e15eb..4c1956d172 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -285,9 +285,12 @@ term_let: [ (* Don't need to document that "( )" is equivalent to "()" *) | REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 | WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200 +| MOVETO destructuring_let "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200 | REPLACE "let" "'" pattern200 ":=" term200 "in" term200 -| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 +| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 | DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200 +| MOVETO destructuring_let "let" "'" pattern200 ":=" term200 OPT case_type "in" term200 +| MOVETO destructuring_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 ] atomic_constr: [ @@ -2478,7 +2481,6 @@ SPLICE: [ | binders | casted_constr | check_module_types -| constr_pattern | decl_sep | function_fix_definition (* loses funind annotation *) | glob @@ -2652,6 +2654,7 @@ RENAME: [ | ssrfwd ssrdefbody | ssrclauses ssr_in | ssrcpat ssrblockpat +| constr_pattern one_pattern ] simple_tactic: [ diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 2a7b283f55..1c07d00d4f 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -12,7 +12,6 @@ (glob_files %{project_root}/parsing/*.mlg) (glob_files %{project_root}/toplevel/*.mlg) (glob_files %{project_root}/vernac/*.mlg) - ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) (glob_files %{project_root}/plugins/btauto/*.mlg) (glob_files %{project_root}/plugins/cc/*.mlg) (glob_files %{project_root}/plugins/derive/*.mlg) @@ -23,8 +22,11 @@ (glob_files %{project_root}/plugins/micromega/*.mlg) (glob_files %{project_root}/plugins/nsatz/*.mlg) (glob_files %{project_root}/plugins/omega/*.mlg) - (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/ring/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/ssr/*.mlg) + (glob_files %{project_root}/plugins/ssrmatching/*.mlg) + (glob_files %{project_root}/plugins/ssrsearch/*.mlg) (glob_files %{project_root}/plugins/syntax/*.mlg) (glob_files %{project_root}/user-contrib/Ltac2/*.mlg) ; Sphinx files diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index a787d769fb..033ece04de 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1623,6 +1623,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "dfs" "eauto" OPT int_or_var auto_using hintbases +| "bfs" "eauto" OPT int_or_var auto_using hintbases | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" hyp | "autounfold_one" hintbases diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c697043f27..e6fc6188b7 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -473,6 +473,10 @@ ssr_dpat: [ term_let: [ | "let" name OPT ( ":" type ) ":=" term "in" term | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term +| destructuring_let +] + +destructuring_let: [ | "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term | "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term @@ -724,7 +728,11 @@ sort_family: [ ] hint_info: [ -| "|" OPT natural OPT one_term +| "|" OPT natural OPT one_pattern +] + +one_pattern: [ +| one_term ] module_binder: [ @@ -1011,7 +1019,7 @@ command: [ | "Prenex" "Implicits" LIST1 qualid (* SSR plugin *) | "Print" "Hint" "View" OPT ssrviewpos (* SSR plugin *) | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) ) (* SSR plugin *) -| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *) +| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_pattern ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural @@ -1107,9 +1115,9 @@ command: [ | "Compute" term | "Check" term | "About" reference OPT univ_name_list -| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body ) | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def ) @@ -1167,7 +1175,7 @@ search_query: [ search_item: [ | OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key ) -| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term +| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_pattern | "is" ":" logical_kind ] @@ -1196,7 +1204,7 @@ hint: [ | "Mode" qualid LIST1 [ "+" | "!" | "-" ] | "Unfold" LIST1 qualid | "Constructors" LIST1 qualid -| "Extern" natural OPT one_term "=>" ltac_expr +| "Extern" natural OPT one_pattern "=>" ltac_expr ] tacdef_body: [ @@ -1746,6 +1754,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases | "autounfold" OPT hintbases OPT clause_dft_concl | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) @@ -2404,9 +2413,9 @@ tac2mode: [ | "Compute" term | "Check" term | "About" reference OPT univ_name_list -| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) ] diff --git a/dune-project b/dune-project index 873d03e8dd..1265c993b7 100644 --- a/dune-project +++ b/dune-project @@ -5,6 +5,79 @@ (formatting (enabled_for ocaml)) -; TODO -; -; (generate_opam_files true) +(generate_opam_files true) + +(license LGPL-2.1-only) +(maintainers "The Coq development team <coqdev@inria.fr>") +(authors "The Coq development team, INRIA, CNRS, and contributors") +; This generates bug-reports and dev-repo +(source (github coq/coq)) +(homepage https://coq.inria.fr/) +(documentation "https://coq.github.io/doc/") +(version dev) + +; Note that we use coq.opam.template to have dune add the correct opam +; prefix for configure +(package + (name coq) + (depends + (ocaml (>= 4.05.0)) + (dune (>= 2.5.0)) + (ocamlfind (>= 1.8.1)) + (zarith (>= 1.10))) + (synopsis "The Coq Proof Assistant") + (description "Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching.")) + +(package + (name coqide-server) + (depends + (dune (>= 2.5.0)) + (coq (= :version))) + (synopsis "The Coq Proof Assistant, XML protocol server") + (description "Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the `coqidetop` language server, an +implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md) +which allows clients, such as CoqIDE, to interact with Coq in a +structured way.")) + +(package + (name coqide) + (depends + (dune (>= 2.5.0)) + (coqide-server (= :version))) + (synopsis "The Coq Proof Assistant --- GTK3 IDE") + (description "Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the CoqIDE, a graphical user interface for the +development of interactive proofs.")) + +(package + (name coq-doc) + (license "OPL-1.0") + (depends + (dune (and :build (>= 2.5.0))) + (coq (and :build (= :version)))) + (synopsis "The Coq Proof Assistant --- Reference Manual") + (description "Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the Coq Reference Manual.")) + diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 0c84dee572..c29de27efb 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -452,6 +452,9 @@ let eq_universes env sigma cstrs cv_pb refargs l l' = let open GlobRef in let open UnivProblem in match refargs with + | Some (ConstRef c, 1) when Environ.is_array_type env c -> + cstrs := compare_cumulative_instances cv_pb true [|Univ.Variance.Irrelevant|] l l' !cstrs; + true | None | Some (ConstRef _, _) -> cstrs := enforce_eq_instances_univs true l l' !cstrs; true | Some (VarRef _, _) -> assert false (* variables don't have instances *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 771571fd3f..ba6a9ea6d9 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -371,7 +371,8 @@ let push_rel_decl_to_named_context let subst = update_var id0 id subst in let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = replace_var_named_declaration id0 id nc in - (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc) + let avoid = Id.Set.add id (Id.Set.add id0 avoid) in + (push_var id0 subst, avoid, push_named_context_val d nc) | Some id0 when hypnaming = FailIfConflict -> user_err Pp.(Id.print id0 ++ str " is already used.") | _ -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 06cf19b4f7..02c3c047d5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1972,9 +1972,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let env = restart_lambda_binders env in let idl_temp = Array.map (fun (id,recarg,bl,ty,_) -> - let recarg = Option.map (function { CAst.v = v } -> match v with + let recarg = Option.map (function { CAst.v = v; loc } -> match v with | CStructRec i -> i - | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg + | _ -> user_err ?loc Pp.(str "Well-founded induction requires Program Fixpoint or Function.")) recarg in let before, after = split_at_annot bl recarg in let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in @@ -2092,9 +2092,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = assert (Option.is_empty isproj); let c = intern_notation intern env ntnvars loc ntn ntnargs in find_appl_head_data c, args - | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in - apply_impargs c env impargs args_scopes - args loc + | _ -> + assert (Option.is_empty isproj); + let f = intern_no_implicit env f in + let f, _, args_scopes = find_appl_head_data f in + (f,[],args_scopes), args + in + apply_impargs c env impargs args_scopes args loc | CRecord fs -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 174125fc57..17feeb9b5a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1098,14 +1098,8 @@ module FNativeEntries = let defined_array = ref false - let farray = ref dummy - let init_array retro = - match retro.Retroknowledge.retro_array with - | Some c -> - defined_array := true; - farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } - | None -> defined_array := false + defined_array := Option.has_some retro.Retroknowledge.retro_array let init env = current_retro := env.retroknowledge; diff --git a/kernel/environ.ml b/kernel/environ.ml index 914c951eb6..69edb1498c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) @@ -569,6 +568,11 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let is_array_type env c = + match env.retroknowledge.Retroknowledge.retro_array with + | None -> false + | Some c' -> Constant.CanOrd.equal c c' + let polymorphic_constant cst env = Declareops.constant_is_polymorphic (lookup_constant cst env) diff --git a/kernel/environ.mli b/kernel/environ.mli index 60696184ef..6a8ddce835 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -37,7 +37,6 @@ val dummy_lazy_val : unit -> lazy_val (** Linking information for the native compiler *) type link_info = | Linked of string - | LinkedInteractive of string | NotLinked type key = int CEphemeron.key option ref @@ -250,6 +249,8 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option val is_primitive : env -> Constant.t -> bool +val is_array_type : env -> Constant.t -> bool + (** {6 Primitive projections} *) (** Checks that the number of parameters is correct. *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 911a879394..09db29d222 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1933,7 +1933,7 @@ and compile_named env sigma univ auxdefs id = | LocalAssum _ -> Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs -let compile_constant env sigma prefix ~interactive con cb = +let compile_constant env sigma con cb = let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in begin match cb.const_body with | Def t -> @@ -1942,10 +1942,6 @@ let compile_constant env sigma prefix ~interactive con cb = if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in - let name = - if interactive then LinkedInteractive prefix - else Linked prefix - in let l = Constant.label con in let auxdefs,code = if no_univs then compile_with_fv env sigma None [] (Some l) code @@ -1959,7 +1955,7 @@ let compile_constant env sigma prefix ~interactive con cb = optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); - code, name + code | _ -> let i = push_symbol (SymbConst con) in let args = @@ -1969,9 +1965,7 @@ let compile_constant env sigma prefix ~interactive con cb = (* let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const) *) - [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)], - if interactive then LinkedInteractive prefix - else Linked prefix + [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)] end module StringOrd = struct type t = string let compare = String.compare end @@ -1984,12 +1978,9 @@ let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = loaded_native_files := StringSet.add s !loaded_native_files -let is_code_loaded ~interactive name = +let is_code_loaded name = match !name with | NotLinked -> false - | LinkedInteractive s -> - if (interactive && is_loaded_native_file s) then true - else (name := NotLinked; false) | Linked s -> if is_loaded_native_file s then true else (name := NotLinked; false) @@ -2049,8 +2040,11 @@ let compile_mind mb mind stack = in Array.fold_left_i f stack mb.mind_packets -type code_location_update = - link_info ref * link_info +type code_location_update = { + upd_info : link_info ref; + upd_prefix : string; +} + type code_location_updates = code_location_update Mindmap_env.t * code_location_update Cmap_env.t @@ -2058,35 +2052,34 @@ type linkable_code = global list * code_location_updates let empty_updates = Mindmap_env.empty, Cmap_env.empty -let compile_mind_deps env prefix ~interactive +let compile_mind_deps env prefix (comp_stack, (mind_updates, const_updates) as init) mind = let mib,nameref = lookup_mind_key mind env in - if is_code_loaded ~interactive nameref + if is_code_loaded nameref || Mindmap_env.mem mind mind_updates then init else let comp_stack = compile_mind mib mind comp_stack in - let name = - if interactive then LinkedInteractive prefix - else Linked prefix - in - let upd = (nameref, name) in + let upd = { + upd_info = nameref; + upd_prefix = prefix; + } in let mind_updates = Mindmap_env.add mind upd mind_updates in (comp_stack, (mind_updates, const_updates)) (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) -let compile_deps env sigma prefix ~interactive init t = +let compile_deps env sigma prefix init t = let rec aux env lvl init t = match kind t with - | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind + | Ind ((mind,_),_u) -> compile_mind_deps env prefix init mind | Const c -> let c,_u = get_alias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in - if is_code_loaded ~interactive nameref + if is_code_loaded nameref || (Cmap_env.mem c const_updates) then init else @@ -2096,19 +2089,21 @@ let compile_deps env sigma prefix ~interactive init t = aux env lvl init (Mod_subst.force_constr t) | _ -> init in - let code, name = - compile_constant env sigma prefix ~interactive c cb - in + let code = compile_constant env sigma c cb in + let upd = { + upd_info = nameref; + upd_prefix = prefix; + } in let comp_stack = code@comp_stack in - let const_updates = Cmap_env.add c (nameref, name) const_updates in + let const_updates = Cmap_env.add c upd const_updates in comp_stack, (mind_updates, const_updates) - | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind + | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix init mind | Proj (p,c) -> - let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in + let init = compile_mind_deps env prefix init (Projection.mind p) in aux env lvl init c | Case (ci, _p, _iv, _c, _ac) -> let mind = fst ci.ci_ind in - let init = compile_mind_deps env prefix ~interactive init mind in + let init = compile_mind_deps env prefix init mind in fold_constr_with_binders succ (aux env) lvl init t | Var id -> let open Context.Named.Declaration in @@ -2130,11 +2125,8 @@ let compile_deps env sigma prefix ~interactive init t = in aux env 0 init t -let compile_constant_field env prefix con acc cb = - let (gl, _) = - compile_constant ~interactive:false env empty_evars prefix - con cb - in +let compile_constant_field env _prefix con acc cb = + let gl = compile_constant env empty_evars con cb in gl@acc let compile_mind_field mp l acc mb = @@ -2152,11 +2144,11 @@ let mk_conv_code env sigma prefix t1 t2 = clear_global_tbl (); let gl, (mind_updates, const_updates) = let init = ([], empty_updates) in - compile_deps env sigma prefix ~interactive:true init t1 + compile_deps env sigma prefix init t1 in let gl, (mind_updates, const_updates) = let init = (gl, (mind_updates, const_updates)) in - compile_deps env sigma prefix ~interactive:true init t2 + compile_deps env sigma prefix init t2 in let code1 = lambda_of_constr env sigma t1 in let code2 = lambda_of_constr env sigma t2 in @@ -2179,7 +2171,7 @@ let mk_norm_code env sigma prefix t = clear_global_tbl (); let gl, (mind_updates, const_updates) = let init = ([], empty_updates) in - compile_deps env sigma prefix ~interactive:true init t + compile_deps env sigma prefix init t in let code = lambda_of_constr env sigma t in let (gl,code) = compile_with_fv env sigma None gl None code in @@ -2196,7 +2188,8 @@ let mk_library_header (symbols : Nativevalues.symbols) = let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))] -let update_location (r,v) = r := v +let update_location r = + r.upd_info := Linked r.upd_prefix let update_locations (ind_updates,const_updates) = Mindmap_env.iter (fun _ -> update_location) ind_updates; diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 913b3843c2..aab6e1d4a0 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -50,7 +50,6 @@ val get_proj : symbols -> int -> inductive * int val get_symbols : unit -> symbols -type code_location_update type code_location_updates type linkable_code = global list * code_location_updates diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index e98e97907a..18f16f427d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -111,14 +111,12 @@ let get_mind_prefix env mind = match !name with | NotLinked -> "" | Linked s -> s - | LinkedInteractive s -> s let get_const_prefix env c = let _,(nameref,_) = lookup_constant_key c env in match !nameref with | NotLinked -> "" | Linked s -> s - | LinkedInteractive s -> s (* A generic map function *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c891b885c4..cf40263f61 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -280,11 +280,12 @@ let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances ctor nargs u1 u2 s, check -let conv_table_key infos k1 k2 cuniv = +let conv_table_key infos ~nargs k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' -> if Univ.Instance.equal u u' then cuniv + else if Int.equal nargs 1 && is_array_type (info_env infos) cst then cuniv else let flex = evaluable_constant cst (info_env infos) && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) @@ -304,6 +305,11 @@ let unfold_ref_with_args infos tab fl v = Some (a, (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) | Undef _ | OpaqueDef _ | Primitive _ -> None +let same_args_size sk1 sk2 = + let n = CClosure.stack_args_size sk1 in + if Int.equal n (CClosure.stack_args_size sk2) then n + else raise NotConvertible + type conv_tab = { cnv_inf : clos_infos; lft_tab : clos_tab; @@ -408,7 +414,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try - let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in + let nargs = same_args_size v1 v2 in + let cuniv = conv_table_key infos.cnv_inf ~nargs fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in @@ -577,17 +584,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in - let nargs = CClosure.stack_args_size v1 in - if not (Int.equal nargs (CClosure.stack_args_size v2)) - then raise NotConvertible - else - match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with - | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - | exception MustExpand -> - let env = info_env infos.cnv_inf in - let hd1 = eta_expand_ind env pind1 in - let hd2 = eta_expand_ind env pind2 in - eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv + let nargs = same_args_size v1 v2 in + match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with + | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + | exception MustExpand -> + let env = info_env infos.cnv_inf in + let hd1 = eta_expand_ind env pind1 in + let hd2 = eta_expand_ind env pind2 in + eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) -> @@ -597,17 +601,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in - let nargs = CClosure.stack_args_size v1 in - if not (Int.equal nargs (CClosure.stack_args_size v2)) - then raise NotConvertible - else - match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with - | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - | exception MustExpand -> - let env = info_env infos.cnv_inf in - let hd1 = eta_expand_constructor env pctor1 in - let hd2 = eta_expand_constructor env pctor2 in - eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv + let nargs = same_args_size v1 v2 in + match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with + | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + | exception MustExpand -> + let env = info_env infos.cnv_inf in + let hd1 = eta_expand_constructor env pctor1 in + let hd2 = eta_expand_constructor env pctor2 in + eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv else raise NotConvertible (* Eta expansion of records *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 44472a1995..7e8400910c 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -116,12 +116,25 @@ END let make_depth n = snd (Eauto.make_dimension n None) +(* deprecated in 8.13; the second int_or_var will be removed *) +let deprecated_eauto_bfs = + CWarnings.create + ~name:"eauto_bfs" ~category:"deprecated" + (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.") + +let deprecated_bfs tacname = + CWarnings.create + ~name:"eauto_bfs" ~category:"deprecated" + (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.") + } TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () ); + Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND new_eauto @@ -135,13 +148,17 @@ END TACTIC EXTEND debug_eauto | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () ); + Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND info_eauto | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () ); + Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND dfs_eauto @@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db } END +TACTIC EXTEND bfs_eauto +| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db } +END + TACTIC EXTEND autounfold | [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl } END @@ -240,10 +263,21 @@ ARGUMENT EXTEND opthints END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF -| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in - Hints.add_hints ~locality - (match dbnames with None -> ["core"] | Some l -> l) entry; +| #[ locality = Attributes.option_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { + let open Goptions in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + let () = match locality with + | OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); + | OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); + | OptDefault | OptLocal -> () + in + Hints.add_hints ~locality + (match dbnames with None -> ["core"] | Some l -> l) entry; } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index c54f8ffa78..c2e95c45f9 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -329,11 +329,11 @@ GRAMMAR EXTEND Gram ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] -> + l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] -> { Vernacexpr.VernacProof (Some (in_tac ta), l) } - | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] -> - { Vernacexpr.VernacProof (ta,Some l) } ] ] + | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr; + "with"; ta = Pltac.tactic -> + { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ] ; hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5de0745d17..a793e217d4 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1784,25 +1784,24 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = !evdref, ans let build_tycon ?loc env tycon_env s subst tycon extenv sigma t = - let sigma, t, tt = match t with + let s = mkSort s in + match t with | None -> (* This is the situation we are building a return predicate and we are in an impossible branch *) let n = Context.Rel.length (rel_context !!env) in let n' = Context.Rel.length (rel_context !!tycon_env) in - let sigma, (impossible_case_type, u) = - Evarutil.new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) - sigma univ_flexible_alg - in - (sigma, lift (n'-n) impossible_case_type, mkSort u) + let src = Loc.tag ?loc Evar_kinds.ImpossibleCase in + let sigma, impossible_case_type = + Evarutil.new_evar (reset_context !!env) sigma ~src ~typeclass_candidate:false s in + (sigma, { uj_val = lift (n'-n) impossible_case_type; uj_type = s }) | Some t -> let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in let sigma, tt = Typing.type_of !!extenv sigma t in - (sigma, t, tt) in - match unify_leq_delay !!env sigma tt (mkSort s) with - | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type."); - | sigma -> - sigma, { uj_val = t; uj_type = tt } + match unify_leq_delay !!env sigma tt s with + | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type."); + | sigma -> (sigma, { uj_val = t; uj_type = tt }) + (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1915,9 +1914,24 @@ let build_inversion_problem ~program_mode loc env sigma tms t = it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) - let s' = Retyping.get_sort_of !!env sigma t in - let sigma, s = Evd.new_sort_variable univ_flexible sigma in - let sigma = Evd.set_leq_sort !!env sigma s' s in + let s = Retyping.get_sort_of !!env sigma t in + let sigma, s = Sorts.(match s with + | SProp | Prop | Set -> + (* To anticipate a possible restriction on an elimination from + SProp, Prop or (impredicative) Set we preserve the sort of the + main branch, knowing that the default impossible case shall + always be coercible to one of those *) + sigma, s + | Type _ -> + (* If the sort has algebraic universes, we cannot use this sort a + type constraint for the impossible case; especially if the + default case is not the canonical one provided in Prop by Coq + but one given by the user, which may be in either sort (an + example is in Vector.caseS', even if this one can probably be + put in Prop too with some care) *) + let sigma, s' = Evd.new_sort_variable univ_flexible sigma in + let sigma = Evd.set_leq_sort !!env sigma s s' in + sigma, s') in let pb = { env = pb_env; pred = (*ty *) mkSort s; @@ -2066,6 +2080,15 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars Some (sigma', p, arsign) with e when precatchable_exception e -> None +let expected_elimination_sort env tomatchl = + List.fold_right (fun (_,tm) s -> + match tm with + | IsInd (_,IndType(indf,_),_) -> + (* Not a degenerated line, see coerce_to_indtype *) + let s' = Inductive.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in + if Sorts.family_leq s s' then s else s' + | NotInd _ -> s) tomatchl Sorts.InType + (* Builds the predicate. If the predicate is dependent, its context is * made of 1+nrealargs assumptions for each matched term in an inductive * type and 1 assumption for each term not _syntactically_ in an @@ -2116,8 +2139,12 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty | Some rtntyp -> (* We extract the signature of the arity *) let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in - let sigma, newt = new_sort_variable univ_flexible sigma in - let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in + (* We put a type constraint on the predicate so that one + branch type-checked first does not lead to a lower type than + another branch; we take into account the possible elimination + constraints on the predicate *) + let sigma, rtnsort = fresh_sort_in_family sigma (expected_elimination_sort !!env tomatchs) in + let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl, building_arsign] in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 90af143a2d..cbf539c1e9 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -567,8 +567,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with | Const (c, u), Const (c', u') when QConstant.equal env c c' -> - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - check_strict evd u u' + if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c + then + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u' + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + check_strict evd u u' | Const _, Const _ -> UnifFailure (evd, NotSameHead) | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' -> if EInstance.is_empty u && EInstance.is_empty u' then Success evd @@ -1312,6 +1317,7 @@ let check_selected_occs env sigma c occ occs = raise (PretypeError (env,sigma,NoOccurrenceFound (c,None))) else () +(* Error local to the module *) exception TypingFailed of evar_map let set_of_evctx l = @@ -1342,12 +1348,6 @@ let thin_evars env sigma sign c = let c' = applyrec (env,0) c in (!sigma, c') -exception NotFoundInstance of exn -let () = CErrors.register_handler (function - | NotFoundInstance e -> - Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e) - | _ -> None) - let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in @@ -1490,9 +1490,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> instantiate_evar evar_unify flags env_rhs evd ev vid | _ -> evd) - with e when CErrors.noncritical e -> - let e, info = Exninfo.capture e in - Exninfo.iraise (NotFoundInstance e, info) + with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ -> + user_err (Pp.str "Cannot find an instance.") else ((if debug_ho_unification () then let evi = Evd.find evd evk in @@ -1709,7 +1708,7 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in let flags = default_flags env in - instantiate_evar evar_unify flags env evd' evk ty + instantiate_evar evar_unify flags env evd' evk ty (* should we protect from raising IllTypedInstance? *) | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 715b80f428..c58ebe1bbd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -810,7 +810,8 @@ let check_evar_instance unify flags env evd evk1 body = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) + with Retyping.RetypeError _ -> + let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance")) in match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd @@ -1575,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs match EConstr.kind !evdref t with | Rel i when i>k -> let open Context.Rel.Declaration in - (match Environ.lookup_rel (i-k) env' with + (match Environ.lookup_rel i env' with | LocalAssum _ -> project_variable (RelAlias (i-k)) | LocalDef (_,b,_) -> try project_variable (RelAlias (i-k)) diff --git a/proofs/proof.ml b/proofs/proof.ml index d864aed25a..24f3ac3f29 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -409,14 +409,28 @@ module V82 = struct let top_evars p = Proofview.V82.top_evars p.entry p.proofview + let warn_deprecated_grab_existentials = + CWarnings.create ~name:"deprecated-grab-existentials" ~category:"deprecated" + Pp.(fun () -> str "The Grab Existential Variables command is " ++ + str"deprecated. Please use the Unshelve command or the unshelve tactical " ++ + str"instead.") + let grab_evars p = + warn_deprecated_grab_existentials (); if not (is_done p) then raise (OpenProof(None, UnfinishedProof)) else { p with proofview = Proofview.V82.grab p.proofview } + let warn_deprecated_existential = + CWarnings.create ~name:"deprecated-existential" ~category:"deprecated" + Pp.(fun () -> str "The Existential command is " ++ + str"deprecated. Please use the Unshelve command or the unshelve " ++ + str"tactical, and the instantiate tactic instead.") + (* Main component of vernac command Existential *) let instantiate_evar env n intern pr = + warn_deprecated_existential (); let tac = Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> let (evk, evi) = diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 5fb038a767..f40bbc813e 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -30,4 +30,5 @@ val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic +val make_depth : int option -> int val make_dimension : int option -> int option -> bool * int diff --git a/tactics/hints.ml b/tactics/hints.ml index 68229dbe26..6fab111e6f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1023,11 +1023,15 @@ let remove_hint dbname grs = type hint_action = | CreateDB of bool * TransparentState.t - | AddTransparency of evaluable_global_reference hints_transparency_target * bool + | AddTransparency of { + superglobal : bool; + grefs : evaluable_global_reference hints_transparency_target; + state : bool; + } | AddHints of { superglobal : bool; hints : hint_entry list } - | RemoveHints of GlobRef.t list - | AddCut of hints_path - | AddMode of GlobRef.t * hint_mode array + | RemoveHints of { superglobal : bool; hints : GlobRef.t list } + | AddCut of { superglobal : bool; paths : hints_path } + | AddMode of { superglobal : bool; gref : GlobRef.t; mode : hint_mode array } let add_cut dbname path = let db = get_db dbname in @@ -1049,12 +1053,16 @@ let load_autohint _ (kn, h) = let name = h.hint_name in match h.hint_action with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b) - | AddTransparency (grs, b) -> add_transparency name grs b + | AddTransparency { superglobal; grefs; state } -> + if superglobal then add_transparency name grefs state | AddHints { superglobal; hints } -> if superglobal then add_hint name hints - | RemoveHints grs -> remove_hint name grs - | AddCut path -> add_cut name path - | AddMode (l, m) -> add_mode name l m + | RemoveHints { superglobal; hints } -> + if superglobal then remove_hint name hints + | AddCut { superglobal; paths } -> + if superglobal then add_cut name paths + | AddMode { superglobal; gref; mode } -> + if superglobal then add_mode name gref mode let open_autohint i (kn, h) = if Int.equal i 1 then match h.hint_action with @@ -1067,7 +1075,15 @@ let open_autohint i (kn, h) = in let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in List.iter add hints - | _ -> () + | AddCut { superglobal; paths } -> + if not superglobal then add_cut h.hint_name paths + | AddTransparency { superglobal; grefs; state } -> + if not superglobal then add_transparency h.hint_name grefs state + | RemoveHints { superglobal; hints } -> + if not superglobal then remove_hint h.hint_name hints + | AddMode { superglobal; gref; mode } -> + if not superglobal then add_mode h.hint_name gref mode + | CreateDB _ -> () let cache_autohint (kn, obj) = load_autohint 1 (kn, obj); open_autohint 1 (kn, obj) @@ -1124,7 +1140,7 @@ let subst_autohint (subst, obj) = in let action = match obj.hint_action with | CreateDB _ -> obj.hint_action - | AddTransparency (target, b) -> + | AddTransparency { superglobal; grefs = target; state = b } -> let target' = match target with | HintsVariables -> target @@ -1134,19 +1150,19 @@ let subst_autohint (subst, obj) = if grs == grs' then target else HintsReferences grs' in - if target' == target then obj.hint_action else AddTransparency (target', b) + if target' == target then obj.hint_action else AddTransparency { superglobal; grefs = target'; state = b } | AddHints { superglobal; hints } -> let hints' = List.Smart.map subst_hint hints in if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' } - | RemoveHints grs -> + | RemoveHints { superglobal; hints = grs } -> let grs' = List.Smart.map (subst_global_reference subst) grs in - if grs == grs' then obj.hint_action else RemoveHints grs' - | AddCut path -> + if grs == grs' then obj.hint_action else RemoveHints { superglobal; hints = grs' } + | AddCut { superglobal; paths = path } -> let path' = subst_hints_path subst path in - if path' == path then obj.hint_action else AddCut path' - | AddMode (l,m) -> + if path' == path then obj.hint_action else AddCut { superglobal; paths = path' } + | AddMode { superglobal; gref = l; mode = m } -> let l' = subst_global_reference subst l in - if l' == l then obj.hint_action else AddMode (l', m) + if l' == l then obj.hint_action else AddMode { superglobal; gref = l'; mode = m } in if action == obj.hint_action then obj else { obj with hint_action = action } @@ -1173,11 +1189,17 @@ let create_hint_db l n st b = let hint = make_hint ~local:l n (CreateDB (b, st)) in Lib.add_anonymous_leaf (inAutoHint hint) -let remove_hints local dbnames grs = +let interp_locality = function +| Goptions.OptDefault | Goptions.OptGlobal -> false, true +| Goptions.OptExport -> false, false +| Goptions.OptLocal -> true, false + +let remove_hints ~locality dbnames grs = + let local, superglobal = interp_locality locality in let dbnames = if List.is_empty dbnames then ["core"] else dbnames in List.iter (fun dbname -> - let hint = make_hint ~local dbname (RemoveHints grs) in + let hint = make_hint ~local dbname (RemoveHints { superglobal; hints = grs }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1185,11 +1207,6 @@ let remove_hints local dbnames grs = (* The "Hint" vernacular command *) (**************************************************************************) -let check_no_export ~local ~superglobal () = - (* TODO: implement export for these entries *) - if not local && not superglobal then - CErrors.user_err Pp.(str "This command does not support the \"export\" attribute") - let add_resolves env sigma clist ~local ~superglobal dbnames = List.iter (fun dbname -> @@ -1229,27 +1246,24 @@ let add_unfolds l ~local ~superglobal dbnames = dbnames let add_cuts l ~local ~superglobal dbnames = - let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddCut l) in + let hint = make_hint ~local dbname (AddCut { superglobal; paths = l }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_mode l m ~local ~superglobal dbnames = - let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let m' = make_mode l m in - let hint = make_hint ~local dbname (AddMode (l, m')) in + let hint = make_hint ~local dbname (AddMode { superglobal; gref = l; mode = m' }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames let add_transparency l b ~local ~superglobal dbnames = - let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddTransparency (l, b)) in + let hint = make_hint ~local dbname (AddTransparency { superglobal; grefs = l; state = b }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1326,11 +1340,7 @@ let prepare_hint check env init (sigma,c) = (c', diff) let add_hints ~locality dbnames h = - let local, superglobal = match locality with - | Goptions.OptDefault | Goptions.OptGlobal -> false, true - | Goptions.OptExport -> false, false - | Goptions.OptLocal -> true, false - in + let local, superglobal = interp_locality locality in if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); assert (not (List.is_empty dbnames)); diff --git a/tactics/hints.mli b/tactics/hints.mli index 3d4d9c7970..54f4716652 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -189,7 +189,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit -val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit +val remove_hints : locality:Goptions.option_locality -> hint_db_name list -> GlobRef.t list -> unit val current_db_names : unit -> String.Set.t diff --git a/test-suite/bugs/closed/bug_11816.v b/test-suite/bugs/closed/bug_11816.v new file mode 100644 index 0000000000..82a317b250 --- /dev/null +++ b/test-suite/bugs/closed/bug_11816.v @@ -0,0 +1,2 @@ +(* This should be an error, not an anomaly *) +Fail Definition foo := fix foo (n : nat) { wf n n } := 0. diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v new file mode 100644 index 0000000000..93ba6f17e0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12348.v @@ -0,0 +1,11 @@ +(* Was raising an anomaly before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := _ in + (fun n : nat => 0 : X) : _. + +(* Was raising an ill-typed instance error before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := true in + (fun n : nat => 0 : X) : _. diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v new file mode 100644 index 0000000000..9831a4d205 --- /dev/null +++ b/test-suite/bugs/closed/bug_13278.v @@ -0,0 +1,15 @@ +Inductive even: nat -> Prop := +| evenB: even 0 +| evenS: forall n, even n -> even (S (S n)). + +Goal even 1 -> False. +Proof. + refine (fun a => match a with end). +Qed. + +Goal even 1 -> False. +Proof. + refine (fun a => match a in even n + return match n with 1 => False | _ => True end : Prop + with evenB => I | evenS _ _ => I end). +Qed. diff --git a/test-suite/bugs/closed/bug_13348.v b/test-suite/bugs/closed/bug_13348.v new file mode 100644 index 0000000000..d3d5d3e5b4 --- /dev/null +++ b/test-suite/bugs/closed/bug_13348.v @@ -0,0 +1,10 @@ +Generalizable All Variables. + +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Arguments populate {_} _. + +Set Mangle Names. +Axioms _0 _1 _2 : Prop. + +Instance impl_inhabited {A} {B} {_3:Inhabited B} : Inhabited (A -> B) + := populate (fun _ => inhabitant). diff --git a/test-suite/bugs/closed/bug_13354.v b/test-suite/bugs/closed/bug_13354.v new file mode 100644 index 0000000000..fbda10a9d2 --- /dev/null +++ b/test-suite/bugs/closed/bug_13354.v @@ -0,0 +1,10 @@ + +Primitive array := #array_type. + +Definition testArray : array nat := [| 1; 2; 4 | 0 : nat |]. + +Definition on_array {A:Type} (x:array A) : Prop := True. + +Check on_array testArray. + +Check @on_array nat testArray. diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v index 462a615d91..f3a19c2b89 100644 --- a/test-suite/bugs/closed/bug_3513.v +++ b/test-suite/bugs/closed/bug_3513.v @@ -13,7 +13,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v index d667022e68..2d4d7d02cc 100644 --- a/test-suite/bugs/closed/bug_4095.v +++ b/test-suite/bugs/closed/bug_4095.v @@ -15,7 +15,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v new file mode 100644 index 0000000000..72f612560b --- /dev/null +++ b/test-suite/bugs/closed/bug_6042.v @@ -0,0 +1,7 @@ +Class C (n: nat) := T{x:True}. +Generalizable All Variables. + +Fail Instance i : C n. + +Instance i : `(C n). +Proof. repeat constructor. Defined. diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out index 2b5648aee6..aceccc25fd 100644 --- a/test-suite/coqdoc/binder.tex.out +++ b/test-suite/coqdoc/binder.tex.out @@ -20,7 +20,8 @@ \begin{coqdoccode} \end{coqdoccode} -Link binders \begin{coqdoccode} +Link binders +\begin{coqdoccode} \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out index d7eba096fc..a8f4c254cb 100644 --- a/test-suite/coqdoc/bug12742.tex.out +++ b/test-suite/coqdoc/bug12742.tex.out @@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx xxxxx xxxx xxxxxx. \end{itemize} + \begin{coqdoccode} \end{coqdoccode} \end{document} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 286e8bba4d..84214a73d3 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -22,8 +22,7 @@ </div> <div class="doc"> -<pre>foo (* bar *) </pre> - +<code> foo (* {bar_bar} *) </code> </div> <div class="code"> <span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/> @@ -32,8 +31,7 @@ </div> <div class="doc"> -<pre>more (* nested (* comments *) within verbatim *) </pre> - +<code> more (* nested (* comments *) within verbatim *) </code> </div> <div class="code"> <span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/> diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 1a1af5dfdd..f2b12f0079 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -20,14 +20,14 @@ \begin{coqdoccode} \end{coqdoccode} -\begin{verbatim}foo (* bar *) \end{verbatim} - \begin{coqdoccode} +\texttt{ foo (* \{bar\_bar\} *) } +\begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol \coqdocemptyline \end{coqdoccode} -\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} - \begin{coqdoccode} +\texttt{ more (* nested (* comments *) within verbatim *) } +\begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol \end{coqdoccode} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v index 839034a48f..fc985276af 100644 --- a/test-suite/coqdoc/bug5700.v +++ b/test-suite/coqdoc/bug5700.v @@ -1,4 +1,4 @@ -(** << foo (* bar *) >> *) +(** << foo (* {bar_bar} *) >> *) Definition const1 := 1. (** << more (* nested (* comments *) within verbatim *) >> *) diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 2304f5ecc1..412a9ca6ac 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -36,6 +36,7 @@ Various checks for coqdoc \item ``..'' should be rendered correctly \end{itemize} + \begin{coqdoccode} \coqdocemptyline \coqdocnoindent @@ -166,7 +167,8 @@ skip skip - skip \begin{coqdoccode} + skip +\begin{coqdoccode} \coqdocemptyline \end{coqdoccode} \end{document} diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out new file mode 100644 index 0000000000..bf9f975ee8 --- /dev/null +++ b/test-suite/coqdoc/verbatim.html.out @@ -0,0 +1,114 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.verbatim</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.verbatim</h1> + +<div class="code"> +</div> + +<div class="doc"> + +<div class="paragraph"> </div> + +<pre> +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +</pre> + +<div class="paragraph"> </div> + +This line and the following shows <code>verbatim </code> text: + +<div class="paragraph"> </div> + +<code> A stand-alone inline verbatim </code> + +<div class="paragraph"> </div> + +<code> A non-ended inline verbatim to test line location +</code> + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> item 1 + +</li> +<li> item 2 is <code>verbatim</code> + +</li> +<li> item 3 is <code>verbatim</code> too +<br/> +<span class="inlinecode"><span class="id" title="var">A</span> <span class="id" title="var">coq</span> <span class="id" title="var">block</span> : <span class="id" title="keyword">ā</span> <span class="id" title="var">n</span>, <span class="id" title="var">n</span> = 0 +<div class="paragraph"> </div> + +</span> +</li> +<li> <code>verbatim</code> again, and a formula <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">True</span></span> <span class="inlinecode">ā</span> <span class="inlinecode"><span class="id" title="var">False</span></span> <span class="inlinecode"></span> + +</li> +<li> +<pre> +multiline +verbatim +</pre> + +</li> +<li> last item + +</li> +</ul> + +<div class="paragraph"> </div> + +<center><table class="infrule"> +<tr class="infruleassumption"> + <td class="infrule">Ī ā¢ A</td> + <td class="infrulenamecol" rowspan="3"> + + </td></tr> +<tr class="infrulemiddle"> + <td class="infrule"><hr /></td> +</tr> +<tr class="infruleassumption"> + <td class="infrule">Ī ā¢ A āØ B</td> + <td></td> +</td> +</table></center> +<div class="paragraph"> </div> + +<pre> +A non-ended block verbatim to test line location + +*) +</pre> +</div> +<div class="code"> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out new file mode 100644 index 0000000000..b692f6ad6a --- /dev/null +++ b/test-suite/coqdoc/verbatim.tex.out @@ -0,0 +1,84 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.verbatim}{Library }{Coqdoc.verbatim} + +\begin{coqdoccode} +\end{coqdoccode} + + +\begin{verbatim} +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +\end{verbatim} + + +This line and the following shows \texttt{verbatim } text: + + +\texttt{ A stand-alone inline verbatim } + + +\texttt{ A non-ended inline verbatim to test line location +} + + + +\begin{itemize} +\item item 1 + +\item item 2 is \texttt{verbatim} + +\item item 3 is \texttt{verbatim} too +\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0 + +\coqdocemptyline + +\item \texttt{verbatim} again, and a formula \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} + +\item +\begin{verbatim} +multiline +verbatim +\end{verbatim} + +\item last item + +\end{itemize} + + +\begin{verbatim} +Ī ā¢ A +---- +Ī ā¢ A āØ B +\end{verbatim} + + +\begin{verbatim} +A non-ended block verbatim to test line location + +*) +\end{verbatim} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v new file mode 100644 index 0000000000..129a5117c9 --- /dev/null +++ b/test-suite/coqdoc/verbatim.v @@ -0,0 +1,40 @@ +(** + +<< +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +>> + +This line and the following shows << verbatim >> text: + +<< A stand-alone inline verbatim >> + +<< A non-ended inline verbatim to test line location + + +- item 1 +- item 2 is <<verbatim>> +- item 3 is <<verbatim>> too +[[ +A coq block : forall n, n = 0 +]] +- <<verbatim>> again, and a formula [ True -> False ] +- +<< +multiline +verbatim +>> +- last item + +[[[ +Ī ā¢ A +---- +Ī ā¢ A āØ B +]]] + +<< +A non-ended block verbatim to test line location + +*) diff --git a/test-suite/output/HintLocality.out b/test-suite/output/HintLocality.out new file mode 100644 index 0000000000..37a0613b25 --- /dev/null +++ b/test-suite/output/HintLocality.out @@ -0,0 +1,92 @@ +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v new file mode 100644 index 0000000000..4481335907 --- /dev/null +++ b/test-suite/output/HintLocality.v @@ -0,0 +1,72 @@ +(** Test hint command locality w.r.t. modules *) + +Create HintDb foodb. +Create HintDb bardb. +Create HintDb quxdb. + +#[global] Hint Immediate O : foodb. +#[global] Hint Immediate O : bardb. +#[global] Hint Immediate O : quxdb. + +Module Test. + +#[global] Hint Cut [ _ ] : foodb. +#[global] Hint Mode S ! : foodb. +#[global] Hint Opaque id : foodb. +#[global] Remove Hints O : foodb. + +#[local] Hint Cut [ _ ] : bardb. +#[local] Hint Mode S ! : bardb. +#[local] Hint Opaque id : bardb. +#[local] Remove Hints O : bardb. + +#[export] Hint Cut [ _ ] : quxdb. +#[export] Hint Mode S ! : quxdb. +#[export] Hint Opaque id : quxdb. +#[export] Remove Hints O : quxdb. + +(** All three agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +End Test. + +(** bardb and quxdb agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +Import Test. + +(** foodb and quxdb agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +(** Test hint command locality w.r.t. sections *) + +Create HintDb secdb. + +#[global] Hint Immediate O : secdb. + +Section Sec. + +Fail #[global] Hint Cut [ _ ] : secdb. +Fail #[global] Hint Mode S ! : secdb. +Fail #[global] Hint Opaque id : secdb. +Fail #[global] Remove Hints O : secdb. + +#[local] Hint Cut [ _ ] : secdb. +#[local] Hint Mode S ! : secdb. +#[local] Hint Opaque id : secdb. +#[local] Remove Hints O : secdb. + +Print HintDb secdb. + +End Sec. + +Print HintDb secdb. diff --git a/test-suite/output/bug_13266.out b/test-suite/output/bug_13266.out new file mode 100644 index 0000000000..034830f1ac --- /dev/null +++ b/test-suite/output/bug_13266.out @@ -0,0 +1,12 @@ +The command has indeed failed with message: +Abstracting over the terms "S", "p" and "u" leads to a term +fun (S0 : Type) (p0 : proc S0) (_ : S0) => p0 = Tick -> True +which is ill-typed. +Reason is: Illegal application: +The term "@eq" of type "forall A : Type, A -> A -> Prop" +cannot be applied to the terms + "proc S0" : "Prop" + "p0" : "proc S0" + "Tick" : "proc unit" +The 3rd term has type "proc unit" which should be coercible to +"proc S0". diff --git a/test-suite/output/bug_13266.v b/test-suite/output/bug_13266.v new file mode 100644 index 0000000000..e59455a326 --- /dev/null +++ b/test-suite/output/bug_13266.v @@ -0,0 +1,18 @@ +Inductive proc : Type -> Type := +| Tick : proc unit +. + +Inductive exec : + forall T, proc T -> T -> Prop := +| ExecTick : + exec _ (Tick) tt +. + +Lemma foo : + exec _ Tick tt -> + True. +Proof. + intros H. + remember Tick as p. + Fail induction H. +Abort. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 382c252727..fb8bbfd043 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -51,8 +51,8 @@ Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ Notation c3 x := ((@pair') _ x). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *) Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *) -Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *) -Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end. +Check c3 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with c3 0 y 0 => 2 | _ => 1 end. (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) (* unless an atomic @ is given *) diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 06697af901..8b7d239dcd 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -26,3 +26,15 @@ Definition c := Īµ : U. Goal True. assert (nat * nat). Abort. + +(* Check propagation of scopes in indirect applications to references *) + +Module PropagateIndirect. +Notation "0" := true : bool_scope. + +Axiom f : bool -> bool -> nat. +Check (@f 0) 0. + +Record R := { p : bool -> nat }. +Check fun r => r.(@p) 0. +End PropagateIndirect. diff --git a/test-suite/success/proof_using_noinit.v b/test-suite/success/proof_using_noinit.v new file mode 100644 index 0000000000..f99b49619c --- /dev/null +++ b/test-suite/success/proof_using_noinit.v @@ -0,0 +1,9 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) + +Section A. +Variable A : Prop. +Hypothesis a : A. +Lemma b : A. +Proof using a. +Admitted. +End A. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 9a3a1d3709..aae24e0e0a 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -1,4 +1,4 @@ -(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *) +(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.CMorphisms") -*- *) (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) @@ -308,7 +308,7 @@ Section GenericInstances. Global Program Instance trans_contra_inv_impl_type_morphism - `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3. + `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -318,7 +318,7 @@ Section GenericInstances. Global Program Instance trans_co_impl_type_morphism - `(Transitive A R) : Proper (R ++> arrow) (R x) | 3. + `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -328,7 +328,7 @@ Section GenericInstances. Global Program Instance trans_sym_co_inv_impl_type_morphism - `(PER A R) : Proper (R ++> flip arrow) (R x) | 3. + `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -337,7 +337,7 @@ Section GenericInstances. Qed. Global Program Instance trans_sym_contra_arrow_morphism - `(PER A R) : Proper (R --> arrow) (R x) | 3. + `(PER A R) {x} : Proper (R --> arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -346,7 +346,7 @@ Section GenericInstances. Qed. Global Program Instance per_partial_app_type_morphism - `(PER A R) : Proper (R ==> iffT) (R x) | 2. + `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2. Next Obligation. Proof with auto. @@ -399,17 +399,17 @@ Section GenericInstances. (** Coq functions are morphisms for Leibniz equality, applied only if really needed. *) - Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') : + Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') {A} : Reflexive (@Logic.eq A ==> R'). Proof. simpl_crelation. Qed. (** [respectful] is a morphism for crelation equivalence . *) - Global Instance respectful_morphism : + Global Instance respectful_morphism {A B} : Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - intros A B R R' HRR' S S' HSS' f g. + intros R R' HRR' S S' HSS' f g. unfold respectful , relation_equivalence in *; simpl in *. split ; intros H x y Hxy. - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). @@ -511,9 +511,9 @@ Ltac partial_application_tactic := (** Bootstrap !!! *) -Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A). +Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A). Proof. - intros A R R' HRR' x y <-. red in HRR'. + intros R R' HRR' x y <-. red in HRR'. split ; red ; intros. - now apply (fst (HRR' _ _)). - now apply (snd (HRR' _ _)). diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 94fcd55aa5..7169aa673d 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -65,6 +65,16 @@ Tactic Notation "decide" constr(P) := Require Import Bool Arith ZArith. +Program Instance Decidable_not {P} `{Decidable P} : Decidable (~ P) := { + Decidable_witness := negb Decidable_witness +}. +Next Obligation. + split; intro Heq. + - apply negb_true_iff in Heq. + eapply Decidable_complete_alt; intuition. + - erewrite Decidable_sound_alt; intuition. +Qed. + Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { Decidable_witness := Bool.eqb x y }. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index c70e3fe478..867d9cb9b3 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *) +(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.Morphisms") -*- *) (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) @@ -309,7 +309,7 @@ Section GenericInstances. Global Program Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Proper (R --> flip impl) (R x) | 3. + `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3. Next Obligation. Proof with auto. @@ -319,7 +319,7 @@ Section GenericInstances. Global Program Instance trans_co_impl_morphism - `(Transitive A R) : Proper (R ++> impl) (R x) | 3. + `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -329,7 +329,7 @@ Section GenericInstances. Global Program Instance trans_sym_co_inv_impl_morphism - `(PER A R) : Proper (R ++> flip impl) (R x) | 3. + `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3. Next Obligation. Proof with auto. @@ -338,7 +338,7 @@ Section GenericInstances. Qed. Global Program Instance trans_sym_contra_impl_morphism - `(PER A R) : Proper (R --> impl) (R x) | 3. + `(PER A R) {x} : Proper (R --> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -347,7 +347,7 @@ Section GenericInstances. Qed. Global Program Instance per_partial_app_morphism - `(PER A R) : Proper (R ==> iff) (R x) | 2. + `(PER A R) {x} : Proper (R ==> iff) (R x) | 2. Next Obligation. Proof with auto. @@ -520,9 +520,9 @@ Ltac partial_application_tactic := (** Bootstrap !!! *) -Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). +Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). Proof. - intros A x y H y0 y1 e; destruct e. + intros x y H y0 y1 e; destruct e. reduce in H. split ; red ; intros H0. - setoid_rewrite <- H. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index a168a8e7cd..964786d8e6 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -22,11 +22,11 @@ Generalizable Variables A l. (** Morphisms for relations *) -Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==> +Instance relation_conjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_conjunction. Proof. firstorder. Qed. -Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> +Instance relation_disjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_disjunction. Proof. firstorder. Qed. @@ -43,11 +43,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed. (** The instantiation at relation allows rewriting applications of relations [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) -Instance relation_equivalence_pointwise : +Instance relation_equivalence_pointwise {A} : Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed. -Instance subrelation_pointwise : +Instance subrelation_pointwise {A} : Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id. Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 5381e91997..401d7007e2 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -395,7 +395,7 @@ Notation "āā„ā" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) -Program Instance predicate_equivalence_equivalence : +Program Instance predicate_equivalence_equivalence {l} : Equivalence (@predicate_equivalence l). Next Obligation. @@ -413,7 +413,7 @@ Program Instance predicate_equivalence_equivalence : firstorder. Qed. -Program Instance predicate_implication_preorder : +Program Instance predicate_implication_preorder {l} : PreOrder (@predicate_implication l). Next Obligation. intro l; induction l ; firstorder. @@ -480,7 +480,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and relation equivalence. *) -Program Instance subrelation_partial_order : +Program Instance subrelation_partial_order {A} : PartialOrder (@relation_equivalence A) subrelation. Next Obligation. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index b4034b9cf9..09c25b38a6 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -61,11 +61,9 @@ Class Measure {A B} (f : A -> B). (** Standard measures. *) -Instance fst_measure : @Measure (A * B) A Fst. -Defined. +Instance fst_measure {A B} : @Measure (A * B) A Fst := {}. -Instance snd_measure : @Measure (A * B) B Snd. -Defined. +Instance snd_measure {A B} : @Measure (A * B) B Snd := {}. (** We define a product relation over [A*B]: each components should satisfy the corresponding initial relation. *) @@ -96,11 +94,11 @@ Section RelCompFun_Instances. `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f). Proof. firstorder. Qed. - Global Program Instance RelCompFun_Equivalence - `(Measure A B f, Equivalence _ R) : Equivalence (R@@f). + Global Instance RelCompFun_Equivalence + `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}. - Global Program Instance RelCompFun_StrictOrder - `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f). + Global Instance RelCompFun_StrictOrder + `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}. End RelCompFun_Instances. diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v index f52b559f84..992b00e834 100644 --- a/theories/Compat/Coq812.v +++ b/theories/Compat/Coq812.v @@ -11,4 +11,6 @@ (** Compatibility file for making Coq act similar to Coq v8.12 *) Require Export Coq.Compat.Coq813. +Local Set Warnings "-deprecated". Set Firstorder Solver auto with *. +Export Set Instance Generalized Output. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 50351d6a14..688db8b812 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -12,8 +12,6 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. -Require Import ProofIrrelevance. -Require Import FunctionalExtensionality. Local Open Scope program_scope. @@ -51,7 +49,7 @@ Section Well_founded. Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. Proof. intro x; induction (Rwf x); intros. - rewrite (proof_irrelevance (Acc R x) r s) ; auto. + rewrite <- 2 Fix_F_eq; intros. apply F_ext; intros []; auto. Qed. Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)). @@ -226,6 +224,7 @@ Ltac fold_sub f := (** This module provides the fixpoint equation provided one assumes functional extensionality. *) +Require Import FunctionalExtensionality. Module WfExtensionality. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 5d210b2e60..e5beab5d33 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -278,8 +278,16 @@ pos_lnum = lcp.pos_lnum + n; pos_bol = lcp.pos_cnum } - let print_position chan p = - Printf.fprintf chan "%s:%d:%d" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) + let print_position_p chan p = + Printf.fprintf chan "%s%d, character %d" + (if p.pos_fname = "" then "Line " else "File \"" ^ p.pos_fname ^ "\", line ") + p.pos_lnum (p.pos_cnum - p.pos_bol) + + let print_position chan {lex_start_p = p} = print_position_p chan p + + let warn msg lexbuf = + eprintf "%a, warning: %s\n" print_position lexbuf msg; + flush stderr exception MismatchPreformatted of position @@ -487,29 +495,29 @@ rule coq_bol = parse then Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" (space_nl as s) - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } | space* "Comments" (space_nl as s) - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); Output.start_coq (); coq lexbuf } | space* begin_hide nl - { Lexing.new_line lexbuf; skip_hide lexbuf; coq_bol lexbuf } + { new_lines 1 lexbuf; skip_hide lexbuf; coq_bol lexbuf } | space* begin_show nl - { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf } + { new_lines 1 lexbuf; begin_show (); coq_bol lexbuf } | space* end_show nl - { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf } + { new_lines 1 lexbuf; end_show (); coq_bol lexbuf } | space* begin_details (* At this point, the comment remains open, and will be closed by [details_body] *) { let s = details_body lexbuf in Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf } | space* end_details nl - { Lexing.new_line lexbuf; + { new_lines 1 lexbuf; Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf } | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in @@ -572,8 +580,7 @@ rule coq_bol = parse add_printing_token tok s; coq_bol lexbuf } | space* "(**" space+ "printing" space+ - { eprintf "warning: bad 'printing' command at character %d\n" - (lexeme_start lexbuf); flush stderr; + { warn "bad 'printing' command" lexbuf; comment_level := 1; ignore (comment lexbuf); coq_bol lexbuf } @@ -582,8 +589,7 @@ rule coq_bol = parse { remove_printing_token (lexeme lexbuf); coq_bol lexbuf } | space* "(**" space+ "remove" space+ "printing" space+ - { eprintf "warning: bad 'remove printing' command at character %d\n" - (lexeme_start lexbuf); flush stderr; + { warn "bad 'remove printing' command" lexbuf; comment_level := 1; ignore (comment lexbuf); coq_bol lexbuf } @@ -616,9 +622,9 @@ rule coq_bol = parse and coq = parse | nl - { Lexing.new_line lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } + { new_lines 1 lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } | "(**" (space_nl as s) - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); @@ -719,7 +725,7 @@ and coq = parse and doc_bol = parse | space* section space+ ([^'\n' '\r' '*'] | '*'+ [^'\n' '\r' ')' '*'])* ('*'+ (nl as s))? - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; let eol, lex = strip_eol (lexeme lexbuf) in let lev, s = sec_title lex in if (!Cdglobals.lib_subtitles) && @@ -731,7 +737,7 @@ and doc_bol = parse | ((space_nl* nl)? as s) (space* '-'+ as line) { let nl_count = count_newlines s in match check_start_list line with - | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf + | Neither -> backtrack_past_newline lexbuf; new_lines 1 lexbuf; doc None lexbuf | List n -> new_lines nl_count lexbuf; if nl_count > 0 then Output.paragraph (); @@ -742,8 +748,10 @@ and doc_bol = parse } | (space_nl* nl) as s { new_lines (count_newlines s) lexbuf; Output.paragraph (); doc_bol lexbuf } - | "<<" space* - { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf } + | "<<" space* nl + { new_lines 1 lexbuf; Output.start_verbatim false; verbatim_block lexbuf; doc_bol lexbuf } + | "<<" + { Output.start_verbatim true; verbatim_inline lexbuf; doc None lexbuf } | eof { true } | '_' @@ -765,27 +773,33 @@ and doc_list_bol indents = parse | InLevel (_,false) -> backtrack lexbuf; doc_bol lexbuf } - | "<<" space* - { Output.start_verbatim false; - verbatim 0 false lexbuf; + | "<<" space* nl + { new_lines 1 lexbuf; Output.start_verbatim false; + verbatim_block lexbuf; doc_list_bol indents lexbuf } + | "<<" space* + { Output.start_verbatim true; + verbatim_inline lexbuf; + doc (Some indents) lexbuf } | "[[" nl - { formatted := Some lexbuf.lex_start_p; + { new_lines 1 lexbuf; formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); ignore(body_bol lexbuf); Output.end_inline_coq_block (); formatted := None; doc_list_bol indents lexbuf } | "[[[" nl - { inf_rules (Some indents) lexbuf } + { new_lines 1 lexbuf; inf_rules (Some indents) lexbuf } | space* nl space* '-' { (* Like in the doc_bol production, these two productions exist only to deal properly with whitespace *) + new_lines 1 lexbuf; Output.paragraph (); backtrack_past_newline lexbuf; doc_list_bol indents lexbuf } | space* nl space* _ - { let buf' = lexeme lexbuf in + { new_lines 1 lexbuf; + let buf' = lexeme lexbuf in let buf = let bufs = Str.split_delim (Str.regexp "['\n']") buf' in match bufs with @@ -830,12 +844,14 @@ and doc_list_bol indents = parse (*s Scanning documentation elsewhere *) and doc indents = parse | nl - { Output.char '\n'; + { new_lines 1 lexbuf; + Output.char '\n'; match indents with | Some ls -> doc_list_bol ls lexbuf | None -> doc_bol lexbuf } | "[[" nl - { if !Cdglobals.plain_comments + { new_lines 1 lexbuf; + if !Cdglobals.plain_comments then (Output.char '['; Output.char '['; doc indents lexbuf) else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); @@ -847,7 +863,7 @@ and doc indents = parse | None -> doc_bol lexbuf else doc indents lexbuf)} | "[[[" nl - { inf_rules indents lexbuf } + { new_lines 1 lexbuf; inf_rules indents lexbuf } | "[]" { Output.proofbox (); doc indents lexbuf } | "{{" { url lexbuf; doc indents lexbuf } @@ -877,7 +893,7 @@ and doc indents = parse doc_bol lexbuf } | '*'* "*)" space* nl - { true } + { new_lines 1 lexbuf; Output.char '\n'; true } | '*'* "*)" { false } | "$" @@ -911,7 +927,7 @@ and doc indents = parse Output.char (lexeme_char lexbuf 1); doc indents lexbuf } | "<<" space* - { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf } + { Output.start_verbatim true; verbatim_inline lexbuf; doc indents lexbuf } | '"' { if !Cdglobals.plain_comments then Output.char '"' @@ -951,20 +967,25 @@ and escaped_html = parse { backtrack lexbuf } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim depth inline = parse - | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | ">>" { Output.stop_verbatim inline } - | "(*" { Output.verbatim_char inline '('; - Output.verbatim_char inline '*'; - verbatim (depth+1) inline lexbuf } - | "*)" { if (depth == 0) - then (Output.stop_verbatim inline; backtrack lexbuf) - else (Output.verbatim_char inline '*'; - Output.verbatim_char inline ')'; - verbatim (depth-1) inline lexbuf) } - | eof { Output.stop_verbatim inline } - | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf } +and verbatim_block = parse + | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char false '\n'; Output.stop_verbatim false } + | nl ">>" + { new_lines 1 lexbuf; + warn "missing newline after \">>\" block" lexbuf; + Output.verbatim_char false '\n'; + Output.stop_verbatim false } + | eof { warn "unterminated \">>\" block" lexbuf; Output.stop_verbatim false } + | nl { new_lines 1 lexbuf; Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf } + | _ { Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf } + +and verbatim_inline = parse + | nl { new_lines 1 lexbuf; + warn "unterminated inline \">>\"" lexbuf; + Output.char '\n'; + Output.stop_verbatim true } + | ">>" { Output.stop_verbatim true } + | eof { warn "unterminated inline \">>\"" lexbuf; Output.stop_verbatim true } + | _ { Output.verbatim_char true (lexeme_char lexbuf 0); verbatim_inline lexbuf } and url = parse | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } @@ -993,7 +1014,8 @@ and escaped_coq = parse else skipped_comment lexbuf); escaped_coq lexbuf } | "*)" - { (* likely to be a syntax error: we escape *) backtrack lexbuf } + { (* likely to be a syntax error *) + warn "unterminated \"]\"" lexbuf; backtrack lexbuf } | eof { Tokens.flush_sublexer () } | identifier @@ -1036,7 +1058,8 @@ and skipped_comment = parse { incr comment_level; skipped_comment lexbuf } | "*)" space* nl - { decr comment_level; + { new_lines 1 lexbuf; + decr comment_level; if !comment_level > 0 then skipped_comment lexbuf else true } | "*)" { decr comment_level; @@ -1050,7 +1073,8 @@ and comment = parse Output.start_comment (); comment lexbuf } | "*)" space* nl - { Output.end_comment (); + { new_lines 1 lexbuf; + Output.end_comment (); Output.line_break (); decr comment_level; if !comment_level > 0 then comment lexbuf else true } @@ -1064,7 +1088,8 @@ and comment = parse escaped_coq lexbuf; Output.end_inline_coq ()); comment lexbuf } | "[[" nl - { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') + { new_lines 1 lexbuf; + if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); let _ = body_bol lexbuf in @@ -1099,13 +1124,14 @@ and comment = parse { Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf } | nl - { Output.line_break (); + { new_lines 1 lexbuf; + Output.line_break (); comment lexbuf } | _ { Output.char (lexeme_char lexbuf 0); comment lexbuf } and skip_to_dot = parse - | '.' space* nl { true } + | '.' space* nl { new_lines 1 lexbuf; true } | eof | '.' space+ { false } | "(*" { comment_level := 1; @@ -1114,14 +1140,14 @@ and skip_to_dot = parse | _ { skip_to_dot lexbuf } and skip_to_dot_or_brace = parse - | '.' space* nl { true } + | '.' space* nl { new_lines 1 lexbuf; true } | eof | '.' space+ { false } | "(*" { comment_level := 1; ignore (skipped_comment lexbuf); skip_to_dot_or_brace lexbuf } | "}" space* nl - { true } + { new_lines 1 lexbuf; true } | "}" { false } | space* @@ -1134,7 +1160,7 @@ and body_bol = parse | "" { Output.indentation 0; body lexbuf } and body = parse - | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf} + | nl { Tokens.flush_sublexer(); Output.line_break(); new_lines 1 lexbuf; body_bol lexbuf} | (nl+ as s) space* "]]" space* nl { new_lines (count_newlines s + 1) lexbuf; Tokens.flush_sublexer(); @@ -1156,7 +1182,7 @@ and body = parse end } | "]]" space* nl { Tokens.flush_sublexer(); - Lexing.new_line lexbuf; + new_lines 1 lexbuf; if is_none !formatted then begin let loc = lexeme_start lexbuf in @@ -1265,31 +1291,31 @@ and string = parse | _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf } and skip_hide = parse - | eof | end_hide nl { Lexing.new_line lexbuf; () } + | eof | end_hide nl { new_lines 1 lexbuf; () } | _ { skip_hide lexbuf } (*s Reading token pretty-print *) and printing_token_body = parse | "*)" (nl as s)? | eof - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } | (nl | _) as s - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } and details_body = parse | "*)" space* (nl as s)? | eof - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; None } | ":" space* { details_body_rec lexbuf } and details_body_rec = parse | "*)" space* (nl as s)? | eof - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; let s = Buffer.contents token_buffer in Buffer.clear token_buffer; Some s } @@ -1300,9 +1326,10 @@ and details_body_rec = parse enclosed in [[[ ]]] brackets *) and inf_rules indents = parse | space* nl (* blank line, before or between definitions *) - { inf_rules indents lexbuf } + { new_lines 1 lexbuf; inf_rules indents lexbuf } | "]]]" nl (* end of the inference rules block *) - { match indents with + { new_lines 1 lexbuf; + match indents with | Some ls -> doc_list_bol ls lexbuf | None -> doc_bol lexbuf } | _ @@ -1315,7 +1342,8 @@ and inf_rules indents = parse *) and inf_rules_assumptions indents assumptions = parse | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *) - { let line = lexeme lexbuf in + { new_lines 1 lexbuf; + let line = lexeme lexbuf in let (spaces,_) = count_spaces line in let dashes_and_name = cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) @@ -1334,7 +1362,8 @@ and inf_rules_assumptions indents assumptions = parse inf_rules_conclusion indents (List.rev assumptions) (spaces, dashes, name) [] lexbuf } | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *) - { let line = lexeme lexbuf in + { new_lines 1 lexbuf; + let line = lexeme lexbuf in let (spaces,_) = count_spaces line in let assumption = cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) @@ -1348,11 +1377,12 @@ and inf_rules_assumptions indents assumptions = parse blank line or a ']]]'. *) and inf_rules_conclusion indents assumptions middle conclusions = parse | space* nl | space* "]]]" nl (* end of conclusions. *) - { backtrack lexbuf; + { new_lines 2 lexbuf; backtrack lexbuf; Output.inf_rule assumptions middle (List.rev conclusions); inf_rules indents lexbuf } | space* [^ '\n']+ nl (* this is a line in the conclusion *) - { let line = lexeme lexbuf in + { new_lines 1 lexbuf; + let line = lexeme lexbuf in let (spaces,_) = count_spaces line in let conc = cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) @@ -1395,16 +1425,16 @@ and st_subtitle = parse { (* coq_bol with error handling *) let coq_bol' f lb = - Lexing.new_line lb; (* Start numbering lines from 1 *) try coq_bol lb with | MismatchPreformatted p -> - Printf.eprintf "%a: mismatched \"[[\"\n" print_position { p with pos_fname = f }; + Printf.eprintf "%a: mismatched \"[[\"\n" print_position_p p; exit 1 let coq_file f m = reset (); let c = open_in f in let lb = from_channel c in + let lb = { lb with lex_start_p = { lb.lex_start_p with pos_fname = f } } in (Index.current_library := m; Output.initialize (); Output.start_module (); diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 32cf05e1eb..a87dfb5b2e 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -313,7 +313,7 @@ module Latex = struct let start_verbatim inline = if inline then printf "\\texttt{" - else printf "\\begin{verbatim}" + else printf "\\begin{verbatim}\n" let stop_verbatim inline = if inline then printf "}" @@ -479,10 +479,6 @@ module Latex = struct let end_coq () = printf "\\end{coqdoccode}\n" - let start_code () = end_doc (); start_coq () - - let end_code () = end_coq (); start_doc () - let section_kind = function | 1 -> "\\section{" | 2 -> "\\subsection{" @@ -632,11 +628,11 @@ module Html = struct let stop_quote () = start_quote () let start_verbatim inline = - if inline then printf "<tt>" - else printf "<pre>" + if inline then printf "<code>" + else printf "<pre>\n" let stop_verbatim inline = - if inline then printf "</tt>" + if inline then printf "</code>" else printf "</pre>\n" let url addr name = @@ -738,7 +734,7 @@ module Html = struct let end_doc () = in_doc := false; stop_item (); - if not !raw_comments then printf "\n</div>\n" + if not !raw_comments then printf "</div>\n" let start_emph () = printf "<i>" @@ -754,10 +750,6 @@ module Html = struct let end_comment () = printf "*)</span>" - let start_code () = end_doc (); start_coq () - - let end_code () = end_coq (); start_doc () - let start_inline_coq () = if !inline_notmono then printf "<span class=\"inlinecodenm\">" else printf "<span class=\"inlinecode\">" @@ -1069,9 +1061,6 @@ module TeXmacs = struct let start_comment () = () let end_comment () = () - let start_code () = in_doc := true; printf "<\\code>\n" - let end_code () = in_doc := false; printf "\n</code>" - let section_kind = function | 1 -> "section" | 2 -> "subsection" @@ -1181,9 +1170,6 @@ module Raw = struct let start_coq () = () let end_coq () = () - let start_code () = end_doc (); start_coq () - let end_code () = end_coq (); start_doc () - let section_kind = function | 1 -> "* " @@ -1240,9 +1226,6 @@ let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq -let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code -let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code - let start_inline_coq = select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index b7a8d4d858..4088fdabf7 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -41,9 +41,6 @@ val end_comment : unit -> unit val start_coq : unit -> unit val end_coq : unit -> unit -val start_code : unit -> unit -val end_code : unit -> unit - val start_inline_coq : unit -> unit val end_inline_coq : unit -> unit diff --git a/vernac/classes.ml b/vernac/classes.ml index 054addc542..062cc90f8f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -502,9 +502,16 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' else declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype -let interp_instance_context ~program_mode env ctx ~generalize pl tclass = +let auto_generalize = + Goptions.declare_bool_option_and_ref + ~depr:true + ~key:["Instance";"Generalized";"Output"] + ~value:false + +let interp_instance_context ~program_mode env ctx ?(generalize=auto_generalize()) pl tclass = let sigma, decl = interp_univ_decl_opt env pl in let tclass = + (* when we remove this code, we can remove the middle argument of CGeneralization *) if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass in @@ -530,10 +537,10 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance_common ~program_mode ~generalize env instid ctx cl = +let new_instance_common ~program_mode ?generalize env instid ctx cl = let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ~generalize ctx pl cl + interp_instance_context ~program_mode env ?generalize ctx pl cl in (* The name generator should not be here *) let id = @@ -548,20 +555,20 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl = let new_instance_interactive ?(global=false) ~poly instid ctx cl - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook + ?generalize ?(tac:unit Proofview.tactic option) ?hook pri opt_props = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = - new_instance_common ~program_mode:false ~generalize env instid ctx cl in + new_instance_common ~program_mode:false ?generalize env instid ctx cl in id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props let new_instance_program ?(global=false) ~pm ~poly instid ctx cl opt_props - ?(generalize=true) ?hook pri = + ?generalize ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = - new_instance_common ~program_mode:true ~generalize env instid ctx cl in + new_instance_common ~program_mode:true ?generalize env instid ctx cl in let pm = do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props in @@ -569,10 +576,10 @@ let new_instance_program ?(global=false) ~pm let new_instance ?(global=false) ~poly instid ctx cl props - ?(generalize=true) ?hook pri = + ?generalize ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = - new_instance_common ~program_mode:false ~generalize env instid ctx cl in + new_instance_common ~program_mode:false ?generalize env instid ctx cl in do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props; id diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index ebec720ce2..5b80ed6794 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -56,6 +56,8 @@ GRAMMAR EXTEND Gram [ [ IDENT "Goal"; c = lconstr -> { VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) } | IDENT "Proof" -> { VernacProof (None,None) } + | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr -> + { VernacProof (None,Some l) } | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn } | IDENT "Proof"; c = lconstr -> { VernacExactProof c } | IDENT "Abort" -> { VernacAbort None } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index f192d67624..1c80d71ea5 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -114,7 +114,8 @@ GRAMMAR EXTEND Gram ; attribute: [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } - | "using" ; v = attr_value -> { "using", v } ] + (* Required because "ident" is declared a keyword when loading Ltac. *) + | IDENT "using" ; v = attr_value -> { "using", v } ] ] ; attr_value: diff --git a/vernac/record.ml b/vernac/record.ml index 2c56604d8f..891d7fcebe 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -11,53 +11,40 @@ open Pp open CErrors open Term -open Sorts open Util open Names -open Nameops open Constr open Context -open Vars open Environ open Declarations open Entries -open Declare -open Constrintern open Type_errors open Constrexpr open Constrexpr_ops -open Goptions open Context.Rel.Declaration -open Libobject module RelDecl = Context.Rel.Declaration (********** definition d'un record (structure) **************) (** Flag governing use of primitive projections. Disabled by default. *) -let primitive_flag = ref false -let () = - declare_bool_option - { optdepr = false; - optkey = ["Primitive";"Projections"]; - optread = (fun () -> !primitive_flag) ; - optwrite = (fun b -> primitive_flag := b) } - -let typeclasses_strict = ref false -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Strict";"Resolution"]; - optread = (fun () -> !typeclasses_strict); - optwrite = (fun b -> typeclasses_strict := b); } - -let typeclasses_unique = ref false -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Unique";"Instances"]; - optread = (fun () -> !typeclasses_unique); - optwrite = (fun b -> typeclasses_unique := b); } +let primitive_flag = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Primitive";"Projections"] + ~value:false + +let typeclasses_strict = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Strict";"Resolution"] + ~value:false + +let typeclasses_unique = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Unique";"Instances"] + ~value:false let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let _, sigma, impls, newfs, _ = @@ -81,7 +68,8 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let impls_env = match i with | Anonymous -> impls_env - | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env + | Name id -> + Id.Map.add id (Constrintern.compute_internalization_data env sigma id Constrintern.Method t impl) impls_env in let d = match b with | None -> LocalAssum (make_annot i r,t) @@ -106,7 +94,7 @@ let compute_constructor_level evars env l = let univ = if is_local_assum d then let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in - Univ.sup (univ_of_sort s) univ + Univ.sup (Sorts.univ_of_sort s) univ else univ in (EConstr.push_rel d env, univ)) l (env, Univ.Universe.sprop) @@ -116,68 +104,123 @@ let check_anonymous_type ind = | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false -let typecheck_params_and_fields def poly pl ps records = +let error_parameters_must_be_named bk {CAst.loc; v=name} = + match bk, name with + | Default _, Anonymous -> + CErrors.user_err ?loc ~hdr:"record" (str "Record parameters must be named") + | _ -> () + +let check_parameters_must_be_named = function + | CLocalDef (b, _, _) -> + error_parameters_must_be_named default_binder_kind b + | CLocalAssum (ls, bk, ce) -> + List.iter (error_parameters_must_be_named bk) ls + | CLocalPattern {CAst.loc} -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters") + +(** [DataI.t] contains the information used in record interpretation, + it is a strict subset of [Ast.t] thus this should be + eventually removed or merged with [Ast.t] *) +module DataI = struct + type t = + { name : Id.t + ; arity : Constrexpr.constr_expr option + (** declared sort for the record *) + ; nots : Vernacexpr.decl_notation list list + (** notations for fields *) + ; fs : Vernacexpr.local_decl_expr list + } +end + +type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; +} + +(** [DataR.t] contains record data after interpretation / + type-inference *) +module DataR = struct + type t = + { min_univ : Univ.Universe.t + ; arity : Constr.t + ; implfs : Impargs.manual_implicits list + ; fields : Constr.rel_declaration list + } +end + +module Data = struct + type t = + { id : Id.t + ; idbuild : Id.t + ; is_coercion : bool + ; coers : projection_flags list + ; rdata : DataR.t + } +end + +let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match arity with + | None -> + let uvarkind = Evd.univ_flexible_alg in + let sigma, s = Evd.new_sort_variable uvarkind sigma in + (sigma, template), (EConstr.mkSort s, s) + | Some t -> + let env = EConstr.push_rel_context newps env0 in + let poly = + match t with + | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in + let impls = Constrintern.empty_internalization_env in + let sigma, s = Constrintern.interp_type_evars ~program_mode:false env sigma ~impls t in + let sred = Reductionops.whd_allnolet env sigma s in + (match EConstr.kind sigma sred with + | Sort s' -> + let s' = EConstr.ESorts.kind sigma s' in + (if poly then + match Evd.is_sort_variable sigma s' with + | Some l -> + let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in + (sigma, template), (s, s') + | None -> + (sigma, false), (s, s') + else (sigma, false), (s, s')) + | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) + +type tc_result = + bool + * Impargs.manual_implicits + (* Part relative to closing the definitions *) + * UnivNames.universe_binders + * Entries.universes_entry + * Constr.rel_context + * DataR.t list + +(* ps = parameter list *) +let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_result = let env0 = Global.env () in (* Special case elaboration for template-polymorphic inductives, lower bound on introduced universes is Prop so that we do not miss any Set <= i constraint for universes that might actually be instantiated with Prop. *) let is_template = - List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in + List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in - let sigma, decl = interp_univ_decl_opt env0 pl in - let () = - let error bk {CAst.loc; v=name} = - match bk, name with - | Default _, Anonymous -> - user_err ?loc ~hdr:"record" (str "Record parameters must be named") - | _ -> () - in - List.iter - (function CLocalDef (b, _, _) -> error default_binder_kind b - | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls - | CLocalPattern {CAst.loc} -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps - in - let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in - let fold (sigma, template) (_, t, _, _) = match t with - | Some t -> - let env = EConstr.push_rel_context newps env0 in - let poly = - match t with - | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in - let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in - let sred = Reductionops.whd_allnolet env sigma s in - (match EConstr.kind sigma sred with - | Sort s' -> - let s' = EConstr.ESorts.kind sigma s' in - (if poly then - match Evd.is_sort_variable sigma s' with - | Some l -> - let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in - (sigma, template), (s, s') - | None -> - (sigma, false), (s, s') - else (sigma, false), (s, s')) - | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) - | None -> - let uvarkind = Evd.univ_flexible_alg in - let sigma, s = Evd.new_sort_variable uvarkind sigma in - (sigma, template), (EConstr.mkSort s, s) - in - let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in + let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in + let () = List.iter check_parameters_must_be_named ps in + let sigma, (impls_env, ((env1,newps), imps)) = + Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in + let (sigma, template), typs = + List.fold_left_map (build_type_telescope newps env0) (sigma, true) records in let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in - let fold accu (id, _, _, _) arity r = - EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in + let fold accu { DataI.name; _ } arity r = + EConstr.push_rel (LocalAssum (make_annot (Name name) r,arity)) accu in let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in let impls_env = - let ids = List.map (fun (id, _, _, _) -> id) records in + let ids = List.map (fun { DataI.name; _ } -> name) records in let imps = List.map (fun _ -> imps) arities in - compute_internalization_env env0 sigma ~impls:impls_env Inductive ids arities imps + Constrintern.compute_internalization_env env0 sigma ~impls:impls_env Constrintern.Inductive ids arities imps in let ninds = List.length arities in let nparams = List.length newps in - let fold sigma (_, _, nots, fs) arity = + let fold sigma { DataI.nots; fs; _ } arity = interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs in let (sigma, data) = List.fold_left2_map fold sigma records arities in @@ -198,12 +241,13 @@ let typecheck_params_and_fields def poly pl ps records = else sigma, (univ, typ) in let (sigma, typs) = List.fold_left2_map fold sigma typs data in + (* TODO: Have this use Declaredef.prepare_definition *) let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf -> let newps = List.map (RelDecl.map_constr_het nf) newps in - let map (impls, newfs) (univ, typ) = - let newfs = List.map (RelDecl.map_constr_het nf) newfs in - let typ = nf typ in - (univ, typ, impls, newfs) + let map (implfs, fields) (min_univ, typ) = + let fields = List.map (RelDecl.map_constr_het nf) fields in + let arity = nf typ in + { DataR.min_univ; arity; implfs; fields } in let ans = List.map2 map data typs in newps, ans) @@ -212,7 +256,7 @@ let typecheck_params_and_fields def poly pl ps records = let ubinders = Evd.universe_binders sigma in let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in let () = List.iter (iter_constr ce) (List.rev newps) in - ubinders, univs, template, newps, imps, ans + template, imps, ubinders, univs, newps, ans type record_error = | MissingProj of Id.t * Id.t list @@ -293,26 +337,107 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in Termops.substl_rel_context (subst @ subst') fields -type projection_flags = { - pf_subclass: bool; - pf_canonical: bool; -} - (* We build projections *) -let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields = + +(* TODO: refactor the declaration part here; this requires some + surgery as Evarutil.finalize is called too early in the path *) +(** This builds and _declares_ a named projection, the code looks + tricky due to the term manipulation. It also handles declaring the + implicits parameters, coercion status, etc... of the projection; + this could be refactored as noted above by moving to the + higher-level declare constant API *) +let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls + paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp = + let ccl = subst_projection fid subst ti in + let body, p_opt = match decl with + | LocalDef (_,ci,_) -> subst_projection fid subst ci, None + | LocalAssum ({binder_relevance=rci},_) -> + (* [ccl] is defined in context [params;x:rp] *) + (* [ccl'] is defined in context [params;x:rp;x:rp] *) + if primitive then + let p = Projection.Repr.make indsp + ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in + mkProj (Projection.make p true, mkRel 1), Some p + else + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 rp, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in + let ci = Inductiveops.make_case_info env indsp rci LetStyle in + (* Record projections are always NoInvert because they're at + constant relevance *) + mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None + in + let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in + let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in + let entry = Declare.definition_entry ~univs ~types:projtyp proj in + let kind = Decls.IsDefinition kind in + let kn = + try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) + with Type_errors.TypeError (ctx,te) as exn when not primitive -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) + in + Declare.definition_message fid; + let term = match p_opt with + | Some p -> + let _ = DeclareInd.declare_primitive_projection p kn in + mkProj (Projection.make p false,mkRel 1) + | None -> + let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in + match decl with + | LocalDef (_,ci,_) when primitive -> body + | _ -> applist (mkConstU (kn,uinstance),proj_args) + in + let refi = GlobRef.ConstRef kn in + Impargs.maybe_declare_manual_implicits false refi impls; + if flags.pf_subclass then begin + let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in + ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl + end; + let i = if is_local_assum decl then i+1 else i in + (Some kn::sp_projs, i, Projection term::subst) + +(** [build_proj] will build a projection for each field, or skip if + the field is anonymous, i.e. [_ : t] *) +let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs + (nfi,i,kinds,sp_projs,subst) flags decl impls = + let fi = RelDecl.get_name decl in + let ti = RelDecl.get_type decl in + let (sp_projs,i,subst) = + match fi with + | Anonymous -> + (None::sp_projs,i,NoProjection fi::subst) + | Name fid -> + try build_named_proj + ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid + subst sp_projs nfi ti i indsp mib lifted_fields x rp + with NotDefinable why as exn -> + let _, info = Exninfo.capture exn in + warning_or_error ~info flags.pf_subclass indsp why; + (None::sp_projs,i,NoProjection fi::subst) + in + (nfi - 1, i, + { Recordops.pk_name = fi + ; pk_true_proj = is_local_assum decl + ; pk_canonical = flags.pf_canonical } :: kinds + , sp_projs, subst) + +(** [declare_projections] prepares the common context for all record + projections and then calls [build_proj] for each one. *) +let declare_projections indsp univs ?(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 - let u = match ctx with + let uinstance = match univs with | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_entry ctx -> Univ.Instance.empty in - let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let r = mkIndU (indsp,u) in + let paramdecls = Inductive.inductive_paramdecls (mib, uinstance) in + let r = mkIndU (indsp,uinstance) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) let x = make_annot (Name binder_name) mip.mind_relevance in - let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in + let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let primitive = match mib.mind_record with @@ -321,74 +446,44 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f in let (_,_,kinds,sp_projs,_) = List.fold_left3 - (fun (nfi,i,kinds,sp_projs,subst) flags decl impls -> - let fi = RelDecl.get_name decl in - let ti = RelDecl.get_type decl in - let (sp_projs,i,subst) = - match fi with - | Anonymous -> - (None::sp_projs,i,NoProjection fi::subst) - | Name fid -> - try - let ccl = subst_projection fid subst ti in - let body, p_opt = match decl with - | LocalDef (_,ci,_) -> subst_projection fid subst ci, None - | LocalAssum ({binder_relevance=rci},_) -> - (* [ccl] is defined in context [params;x:rp] *) - (* [ccl'] is defined in context [params;x:rp;x:rp] *) - if primitive then - let p = Projection.Repr.make indsp - ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in - mkProj (Projection.make p true, mkRel 1), Some p - else - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 rp, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in - let ci = Inductiveops.make_case_info env indsp rci LetStyle in - (* Record projections are always NoInvert because - they're at constant relevance *) - mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None - in - let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in - let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in - let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in - let kind = Decls.IsDefinition kind in - let kn = - try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) - with Type_errors.TypeError (ctx,te) as exn when not primitive -> - let _, info = Exninfo.capture exn in - Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) - in - Declare.definition_message fid; - let term = match p_opt with - | Some p -> - let _ = DeclareInd.declare_primitive_projection p kn in - mkProj (Projection.make p false,mkRel 1) - | None -> - let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - match decl with - | LocalDef (_,ci,_) when primitive -> body - | _ -> applist (mkConstU (kn,u),proj_args) - in - let refi = GlobRef.ConstRef kn in - Impargs.maybe_declare_manual_implicits false refi impls; - if flags.pf_subclass then begin - let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in - ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl - end; - let i = if is_local_assum decl then i+1 else i in - (Some kn::sp_projs, i, Projection term::subst) - with NotDefinable why as exn -> - let _, info = Exninfo.capture exn in - warning_or_error ~info flags.pf_subclass indsp why; - (None::sp_projs,i,NoProjection fi::subst) - in - (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst)) + (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs) (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) open Typeclasses +let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min_univ; fields; _ }; _ } = + let template_candidate () = + (* we use some dummy values for the arities in the rel_context + as univs_of_constr doesn't care about localassums and + getting the real values is too annoying *) + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + let ctor_levels = List.fold_left + (fun univs d -> + let univs = + RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs + in + univs) + param_levels fields + in + ComInductive.template_polymorphism_candidate ~ctor_levels univs params + (Some (Sorts.sort_of_univ min_univ)) + in + match template with + | Some template, _ -> + (* templateness explicitly requested *) + if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); + template + | None, template -> + (* auto detect template *) + ComInductive.should_auto_template id (template && template_candidate ()) + let load_structure i (_, structure) = Recordops.register_structure structure @@ -402,7 +497,8 @@ let discharge_structure (_, x) = Some x let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s -let inStruc : Recordops.struc_typ -> obj = +let inStruc : Recordops.struc_typ -> Libobject.obj = + let open Libobject in declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; @@ -414,7 +510,22 @@ let inStruc : Recordops.struc_typ -> obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -let declare_structure ~cumulative finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data = +(** Main record declaration part: + + The entry point is [definition_structure], which will match on the + declared [kind] and then either follow the regular record + declaration path to [declare_structure] or handle the record as a + class declaration with [declare_class]. + +*) + +(** [declare_structure] does two principal things: + + - prepares and declares the low-level (mutual) inductive corresponding to [record_data] + - prepares and declares the corresponding record projections, mainly taken care of by + [declare_projections] +*) +let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) = let nparams = List.length params in let poly, ctx = match univs with @@ -426,14 +537,14 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let binder_name = match name with | None -> - let map (id, _, _, _, _, _, _, _) = + let map { Data.id; _ } = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in Array.map_of_list map record_data | Some n -> n in let ntypes = List.length record_data in - let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) = + let mk_block i { Data.id; idbuild; rdata = { DataR.min_univ; arity; fields; _ }; _ } = let nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in @@ -444,42 +555,10 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_lc = [type_constructor] } in let blocks = List.mapi mk_block record_data in - let check_template (id, _, min_univ, _, _, fields, _, _) = - let template_candidate () = - (* we use some dummy values for the arities in the rel_context - as univs_of_constr doesn't care about localassums and - getting the real values is too annoying *) - let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in - let param_levels = - List.fold_left (fun levels d -> match d with - | LocalAssum _ -> levels - | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) - Univ.LSet.empty params - in - let ctor_levels = List.fold_left - (fun univs d -> - let univs = - RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs - in - univs) - param_levels fields - in - ComInductive.template_polymorphism_candidate ~ctor_levels univs params - (Some (Sorts.sort_of_univ min_univ)) - in - match template with - | Some template, _ -> - (* templateness explicitly requested *) - if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); - template - | None, template -> - (* auto detect template *) - ComInductive.should_auto_template id (template && template_candidate ()) - in - let template = List.for_all check_template record_data in + let template = List.for_all (check_template ~template ~univs ~poly ~params) record_data in let primitive = - !primitive_flag && - List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data + primitive_flag () && + List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data in let mie = { mind_entry_params = params; @@ -493,15 +572,15 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa } in let impls = List.map (fun _ -> paramimpls, []) record_data in - let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls - ~primitive_expected:!primitive_flag + let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubind impls + ~primitive_expected:(primitive_flag ()) in - let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = + let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in let build = GlobRef.ConstructRef cstr in - let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in + let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in let npars = Inductiveops.inductive_nparams (Global.env()) rsp in let struc = { Recordops.s_CONST = cstr; @@ -519,68 +598,103 @@ 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 cumulative ubinders univs id idbuild paramimpls params univ arity - template fieldimpls fields ?(kind=Decls.StructureComponent) coers = - let fieldimpls = +let build_class_constant ~univs ~rdata field implfs params paramimpls coers binder id proj_name = + let class_body = it_mkLambda_or_LetIn field params in + let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in + let class_entry = + Declare.definition_entry ~types:class_type ~univs class_body in + let cst = Declare.declare_constant ~name:id + (Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) + in + let inst, univs = match univs with + | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs + | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty + in + let cstu = (cst, inst) in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in + 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 ~name:proj_name + (Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) + in + let cref = GlobRef.ConstRef cst in + Impargs.declare_manual_implicits false cref paramimpls; + Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs); + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = List.hd coers in + let m = { + meth_name = Name proj_name; + meth_info = sub; + meth_const = Some proj_cst; + } in + [cref, [m]] + +let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name = + let record_data = + { Data.id + ; idbuild + ; is_coercion = false + ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields + ; rdata + } in + let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs paramimpls + params template ~kind:Decls.Method ~name:[|binder_name|] [record_data] + in + let map ind = + let map decl b y = { + meth_name = RelDecl.get_name decl; + meth_info = b; + meth_const = y; + } in + let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in + GlobRef.IndRef ind, l + in + List.map map inds + +(** [declare_class] will prepare and declare a [Class]. This is done in + 2 steps: + + 1. two markely different paths are followed depending on whether the + class declaration refers to a constant "definitional classes" or to + a record, that is to say: + + Class foo := bar : T. + + which is equivalent to + + Definition foo := T. + Definition bar (x:foo) : T := x. + Existing Class foo. + + vs + + Class foo := { ... }. + + 2. declare the class, using the information from 1. in the form of [Classes.typeclass] + + *) +let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params + rdata template ?(kind=Decls.StructureComponent) coers = + let implfs = (* Make the class implicit in the projections, and the params if applicable. *) let impls = implicits_of_context params in - List.map (fun x -> impls @ x) fieldimpls + List.map (fun x -> impls @ x) rdata.DataR.implfs in + let rdata = { rdata with DataR.implfs } in let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in + let fields = rdata.DataR.fields in let data = match fields with - | [LocalAssum ({binder_name=Name proj_name} as binder, field) - | LocalDef ({binder_name=Name proj_name} as binder, _, field)] when def -> + | [ LocalAssum ({binder_name=Name proj_name} as binder, field) + | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def -> let binder = {binder with binder_name=Name binder_name} in - let class_body = it_mkLambda_or_LetIn field params in - 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 ~name:id - (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) - in - let inst, univs = match univs with - | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs - | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty - in - let cstu = (cst, inst) in - let inst_type = appvectc (mkConstU cstu) - (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in - 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 ~name:proj_name - (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) - in - let cref = GlobRef.ConstRef cst in - Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls); - Classes.set_typeclass_transparency (EvalConstRef cst) false false; - let sub = List.hd coers in - let m = { - meth_name = Name proj_name; - meth_info = sub; - meth_const = Some proj_cst; - } in - [cref, [m]] + build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name | _ -> - let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false, - List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in - let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls - params template ~kind:Decls.Method ~name:[|binder_name|] record_data - in - let map ind = - let map decl b y = { - meth_name = RelDecl.get_name decl; - meth_info = b; - meth_const = y; - } in - let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in - GlobRef.IndRef ind, l - in - List.map map inds + build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name in let univs, params, fields = match univs with @@ -598,8 +712,8 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni let k = { cl_univs = univs; cl_impl = impl; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique; + cl_strict = typeclasses_strict (); + cl_unique = typeclasses_unique (); cl_context = params; cl_props = fields; cl_projs = projs } @@ -610,7 +724,6 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni in List.map map data - let add_constant_class env sigma cst = let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in let r = (Environ.lookup_constant cst env).const_relevance in @@ -623,8 +736,8 @@ let add_constant_class env sigma cst = cl_context = ctx; cl_props = [LocalAssum (make_annot Anonymous r, t)]; cl_projs = []; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique + cl_strict = typeclasses_strict (); + cl_unique = typeclasses_unique () } in Classes.add_class env sigma tc; @@ -645,8 +758,8 @@ let add_inductive_class env sigma ind = cl_context = ctx; cl_props = [LocalAssum (make_annot Anonymous r, ty)]; cl_projs = []; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique } + cl_strict = typeclasses_strict (); + cl_unique = typeclasses_unique () } in Classes.add_class env sigma k @@ -667,14 +780,33 @@ let declare_existing_class g = open Vernacexpr +module Ast = struct + type t = + { name : Names.lident + ; is_coercion : coercion_flag + ; binders: local_binder_expr list + ; cfs : (local_decl_expr * record_field_attr) list + ; idbuild : Id.t + ; sort : constr_expr option + } + + let to_datai { name; is_coercion; cfs; idbuild; sort } = + let fs = List.map fst cfs in + { DataI.name = name.CAst.v + ; arity = sort + ; nots = List.map (fun (_, { rf_notation }) -> rf_notation) cfs + ; fs + } +end + let check_unique_names records = let extract_name acc (rf_decl, _) = match rf_decl with Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc | _ -> acc in let allnames = - List.fold_left (fun acc (_, id, _, cfs, _, _) -> - id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records + List.fold_left (fun acc { Ast.name; cfs; _ } -> + name.CAst.v :: (List.fold_left extract_name acc cfs)) [] records in match List.duplicates Id.equal allnames with | [] -> () @@ -682,19 +814,15 @@ let check_unique_names records = let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - let has_priority (_, _, _, cfs, _, _) = + let has_priority { Ast.cfs; _ } = List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs in if isnot_class && List.exists has_priority records then user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = - let map (is_coe, id, _, cfs, idbuild, s) = - let fs = List.map fst cfs in - id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs - in - let data = List.map map records in - let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in + let data = List.map Ast.to_datai records in + let pss = List.map (fun { Ast.binders; _ } -> binders) records in let ps = match pss with | [] -> CErrors.anomaly (str "Empty record block") | ps :: rem -> @@ -708,43 +836,66 @@ let extract_record_data records = in ps, data -(* [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 ~cumulative ~poly finite records = +(* declaring structures, common data to refactor *) +let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def records data = + let { Ast.name; cfs; idbuild; _ }, rdata = match records, data with + | [r], [d] -> r, d + | _, _ -> + CErrors.user_err (str "Mutual definitional classes are not handled") + in + let coers = List.map (fun (_, { rf_subclass; rf_priority }) -> + match rf_subclass with + | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None} + | Vernacexpr.NoInstance -> None) + cfs + in + declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild + impargs params rdata template coers + +let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data = + let adjust_impls impls = impargs @ [CAst.make None] @ impls in + let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in + (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *) + let map rdata { Ast.name; is_coercion; cfs; idbuild; _ } = + let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) -> + { pf_subclass = + (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false); + pf_canonical = rf_canonical }) + cfs + in + { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers } + in + let data = List.map2 map data records in + let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in + List.map (fun ind -> GlobRef.IndRef ind) inds + +(** [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 ~cumulative ~poly finite (records : Ast.t list) = let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in - let ubinders, univs, auto_template, params, implpars, data = + let auto_template, impargs, ubind, univs, params, data = + (* In theory we should be able to use + [Notation.with_notation_protection], due to the call to + Metasyntax.set_notation_for_interpretation, however something + is messing state beyond that. + *) Vernacstate.System.protect (fun () -> typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in let template = template, auto_template in match kind with | Class def -> - let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with - | [r], [d] -> r, d - | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") - in - let coers = List.map (fun (_, { rf_subclass=coe; rf_priority=pri }) -> - match coe with - | Vernacexpr.BackInstance -> Some {hint_priority = pri ; hint_pattern = None} - | Vernacexpr.NoInstance -> None) - cfs - in - declare_class def cumulative ubinders univs id.CAst.v idbuild - implpars params univ arity template implfs fields coers - | _ -> - let map impls = implpars @ [CAst.make None] @ impls in - let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in - let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = - let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> - { pf_subclass = - (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false); - pf_canonical = rf_canonical }) - cfs - in - id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe - in - let data = List.map2 map data records in - let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in - List.map (fun ind -> GlobRef.IndRef ind) inds + class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data + | Inductive_kw | CoInductive | Variant | Record | Structure -> + regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data + +module Internal = struct + type nonrec projection_flags = projection_flags = { + pf_subclass: bool; + pf_canonical: bool; + } + let declare_projections = declare_projections + let declare_structure_entry = declare_structure_entry +end diff --git a/vernac/record.mli b/vernac/record.mli index 38a622977a..ffcae2975e 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -12,22 +12,16 @@ open Names open Vernacexpr open Constrexpr -val primitive_flag : bool ref - -type projection_flags = { - pf_subclass: bool; - pf_canonical: bool; -} - -val declare_projections : - inductive -> - Entries.universes_entry -> - ?kind:Decls.definition_object_kind -> - Id.t -> - projection_flags list -> - Impargs.manual_implicits list -> - Constr.rel_context -> - Recordops.proj_kind list * Constant.t option list +module Ast : sig + type t = + { name : Names.lident + ; is_coercion : coercion_flag + ; binders: local_binder_expr list + ; cfs : (local_decl_expr * record_field_attr) list + ; idbuild : Id.t + ; sort : constr_expr option + } +end val definition_structure : universe_decl_expr option @@ -36,14 +30,29 @@ val definition_structure -> cumulative:bool -> poly:bool -> Declarations.recursivity_kind - -> (coercion_flag * - Names.lident * - local_binder_expr list * - (local_decl_expr * record_field_attr) list * - Id.t * constr_expr option) list + -> Ast.t list -> GlobRef.t list val declare_existing_class : GlobRef.t -> unit -(** Used by elpi *) -val declare_structure_entry : Recordops.struc_typ -> unit +(* Implementation internals, consult Coq developers before using; + current user Elpi, see https://github.com/LPCIC/coq-elpi/pull/151 *) +module Internal : sig + type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; + } + + val declare_projections + : Names.inductive + -> Entries.universes_entry + -> ?kind:Decls.definition_object_kind + -> Names.Id.t + -> projection_flags list + -> Impargs.manual_implicits list + -> Constr.rel_context + -> Recordops.proj_kind list * Names.Constant.t option list + + val declare_structure_entry : Recordops.struc_typ -> unit + +end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 824bf35b1d..761f6ef5b7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -715,16 +715,16 @@ let should_treat_as_uniform () = else ComInductive.NonUniformParameters let vernac_record ~template udecl ~cumulative k ~poly finite records = - let map ((coe, id), binders, sort, nameopt, cfs) = - let const = match nameopt with - | None -> Nameops.add_prefix "Build_" id.v + let map ((is_coercion, name), binders, sort, nameopt, cfs) = + let idbuild = match nameopt with + | None -> Nameops.add_prefix "Build_" name.v | Some lid -> let () = Dumpglob.dump_definition lid false "constr" in lid.v in let () = if Dumpglob.dump () then - let () = Dumpglob.dump_definition id false "rec" in + let () = Dumpglob.dump_definition name false "rec" in let iter (x, _) = match x with | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) -> Dumpglob.dump_definition (make ?loc id) false "proj" @@ -732,7 +732,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records = in List.iter iter cfs in - coe, id, binders, cfs, const, sort + Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort } in let records = List.map map records in ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records) @@ -1314,13 +1314,26 @@ let warn_implicit_core_hint_db = (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " ++ strbrk"Please specify a hint database.") -let vernac_remove_hints ~module_local dbnames ids = +let check_hint_locality = function +| OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); +| OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); +| OptDefault | OptLocal -> () + +let vernac_remove_hints ~atts dbnames ids = + let locality = Attributes.(parse option_locality atts) in + let () = check_hint_locality locality in let dbnames = if List.is_empty dbnames then (warn_implicit_core_hint_db (); ["core"]) else dbnames in - Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids) + Hints.remove_hints ~locality dbnames (List.map Smartlocate.global_with_alias ids) let vernac_hints ~atts dbnames h = let dbnames = @@ -1329,17 +1342,7 @@ let vernac_hints ~atts dbnames h = else dbnames in let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in - let () = match locality with - | OptGlobal -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the global attribute in sections."); - | OptExport -> - if Global.sections_are_opened () then - CErrors.user_err Pp.(str - "This command does not support the export attribute in sections."); - | OptDefault | OptLocal -> () - in + let () = check_hint_locality locality in Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = @@ -2184,7 +2187,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with with_module_locality ~atts vernac_create_hintdb dbname b) | VernacRemoveHints (dbnames,ids) -> VtDefault(fun () -> - with_module_locality ~atts vernac_remove_hints dbnames ids) + vernac_remove_hints ~atts dbnames ids) | VernacHints (dbnames,hints) -> VtDefault(fun () -> vernac_hints ~atts dbnames hints) |