diff options
93 files changed, 1490 insertions, 854 deletions
diff --git a/Makefile.common b/Makefile.common index caf1821ce5..1f59bff183 100644 --- a/Makefile.common +++ b/Makefile.common @@ -122,7 +122,7 @@ LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) BYTERUN:=$(addprefix kernel/byterun/, \ - coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) + coq_fix_code.o coq_float64.o coq_memory.o coq_values.o coq_interp.o ) # LINK ORDER: # respecting this order is useful for developers that want to load or link diff --git a/clib/cArray.ml b/clib/cArray.ml index 7249bcada0..95ae48a7ba 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -56,6 +56,7 @@ sig (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array val map_left : ('a -> 'b) -> 'a array -> 'b array val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit + val iter3 : ('a -> 'b -> 'c -> unit) -> 'a array -> 'b array -> 'c array -> unit val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array @@ -392,6 +393,13 @@ let iter2_i f v1 v2 = let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done +let iter3 f v1 v2 v3 = + let len1 = Array.length v1 in + let len2 = Array.length v2 in + let len3 = Array.length v3 in + let () = if not (Int.equal len2 len1) || not (Int.equal len1 len3) then invalid_arg "Array.iter3" in + for i = 0 to len1 - 1 do f (uget v1 i) (uget v2 i) (uget v3 i) done + let map_right f a = let l = length a in if l = 0 then [||] else begin diff --git a/clib/cArray.mli b/clib/cArray.mli index f40ceb56db..664bad4c0a 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -92,6 +92,9 @@ sig val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit (** Iter on two arrays. Raise [Invalid_argument "Array.iter2_i"] if sizes differ. *) + val iter3 : ('a -> 'b -> 'c -> unit) -> 'a array -> 'b array -> 'c array -> unit + (** Iter on three arrays. Raise [Invalid_argument "Array.iter3"] if sizes differ. *) + val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array (** [fold_left_map f e_0 [|l_1...l_n|] = e_n,[|k_1...k_n|]] where [(e_i,k_i)=f e_{i-1} l_i]; see also [Smart.fold_left_map] *) diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index d2e150be9a..7796ae3b01 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -52,7 +52,7 @@ check_variable "CI_JOB_URL" : "${new_coq_opam_archive_git_branch:=master}" : "${old_coq_opam_archive_git_branch:=master}" : "${num_of_iterations:=1}" -: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast}" +: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial}" new_coq_commit=$(git rev-parse HEAD^2) old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit) @@ -269,6 +269,9 @@ create_opam() { opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev" opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released" + # Pinning for packages that are not in a repository + opam pin add -ynq coq-perennial.dev git+https://github.com/mit-pdos/perennial#coq/tested + opam install -qy -j$number_of_processors $initial_opam_packages if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fc8921e63d..6f6b3cd6d2 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -404,8 +404,7 @@ function build_prep { # ------------------------------------------------------------------------------ # Like build_prep, but gets the data from an entry in ci-basic-overlay.sh -# This assumes the following definitions exist in ci-basic-overlay.sh, -# or in a file in the user-overlays folder: +# This assumes the following definitions exist in ci-basic-overlay.sh # $1_CI_REF # $1_CI_ARCHIVEURL # $1_CI_GITURL @@ -432,7 +431,7 @@ function build_prep_overlay { } # ------------------------------------------------------------------------------ -# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh +# Load overlay version variables from ci-basic-overlay.sh # ------------------------------------------------------------------------------ function load_overlay_data { @@ -448,9 +447,6 @@ function load_overlay_data { export CI_PULL_REQUEST="" fi - for overlay in /build/user-overlays/*.sh; do - . "$overlay" - done . /build/ci-basic-overlay.sh } @@ -1441,7 +1437,6 @@ function make_coq { # Copy these files somewhere the plugin builds can find them logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ - logn copy-user-overlays cp -r dev/ci/user-overlays /build/ build_post fi diff --git a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh new file mode 100644 index 0000000000..3bdbcf7d6e --- /dev/null +++ b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then + + overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single + overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single + +fi diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh new file mode 100644 index 0000000000..95f0de2bd3 --- /dev/null +++ b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then + + unicoq_CI_REF=master+adapting-coq-pr13386 + unicoq_CI_GITURL=https://github.com/herbelin/unicoq + + elpi_CI_REF=coq-master+adapting-coq-pr13386 + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst new file mode 100644 index 0000000000..f069bc616b --- /dev/null +++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst @@ -0,0 +1,17 @@ +- **Changed:** + :term:`Boolean attributes <boolean attribute>` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`, + :attr:`universes(template=no) <universes(template)>` + and :attr:`universes(cumulative=no) <universes(cumulative)>`. + Attributes :attr:`program` and :attr:`canonical` are also affected, + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + + (`#13312 <https://github.com/coq/coq/pull/13312>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst new file mode 100644 index 0000000000..4bd214d7be --- /dev/null +++ b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst @@ -0,0 +1,6 @@ +- **Fixed:** + issue when two expressions involving different projections and one is + primitive need to be unified + (`#13386 <https://github.com/coq/coq/pull/13386>`_, + fixes `#9971 <https://github.com/coq/coq/issues/9971>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst new file mode 100644 index 0000000000..e63ab9696e --- /dev/null +++ b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Capture of the name of global references by + binders in the presence of notations for binders + (`#12965 <https://github.com/coq/coq/pull/12965>`_, + fixes `#9569 <https://github.com/coq/coq/issues/9569>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst new file mode 100644 index 0000000000..d472e6fdf0 --- /dev/null +++ b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst @@ -0,0 +1,12 @@ +- **Changed:** + Redeclaring a notation reactivates also its printing rule; in + particular a second :cmd:`Import` of the same module reactivates the + printing rules declared in this module. In theory, this leads to + changes of behavior for printing. However, this is mitigated in + general by the adoption in `#12986 + <https://github.com/coq/coq/pull/12986>`_ of a priority given to + notations which match a larger part of the term to print + (`#12984 <https://github.com/coq/coq/pull/12984>`_, + fixes `#7443 <https://github.com/coq/coq/issues/7443>`_ + and `#10824 <https://github.com/coq/coq/issues/10824>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst new file mode 100644 index 0000000000..8b233972bf --- /dev/null +++ b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst @@ -0,0 +1,5 @@ +- **Changed:** + Use of notations for printing now gives preference + to notations which match a larger part of the term to abbreviate + (`#12986 <https://github.com/coq/coq/pull/12986>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst new file mode 100644 index 0000000000..bc67fd025a --- /dev/null +++ b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst @@ -0,0 +1,6 @@ +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 <https://github.com/coq/coq/pull/13236>`_, + fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst index a51f96d0a2..f37fbfe52b 100644 --- a/doc/changelog/04-tactics/13381-bfs_eauto.rst +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -1,6 +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. + Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``. + (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) (`#13381 <https://github.com/coq/coq/pull/13381>`_, by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13403-occs_nums_nat.rst b/doc/changelog/04-tactics/13403-occs_nums_nat.rst new file mode 100644 index 0000000000..5dfa90a267 --- /dev/null +++ b/doc/changelog/04-tactics/13403-occs_nums_nat.rst @@ -0,0 +1,7 @@ +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 <https://github.com/coq/coq/pull/13403>`_, + by Jim Fehrle). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 298ea4b4ab..104f84a253 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -99,15 +99,15 @@ coercions. Enables the program mode, in which 1) typechecking allows subset coercions and 2) the elaboration of pattern matching of :cmd:`Fixpoint` and - :cmd:`Definition` act as if the :attr:`program` attribute had been + :cmd:`Definition` acts as if the :attr:`program` attribute has been used, generating obligations if there are unresolved holes after typechecking. -.. attr:: program +.. attr:: program{? = {| yes | no } } :name: program; Program - Allows using the Program mode on a specific - definition. An alternative syntax is to use the legacy ``Program`` + This :term:`boolean attribute` allows using or disabling the Program mode on a specific + definition. An alternative and commonly used syntax is to use the legacy ``Program`` prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter. .. _syntactic_control: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 2474c784b8..22527dc379 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -320,10 +320,9 @@ Summary of the commands maintained. Like any command declaring a record, this command supports the - :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and - :attr:`private(matching)` attributes. + :attr:`universes(polymorphic)`, :attr:`universes(template)`, + :attr:`universes(cumulative)`, and :attr:`private(matching)` + attributes. .. cmd:: Existing Class @qualid diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 064107d088..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,33 +122,37 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. attr:: universes(polymorphic) - :name: universes(polymorphic); Polymorphic +.. attr:: universes(polymorphic{? = {| yes | no } }) + :name: universes(polymorphic); Polymorphic; Monomorphic + + This :term:`boolean attribute` can be used to control whether universe + polymorphism is enabled in the definition of an inductive type. + There is also a legacy syntax using the ``Polymorphic`` prefix (see + :n:`@legacy_attr`) which, as shown in the examples, is more + commonly used. + + When ``universes(polymorphic=no)`` is used, global universe constraints + are produced, even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). - This attribute can be used to declare universe polymorphic - definitions and inductive types. There is also a legacy syntax - using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as - shown in the examples, is more commonly used. +.. attr:: universes(monomorphic) -.. flag:: Universe Polymorphism + .. deprecated:: 8.13 - This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(monomorphic)` attribute is - used. + Use :attr:`universes(polymorphic=no) <universes(polymorphic)>` + instead. -.. attr:: universes(monomorphic) - :name: universes(monomorphic); Monomorphic +.. flag:: Universe Polymorphism - This attribute can be used to declare universe monomorphic - definitions and inductive types (i.e. global universe constraints - are produced), even when the :flag:`Universe Polymorphism` flag is - on. There is also a legacy syntax using the ``Monomorphic`` prefix - (see :n:`@legacy_attr`). + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(polymorphic=no) <universes(polymorphic)>` + attribute is used to override the default. Many other commands can be used to declare universe polymorphic or monomorphic constants depending on whether the :flag:`Universe -Polymorphism` flag is on or the :attr:`universes(polymorphic)` or -:attr:`universes(monomorphic)` attributes are used: +Polymorphism` flag is on or the :attr:`universes(polymorphic)` +attribute is used: - :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe polymorphic constants. @@ -171,19 +175,27 @@ Polymorphism` flag is on or the :attr:`universes(polymorphic)` or Cumulative, NonCumulative ------------------------- -.. attr:: universes(cumulative) - :name: universes(cumulative); Cumulative +.. attr:: universes(cumulative{? = {| yes | no } }) + :name: universes(cumulative); Cumulative; NonCumulative Polymorphic inductive types, coinductive types, variants and - records can be declared cumulative using this attribute or the - legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + records can be declared cumulative using this :term:`boolean attribute` + or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as shown in the examples, is more commonly used. This means that two instances of the same inductive type (family) are convertible based on the universe variances; they do not need to be equal. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + When the attribtue is off, the inductive type is non-cumulative + even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. + There is also a legacy syntax using the ``NonCumulative`` prefix + (see :n:`@legacy_attr`). + + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. + + .. exn:: The cumulative attribute can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, i.e. either having the :flag:`Universe Polymorphism` flag on, or @@ -192,26 +204,21 @@ Cumulative, NonCumulative .. note:: - ``#[ universes(polymorphic), universes(cumulative) ]`` can be - abbreviated into ``#[ universes(polymorphic, cumulative) ]``. + :n:`#[ universes(polymorphic{? = yes }), universes(cumulative{? = {| yes | no } }) ]` can be + abbreviated into :n:`#[ universes(polymorphic{? = yes }, cumulative{? = {| yes | no } }) ]`. -.. flag:: Polymorphic Inductive Cumulativity +.. attr:: universes(noncumulative) - When this flag is on (it is off by default), it makes all - subsequent *polymorphic* inductive definitions cumulative, unless - the :attr:`universes(noncumulative)` attribute is used. It has no - effect on *monomorphic* inductive definitions. + .. deprecated:: 8.13 -.. attr:: universes(noncumulative) - :name: universes(noncumulative); NonCumulative + Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead. - Declares the inductive type as non-cumulative even if the - :flag:`Polymorphic Inductive Cumulativity` flag is on. There is - also a legacy syntax using the ``NonCumulative`` prefix (see - :n:`@legacy_attr`). +.. flag:: Polymorphic Inductive Cumulativity - This means that two instances of the same inductive type (family) - are convertible only if all the universes are equal. + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(cumulative=no) <universes(cumulative)>` attribute is + used to override the default. It has no effect on *monomorphic* inductive definitions. Consider the examples below. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index de5dbe79cc..24fa71059c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Specification language, type inference This makes typeclasses with declared modes more robust with respect to the order of resolution. (`#10858 <https://github.com/coq/coq/pull/10858>`_, - fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). + fixes `#9058 <https://github.com/coq/coq/issues/9058>`_, by Matthieu Sozeau). - **Added:** Warn when manual implicit arguments are used in unexpected positions of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit @@ -533,8 +533,8 @@ Flags, options and attributes - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)` and :attr:`universes(notemplate)` instead + Use :attr:`universes(polymorphic)`, ``universes(monomorphic)``, + :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** :flag:`Hide Obligations` flag @@ -545,7 +545,7 @@ Flags, options and attributes <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). - **Added:** New attributes supported when defining an inductive type - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`universes(cumulative)`, ``universes(noncumulative)`` and :attr:`private(matching)`, which correspond to legacy attributes ``Cumulative``, ``NonCumulative``, and the previously undocumented ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 5406da38a1..2b262b89c0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -369,6 +369,7 @@ this attribute`. attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr } attribute ::= @ident {? @attr_value } attr_value ::= = @string + | = @ident | ( {*, @attribute } ) legacy_attr ::= {| Local | Global } | {| Polymorphic | Monomorphic } @@ -379,21 +380,22 @@ this attribute`. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. +:gdef:`Boolean attributes <boolean attribute>` take the form :n:`@ident__attr{? = {| yes | no } }`. +When the :n:`{| yes | no }` value is omitted, the default is :n:`yes`. + The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: -================ ================================ -Legacy attribute New attribute -================ ================================ -`Local` :attr:`local` -`Global` :attr:`global` -`Polymorphic` :attr:`universes(polymorphic)` -`Monomorphic` :attr:`universes(monomorphic)` -`Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(noncumulative)` -`Private` :attr:`private(matching)` -`Program` :attr:`program` -================ ================================ +============================= ================================ +Legacy attribute New attribute +============================= ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic`, `Monomorphic` :attr:`universes(polymorphic)` +`Cumulative`, `NonCumulative` :attr:`universes(cumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +============================= ================================ Attributes appear in the HTML documentation in blue or gray boxes after the label "Attribute". In the pdf, they appear after the diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 3e2ecdc0f0..43bbc8b40d 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -26,10 +26,8 @@ More information on co-inductive definitions can be found in For co-inductive types, the only elimination principle is case analysis. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)`, :attr:`private(matching)` - and :attr:`using` attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`private(matching)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 79489c85f6..57771c9036 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,7 +90,7 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`program` (see :ref:`program_definition`), :attr:`canonical` and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index ad7d6f3963..251b5e4955 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,10 +32,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -1058,7 +1056,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the :attr:`universes(notemplate)` + This can be prevented using the :attr:`universes(template=no) <universes(template)>` attribute. Template polymorphism and full universe polymorphism (see Chapter @@ -1077,11 +1075,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or the :attr:`universes(template)` attribute: in this case, the warning is not emitted. -.. attr:: universes(template) +.. attr:: universes(template{? = {| yes | no } }) + :name: universes(template) - This attribute can be used to explicitly declare an inductive type - as template polymorphic, whether the :flag:`Auto Template - Polymorphism` flag is on or off. + This :term:`boolean attribute` can be used to explicitly declare an + inductive type as template polymorphic, whether the :flag:`Auto + Template Polymorphism` flag is on or off. .. exn:: template and polymorphism not compatible @@ -1094,11 +1093,15 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or The attribute was used but the inductive definition does not satisfy the criterion to be template polymorphic. + When ``universes(template=no)`` is used, it will prevent an + inductive type to be template polymorphic, even if the :flag:`Auto + Template Polymorphism` flag is on. + .. attr:: universes(notemplate) - This attribute can be used to prevent an inductive type to be - template polymorphic, even if the :flag:`Auto Template - Polymorphism` flag is on. + .. deprecated:: 8.13 + + Use :attr:`universes(template=no) <universes(template)>` instead. In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index e6df3ee9f5..7eedbcd59a 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -53,10 +53,8 @@ expressions. In this sense, the :cmd:`Record` construction allows defining :cmd:`Record` and :cmd:`Structure` are synonyms. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 645986be9c..6ac6626dbe 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -17,10 +17,8 @@ Variants this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. .. exn:: The @natural th argument of @ident must be @ident in @type. :undocumented: diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index 48120503af..f7ce7f1c6c 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,29 +87,27 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. attr:: canonical(false) +.. attr:: canonical{? = {| yes | no } } + :name: canonical - To prevent a field from being involved in the inference of - canonical instances, its declaration can be annotated with the - :attr:`canonical(false)` attribute (cf. the syntax of - :n:`@record_field`). + This boolean attribute can decorate a :cmd:`Definition` or + :cmd:`Let` command. It is equivalent to having a :cmd:`Canonical + Structure` declaration just after the command. - .. example:: + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with + ``canonical=no`` (cf. the syntax of :n:`@record_field`). - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. - - .. coqdoc:: + .. example:: - #[canonical(false)] Prf_equiv : equivalence Carrier Equal + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. - See :ref:`canonicalstructures` for a more realistic example. + .. coqdoc:: -.. attr:: canonical + #[canonical=no] Prf_equiv : equivalence Carrier Equal - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. + See :ref:`hierarchy_of_structures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -248,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*`` relation ``pair_eq`` whenever the type constructor ``*`` is applied to two types being themselves in the ``EQ`` class. +.. _hierarchy_of_structures: + Hierarchy of structures ---------------------------- @@ -331,7 +331,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }. Arguments Mixin {e le} _. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..5283f60b11 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -274,9 +274,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + In the presence of :n:`with`, this applies :tacn:`change` to the + occurrences specified by :n:`@goal_occurrences`. In the + absence of :n:`with`, :n:`@goal_occurrences` is expected to + only list hypotheses (and optionally the conclusion) without + specifying occurrences (i.e. no :n:`at` clause). .. tacv:: now_show @term @@ -320,7 +324,7 @@ Performing computations ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + | - {+ {| @natural | @ident } } int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 56b14d0935..16c8586a9f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -214,7 +214,7 @@ have to be observed for notations starting with a symbol, e.g., rules starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. -Displaying symbolic notations +Use of notations for printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The command :cmd:`Notation` has an effect both on the Coq parser and on the @@ -323,6 +323,26 @@ at the time of use of the notation. scope. Obviously, expressions printed by means of such extra printing rules will not be reparsed to the same form. +.. note:: + + When several notations can be used to print a given term, the + notations which capture the largest subterm of the term are used + preferentially. Here is an example: + + .. coqtop:: in + + Notation "x < y" := (lt x y) (at level 70). + Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level). + + Check (0 < 1 /\ 1 < 2). + + When several notations match the same subterm, or incomparable + subterms of the term to print, the notation declared most recently + is selected. Moreover, reimporting a library or module declares the + notations of this library or module again. If the notation is in a + scope (see :ref:`Scopes`), either the scope has to be opened or a + delimiter has to exist in the scope for the notation to be usable. + The Infix command ~~~~~~~~~~~~~~~~~~ diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4c1956d172..816acba4c1 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1939,11 +1939,6 @@ tac2rec_fields: [ | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] -(* todo: weird productions, ints only after an initial "-"??: - occs_nums: [ - | LIST1 [ natural | ident ] - | "-" [ natural | ident ] LIST0 int_or_var -*) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 033ece04de..03a20d621b 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -480,6 +480,7 @@ opt_hintbases: [ command: [ | "Goal" lconstr | "Proof" +| "Proof" "using" G_vernac.section_subset_expr | "Proof" "Mode" string | "Proof" lconstr | "Abort" @@ -604,7 +605,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 reference | "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] -| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic | "Print" "Ltac" reference | "Locate" "Ltac" reference @@ -764,6 +765,7 @@ attribute: [ attr_value: [ | "=" string +| "=" IDENT | "(" attribute_list ")" | ] @@ -2327,7 +2329,7 @@ conversion: [ occs_nums: [ | LIST1 nat_or_var -| "-" nat_or_var LIST0 int_or_var +| "-" LIST1 nat_or_var ] occs: [ @@ -2537,6 +2539,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index dfd3a18908..0209cf762a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -383,6 +383,7 @@ attribute: [ attr_value: [ | "=" string +| "=" ident | "(" LIST0 attribute SEP "," ")" ] @@ -652,7 +653,7 @@ ref_or_pattern_occ: [ occs_nums: [ | LIST1 [ natural | ident ] -| "-" [ natural | ident ] LIST0 int_or_var +| "-" LIST1 [ natural | ident ] ] int_or_var: [ @@ -952,6 +953,7 @@ command: [ | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) | "Show" "Extraction" (* extraction plugin *) | "Proof" +| "Proof" "using" section_var_expr | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] @@ -1032,7 +1034,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ] -| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ] +| "Proof" "using" section_var_expr "with" ltac_expr | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid @@ -1968,6 +1970,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern ] eqn_ipat: [ diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d1bec16a3f..8d3cf7274a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -85,7 +85,7 @@ let is_reserved_type na t = | Name id -> try let pat = Reserve.find_reserved_type id in - let _ = match_notation_constr false t ([],pat) in + let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([],pat) in true with Not_found | No_match -> false @@ -1273,7 +1273,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = - match_notation_constr !print_universes t pat in + match_notation_constr ~print_univ:(!print_universes) t ~vars pat in (* Try availability of interpretation ... *) match keyrule with | NotationRule (_,ntn as specific_ntn) -> @@ -1293,20 +1293,20 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | Some (scopt,key) -> let scopes' = Option.List.cons scopt (snd scopes) in let l = - List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true (subentry,(scopt,scl@scopes')) vars c) terms in let ll = - List.map (fun (c,(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) c) + List.map (fun ((vars,l),(subentry,(scopt,scl))) -> + List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) termlists in let bl = - List.map (fun (bl,(subentry,(scopt,scl))) -> + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)) binders in let bll = - List.map (fun (bl,(subentry,(scopt,scl))) -> + List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in let c = make_notation loc specific_ntn (l,ll,bl,bll) in @@ -1316,7 +1316,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = - List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c) terms in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b86ad7175a..c7ed066f7e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars in let na = match na with | Anonymous -> - let name = - let id = - match ty with - | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> - qualid_basename qid - | _ -> default_non_dependent_ident - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na in + let id = + match ty with + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> default_non_dependent_ident + in + let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in + let id = + Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in + Name id + | _ -> na + in let impls = impls_type_list 1 ty' in (push_name_env ntnvars impls env' (make ?loc na), (make ?loc (na,b',ty')) :: List.rev bl) diff --git a/interp/notation.ml b/interp/notation.ml index 1a361dc1a6..286ece6cb6 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -345,11 +345,23 @@ let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) = (* No need in principle to compare also_cases as it is inferred *) also_cases1 = also_cases2 && notation_rule_eq rule1 rule2 +let adjust_application c1 c2 = + match c1, c2 with + | NApp (t1, a1), (NList (_,_,NApp (_, a2),_,_) | NApp (_, a2)) when List.length a1 >= List.length a2 -> + NApp (t1, List.firstn (List.length a2) a1) + | NApp (t1, a1), _ -> + t1 + | _ -> c1 + +let strictly_finer_interpretation_than (_,(_,(vars1,c1),_)) (_,(_,(vars2,c2),_)) = + let c1 = adjust_application c1 c2 in + Notation_ops.strictly_finer_notation_constr (List.map fst vars1, List.map fst vars2) c1 c2 + let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in - (* In case of re-import, no need to keep the previous copy *) - let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in - KeyMap.add key (interp :: old) map + (* strictly finer interpretation are kept in front *) + let strictly_finer, rest = List.partition (fun c -> strictly_finer_interpretation_than c interp) old in + KeyMap.add key (strictly_finer @ interp :: rest) map let keymap_remove key interp map = let old = try KeyMap.find key map with Not_found -> [] in @@ -1419,12 +1431,12 @@ let check_parsing_override (scopt,ntn) data = function | OnlyParsingData (_,old_data) -> let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in warn_override_if_needed (scopt,ntn) overridden data old_data; - None, not overridden + None | ParsingAndPrintingData (_,on_printing,old_data) -> let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in warn_override_if_needed (scopt,ntn) overridden data old_data; - (if on_printing then Some old_data.not_interp else None), not overridden - | NoParsingData -> None, false + if on_printing then Some old_data.not_interp else None + | NoParsingData -> None let check_printing_override (scopt,ntn) data parsingdata printingdata = let parsing_update = match parsingdata with @@ -1453,15 +1465,15 @@ let update_notation_data (scopt,ntn) use data table = try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in match use with | OnlyParsing -> - let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in - NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists + let printing_update = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update | ParsingAndPrinting -> - let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in - NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists + let printing_update = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update | OnlyPrinting -> let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in let printingdata = if exists then printingdata else (true,data) :: printingdata in - NotationMap.add ntn (parsingdata, printingdata) table, None, exists + NotationMap.add ntn (parsingdata, printingdata) table, None let rec find_interpretation ntn find = function | [] -> raise Not_found @@ -1734,23 +1746,22 @@ let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecat not_location = df; not_deprecation = deprecation; } in - let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in - if not exists then - let sc = { sc with notations = notation_update } in - scope_map := String.Map.add scope sc !scope_map; + let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in + let sc = { sc with notations = notation_update } in + scope_map := String.Map.add scope sc !scope_map; (* Update the uninterpretation cache *) begin match printing_update with | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat | None -> () end; - if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat; + if use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat; (* Register visibility of lonely notations *) - if not exists then begin match scopt with + begin match scopt with | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack | NotationInScope _ -> () end; (* Declare a possible coercion *) - if not exists then begin match coe with + begin match coe with | Some (IsEntryCoercion entry) -> let (_,level,_) = level_of_notation ntn in let level = match fst ntn with diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7cb3ca25ee..c4d2a2a496 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -24,82 +24,182 @@ open Notation_term (**********************************************************************) (* Utilities *) -(* helper for NVar, NVar case in eq_notation_constr *) -let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None - -let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = -(vars1 == vars2 && t1 == t2) || -match t1, t2 with -| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 -| NVar id1, NVar id2 -> ( - match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with - | Some n,Some m -> Int.equal n m - | None ,None -> Id.equal id1 id2 - | _ -> false) -| NApp (t1, a1), NApp (t2, a2) -> - (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *) -| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && - (eq_notation_constr vars) u1 u2 && b1 == b2 -| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> - Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && - (eq_notation_constr vars) u1 u2 && b1 == b2 -| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr vars b1 b2 && - Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) - let eqpat (p1, t1) (p2, t2) = - List.equal cases_pattern_eq p1 p2 && - (eq_notation_constr vars) t1 t2 - in - let eqf (t1, (na1, o1)) (t2, (na2, o2)) = - let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in - (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 - in - Option.equal (eq_notation_constr vars) o1 o2 && - List.equal eqf r1 r2 && - List.equal eqpat p1 p2 -| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> - List.equal Name.equal nas1 nas2 && - Name.equal na1 na2 && - Option.equal (eq_notation_constr vars) o1 o2 && - (eq_notation_constr vars) t1 t2 && - (eq_notation_constr vars) u1 u2 -| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - (eq_notation_constr vars) t1 t2 && - Name.equal na1 na2 && - Option.equal (eq_notation_constr vars) o1 o2 && - (eq_notation_constr vars) u1 u2 && - (eq_notation_constr vars) r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) - let eq (na1, o1, t1) (na2, o2, t2) = - Name.equal na1 na2 && - Option.equal (eq_notation_constr vars) o1 o2 && - (eq_notation_constr vars) t1 t2 - in - Array.equal Id.equal ids1 ids2 && - Array.equal (List.equal eq) ts1 ts2 && - Array.equal (eq_notation_constr vars) us1 us2 && - Array.equal (eq_notation_constr vars) rs1 rs2 -| NSort s1, NSort s2 -> - glob_sort_eq s1 s2 -| NCast (t1, c1), NCast (t2, c2) -> - (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 -| NInt i1, NInt i2 -> - Uint63.equal i1 i2 -| NFloat f1, NFloat f2 -> - Float64.equal f1 f2 -| NArray(t1,def1,ty1), NArray(t2,def2,ty2) -> - Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2 - && eq_notation_constr vars ty1 ty2 -| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ - | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false +let ldots_var = Id.of_string ".." + +let rec alpha_var id1 id2 = function + | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2 + | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1 + | _::idl -> alpha_var id1 id2 idl + | [] -> Id.equal id1 id2 + +let cast_type_iter2 f t1 t2 = match t1, t2 with + | CastConv t1, CastConv t2 -> f t1 t2 + | CastVM t1, CastVM t2 -> f t1 t2 + | CastCoerce, CastCoerce -> () + | CastNative t1, CastNative t2 -> f t1 t2 + | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit + +(* used to update the notation variable with the local variables used + in NList and NBinderList, since the iterator has its own variable *) +let replace_var i j var = j :: List.remove Id.equal i var + +(* When [lt] is [true], tell if [t1] is a strict refinement of [t2] + (this is a partial order, so returning [false] does not mean that + [t2] is finer than [t1]); when [lt] is false, tell if [t1] is the + same pattern as [t2] *) + +let compare_notation_constr lt (vars1,vars2) t1 t2 = + (* this is used to reason up to order of notation variables *) + let alphameta = ref [] in + (* this becomes true when at least one subterm is detected as strictly smaller *) + let strictly_lt = ref false in + (* this is the stack of inner of iter patterns for comparison with a + new iteration or the tail of a recursive pattern *) + let tail = ref [] in + let check_alphameta id1 id2 = + try if not (Id.equal (List.assoc id1 !alphameta) id2) then raise Exit + with Not_found -> + if (List.mem_assoc id1 !alphameta) then raise Exit; + alphameta := (id1,id2) :: !alphameta in + let check_eq_id (vars1,vars2) renaming id1 id2 = + let ismeta1 = List.mem_f Id.equal id1 vars1 in + let ismeta2 = List.mem_f Id.equal id2 vars2 in + match ismeta1, ismeta2 with + | true, true -> check_alphameta id1 id2 + | false, false -> if not (alpha_var id1 id2 renaming) then raise Exit + | false, true -> + if not lt then raise Exit + else + (* a binder which is not bound in the notation can be + considered as strictly more precise since it prevents the + notation variables in its scope to be bound by this binder; + i.e. it is strictly more precise in the sense that it + covers strictly less patterns than a notation where the + same binder is bound in the notation; this is hawever + disputable *) + strictly_lt := true + | true, false -> if not lt then raise Exit in + let check_eq_name vars renaming na1 na2 = + match na1, na2 with + | Name id1, Name id2 -> check_eq_id vars renaming id1 id2; (id1,id2)::renaming + | Anonymous, Anonymous -> renaming + | Anonymous, Name _ when lt -> renaming + | _ -> raise Exit in + let rec aux (vars1,vars2 as vars) renaming t1 t2 = match t1, t2 with + | NVar id1, NVar id2 when id1 = ldots_var && id2 = ldots_var -> () + | _, NVar id2 when lt && id2 = ldots_var -> tail := t1 :: !tail + | NVar id1, _ when lt && id1 = ldots_var -> tail := t2 :: !tail + | NVar id1, NVar id2 -> check_eq_id vars renaming id1 id2 + | NHole _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> () + | NVar id1, NHole (_, _, _) when lt && List.mem_f Id.equal id1 vars1 -> () + | _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> strictly_lt := true + | NRef gr1, NRef gr2 when GlobRef.equal gr1 gr2 -> () + | NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *) + | _, NHole (_, _, _) when lt -> strictly_lt := true + | NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2) + | NBinderList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) -> + if b1 <> b2 then raise Exit; + let vars1 = replace_var i1 j1 vars1 in + let vars2 = replace_var i2 j2 vars2 in + check_alphameta i1 i2; aux (vars1,vars2) renaming iter1 iter2; aux vars renaming tail1 tail2; + | NBinderList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2) + | NList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) -> + (* They may overlap on a unique iteration of them *) + let vars1 = replace_var i1 j1 vars1 in + let vars2 = replace_var i2 j2 vars2 in + aux (vars1,vars2) renaming iter1 iter2; + aux vars renaming tail1 tail2 + | t1, NList (i2, j2, iter2, tail2, b2) + | t1, NBinderList (i2, j2, iter2, tail2, b2) when lt -> + (* checking if t1 is a finite iteration of the pattern *) + let vars2 = replace_var i2 j2 vars2 in + aux (vars1,vars2) renaming t1 iter2; + let t1 = List.hd !tail in + tail := List.tl !tail; + (* either matching a new iteration, or matching the tail *) + (try aux vars renaming t1 tail2 with Exit -> aux vars renaming t1 t2) + | NList (i1, j1, iter1, tail1, b1), t2 + | NBinderList (i1, j1, iter1, tail1, b1), t2 when lt -> + (* we see the NList as a single iteration *) + let vars1 = replace_var i1 j1 vars1 in + aux (vars1,vars2) renaming iter1 t2; + let t2 = match !tail with + | t::rest -> tail := rest; t + | _ -> (* ".." is in a discarded fine-grained position *) raise Exit in + (* it had to be a single iteration of iter1 *) + aux vars renaming tail1 t2 + | NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2 + | NLambda (na1, t1, u1), NLambda (na2, t2, u2) + | NProd (na1, t1, u1), NProd (na2, t2, u2) -> + aux vars renaming t1 t2; + let renaming = check_eq_name vars renaming na1 na2 in + aux vars renaming u1 u2 + | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> + aux vars renaming b1 b2; + Option.iter2 (aux vars renaming) t1 t2;(* TODO : subtyping? *) + let renaming = check_eq_name vars renaming na1 na2 in + aux vars renaming u1 u2 + | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) + let check_pat (p1, t1) (p2, t2) = + if not (List.equal cases_pattern_eq p1 p2) then raise Exit; (* TODO: subtyping and renaming *) + aux vars renaming t1 t2 + in + let eqf renaming (t1, (na1, o1)) (t2, (na2, o2)) = + aux vars renaming t1 t2; + let renaming = check_eq_name vars renaming na1 na2 in + let eq renaming (i1, n1) (i2, n2) = + if not (Ind.CanOrd.equal i1 i2) then raise Exit; + List.fold_left2 (check_eq_name vars) renaming n1 n2 in + Option.fold_left2 eq renaming o1 o2 in + let renaming = List.fold_left2 eqf renaming r1 r2 in + Option.iter2 (aux vars renaming) o1 o2; + List.iter2 check_pat p1 p2 + | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> + aux vars renaming t1 t2; + let renaming = check_eq_name vars renaming na1 na2 in + Option.iter2 (aux vars renaming) o1 o2; + let renaming' = List.fold_left2 (check_eq_name vars) renaming nas1 nas2 in + aux vars renaming' u1 u2 + | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + aux vars renaming t1 t2; + aux vars renaming u1 u2; + aux vars renaming r1 r2; + let renaming = check_eq_name vars renaming na1 na2 in + Option.iter2 (aux vars renaming) o1 o2 + | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) + let eq renaming (na1, o1, t1) (na2, o2, t2) = + Option.iter2 (aux vars renaming) o1 o2; + aux vars renaming t1 t2; + check_eq_name vars renaming na1 na2 + in + let renaming = Array.fold_left2 (fun r id1 id2 -> check_eq_id vars r id1 id2; (id1,id2)::r) renaming ids1 ids2 in + let renamings = Array.map2 (List.fold_left2 eq renaming) ts1 ts2 in + Array.iter3 (aux vars) renamings us1 us2; + Array.iter3 (aux vars) (Array.map ((@) renaming) renamings) rs1 rs2 + | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> () + | NCast (t1, c1), NCast (t2, c2) -> + aux vars renaming t1 t2; + cast_type_iter2 (aux vars renaming) c1 c2 + | NInt i1, NInt i2 when Uint63.equal i1 i2 -> () + | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> () + | NArray(t1,def1,ty1), NArray(t2,def2,ty2) -> + Array.iter2 (aux vars renaming) t1 t2; + aux vars renaming def1 def2; + aux vars renaming ty1 ty2 + | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ + | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise Exit in + try + let _ = aux (vars1,vars2) [] t1 t2 in + if not lt then + (* Check that order of notation metavariables does not matter *) + List.iter2 check_alphameta vars1 vars2; + not lt || !strictly_lt + with Exit | (* Option.iter2: *) Option.Heterogeneous | Invalid_argument _ -> false + +let eq_notation_constr vars t1 t2 = t1 == t2 || compare_notation_constr false vars t1 t2 + +let strictly_finer_notation_constr vars t1 t2 = compare_notation_constr true vars t1 t2 (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -154,8 +254,6 @@ let rec subst_glob_vars l gc = DAst.map (function | _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *) ) gc -let ldots_var = Id.of_string ".." - type 'a binder_status_fun = { no : 'a -> 'a; restart_prod : 'a -> 'a; @@ -723,6 +821,20 @@ let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn +let rec push_pattern_binders vars pat = + match DAst.get pat with + | PatVar na -> Termops.add_vname vars na + | PatCstr (c, pl, na) -> List.fold_left push_pattern_binders (Termops.add_vname vars na) pl + +let rec push_context_binders vars = function + | [] -> vars + | b :: bl -> + let vars = match DAst.get b with + | GLocalAssum (na,_,_) -> Termops.add_vname vars na + | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars + | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in + push_context_binders vars bl + let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false with Not_found -> false @@ -749,17 +861,11 @@ let is_bindinglist_meta id metas = exception No_match -let rec alpha_var id1 id2 = function - | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2 - | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1 - | _::idl -> alpha_var id1 id2 idl - | [] -> Id.equal id1 id2 - let alpha_rename alpmetas v = if alpmetas == [] then v else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match -let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v = +let add_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var v = (* Check that no capture of binding variables occur *) (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..." with an actual term "fun z => ... z ..." when "x" is not bound in the @@ -787,19 +893,19 @@ let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v = refinement *) let v = alpha_rename alpmetas v in (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::terms,termlists,binders,binderlists) + ((var,(vars,v))::terms,termlists,binders,binderlists) -let add_termlist_env (alp,alpmetas) (terms,termlists,binders,binderlists) var vl = +let add_termlist_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var vl = if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match; let vl = List.map (alpha_rename alpmetas) vl in - (terms,(var,vl)::termlists,binders,binderlists) + (terms,(var,(vars,vl))::termlists,binders,binderlists) -let add_binding_env alp (terms,termlists,binders,binderlists) var v = +let add_binding_env (vars,alp) (terms,termlists,binders,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) - (terms,termlists,(var,v)::binders,binderlists) + (terms,termlists,(var,(vars,v))::binders,binderlists) -let add_bindinglist_env (terms,termlists,binders,binderlists) x bl = - (terms,termlists,binders,(x,bl)::binderlists) +let add_bindinglist_env (vars,alp) (terms,termlists,binders,binderlists) var bl = + (terms,termlists,binders,(var,(vars,bl))::binderlists) let rec map_cases_pattern_name_left f = DAst.map (function | PatVar na -> PatVar (f na) @@ -844,18 +950,19 @@ let rec pat_binder_of_term t = DAst.map (function | _ -> raise No_match ) t -let unify_name_upto alp na na' = +let unify_name_upto (vars,alp) na na' = match na, na' with - | Anonymous, na' -> alp, na' - | na, Anonymous -> alp, na + | Anonymous, na' -> (Termops.add_vname vars na',alp), na' + | na, Anonymous -> (Termops.add_vname vars na,alp), na | Name id, Name id' -> - if Id.equal id id' then alp, na' - else (fst alp,(id,id')::snd alp), na' + let vars = Termops.add_vname vars na' in + if Id.equal id id' then (vars,alp), na' + else (vars,(fst alp,(id,id')::snd alp)), na' let unify_pat_upto alp p p' = try fold_cases_pattern_eq unify_name_upto alp p p' with Failure _ -> raise No_match -let unify_term alp v v' = +let unify_term (_,alp) v v' = match DAst.get v, DAst.get v' with | GHole _, _ -> v' | _, GHole _ -> v @@ -898,13 +1005,13 @@ let rec unify_binders_upto alp bl bl' = alp, b :: bl | _ -> raise No_match -let unify_id alp id na' = +let unify_id (_,alp) id na' = match na' with | Anonymous -> Name (rename_var (snd alp) id) | Name id' -> if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match -let unify_pat alp p p' = +let unify_pat (_,alp) p p' = if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p' else raise No_match @@ -930,33 +1037,37 @@ let rec unify_terms_binders alp cl bl' = let bind_term_env alp (terms,termlists,binders,binderlists as sigma) var v = try (* If already bound to a term, unify with the new term *) - let v' = Id.List.assoc var terms in + let vars,v' = Id.List.assoc var terms in let v'' = unify_term alp v v' in if v'' == v' then sigma else let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in - add_env alp sigma var v + add_env (Id.Set.union vars (fst alp),snd alp) sigma var v with Not_found -> add_env alp sigma var v let bind_termlist_env alp (terms,termlists,binders,binderlists as sigma) var vl = try (* If already bound to a list of term, unify with the new terms *) - let vl' = Id.List.assoc var termlists in + let vars,vl' = Id.List.assoc var termlists in let vl = unify_terms alp vl vl' in let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in - add_termlist_env alp sigma var vl + add_termlist_env (Id.Set.union vars (fst alp),snd alp) sigma var vl with Not_found -> add_termlist_env alp sigma var vl let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) var id = try (* If already bound to a term, unify the binder and the term *) - match DAst.get (Id.List.assoc var terms) with + let vars',v' = Id.List.assoc var terms in + match DAst.get v' with | GVar id' | GRef (GlobRef.VarRef id',None) -> - (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), - sigma + let (vars,(alpha,alpmetas)) = alp in + let vars = Id.Set.add id' vars in + let alpmetas = if not (Id.equal id id') then (id,id')::alpmetas else alpmetas in + (Id.Set.union vars' vars,(alpha,alpmetas)), sigma | t -> (* The term is a non-variable pattern *) raise No_match with Not_found -> + let alp = (Id.Set.add id (fst alp), snd alp) in (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) (* TODO: look at the consequences for alp *) @@ -967,43 +1078,56 @@ let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) - let patl' = Id.List.assoc var binders in + let vars,patl' = Id.List.assoc var binders in let patl'' = List.map2 (unify_pat alp) [pat] patl' in if patl' == patl'' then sigma else let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in - add_binding_env alp sigma var patl'' + add_binding_env (Id.Set.union vars (fst alp),snd alp) sigma var patl'' with Not_found -> add_binding_env alp sigma var [pat] let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var disjpat = try (* If already bound to a binder possibly *) (* generating an alpha-renaming from unifying the new binder *) - let disjpat' = Id.List.assoc var binders in + let vars,disjpat' = Id.List.assoc var binders in + (* if, maybe, there is eventually casts in patterns, the common types have *) + (* to exclude the spine of variable from the two locations they occur *) + let alp' = (Id.Set.union vars (fst alp),snd alp) in let alp, disjpat = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in + alp, add_binding_env alp' sigma var disjpat + with Not_found -> + (* Note: all patterns of the disjunction are supposed to have the same + variables, thus one is enough *) + let alp = (push_pattern_binders (fst alp) (List.hd disjpat), snd alp) in alp, add_binding_env alp sigma var disjpat - with Not_found -> alp, add_binding_env alp sigma var disjpat let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl = let bl = List.rev bl in try (* If already bound to a list of binders possibly *) (* generating an alpha-renaming from unifying the new binders *) - let bl' = Id.List.assoc var binderlists in + let vars, bl' = Id.List.assoc var binderlists in + (* The shared subterm can be under two different spines of *) + (* variables (themselves bound in the notation) , so we take the *) + (* union of both locations *) + let alp' = (Id.Set.union vars (fst alp),snd alp) in let alp, bl = unify_binders_upto alp bl bl' in let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in - alp, add_bindinglist_env sigma var bl + alp, add_bindinglist_env alp' sigma var bl with Not_found -> - alp, add_bindinglist_env sigma var bl + let alp = (push_context_binders (fst alp) bl, snd alp) in + alp, add_bindinglist_env alp sigma var bl let bind_bindinglist_as_termlist_env alp (terms,termlists,binders,binderlists) var cl = try (* If already bound to a list of binders, unify the terms and binders *) - let bl' = Id.List.assoc var binderlists in + let vars,bl' = Id.List.assoc var binderlists in let bl = unify_terms_binders alp cl bl' in + let alp = (Id.Set.union vars (fst alp),snd alp) in let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in - add_bindinglist_env sigma var bl + add_bindinglist_env alp sigma var bl with Not_found -> anomaly (str "There should be a binder list bindings this list of terms.") @@ -1037,7 +1161,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Name id2) when is_term_meta id2 metas -> (* We let the non-binding occurrence define the rhs *) alp, sigma - | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma + | (Name id1,Name id2) -> + let (vars,(alp,alpmetas)) = alp in + (vars,((id1,id2)::alp,alpmetas)),sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -1080,9 +1206,9 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = try let metas = add_ldots_var (add_meta_bindinglist y metas) in let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in - let rest = Id.List.assoc ldots_var terms in + let _,rest = Id.List.assoc ldots_var terms in let b = - match Id.List.assoc y binderlists with [b] -> b | _ ->assert false + match Id.List.assoc y binderlists with _,[b] -> b | _ ->assert false in let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in (* In case y is bound not only to a binder but also to a term *) @@ -1111,18 +1237,20 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *) let match_termlist match_fun alp metas sigma rest x y iter termin revert = - let rec aux sigma acc rest = + let rec aux alp sigma acc rest = try let metas = add_ldots_var (add_meta_term y metas) in let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in - let rest = Id.List.assoc ldots_var terms in - let t = Id.List.assoc y terms in + let _,rest = Id.List.assoc ldots_var terms in + let vars,t = Id.List.assoc y terms in let sigma = remove_sigma y (remove_sigma ldots_var sigma) in if !print_parentheses && not (List.is_empty acc) then raise No_match; - aux sigma (t::acc) rest + (* The union is overkill at the current time because each term matches *) + (* at worst the same binder metavariable of the same pattern *) + aux (Id.Set.union vars (fst alp),snd alp) sigma (t::acc) rest with No_match when not (List.is_empty acc) -> - acc, match_fun metas sigma rest termin in - let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in + alp, acc, match_fun metas sigma rest termin in + let alp,l,(terms,termlists,binders,binderlists as sigma) = aux alp sigma [] rest in let l = if revert then l else List.rev l in if is_bindinglist_meta x metas then (* This is a recursive pattern for both bindings and terms; it is *) @@ -1183,7 +1311,7 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert (* Matching compositionally *) - | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma + | GVar id1, NVar id2 when alpha_var id1 id2 (fst (snd alp)) -> sigma | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma | GApp (f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in @@ -1353,9 +1481,9 @@ and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)} (alp,sigma) disjpatl1 disjpatl2 in match_in u alp metas sigma rhs1 rhs2 -let match_notation_constr u c (metas,pat) = +let match_notation_constr ~print_univ c ~vars (metas,pat) = let terms,termlists,binders,binderlists = - match_ false u ([],[]) metas ([],[],[],[]) c pat in + match_ false print_univ (vars,([],[])) metas ([],[],[],[]) c pat in (* Turning substitution based on binding/constr distinction into a substitution based on entry productions *) List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') -> @@ -1365,9 +1493,9 @@ let match_notation_constr u c (metas,pat) = ((term, scl)::terms',termlists',binders',binderlists') | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with - | [pat] -> + | vars,[pat] -> let v = glob_constr_of_cases_pattern (Global.env()) pat in - ((v,scl)::terms',termlists',binders',binderlists') + (((vars,v),scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 3cc6f82ec8..9d451a5bb9 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -16,6 +16,11 @@ open Glob_term val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool +val strictly_finer_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool +(** Tell if [t1] is a strict refinement of [t2] + (this is a partial order and returning [false] does not mean that + [t2] is finer than [t1]) *) + (** Substitution of kernel names in interpretation data *) val subst_interpretation : @@ -63,10 +68,11 @@ exception No_match val print_parentheses : bool ref -val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> - ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list * - ('a cases_pattern_disjunction_g * extended_subscopes) list * - ('a extended_glob_local_binder_g list * extended_subscopes) list +val match_notation_constr : print_univ:bool -> 'a glob_constr_g -> vars:Id.Set.t -> interpretation -> + ((Id.Set.t * 'a glob_constr_g) * extended_subscopes) list * + ((Id.Set.t * 'a glob_constr_g list) * extended_subscopes) list * + ((Id.Set.t * 'a cases_pattern_disjunction_g) * extended_subscopes) list * + ((Id.Set.t * 'a extended_glob_local_binder_g list) * extended_subscopes) list val match_notation_constr_cases_pattern : 'a cases_pattern_g -> interpretation -> diff --git a/interp/reserve.ml b/interp/reserve.ml index 1d5af3ff39..274d3655d3 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -119,7 +119,7 @@ let revert_reserved_type t = then I've introduced a bug... *) let filter _ pat = try - let _ = match_notation_constr false t ([], pat) in + let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([], pat) in true with No_match -> false in diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 9118410549..1ba6a8c8fe 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,9 +43,7 @@ void init_arity () { arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= - arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= - arity[LTFLOAT]=arity[LEFLOAT]= - arity[ISINT]=arity[AREINT2]=0; + 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= @@ -75,9 +73,10 @@ void init_arity () { arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]= - arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]= - arity[PROJ]=2; + arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= + arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]= + arity[PROJ]= + 2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.c index 84a3edf1c7..bea47dd47e 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.c @@ -8,19 +8,40 @@ /* * (see LICENSE file for the text of the license) */ /************************************************************************/ -#ifndef _COQ_FLOAT64_ -#define _COQ_FLOAT64_ - #include <math.h> +#include <stdint.h> -#define DECLARE_FREL(name, e) \ - int coq_##name(double x, double y) { \ - return e; \ - } \ - \ - value coq_##name##_byte(value x, value y) { \ - return coq_##name(Double_val(x), Double_val(y)); \ - } +#define CAML_INTERNALS +#include <caml/alloc.h> + +#include "coq_values.h" + +union double_bits { + double d; + uint64_t u; +}; + +static double next_up(double x) { + union double_bits bits; + if (!(x < INFINITY)) return x; // x is +oo or NaN + bits.d = x; + int64_t i = bits.u; + if (i >= 0) ++bits.u; // x >= +0.0, go away from zero + else if (bits.u + bits.u == 0) bits.u = 1; // x is -0.0, should almost never happen + else --bits.u; // x < 0.0, go toward zero + return bits.d; +} + +static double next_down(double x) { + union double_bits bits; + if (!(x > -INFINITY)) return x; // x is -oo or NaN + bits.d = x; + int64_t i = bits.u; + if (i == 0) bits.u = INT64_MIN + 1; // x is +0.0 + else if (i < 0) ++bits.u; // x <= -0.0, go away from zero + else --bits.u; // x > 0.0, go toward zero + return bits.d; +} #define DECLARE_FBINOP(name, e) \ double coq_##name(double x, double y) { \ @@ -40,19 +61,14 @@ return caml_copy_double(coq_##name(Double_val(x))); \ } -DECLARE_FREL(feq, x == y) -DECLARE_FREL(flt, x < y) -DECLARE_FREL(fle, x <= y) DECLARE_FBINOP(fmul, x * y) DECLARE_FBINOP(fadd, x + y) DECLARE_FBINOP(fsub, x - y) DECLARE_FBINOP(fdiv, x / y) DECLARE_FUNOP(fsqrt, sqrt(x)) -DECLARE_FUNOP(next_up, nextafter(x, INFINITY)) -DECLARE_FUNOP(next_down, nextafter(x, -INFINITY)) +DECLARE_FUNOP(next_up, next_up(x)) +DECLARE_FUNOP(next_down, next_down(x)) value coq_is_double(value x) { return Val_long(Is_double(x)); } - -#endif /* _COQ_FLOAT64_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1b6da7dd6f..8990743de2 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -28,7 +28,6 @@ #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" -#include "coq_float64.h" #if OCAML_VERSION < 41000 extern void caml_minor_collection(void); @@ -113,7 +112,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } #define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; } -#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; } +#define Restore_after_caml_call coq_env = *sp++; /* Register optimization. Some compilers underestimate the use of the local variables representing @@ -193,7 +192,9 @@ if (sp - num_args < coq_stack_threshold) { \ #endif #endif -#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate) +/* We should also check "Code_val(v) == accumulate" to be sure, + but Is_accu is only used in places where closures cannot occur. */ +#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag) #define CheckPrimArgs(cond, apply_lbl) do{ \ if (cond) pc++; \ @@ -237,6 +238,9 @@ extern intnat volatile caml_pending_signals[]; extern void caml_process_pending_signals(void); #endif +extern double coq_next_up(double); +extern double coq_next_down(double); + /* The interpreter itself */ value coq_interprete @@ -1271,11 +1275,8 @@ value coq_interprete Instruct(CHECKADDINT63){ print_instr("CHECKADDINT63"); CheckInt2(); - } - Instruct(ADDINT63) { /* Adds the integer in the accumulator with the one ontop of the stack (which is poped)*/ - print_instr("ADDINT63"); Uint63_add(accu, *sp++); Next; } @@ -1309,9 +1310,6 @@ value coq_interprete Instruct (CHECKSUBINT63) { print_instr("CHECKSUBINT63"); CheckInt2(); - } - Instruct (SUBINT63) { - print_instr("SUBINT63"); /* returns the subtraction */ Uint63_sub(accu, *sp++); Next; @@ -1517,9 +1515,6 @@ value coq_interprete Instruct (CHECKLTINT63) { print_instr("CHECKLTINT63"); CheckInt2(); - } - Instruct (LTINT63) { - print_instr("LTINT63"); int b; Uint63_lt(b,accu,*sp++); accu = b ? coq_true : coq_false; @@ -1529,9 +1524,6 @@ value coq_interprete Instruct (CHECKLEINT63) { print_instr("CHECKLEINT63"); CheckInt2(); - } - Instruct (LEINT63) { - print_instr("LEINT63"); int b; Uint63_leq(b,accu,*sp++); accu = b ? coq_true : coq_false; @@ -1570,20 +1562,6 @@ value coq_interprete Next; } - Instruct (ISINT){ - print_instr("ISINT"); - accu = (Is_uint63(accu)) ? coq_true : coq_false; - Next; - } - - Instruct (AREINT2){ - print_instr("AREINT2"); - accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false; - sp++; - Next; - } - - Instruct (CHECKOPPFLOAT) { print_instr("CHECKOPPFLOAT"); CheckFloat1(); @@ -1601,27 +1579,21 @@ value coq_interprete Instruct (CHECKEQFLOAT) { print_instr("CHECKEQFLOAT"); CheckFloat2(); - accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + accu = Double_val(accu) == Double_val(*sp++) ? coq_true : coq_false; Next; } Instruct (CHECKLTFLOAT) { print_instr("CHECKLTFLOAT"); CheckFloat2(); - } - Instruct (LTFLOAT) { - print_instr("LTFLOAT"); - accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + accu = Double_val(accu) < Double_val(*sp++) ? coq_true : coq_false; Next; } Instruct (CHECKLEFLOAT) { print_instr("CHECKLEFLOAT"); CheckFloat2(); - } - Instruct (LEFLOAT) { - print_instr("LEFLOAT"); - accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; + accu = Double_val(accu) <= Double_val(*sp++) ? coq_true : coq_false; Next; } @@ -1674,35 +1646,35 @@ value coq_interprete Instruct (CHECKADDFLOAT) { print_instr("CHECKADDFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) + Double_val(*sp++)); Next; } Instruct (CHECKSUBFLOAT) { print_instr("CHECKSUBFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) - Double_val(*sp++)); Next; } Instruct (CHECKMULFLOAT) { print_instr("CHECKMULFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) * Double_val(*sp++)); Next; } Instruct (CHECKDIVFLOAT) { print_instr("CHECKDIVFLOAT"); CheckFloat2(); - Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++))); + Coq_copy_double(Double_val(accu) / Double_val(*sp++)); Next; } Instruct (CHECKSQRTFLOAT) { print_instr("CHECKSQRTFLOAT"); CheckFloat1(); - Coq_copy_double(coq_fsqrt(Double_val(accu))); + Coq_copy_double(sqrt(Double_val(accu))); Next; } @@ -1784,11 +1756,25 @@ value coq_interprete Next; } + Instruct (CHECKNEXTUPFLOATINPLACE) { + print_instr("CHECKNEXTUPFLOATINPLACE"); + CheckFloat1(); + Store_double_val(accu, coq_next_up(Double_val(accu))); + Next; + } + + Instruct (CHECKNEXTDOWNFLOATINPLACE) { + print_instr("CHECKNEXTDOWNFLOATINPLACE"); + CheckFloat1(); + Store_double_val(accu, coq_next_down(Double_val(accu))); + Next; + } - Instruct(ISINT_CAML_CALL2) { + Instruct(CHECKCAMLCALL2_1) { + // arity-2 callback, the last argument can be an accumulator value arg; - print_instr("ISINT_CAML_CALL2"); - if (Is_uint63(accu)) { + print_instr("CHECKCAMLCALL2_1"); + if (!Is_accu(accu)) { pc++; print_int(*pc); arg = sp[0]; @@ -1801,47 +1787,50 @@ value coq_interprete Next; } - Instruct(ISARRAY_CAML_CALL1) { - print_instr("ISARRAY_CAML_CALL1"); - if (Is_coq_array(accu)) { - pc++; - Setup_for_caml_call; - print_int(*pc); - accu = caml_callback(Field(coq_global_data, *pc),accu); - Restore_after_caml_call; - pc++; - } - else pc += *pc; - Next; + Instruct(CHECKCAMLCALL1) { + // arity-1 callback, no argument can be an accumulator + print_instr("CHECKCAMLCALL1"); + if (!Is_accu(accu)) { + pc++; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback(Field(coq_global_data, *pc), accu); + Restore_after_caml_call; + pc++; + } + else pc += *pc; + Next; } - Instruct(ISARRAY_INT_CAML_CALL2) { + Instruct(CHECKCAMLCALL2) { + // arity-2 callback, no argument can be an accumulator value arg; - print_instr("ISARRAY_INT_CAML_CALL2"); - if (Is_coq_array(accu) && Is_uint63(sp[0])) { - pc++; - arg = sp[0]; - Setup_for_caml_call; - print_int(*pc); - accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); - Restore_after_caml_call; - sp += 1; - pc++; - } else pc += *pc; - Next; + print_instr("CHECKCAMLCALL2"); + if (!Is_accu(accu) && !Is_accu(sp[0])) { + pc++; + arg = sp[0]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; } - Instruct(ISARRAY_INT_CAML_CALL3) { + Instruct(CHECKCAMLCALL3_1) { + // arity-3 callback, the last argument can be an accumulator value arg1; value arg2; - print_instr("ISARRAY_INT_CAML_CALL3"); - if (Is_coq_array(accu) && Is_uint63(sp[0])) { + print_instr("CHECKCAMLCALL3_1"); + if (!Is_accu(accu) && !Is_accu(sp[0])) { pc++; arg1 = sp[0]; arg2 = sp[1]; Setup_for_caml_call; print_int(*pc); - accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2); + accu = caml_callback3(Field(coq_global_data, *pc), accu, arg1, arg2); Restore_after_caml_call; sp += 2; pc++; diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index ae5251c252..fe076f8f04 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -65,9 +65,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { + if (!Is_block(*i)) continue; #ifdef NO_NAKED_POINTERS /* The VM stack may contain C-allocated bytecode */ - if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; + if (!Is_in_heap_or_young(*i)) continue; #endif (*action) (*i, i); }; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index f07018711b..0cdef34050 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -30,9 +30,6 @@ #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -/* coq array */ -#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) - /* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 2998178be2..d3e2a2fa7f 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -4,7 +4,7 @@ (public_name coq.vm) (foreign_stubs (language c) - (names coq_fix_code coq_memory coq_values coq_interp) + (names coq_fix_code coq_float64 coq_memory coq_values coq_interp) (flags (:include %{project_root}/config/dune.c_flags)))) (rule diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index f052e03cde..dc2cd349ce 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -104,11 +104,9 @@ let opcodes = "MAKEPROD"; "BRANCH"; "CHECKADDINT63"; - "ADDINT63"; "CHECKADDCINT63"; "CHECKADDCARRYCINT63"; "CHECKSUBINT63"; - "SUBINT63"; "CHECKSUBCINT63"; "CHECKSUBCARRYCINT63"; "CHECKMULINT63"; @@ -127,21 +125,15 @@ let opcodes = "CHECKLSRINT63CONST1"; "CHECKEQINT63"; "CHECKLTINT63"; - "LTINT63"; "CHECKLEINT63"; - "LEINT63"; "CHECKCOMPAREINT63"; "CHECKHEAD0INT63"; "CHECKTAIL0INT63"; - "ISINT"; - "AREINT2"; "CHECKOPPFLOAT"; "CHECKABSFLOAT"; "CHECKEQFLOAT"; "CHECKLTFLOAT"; - "LTFLOAT"; "CHECKLEFLOAT"; - "LEFLOAT"; "CHECKCOMPAREFLOAT"; "CHECKCLASSIFYFLOAT"; "CHECKADDFLOAT"; @@ -155,10 +147,12 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; - "ISINT_CAML_CALL2"; - "ISARRAY_CAML_CALL1"; - "ISARRAY_INT_CAML_CALL2"; - "ISARRAY_INT_CAML_CALL3"; + "CHECKNEXTUPFLOATINPLACE"; + "CHECKNEXTDOWNFLOATINPLACE"; + "CHECKCAMLCALL2_1"; + "CHECKCAMLCALL1"; + "CHECKCAMLCALL2"; + "CHECKCAMLCALL3_1"; "STOP" |] diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index c156a21c86..4977aec00a 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -56,13 +56,12 @@ type instruction = | Kfield of int | Ksetfield of int | Kstop - | Ksequence of bytecodes * bytecodes + | Ksequence of bytecodes | Kproj of Projection.Repr.t | Kensurestackcapacity of int | Kbranch of Label.t (* jump to label *) - | Kprim of CPrimitives.t * pconstant option + | Kprim of CPrimitives.t * pconstant | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int and bytecodes = instruction list @@ -146,21 +145,19 @@ let rec pp_instr i = | Kensurestackcapacity size -> str "growstack " ++ int size | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ - (match id with Some (id,_u) -> Constant.print id | None -> str "") + (Constant.print (fst id)) | Kcamlprim (op, lbl) -> str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ pp_lbl lbl - | Kareint n -> str "areint " ++ int n - and pp_bytecodes c = match c with | [] -> str "" | Klabel lbl :: c -> str "L" ++ int lbl ++ str ":" ++ fnl () ++ pp_bytecodes c - | Ksequence (l1, l2) :: c -> - pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c + | Ksequence l :: c -> + pp_bytecodes l ++ pp_bytecodes c | i :: c -> pp_instr i ++ fnl () ++ pp_bytecodes c diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index b703058fb7..003a77ab78 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -54,14 +54,13 @@ type instruction = | Kfield of int (** accu = accu[n] *) | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *) | Kstop - | Ksequence of bytecodes * bytecodes + | Ksequence of bytecodes | Kproj of Projection.Repr.t | Kensurestackcapacity of int | Kbranch of Label.t (** jump to label, is it needed ? *) - | Kprim of CPrimitives.t * pconstant option + | Kprim of CPrimitives.t * pconstant | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int and bytecodes = instruction list diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 16a0f42664..70c92fd8f0 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -315,12 +315,10 @@ let pos_evar evk r = (* non-terminating instruction (branch, raise, return, appterm) *) (* in front of it. *) -let discard_dead_code cont = cont -(*function - [] -> [] +let rec discard_dead_code = function + | [] -> [] | (Klabel _ | Krestart ) :: _ as cont -> cont | _ :: cont -> discard_dead_code cont -*) (* Return a label to the beginning of the given continuation. *) (* If the sequence starts with a branch, use the target of that branch *) @@ -581,7 +579,7 @@ let rec compile_lam env cenv lam sz cont = let cont_fun = ensure_stack_capacity (compile_lam env r_fun body arity) [Kreturn arity] in - fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; + fun_code := Ksequence (add_grab arity lbl_fun cont_fun) :: !fun_code; let fv = fv r_fun in compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) @@ -604,7 +602,7 @@ let rec compile_lam env cenv lam sz cont = in let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; - fun_code := [Ksequence(fcode,!fun_code)] + fun_code := Ksequence fcode :: !fun_code done; (* Compiling bodies *) for i = 0 to ndef - 1 do @@ -617,7 +615,7 @@ let rec compile_lam env cenv lam sz cont = let lbl = Label.create () in lbl_bodies.(i) <- lbl; let fcode = add_grabrec rec_args.(i) arity lbl cont1 in - fun_code := [Ksequence(fcode,!fun_code)] + fun_code := Ksequence fcode :: !fun_code done; let fv = !rfv in compile_fv cenv fv.fv_rev sz @@ -637,7 +635,7 @@ let rec compile_lam env cenv lam sz cont = in let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; - fun_code := [Ksequence(fcode,!fun_code)] + fun_code := Ksequence fcode :: !fun_code done; (* Compiling bodies *) for i = 0 to ndef - 1 do @@ -652,25 +650,13 @@ let rec compile_lam env cenv lam sz cont = in let cont = ensure_stack_capacity comp arity in lbl_bodies.(i) <- lbl; - fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; + fun_code := Ksequence (add_grab (arity+1) lbl cont) :: !fun_code; done; let fv = !rfv in set_max_stack_size (sz + fv.size + ndef + 2); compile_fv cenv fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) - | Lif(t, bt, bf) -> - let branch, cont = make_branch cont in - let lbl_true = Label.create() in - let lbl_false = Label.create() in - compile_lam env cenv t sz - (Kswitch([|lbl_true;lbl_false|],[||]) :: - Klabel lbl_false :: - compile_lam env cenv bf sz - (branch :: - Klabel lbl_true :: - compile_lam env cenv bt sz cont)) - | Lcase(ci,rtbl,t,a,branches) -> let ind = ci.ci_ind in let mib = lookup_mind (fst ind) env in @@ -688,7 +674,7 @@ let rec compile_lam env cenv lam sz cont = ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop] in let lbl_typ,fcode = label_code fcode in - fun_code := [Ksequence(fcode,!fun_code)]; + fun_code := Ksequence fcode :: !fun_code; (* Compilation of the branches *) let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = @@ -700,6 +686,7 @@ let rec compile_lam env cenv lam sz cont = | _ -> assert false in + let cont = discard_dead_code cont in let c = ref cont in (* Perform the extra match if needed (too many block constructors) *) if neblock <> 0 then begin @@ -770,7 +757,7 @@ let rec compile_lam env cenv lam sz cont = let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in comp_args (compile_lam env) cenv args sz cont - | Lprim (Some (kn,u), op, args) when is_caml_prim op -> + | Lprim ((kn,u), op, args) when is_caml_prim op -> let arity = CPrimitives.arity op in let nparams = CPrimitives.nparams op in let nargs = arity - nparams in @@ -788,7 +775,7 @@ let rec compile_lam env cenv lam sz cont = if Int.equal nparams 0 then cont else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) in - fun_code := [Ksequence(default, !fun_code)]; + fun_code := Ksequence default :: !fun_code; comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) | Lprim (kn, op, args) -> @@ -878,7 +865,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = ensure_stack_capacity (compile_lam env r_fun body full_arity) [Kreturn full_arity] in - fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; + fun_code := Ksequence (add_grab full_arity lbl_fun cont_fun) :: !fun_code; let fv = fv r_fun in let init_code = ensure_stack_capacity (compile_fv cenv fv.fv_rev 0) diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index babc57794b..c1d8fcb855 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -208,14 +208,6 @@ let slot_for_caml_prim env op = (* Emission of one instruction *) -let nocheck_prim_op = function - | Int63add -> opADDINT63 - | Int63sub -> opSUBINT63 - | Int63lt -> opLTINT63 - | Int63le -> opLEINT63 - | _ -> assert false - - let check_prim_op = function | Int63head0 -> opCHECKHEAD0INT63 | Int63tail0 -> opCHECKTAIL0INT63 @@ -259,11 +251,20 @@ let check_prim_op = function | Float64ldshiftexp -> opCHECKLDSHIFTEXP | Float64next_up -> opCHECKNEXTUPFLOAT | Float64next_down -> opCHECKNEXTDOWNFLOAT - | Arraymake -> opISINT_CAML_CALL2 - | Arrayget -> opISARRAY_INT_CAML_CALL2 - | Arrayset -> opISARRAY_INT_CAML_CALL3 + | Arraymake -> opCHECKCAMLCALL2_1 + | Arrayget -> opCHECKCAMLCALL2 + | Arrayset -> opCHECKCAMLCALL3_1 | Arraydefault | Arraycopy | Arraylength -> - opISARRAY_CAML_CALL1 + opCHECKCAMLCALL1 + +let inplace_prim_op = function + | Float64next_up | Float64next_down -> true + | _ -> false + +let check_prim_op_inplace = function + | Float64next_up -> opCHECKNEXTUPFLOATINPLACE + | Float64next_down -> opCHECKNEXTDOWNFLOATINPLACE + | _ -> assert false let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -354,10 +355,7 @@ let emit_instr env = function | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size | Kbranch lbl -> out env opBRANCH; out_label env lbl - | Kprim (op,None) -> - out env (nocheck_prim_op op) - - | Kprim(op,Some (q,_u)) -> + | Kprim (op, (q,_u)) -> out env (check_prim_op op); slot_for_getglobal env q @@ -366,13 +364,8 @@ let emit_instr env = function out_label env lbl; slot_for_caml_prim env op - | Kareint 1 -> out env opISINT - | Kareint 2 -> out env opAREINT2; - | Kstop -> out env opSTOP - | Kareint _ -> assert false - (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) let rec emit env insns remaining = match insns with @@ -406,8 +399,14 @@ let rec emit env insns remaining = match insns with emit env c remaining | Kpop n :: Kjump :: c -> out env opRETURN; out_int env n; emit env c remaining - | Ksequence(c1,c2)::c -> - emit env c1 (c2::c::remaining) + | Ksequence c1 :: c -> + emit env c1 (c :: remaining) + | Kprim (op1, (q1, _)) :: Kprim (op2, (q2, _)) :: c when inplace_prim_op op2 -> + out env (check_prim_op op1); + slot_for_getglobal env q1; + out env (check_prim_op_inplace op2); + slot_for_getglobal env q2; + emit env c remaining (* Default case *) | instr :: c -> emit_instr env instr; emit env c remaining diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 332a331a7a..9cca204e8c 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -19,10 +19,8 @@ type lambda = | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of pconstant - | Lprim of pconstant option * CPrimitives.t * lambda array - (* No check if None *) + | Lprim of pconstant * CPrimitives.t * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int @@ -112,10 +110,6 @@ let rec pp_lam lam = pp_names ids ++ str " => " ++ pp_lam c) (Array.to_list branches.nonconstant_branches))) ++ cut() ++ str "end") - | Lif (t, bt, bf) -> - v 0 (str "(if " ++ pp_lam t ++ - cut () ++ str "then " ++ pp_lam bt ++ - cut() ++ str "else " ++ pp_lam bf ++ str ")") | Lfix((t,i),(lna,tl,bl)) -> let fixl = Array.mapi (fun i id -> (id,t.(i),tl.(i),bl.(i))) lna in hov 1 @@ -148,16 +142,11 @@ let rec pp_lam lam = | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim(Some (kn,_u),_op,args) -> + | Lprim ((kn,_u),_op,args) -> hov 1 (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") - | Lprim(None,op,args) -> - hov 1 - (str "(PRIM_NC " ++ str (CPrimitives.to_string op) ++ spc() ++ - prlist_with_sep spc pp_lam (Array.to_list args) ++ - str")") | Lproj(p,arg) -> hov 1 (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg @@ -237,11 +226,6 @@ let map_lam_with_binders g f n lam = in if t == t' && a == a' && branches == branches' then lam else Lcase(ci,rtbl,t',a',branches') - | Lif(t,bt,bf) -> - let t' = f n t in - let bt' = f n bt in - let bf' = f n bf in - if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf') | Lfix(init,(ids,ltypes,lbodies)) -> let ltypes' = Array.Smart.map (f n) ltypes in let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in @@ -312,28 +296,6 @@ let can_subst lam = | Lval _ | Lsort _ | Lind _ -> true | _ -> false - -let can_merge_if bt bf = - match bt, bf with - | Llam(_idst,_), Llam(_idsf,_) -> true - | _ -> false - -let merge_if t bt bf = - let (idst,bodyt) = decompose_Llam bt in - let (idsf,bodyf) = decompose_Llam bf in - let nt = Array.length idst in - let nf = Array.length idsf in - let common,idst,idsf = - if nt = nf then idst, [||], [||] - else - if nt < nf then idst,[||], Array.sub idsf nt (nf - nt) - else idsf, Array.sub idst nf (nt - nf), [||] in - Llam(common, - Lif(lam_lift (Array.length common) t, - mkLlam idst bodyt, - mkLlam idsf bodyf)) - - let rec simplify subst lam = match lam with | Lrel(id,i) -> lam_subst_rel lam id i subst @@ -352,14 +314,6 @@ let rec simplify subst lam = | lam' -> lam' end - | Lif(t,bt,bf) -> - let t' = simplify subst t in - let bt' = simplify subst bt in - let bf' = simplify subst bf in - if can_merge_if bt' bf' then merge_if t' bt' bf' - else - if t == t' && bt == bt' && bf == bf' then lam - else Lif(t',bt',bf') | _ -> map_lam_with_binders liftn simplify subst lam and simplify_app substf f substa args = @@ -442,9 +396,6 @@ let rec occurrence k kind lam = in Array.iter on_b branches.nonconstant_branches; !r - | Lif (t, bt, bf) -> - let kind = occurrence k kind t in - kind && occurrence k kind bt && occurrence k kind bf | Lfix(_,(ids,ltypes,lbodies)) | Lcofix(_,(ids,ltypes,lbodies)) -> let kind = occurrence_args k kind ltypes in @@ -566,7 +517,7 @@ let rec get_alias env kn = (* Compilation of primitive *) let prim kn p args = - Lprim(Some kn, p, args) + Lprim (kn, p, args) let expand_prim kn op arity = (* primitives are always Relevant *) diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli index bd11c2667f..ad5f81638f 100644 --- a/kernel/vmlambda.mli +++ b/kernel/vmlambda.mli @@ -12,10 +12,8 @@ type lambda = | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of pconstant - | Lprim of pconstant option * CPrimitives.t * lambda array - (* No check if None *) + | Lprim of pconstant * CPrimitives.t * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches - | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 7b4101b9d0..9944458d6b 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -381,7 +381,15 @@ let rec whd_accu a stk = CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") -external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" +[@@@warning "-37"] +type vm_closure_kind = + | VCfun (** closure, or fixpoint applied past the recursive argument *) + | VCfix (** unapplied fixpoint *) + | VCfix_partial (** partially applied fixpoint, but not sufficiently for recursion *) + | VCaccu (** accumulator *) +[@@@warning "+37"] + +external kind_of_closure : Obj.t -> vm_closure_kind = "coq_kind_of_closure" external is_accumulate : tcode -> bool = "coq_is_accumulate_code" external int_tcode : tcode -> int -> int = "coq_int_tcode" external accumulate : unit -> tcode = "accumulate_code" @@ -400,12 +408,11 @@ let whd_val (v: values) = else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then whd_accu o [] else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) + match kind_of_closure o with + | VCfun -> Vfun (Obj.obj o) + | VCfix -> Vfix (Obj.obj o, None) + | VCfix_partial -> Vfix (Obj.obj (Obj.field o 2), Some (Obj.obj o)) + | VCaccu -> Vatom_stk (Aid (RelKey (int_tcode (fun_code o) 1)), []) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 236de65462..072206c39c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -234,9 +234,7 @@ GRAMMAR EXTEND Gram ; occs_nums: [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl } - | "-"; n = nat_or_var; nl = LIST0 int_or_var -> - (* have used int_or_var instead of nat_or_var for compatibility *) - { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ] + | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ] ; occs: [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] @@ -379,9 +377,11 @@ GRAMMAR EXTEND Gram { {onhyps=None; concl_occs=occs} } | "*"; "|-"; occs=concl_occ -> { {onhyps=None; concl_occs=occs} } - | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> + | "|-"; occs=concl_occ -> + { {onhyps=Some []; concl_occs=occs} } + | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ -> { {onhyps=Some hl; concl_occs=occs} } - | hl=LIST0 hypident_occ SEP"," -> + | hl = LIST1 hypident_occ SEP "," -> { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ] ; clause_dft_concl: diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 9c75175889..292fbefb84 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -71,7 +71,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") + CErrors.user_err ~hdr:"lookup_map" (str"Map "++qs map++str"not found") let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in @@ -135,15 +135,11 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" (****************************************************************************) -let ic c = - let env = Global.env() in - let sigma = Evd.from_env env in +let ic env sigma c = let c, uctx = Constrintern.interp_constr env sigma c in (Evd.from_ctx uctx, c) -let ic_unsafe c = (*FIXME remove *) - let env = Global.env() in - let sigma = Evd.from_env env in +let ic_unsafe env sigma c = (*FIXME remove *) fst (Constrintern.interp_constr env sigma c) let decl_constant name univs c = @@ -170,8 +166,8 @@ let dummy_goal env sigma = Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in {Evd.it = gl; Evd.sigma = sigma} -let constr_of evd v = match Value.to_constr v with - | Some c -> EConstr.to_constr evd c +let constr_of sigma v = match Value.to_constr v with + | Some c -> EConstr.to_constr sigma c | None -> failwith "Ring.exec_tactic: anomaly" let tactic_res = ref [||] @@ -189,7 +185,7 @@ let get_res = Tacenv.register_ml_tactic name [| tac |]; entry -let exec_tactic env evd n f args = +let exec_tactic env sigma n f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in let x = Reference (ArgVar CAst.(make id)) in @@ -203,11 +199,11 @@ let exec_tactic env evd n f args = let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (* Evaluate the whole result *) - let gl = dummy_goal env evd in + let gl = dummy_goal env sigma in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd = Evd.minimize_universes gls.Evd.sigma in - let nf c = constr_of evd c in - Array.map nf !tactic_res, Evd.universe_context_set evd + let sigma = Evd.minimize_universes gls.Evd.sigma in + let nf c = constr_of sigma c in + Array.map nf !tactic_res, Evd.universe_context_set sigma let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))) let gen_reference n = lazy (Coqlib.lib_ref n) @@ -222,10 +218,9 @@ let coq_nil = gen_reference "core.list.nil" let lapp f args = mkApp(Lazy.force f,args) -let plapp evdref f args = - let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in - evdref := evd; - mkApp(fc,args) +let plapp sigma f args = + let sigma, fc = Evarutil.new_global sigma (Lazy.force f) in + sigma, mkApp(fc,args) let dest_rel0 sigma t = match EConstr.kind sigma t with @@ -351,14 +346,14 @@ let find_ring_structure env sigma l = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then CErrors.user_err ~hdr:"ring" - (str"arguments of ring_simplify do not have all the same type") + (str"Arguments of ring_simplify do not have all the same type.") in List.iter check cl'; (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> CErrors.user_err ~hdr:"ring" - (str"cannot find a declared ring structure over"++ - spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) + (str"Cannot find a declared ring structure over"++ + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\".")) | [] -> assert false let add_entry e = @@ -411,16 +406,14 @@ let theory_to_obj : ring_info -> obj = ~cache:cache_th ~subst:(Some subst_th) -let setoid_of_relation env evd a r = +let setoid_of_relation env sigma a r = try - let evm = !evd in - let evm, refl = Rewrite.get_reflexive_proof env evm a r in - let evm, sym = Rewrite.get_symmetric_proof env evm a r in - let evm, trans = Rewrite.get_transitive_proof env evm a r in - evd := evm; - lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] + let sigma, refl = Rewrite.get_reflexive_proof env sigma a r in + let sigma, sym = Rewrite.get_symmetric_proof env sigma a r in + let sigma, trans = Rewrite.get_transitive_proof env sigma a r in + sigma, lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] with Not_found -> - error "cannot find setoid relation" + CErrors.user_err (str "Cannot find a setoid structure for relation " ++ pr_econstr_env env sigma r ++ str ".") let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] @@ -428,61 +421,59 @@ let op_morph r add mul opp req m1 m2 m3 = let op_smorph r add mul req m1 m2 = lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |] -let ring_equality env evd (r,add,mul,opp,req) = - match EConstr.kind !evd req with - | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let setoid = plapp evd coq_eq_setoid [|r|] in - let op_morph = +let ring_equality env sigma (r,add,mul,opp,req) = + match EConstr.kind sigma req with + | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) -> + let sigma, setoid = plapp sigma coq_eq_setoid [|r|] in + let sigma, op_morph = match opp with - Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] - | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let sigma = !evd in + Some opp -> plapp sigma coq_eq_morph [|r;add;mul;opp|] + | None -> plapp sigma coq_eq_smorph [|r;add;mul|] in let sigma, setoid = Typing.solve_evars env sigma setoid in let sigma, op_morph = Typing.solve_evars env sigma op_morph in - evd := sigma; (setoid,op_morph) | _ -> - let setoid = setoid_of_relation (Global.env ()) evd r req in + let sigma, setoid = setoid_of_relation env sigma r req in let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in let add_m, add_m_lem = try Rewrite.default_morphism signature add with Not_found -> - error "ring addition should be declared as a morphism" in + CErrors.user_err (str "Ring addition " ++ pr_econstr_env env sigma add ++ str " should be declared as a morphism.") in let mul_m, mul_m_lem = try Rewrite.default_morphism signature mul with Not_found -> - error "ring multiplication should be declared as a morphism" in + CErrors.user_err (str "Ring multiplication " ++ pr_econstr_env env sigma mul ++ str " should be declared as a morphism.") in let op_morph = match opp with | Some opp -> (let opp_m,opp_m_lem = try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp with Not_found -> - error "ring opposite should be declared as a morphism" in + CErrors.user_err (str "Ring opposite " ++ pr_econstr_env env sigma opp ++ str " should be declared as a morphism.") in let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ - str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ - str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ - str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env sigma req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env sigma add_m ++ + str"\","++spc()++ str"\""++pr_econstr_env env sigma mul_m++ + str"\""++spc()++str"and \""++pr_econstr_env env sigma opp_m++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env sigma req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env sigma add_m ++ str"\""++spc()++str"and \""++ - pr_econstr_env env !evd mul_m_lem++str"\""); + pr_econstr_env env sigma mul_m++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) -let build_setoid_params env evd r add mul opp req eqth = +let build_setoid_params env sigma r add mul opp req eqth = match eqth with Some th -> th - | None -> ring_equality env evd (r,add,mul,opp,req) + | None -> ring_equality env sigma (r,add,mul,opp,req) let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in @@ -515,71 +506,69 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in TacArg(CAst.make (TacCall(CAst.make (t,[])))) -let make_hyp env evd c = - let t = Retyping.get_type_of env !evd c in - plapp evd coq_mkhypo [|t;c|] +let make_hyp env sigma c = + let t = Retyping.get_type_of env sigma c in + plapp sigma coq_mkhypo [|t;c|] -let make_hyp_list env evdref lH = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; - let l = +let make_hyp_list env sigma lH = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in + let sigma, l = List.fold_right - (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH - (plapp evdref coq_nil [|carrier|]) + (fun c (sigma,l) -> + let sigma, c = make_hyp env sigma c in + plapp sigma coq_cons [|carrier; c; l|]) lH + (plapp sigma coq_nil [|carrier|]) in - let sigma, l' = Typing.solve_evars env !evdref l in - evdref := sigma; + let sigma, l' = Typing.solve_evars env sigma l in let l' = EConstr.Unsafe.to_constr l' in - Evarutil.nf_evars_universes !evdref l' + sigma, Evarutil.nf_evars_universes sigma l' -let interp_power env evdref pow = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; +let interp_power env sigma pow = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in match pow with | None -> let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in - (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|]) + let sigma, c = plapp sigma coq_None [|carrier|] in + sigma, (TacArg(CAst.make (TacCall(CAst.make (t,[])))), c) | Some (tac, spec) -> let tac = match tac with | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env evdref (ic_unsafe spec) in - (tac, plapp evdref coq_Some [|carrier; spec|]) + let spec = ic_unsafe env sigma spec in + let sigma, spec = make_hyp env sigma spec in + let sigma, pow = plapp sigma coq_Some [|carrier; spec|] in + sigma, (tac, pow) -let interp_sign env evdref sign = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; +let interp_sign env sigma sign = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in match sign with - | None -> plapp evdref coq_None [|carrier|] + | None -> plapp sigma coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evdref (ic_unsafe spec) in - plapp evdref coq_Some [|carrier;spec|] + let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in + plapp sigma coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let interp_div env evdref div = - let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in - evdref := evd; +let interp_div env sigma div = + let sigma, carrier = Evarutil.new_global sigma (Lazy.force coq_hypo) in match div with - | None -> plapp evdref coq_None [|carrier|] + | None -> plapp sigma coq_None [|carrier|] | Some spec -> - let spec = make_hyp env evdref (ic_unsafe spec) in - plapp evdref coq_Some [|carrier;spec|] + let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in + plapp sigma coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div = +let add_theory0 env sigma name rth eqth morphth cst_tac (pre,post) power sign div = check_required_library (cdir@["Ring_base"]); - let env = Global.env() in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in - let evd = ref sigma in - let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in - let (pow_tac, pspec) = interp_power env evd power in - let sspec = interp_sign env evd sign in - let dspec = interp_div env evd div in + let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in + let sigma, (pow_tac, pspec) = interp_power env sigma power in + let sigma, sspec = interp_sign env sigma sign in + let sigma, dspec = interp_div env sigma div in let rk = reflect_coeff morphth in let params,ctx = - exec_tactic env !evd 5 (zltac "ring_lemmas") + exec_tactic env sigma 5 (zltac "ring_lemmas") [sth;ext;rth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in @@ -619,16 +608,16 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div ring_post_tac = posttac }) in () -let ic_coeff_spec = function - | Computational t -> Computational (ic_unsafe t) - | Morphism t -> Morphism (ic_unsafe t) +let ic_coeff_spec env sigma = function + | Computational t -> Computational (ic_unsafe env sigma t) + | Morphism t -> Morphism (ic_unsafe env sigma t) | Abstract -> Abstract let set_once s r v = if Option.is_empty !r then r := Some v else error (s^" cannot be set twice") -let process_ring_mods l = +let process_ring_mods env sigma l = let kind = ref None in let set = ref None in let cst_tac = ref None in @@ -638,11 +627,11 @@ let process_ring_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k) + Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec env sigma k) | Const_tac t -> set_once "tactic recognizing constants" cst_tac t | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) + | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext) | Pow_spec(t,spec) -> set_once "power" power (t,spec) | Sign_spec t -> set_once "sign" sign t | Div_spec t -> set_once "div" div t) l; @@ -650,9 +639,11 @@ let process_ring_mods l = (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) let add_theory id rth l = - let (sigma, rth) = ic rth in - let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in - add_theory0 id (sigma, rth) set k cst (pre,post) power sign div + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, rth = ic env sigma rth in + let (k,set,cst,pre,post,power,sign, div) = process_ring_mods env sigma l in + add_theory0 env sigma id rth set k cst (pre,post) power sign div (*****************************************************************************) (* The tactics consist then only in a lookup in the ring database and @@ -663,13 +654,12 @@ let make_args_list sigma rl t = | [] -> let (_,t1,t2) = dest_rel0 sigma t in [t1;t2] | _ -> rl -let make_term_list env evd carrier rl = - let l = List.fold_right - (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl - (plapp evd coq_nil [|carrier|]) +let make_term_list env sigma carrier rl = + let sigma, l = List.fold_right + (fun x (sigma,l) -> plapp sigma coq_cons [|carrier;x;l|]) rl + (plapp sigma coq_nil [|carrier|]) in - let sigma, l = Typing.solve_evars env !evd l in - evd := sigma; l + Typing.solve_evars env sigma l let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c) let tacarg expr = @@ -695,12 +685,13 @@ let ring_lookup (f : Value.t) lH rl t = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let rl = make_args_list sigma rl t in - let evdref = ref sigma in let e = find_ring_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in + let sigma, l = make_term_list env sigma (EConstr.of_constr e.ring_carrier) rl in + let rl = Value.of_constr l in + let sigma, l = make_hyp_list env sigma lH in + let lH = carg l in let ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (ring@[lH;rl])) end (***********************************************************************) @@ -758,23 +749,23 @@ let sfield_theory = my_reference "semi_field_theory" let af_ar = my_reference"AF_AR" let f_r = my_reference"F_R" let sf_sr = my_reference"SF_SR" -let dest_field env evd th_spec = - let th_typ = Retyping.get_type_of env !evd th_spec in - match EConstr.kind !evd th_typ with +let dest_field env sigma th_spec = + let th_typ = Retyping.get_type_of env sigma th_spec in + match EConstr.kind sigma th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when isRefX !evd (Lazy.force afield_theory) f -> - let rth = plapp evd af_ar + when isRefX sigma (Lazy.force afield_theory) f -> + let sigma, rth = plapp sigma af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when isRefX !evd (Lazy.force field_theory) f -> - let rth = - plapp evd f_r + when isRefX sigma (Lazy.force field_theory) f -> + let sigma, rth = + plapp sigma f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when isRefX !evd (Lazy.force sfield_theory) f -> - let rth = plapp evd sf_sr + when isRefX sigma (Lazy.force sfield_theory) f -> + let sigma, rth = plapp sigma sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" @@ -804,14 +795,14 @@ let find_field_structure env sigma l = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then CErrors.user_err ~hdr:"field" - (str"arguments of field_simplify do not have all the same type") + (str"Arguments of field_simplify do not have all the same type.") in List.iter check cl'; (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> CErrors.user_err ~hdr:"field" - (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) + (str"Cannot find a declared field structure over"++ + spc()++str"\""++pr_econstr_env env sigma ty++str"\".")) | [] -> assert false let add_field_entry e = @@ -860,14 +851,14 @@ let ftheory_to_obj : field_info -> obj = ~cache:cache_th ~subst:(Some subst_th) -let field_equality evd r inv req = - match EConstr.kind !evd req with - | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> +let field_equality env sigma r inv req = + match EConstr.kind sigma req with + | App (f, [| _ |]) when eq_constr_nounivs sigma f (Lazy.force coq_eq) -> let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> - let _setoid = setoid_of_relation (Global.env ()) evd r req in + let _setoid = setoid_of_relation env sigma r req in let signature = [Some (r,Some req)],Some(r,Some req) in let inv_m, inv_m_lem = try Rewrite.default_morphism signature inv @@ -875,24 +866,22 @@ let field_equality evd r inv req = error "field inverse should be declared as a morphism" in inv_m_lem -let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv = +let add_field_theory0 env sigma name fth eqth morphth cst_tac inj (pre,post) power sign odiv = let open Constr in check_required_library (cdir@["Field_tac"]); - let (sigma,fth) = ic fth in - let env = Global.env() in - let evd = ref sigma in + let (sigma,fth) = ic env sigma fth in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = - dest_field env evd fth in - let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in + dest_field env sigma fth in + let (sth,ext) = build_setoid_params env sigma r add mul opp req eqth in let eqth = Some(sth,ext) in - let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in - let (pow_tac, pspec) = interp_power env evd power in - let sspec = interp_sign env evd sign in - let dspec = interp_div env evd odiv in - let inv_m = field_equality evd r inv req in + let _ = add_theory0 env sigma name rth eqth morphth cst_tac (None,None) power sign odiv in + let sigma, (pow_tac, pspec) = interp_power env sigma power in + let sigma, sspec = interp_sign env sigma sign in + let sigma, dspec = interp_div env sigma odiv in + let inv_m = field_equality env sigma r inv req in let rk = reflect_coeff morphth in let params,ctx = - exec_tactic env !evd 9 (field_ltac"field_lemmas") + exec_tactic env sigma 9 (field_ltac"field_lemmas") [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in let lemma1 = params.(3) in let lemma2 = params.(4) in @@ -940,7 +929,7 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od field_pre_tac = pretac; field_post_tac = posttac }) in () -let process_field_mods l = +let process_field_mods env sigma l = let kind = ref None in let set = ref None in let cst_tac = ref None in @@ -951,22 +940,24 @@ let process_field_mods l = let power = ref None in let div = ref None in List.iter(function - Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k) + Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec env sigma k) | Ring_mod(Const_tac t) -> set_once "tactic recognizing constants" cst_tac t | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t - | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) + | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext) | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) | Ring_mod(Sign_spec t) -> set_once "sign" sign t | Ring_mod(Div_spec t) -> set_once "div" div t - | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l; + | Inject i -> set_once "infinite property" inj (ic_unsafe env sigma i)) l; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) + (env, sigma, k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) let add_field_theory id t mods = - let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in - add_field_theory0 id t set k cst_tac inj (pre,post) power sign div + let env = Global.env () in + let sigma = Evd.from_env env in + let (env,sigma,k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods env sigma mods in + add_field_theory0 env sigma id t set k cst_tac inj (pre,post) power sign div let ltac_field_structure e = let req = carg e.field_req in @@ -987,10 +978,11 @@ let field_lookup (f : Value.t) lH rl t = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let rl = make_args_list sigma rl t in - let evdref = ref sigma in let e = find_field_structure env sigma rl in - let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in - let lH = carg (make_hyp_list env evdref lH) in + let sigma, c = make_term_list env sigma (EConstr.of_constr e.field_carrier) rl in + let rl = Value.of_constr c in + let sigma, l = make_hyp_list env sigma lH in + let lH = carg l in let field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (field@[lH;rl])) end diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index bd514f15d5..a4aa08300d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = - List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in + List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 00d4c7b3d8..cdf2922516 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -244,24 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then - lookup_canonical_conversion (proji, Prod_cs), + lookup_canonical_conversion env (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> let s = ESorts.kind sigma s in - lookup_canonical_conversion + lookup_canonical_conversion env (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> - let c2 = GlobRef.ConstRef (Projection.constant p) in - let c = Retyping.expand_projection env sigma p c [] in - let _, args = destApp sigma c in - let sk2 = Stack.append_app args sk2 in - lookup_canonical_conversion (proji, Const_cs c2), sk2 + lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2 | _ -> let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in - lookup_canonical_conversion (proji, Const_cs c2),sk2 + lookup_canonical_conversion env (proji, Const_cs c2),sk2 with Not_found -> - let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in + let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in (c,cs),[] in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; @@ -273,6 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = + (* Are we sure that ty is not an evar? *) try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e6e5ad8dd4..b6e44265ae 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,19 +144,21 @@ type obj_typ = { type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs -let eq_cs_pattern p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2 +let eq_cs_pattern env p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2 +| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true | _ -> false -let rec assoc_pat a = function - | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs +let rec assoc_pat env a = function + | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs | [] -> raise Not_found @@ -179,10 +181,7 @@ let rec cs_pattern_of_constr env t = patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> - let ty = Retyping.get_type_of_constr env c in - let _, params = Inductive.find_rectype env ty in - Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] + | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] @@ -238,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let pr_cs_pattern = function Const_cs c -> Nametab.pr_global_env Id.Set.empty c + | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p)) | Prod_cs -> str "_ -> _" | Default_cs -> str "_" | Sort_cs s -> Sorts.pr_sort_family s @@ -253,7 +253,7 @@ let register_canonical_structure ~warn env sigma o = compute_canonical_projections env ~warn o |> List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in - match assoc_pat cs_pat l with + match assoc_pat env cs_pat l with | exception Not_found -> object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table | _, cs -> @@ -320,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref = error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (ref,indsp) -let lookup_canonical_conversion (proj,pat) = - assoc_pat pat (GlobRef.Map.find proj !object_table) +let lookup_canonical_conversion env (proj,pat) = + assoc_pat env pat (GlobRef.Map.find proj !object_table) let decompose_projection sigma c args = match EConstr.kind sigma c with diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3be60d5e62..5b8dc8184a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t type cs = GlobRef.t * inductive -val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 4bd22e76cb..34bcd0982c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t = | _ -> raise Not_found else raise Not_found +let sort_of_arity_with_constraints env sigma t = + try Reductionops.sort_of_arity env sigma t + with Reduction.NotArity -> + try + let t = get_type_from_constraints env sigma t in + Reductionops.sort_of_arity env sigma t + with Not_found | Reduction.NotArity -> retype_error NotAnArity + let rec subst_type env sigma typ = function | [] -> typ | h::rest -> @@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma = let mip = lookup_mind_specif env ind in let paramtyps = Array.map_to_list (fun arg () -> let t = type_of env arg in - let s = try Reductionops.sort_of_arity env sigma t - with Reduction.NotArity -> retype_error NotAnArity - in + let s = sort_of_arity_with_constraints env sigma t in Sorts.univ_of_sort (ESorts.kind sigma s)) args in diff --git a/stm/stm.ml b/stm/stm.ml index df7e35beb5..f7d66b7b53 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1003,9 +1003,9 @@ end = struct (* {{{ *) end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) -let stm_qed_delay_proof ?route ~proof ~pinfo ~id ~st ~loc ~control pending : Vernacstate.t = +let stm_qed_delay_proof ?route ~proof ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacinterp.interp_qed_delayed_proof ~proof ~pinfo ~st ~control (CAst.make ?loc pending) + Vernacinterp.interp_qed_delayed_proof ~proof ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly @@ -1470,16 +1470,15 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _info = + let pobject = PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in let st = Vernacstate.freeze_interp_state ~marshallable:false in let opaque = Opaque in try let _pstate = - let pinfo = Declare.Proof.Proof_info.default () in stm_qed_delay_proof ~st ~id:stop - ~proof:pobject ~pinfo ~loc ~control:[] (Proved (opaque,None)) in + ~proof:pobject ~loc ~control:[] (Proved (opaque,None)) in () with exn -> (* If [stm_qed_delay_proof] fails above we need to use the @@ -1621,12 +1620,9 @@ end = struct (* {{{ *) else begin let opaque = Opaque in - (* The original terminator, a hook, has not been saved in the .vio*) - let proof, _info = + let proof = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in - let pinfo = Declare.Proof.Proof_info.default () in - (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1638,7 +1634,7 @@ end = struct (* {{{ *) *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~pinfo ~loc ~control:[] (Proved (opaque,None))); + ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~loc ~control:[] (Proved (opaque,None))); (* Is this name the same than the one in scope? *) let name = Declare.Proof.get_po_name proof in `OK name @@ -2219,13 +2215,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeepDefined -> CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.") in - let proof, pinfo = + let proof = PG_compat.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in let control, pe = extract_pe x in - ignore(stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe); + ignore(stm_qed_delay_proof ~id ~st ~proof ~loc ~control pe); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; @@ -2264,9 +2260,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Vernacstate.freeze_interp_state ~marshallable:false in let _st = match proof with | None -> stm_vernac_interp id st x - | Some (proof, pinfo) -> + | Some proof -> let control, pe = extract_pe x in - stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe + stm_qed_delay_proof ~id ~st ~proof ~loc ~control pe in let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time" diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v new file mode 100644 index 0000000000..06f7ddbd3a --- /dev/null +++ b/test-suite/bugs/closed/bug_13249.v @@ -0,0 +1,9 @@ +Global Generalizable All Variables. + +Section test. + Context {A : Type}. + Context `{!foo A}. + + Goal foo A. + Proof. assumption. Defined. +End test. diff --git a/test-suite/bugs/closed/bug_13300.v b/test-suite/bugs/closed/bug_13300.v new file mode 100644 index 0000000000..e4fcd6dacc --- /dev/null +++ b/test-suite/bugs/closed/bug_13300.v @@ -0,0 +1,7 @@ +Polymorphic Definition type := Type. + +Inductive bad : type := . + +Fail Check bad : Prop. +Check bad : Set. +(* lowered as much as possible *) diff --git a/test-suite/bugs/closed/bug_13366.v b/test-suite/bugs/closed/bug_13366.v new file mode 100644 index 0000000000..06918a9266 --- /dev/null +++ b/test-suite/bugs/closed/bug_13366.v @@ -0,0 +1,5 @@ +Class Functor (F : Type -> Type) : Type := + fmap : F nat. + +Fail Definition blah := sum fmap. +(* used to be anomaly not an arity *) diff --git a/test-suite/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v new file mode 100644 index 0000000000..4a7d2c7fac --- /dev/null +++ b/test-suite/bugs/closed/bug_9809.v @@ -0,0 +1,30 @@ +Section FreeMonad. + + Variable S : Type. + Variable P : S -> Type. + + Inductive FreeF A : Type := + | retFree : A -> FreeF A + | opr : forall s, (P s -> FreeF A) -> FreeF A. + +End FreeMonad. + +Section Fibonnacci. + + Inductive gen_op := call_op : nat -> gen_op. + Definition gen_ty (op : gen_op) := + match op with + | call_op _ => nat + end. + + Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat := + match n with + | 0 + | 1 => retFree _ _ _ 1 + | S (S k) => + opr _ _ _ (call_op (S k)) + (fun r1 => opr _ _ _ (call_op k) + (fun r0 => retFree (* _ _ _ *) (r1 + r0))) + end. + +End Fibonnacci. diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v new file mode 100644 index 0000000000..ef526dcd7d --- /dev/null +++ b/test-suite/bugs/closed/bug_9971.v @@ -0,0 +1,27 @@ +(* Test that it raises a normal error and not an anomaly *) +Set Primitive Projections. +Record prod A B := pair { fst : A ; snd : B }. +Arguments fst {A B} _. +Arguments snd {A B} _. +Arguments pair {A B} _ _. +Record piis := { dep_types : Type; indep_args : dep_types -> Type }. +Import EqNotations. +Goal forall (id : Set) (V : id) (piiio : id -> piis) + (Z : {ridc : id & prod (dep_types (piiio ridc)) True}) + (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}), + let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in + prod True (ida V (projT1 W)) -> + Z = existT _ V (pair (projT1 W) I) -> + ida (projT1 Z) (fst (projT2 Z)). + intros. + refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + _); + refine (snd X). + Undo. +Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + snd X). +Abort. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 623ca316c9..a9bed49922 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -120,14 +120,14 @@ where letpair x [1] = {0}; return (1, 2, 3, 4) : nat * nat * nat * nat -{{ 1 | 1 // 1 }} - : nat -!!! _ _ : nat, True - : (nat -> Prop) * ((nat -> Prop) * Prop) ((*1).2).3 : nat *(1.2) : nat +{{ 1 | 1 // 1 }} + : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) ! '{{x, y}}, x.y = 0 : Prop exists x : nat, diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index ce97d909a7..04a91c14d9 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := (let x:=a in ( .. (b0,b1) .., b2)). Check letpair x [1] = {0}; return (1,2,3,4). +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). + (* Test spacing in #5569 *) Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) @@ -191,13 +198,6 @@ Check 1+1+1. Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). Check !!! (x y:nat), True. -(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) - -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). -Check (((id 1) + 2) + 3). -Check (id (1 + 2)). - (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index a6fd39c29b..86c4b3cccc 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -179,3 +179,21 @@ Found an inductive type while a pattern was expected. : Prop !!!! (nat, id), nat = true /\ id = false : Prop +∀ x : nat, x = 0 + : Prop +∀₁ x, x = 0 + : Prop +∀₁ x, x = 0 + : Prop +∀₂ x y, x + y = 0 + : Prop +((1, 2)) + : nat * nat +%% [x == 1] + : Prop +%%% [1] + : Prop +[[2]] + : nat * nat +%%% + : Type diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 0731819bba..6af192ea82 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -414,3 +414,76 @@ Module P. End NotationBinderNotMixedWithTerms. End P. + +Module MorePrecise1. + +(* A notation with limited iteration is strictly more precise than a + notation with unlimited iteration *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Check forall x, x = 0. + +Notation "∀₁ z , P" := (forall z, P) + (at level 200, right associativity) : type_scope. + +Check forall x, x = 0. + +Notation "∀₂ y x , P" := (forall y x, P) + (at level 200, right associativity) : type_scope. + +Check forall x, x = 0. +Check forall x y, x + y = 0. + +Notation "(( x , y ))" := (x,y) : core_scope. + +Check ((1,2)). + +End MorePrecise1. + +Module MorePrecise2. + +(* Case of a bound binder *) +Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60). + +(* Case of an internal binder *) +Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0). + +(* Check that the two previous notations are indeed finer *) +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'"). +Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀' x .. y ']' , '/' P ']'"). + +Check %% [x == 1]. +Check %%% [1]. + +Notation "[[ x ]]" := (pair 1 x). + +Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z). +Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y). + +(* Check which is finer *) +Check [[ 2 ]]. + +End MorePrecise2. + +Module MorePrecise3. + +(* This is about a binder not bound in a notation being strictly more + precise than a binder bound in the notation (since the notation + applies - a priori - stricly less often) *) + +Notation "%%%" := (forall x, x) (at level 0). + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'"). + +Check %%%. + +End MorePrecise3. diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out new file mode 100644 index 0000000000..25572ee2aa --- /dev/null +++ b/test-suite/output/attributes.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +Attribute for canonical specified twice. +The command has indeed failed with message: +key 'polymorphic' has been already set. +The command has indeed failed with message: +Invalid value 'foo' for key polymorphic +use one of {yes, no} +The command has indeed failed with message: +Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead. +The command has indeed failed with message: +Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead. diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v new file mode 100644 index 0000000000..aef05e6cd4 --- /dev/null +++ b/test-suite/output/attributes.v @@ -0,0 +1,9 @@ +Fail #[canonical=yes, canonical=no] Definition a := 3. + +Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3. + +Fail #[universes(polymorphic=foo)] Definition a := 3. + +Fail #[universes(polymorphic(foo))] Definition a := 3. + +Fail #[universes(polymorphic(foo,bar))] Definition a := 3. diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out new file mode 100644 index 0000000000..4bc5aafbca --- /dev/null +++ b/test-suite/output/bug_10824.out @@ -0,0 +1,4 @@ +!! + : Prop +!! + : Prop diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v new file mode 100644 index 0000000000..01271f7d61 --- /dev/null +++ b/test-suite/output/bug_10824.v @@ -0,0 +1,12 @@ +Module A. +Notation F := False. +Notation "!!" := False (at level 100). +Check False. +End A. + +Module B. +Notation "!!" := False (at level 100). +Notation F := False. +Notation "!!" := False (at level 100). +Check False. +End B. diff --git a/test-suite/output/bug_7443.out b/test-suite/output/bug_7443.out new file mode 100644 index 0000000000..446ec6a1ad --- /dev/null +++ b/test-suite/output/bug_7443.out @@ -0,0 +1,13 @@ +Literal 1 + : Type +[1] + : Type +Literal 1 + : Type +[1] + : Type +The command has indeed failed with message: +The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". +Literal 1 + : Type diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v new file mode 100644 index 0000000000..33f76dbcfa --- /dev/null +++ b/test-suite/output/bug_7443.v @@ -0,0 +1,37 @@ +Inductive type := nat | bool. +Definition denote (t : type) + := match t with + | nat => Datatypes.nat + | bool => Datatypes.bool + end. +Ltac reify t := + lazymatch eval cbv beta in t with + | Datatypes.nat => nat + | Datatypes.bool => bool + end. +Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing). +Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing). +Axiom Literal : forall {t}, denote t -> Type. +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Open Scope foo_scope. +Section A. + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Literal 1 : Type *) (* as expected *) + Notation "[ x ]" := (Literal x) : foo_scope. + Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *) + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable: + #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *) +End A. +Section B. + Notation "[ x ]" := (Literal x) : foo_scope. + Check @Literal nat 1. (* [1] : Type *) + Fail Check [1]. (* As expected: The command has indeed failed with message: + The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". *) + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Should succeed, but instead fails with: Error: + The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *) +End B. diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out new file mode 100644 index 0000000000..2d474e4933 --- /dev/null +++ b/test-suite/output/bug_9569.out @@ -0,0 +1,16 @@ +1 subgoal + + ============================ + exists I : True, I = Logic.I +1 subgoal + + ============================ + f True False True False (Logic.True /\ Logic.False) +1 subgoal + + ============================ + [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I] +1 subgoal + + ============================ + [I & I = Logic.I | I = Logic.I; Logic.I = I] diff --git a/test-suite/output/bug_9569.v b/test-suite/output/bug_9569.v new file mode 100644 index 0000000000..ee5b052811 --- /dev/null +++ b/test-suite/output/bug_9569.v @@ -0,0 +1,18 @@ +Goal exists I, I = Logic.I. +Show. +Abort. + +Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r). +Goal f True False True False (Logic.True /\ Logic.False). +Show. +Abort. + +Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)). +Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ]. +Show. +Abort. + +Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..). +Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ]. +Show. +Abort. diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v index 4f8427dc5b..ea45fb3983 100644 --- a/test-suite/primitive/float/next_up_down.v +++ b/test-suite/primitive/float/next_up_down.v @@ -120,3 +120,46 @@ Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Pr Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). + +Check (eq_refl : next_up nan = nan). +Check (eq_refl : next_down nan = nan). +Check (eq_refl : next_up neg_infinity = -0x1.fffffffffffffp+1023). +Check (eq_refl : next_down neg_infinity = neg_infinity). +Check (eq_refl : next_up (-0x1.fffffffffffffp+1023) = -0x1.ffffffffffffep+1023). +Check (eq_refl : next_down (-0x1.fffffffffffffp+1023) = neg_infinity). +Check (eq_refl : next_up (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffff9p+1023). +Check (eq_refl : next_down (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffffbp+1023). +Check (eq_refl : next_up (-0x1.fffffffffffff) = -0x1.ffffffffffffe). +Check (eq_refl : next_down (-0x1.fffffffffffff) = -0x1p+1). +Check (eq_refl : next_up (-0x1p1) = -0x1.fffffffffffff). +Check (eq_refl : next_down (-0x1p1) = -0x1.0000000000001p+1). +Check (eq_refl : next_up (-0x1p-1022) = -0x0.fffffffffffffp-1022). +Check (eq_refl : next_down (-0x1p-1022) = -0x1.0000000000001p-1022). +Check (eq_refl : next_up (-0x0.fffffffffffffp-1022) = -0x0.ffffffffffffep-1022). +Check (eq_refl : next_down (-0x0.fffffffffffffp-1022) = -0x1p-1022). +Check (eq_refl : next_up (-0x0.01p-1022) = -0x0.00fffffffffffp-1022). +Check (eq_refl : next_down (-0x0.01p-1022) = -0x0.0100000000001p-1022). +Check (eq_refl : next_up (-0x0.0000000000001p-1022) = -0). +Check (eq_refl : next_down (-0x0.0000000000001p-1022) = -0x0.0000000000002p-1022). +Check (eq_refl : next_up (-0) = 0x0.0000000000001p-1022). +Check (eq_refl : next_down (-0) = -0x0.0000000000001p-1022). +Check (eq_refl : next_up 0 = 0x0.0000000000001p-1022). +Check (eq_refl : next_down 0 = -0x0.0000000000001p-1022). +Check (eq_refl : next_up 0x0.0000000000001p-1022 = 0x0.0000000000002p-1022). +Check (eq_refl : next_down 0x0.0000000000001p-1022 = 0). +Check (eq_refl : next_up 0x0.01p-1022 = 0x0.0100000000001p-1022). +Check (eq_refl : next_down 0x0.01p-1022 = 0x0.00fffffffffffp-1022). +Check (eq_refl : next_up 0x0.fffffffffffffp-1022 = 0x1p-1022). +Check (eq_refl : next_down 0x0.fffffffffffffp-1022 = 0x0.ffffffffffffep-1022). +Check (eq_refl : next_up 0x1p-1022 = 0x1.0000000000001p-1022). +Check (eq_refl : next_down 0x1p-1022 = 0x0.fffffffffffffp-1022). +Check (eq_refl : next_up 0x1p1 = 0x1.0000000000001p+1). +Check (eq_refl : next_down 0x1p1 = 0x1.fffffffffffff). +Check (eq_refl : next_up 0x1.fffffffffffff = 0x1p+1). +Check (eq_refl : next_down 0x1.fffffffffffff = 0x1.ffffffffffffe). +Check (eq_refl : next_up 0x1.ffffffffffffap+1023 = 0x1.ffffffffffffbp+1023). +Check (eq_refl : next_down 0x1.ffffffffffffap+1023 = 0x1.ffffffffffff9p+1023). +Check (eq_refl : next_up 0x1.fffffffffffffp+1023 = infinity). +Check (eq_refl : next_down 0x1.fffffffffffffp+1023 = 0x1.ffffffffffffep+1023). +Check (eq_refl : next_up infinity = infinity). +Check (eq_refl : next_down infinity = 0x1.fffffffffffffp+1023). diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index 656362b8fc..d11ae20b8d 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -37,7 +37,7 @@ Module Yes. End Yes. Module No. - #[universes(notemplate)] + #[universes(template=no)] Inductive Box (A:Type) : Type := box : A -> Box A. About Box. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index b403fc120c..b866c4b074 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -16,11 +16,16 @@ Definition ι T (x: T) := x. Check ι _ ι. +#[universes(polymorphic=no)] +Definition ιι T (x: T) := x. + +Fail Check ιι _ ιι. + #[program] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. -#[program(true)] +#[program=yes] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. @@ -43,3 +48,14 @@ Export Set Foo. Fail #[ export ] Export Foo. (* Attribute for Locality specified twice *) + +(* Tests for deprecated attribute syntax *) +Set Warnings "-deprecated-attribute-syntax". + +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + +#[universes(monomorphic)] +Definition ιιι T (x: T) := x. +Fail Check ιιι _ ιιι. diff --git a/theories/setoid_ring/Ring_tac.v b/theories/setoid_ring/Ring_tac.v index 76e9b1e947..9323ae23b9 100644 --- a/theories/setoid_ring/Ring_tac.v +++ b/theories/setoid_ring/Ring_tac.v @@ -41,7 +41,7 @@ Ltac Get_goal := match goal with [|- ?G] => G end. Ltac OnEquation req := match goal with | |- req ?lhs ?rhs => (fun f => f lhs rhs) - | _ => (fun _ => fail "Goal is not an equation (of expected equality)") + | _ => (fun _ => fail "Goal is not an equation (of expected equality)" req) end. Ltac OnEquationHyp req h := diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index b205965ed1..d1cefeb552 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -22,9 +22,10 @@ Require Import ssreflect ssrfun. is_true b == the coercion of b : bool to Prop (:= b = true). This is just input and displayed as `b''. reflect P b == the reflection inductive predicate, asserting - that the logical proposition P : prop with the - formula b : bool. Lemmas asserting reflect P b - are often referred to as "views". + that the logical proposition P : Prop holds iff + the formula b : bool is equal to true. Lemmas + asserting reflect P b are often referred to as + "views". iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection views: iffP is used to prove reflection from logical equivalence, appP to compose views, and @@ -33,7 +34,7 @@ Require Import ssreflect ssrfun. elimT :: coercion reflect >-> Funclass, which allows the direct application of `reflect' views to boolean assertions. - decidable P <-> P is effectively decidable (:= {P} + {~ P}. + decidable P <-> P is effectively decidable (:= {P} + {~ P}). contra, contraL, ... :: contraposition lemmas. altP my_viewP :: natural alternative for reflection; given lemma myviewP: reflect my_Prop my_formula, diff --git a/vernac/attributes.ml b/vernac/attributes.ml index efba6d332a..fdaeedef8c 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -11,13 +11,29 @@ open CErrors (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +let pr_vernac_flag_leaf = function + | FlagIdent b -> Pp.str b + | FlagString s -> Pp.(quote (str s)) + +let rec pr_vernac_flag_value = let open Pp in function + | VernacFlagEmpty -> mt () + | VernacFlagLeaf l -> str "=" ++ pr_vernac_flag_leaf l + | VernacFlagList s -> surround (prlist_with_sep pr_comma pr_vernac_flag s) +and pr_vernac_flag (s, arguments) = + let open Pp in + str s ++ (pr_vernac_flag_value arguments) + let warn_unsupported_attributes = CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError (fun atts -> @@ -105,16 +121,82 @@ let single_key_parser ~name ~key v prev args = assert_once ~name prev; v -let bool_attribute ~name ~on ~off : bool option attribute = - attribute_of_list [(on, single_key_parser ~name ~key:on true); - (off, single_key_parser ~name ~key:off false)] +let pr_possible_values ~values = + Pp.(str "{" ++ prlist_with_sep pr_comma str (List.map fst values) ++ str "}") + +(** [key_value_attribute ~key ~default ~values] parses a attribute [key=value] + with possible [key] [value] in [values], [default] is for compatibility for users + doing [qualif(key)] which is parsed as [qualif(key=default)] *) +let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option attribute = + let parser = function + | Some v -> + CErrors.user_err Pp.(str "key '" ++ str key ++ str "' has been already set.") + | None -> + begin function + | VernacFlagLeaf (FlagIdent b) -> + begin match CList.assoc_f String.equal b values with + | exception Not_found -> + CErrors.user_err + Pp.(str "Invalid value '" ++ str b ++ str "' for key " ++ str key ++ fnl () ++ + str "use one of " ++ pr_possible_values ~values) + | value -> value + end + | VernacFlagEmpty -> + default + | err -> + CErrors.user_err + Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try " + ++ str key ++ str "=" ++ pr_possible_values ~values ++ str " instead.") + end + in + attribute_of_list [key, parser] + +let bool_attribute ~name : bool option attribute = + let values = ["yes", true; "no", false] in + key_value_attribute ~key:name ~default:true ~values + +let legacy_bool_attribute ~name ~on ~off : bool option attribute = + attribute_of_list + [(on, single_key_parser ~name ~key:on true); + (off, single_key_parser ~name ~key:off false)] + +(* important note: we use on as the default for the new bool_attribute ! *) +let deprecated_bool_attribute_warning = + CWarnings.create + ~name:"deprecated-attribute-syntax" + ~category:"parsing" + ~default:CWarnings.Enabled + (fun name -> + Pp.(str "Syntax for switching off boolean attributes has been updated, use " ++ str name ++ str "=no instead.")) + +let deprecated_bool_attribute ~name ~on ~off : bool option attribute = + bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function + | None, None -> + None + | None, Some v -> + deprecated_bool_attribute_warning name; + Some v + | Some v, None -> Some v + | Some v1, Some v2 -> + CErrors.user_err + Pp.(str "attribute " ++ str name ++ + str ": cannot specify legacy and modern syntax at the same time.") + ) (* Variant of the [bool] attribute with only two values (bool has three). *) let get_bool_value ~key ~default = function | VernacFlagEmpty -> default - | VernacFlagList [ "true", VernacFlagEmpty ] -> true - | VernacFlagList [ "false", VernacFlagEmpty ] -> false + | VernacFlagList [ "true", VernacFlagEmpty ] -> + deprecated_bool_attribute_warning key; + true + | VernacFlagList [ "false", VernacFlagEmpty ] -> + deprecated_bool_attribute_warning key; + false + | VernacFlagLeaf (FlagIdent "yes") -> + true + | VernacFlagLeaf (FlagIdent "no") -> + false | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.") let enable_attribute ~key ~default : bool attribute = @@ -161,18 +243,37 @@ let () = let open Goptions in let program = enable_attribute ~key:"program" ~default:(fun () -> !program_mode) -let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" - -let option_locality = +(* This is a bit complex as the grammar in g_vernac.mlg doesn't + distingish between the boolean and ternary case.*) +let option_locality_parser = let name = "Locality" in attribute_of_list [ - ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal); - ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal); - ("export", single_key_parser ~name ~key:"export" Goptions.OptExport); - ] >>= function + ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal) + ; ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal) + ; ("export", single_key_parser ~name ~key:"export" Goptions.OptExport) + ] + +let option_locality = + option_locality_parser >>= function | None -> return Goptions.OptDefault | Some l -> return l +(* locality is supposed to be true when local, false when global *) +let locality = + let locality_to_bool = + function + | Goptions.OptLocal -> + true + | Goptions.OptGlobal -> + false + | Goptions.OptExport -> + CErrors.user_err Pp.(str "export attribute not supported here") + | Goptions.OptDefault -> + CErrors.user_err Pp.(str "default attribute not supported here") + in + option_locality_parser >>= function l -> + return (Option.map locality_to_bool l) + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] @@ -188,12 +289,17 @@ let is_universe_polymorphism = fun () -> !b let polymorphic_base = - bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function + deprecated_bool_attribute + ~name:"Polymorphism" + ~on:"polymorphic" ~off:"monomorphic" >>= function | Some b -> return b | None -> return (is_universe_polymorphism()) let template = - qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") + qualify_attribute ukey + (deprecated_bool_attribute + ~name:"Template" + ~on:"template" ~off:"notemplate") let polymorphic = qualify_attribute ukey polymorphic_base @@ -201,12 +307,12 @@ let polymorphic = let deprecation_parser : Deprecation.t key_parser = fun orig args -> assert_once ~name:"deprecation" orig; match args with - | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] - | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> + | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ; "note", VernacFlagLeaf (FlagString note) ] + | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ; "since", VernacFlagLeaf (FlagString since) ] -> Deprecation.make ~since ~note () - | VernacFlagList [ "since", VernacFlagLeaf since ] -> + | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ] -> Deprecation.make ~since () - | VernacFlagList [ "note", VernacFlagLeaf note ] -> + | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ] -> Deprecation.make ~note () | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") @@ -218,7 +324,7 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] -let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] +let vernac_monomorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagLeaf (FlagIdent "no")] let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) @@ -228,7 +334,7 @@ let canonical_instance = let uses_parser : string key_parser = fun orig args -> assert_once ~name:"using" orig; match args with - | VernacFlagLeaf str -> str + | VernacFlagLeaf (FlagString str) -> str | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute") let using = attribute_of_list ["using",uses_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 1969665082..03a14a03ff 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -9,13 +9,19 @@ (************************************************************************) (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +val pr_vernac_flag : vernac_flag -> Pp.t + type +'a attribute (** The type of attributes. When parsing attributes if an ['a attribute] is present then an ['a] value will be produced. @@ -82,10 +88,19 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute (** Make an attribute from a list of key parsers together with their associated key. *) -val bool_attribute : name:string -> on:string -> off:string -> bool option attribute -(** Define boolean attribute [name] with value [true] when [on] is - provided and [false] when [off] is provided. The attribute may only - be set once for a command. *) +(** Define boolean attribute [name], of the form [name={yes,no}]. The + attribute may only be set once for a command. *) +val bool_attribute : name:string -> bool option attribute + +val deprecated_bool_attribute + : name:string + -> on:string + -> off:string + -> bool option attribute +(** Define boolean attribute [name] with will be set when [on] is + provided and unset when [off] is provided. The attribute may only + be set once for a command; this attribute both accepts the old [on] + [off] syntax and new attribute syntax [on=yes] [on=no] *) val qualify_attribute : string -> 'a attribute -> 'a attribute (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att] diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 597e55a39e..8cb077ca21 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -271,9 +271,8 @@ let inductive_levels env evd arities inds = if Sorts.is_prop a || Sorts.is_sprop a then None else Some (univ_of_sort a)) destarities in - let cstrs_levels, min_levels, sizes = - CList.split3 - (List.map2 (fun (_,tys) (arity,(ctx,du)) -> + let cstrs_levels, sizes = + CList.split (List.map2 (fun (_,tys) (arity,(ctx,du)) -> let len = List.length tys in let minlev = Sorts.univ_of_sort du in let minlev = @@ -283,13 +282,15 @@ let inductive_levels env evd arities inds = in let minlev = (* Indices contribute. *) - if indices_matter env && List.length ctx > 0 then ( + if indices_matter env then begin let ilev = sign_level env evd ctx in - Univ.sup ilev minlev) + Univ.sup ilev minlev + end else minlev in let clev = extract_level env evd minlev tys in - (clev, minlev, len)) inds destarities) + (clev, len)) + inds destarities) in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) @@ -326,8 +327,13 @@ let inductive_levels env evd arities inds = let duu = Sorts.univ_of_sort du in let template_prop, evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then - if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - true, Evd.set_eq_sort env evd Sorts.prop du + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) + then if Term.isArity arity + (* If not a syntactic arity, the universe may be used in a + polymorphic instance and so cannot be lowered to Prop. + See #13300. *) + then true, Evd.set_eq_sort env evd Sorts.prop du + else false, Evd.set_eq_sort env evd Sorts.set du else false, evd else false, Evd.set_eq_sort env evd (sort_of_univ cu) du in diff --git a/vernac/declare.ml b/vernac/declare.ml index 1e8771b641..73ebca276d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -39,8 +39,10 @@ module Hook = struct let make_g hook = CEphemeron.create hook let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x) - let call_g ?hook x s = Option.cata (fun hook -> CEphemeron.get hook x s) s hook - let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook + let hcall hook x s = CEphemeron.default hook (fun _ x -> x) x s + + let call_g ?hook x s = Option.cata (fun hook -> hcall hook x s) s hook + let call ?hook x = Option.iter (fun hook -> hcall hook x ()) hook end @@ -1367,14 +1369,6 @@ module Proof_info = struct ; proof_ending = CEphemeron.create proof_ending } - (* This is used due to a deficiency on the API, should fix *) - let add_first_thm ~pinfo ~name ~typ ~impargs = - let cinfo : Constr.t CInfo.t = CInfo.make ~name ~impargs ~typ:(EConstr.Unsafe.to_constr typ) () in - { pinfo with cinfo = cinfo :: pinfo.cinfo } - - (* This is called by the STM, and we have to fixup cinfo later as - indeed it will not be correct *) - let default () = make ~cinfo:[] ~info:(Info.make ()) () end type t = @@ -1388,7 +1382,6 @@ type t = (*** Proof Global manipulation ***) -let info { pinfo } = pinfo let get ps = ps.proof let get_name ps = (Proof.data ps.proof).Proof.name let get_initial_euctx ps = ps.initial_euctx @@ -1566,6 +1559,7 @@ type proof_object = (* [name] only used in the STM *) ; entries : Evd.side_effects proof_entry list ; uctx: UState.t + ; pinfo : Proof_info.t } let get_po_name { name } = name @@ -1673,7 +1667,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in let entries = CList.map make_entry elist in - { name; entries; uctx } + { name; entries; uctx; pinfo } type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t @@ -1718,7 +1712,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types in let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in - { name; entries; uctx = initial_euctx } + { name; entries; uctx = initial_euctx; pinfo } let close_future_proof = close_proof_delayed @@ -1961,7 +1955,7 @@ let compute_proof_using_for_admitted proof typ pproofs = let finish_admitted ~pm ~pinfo ~uctx ~sec_vars ~univs = let cst = MutualEntry.declare_variable ~pinfo ~uctx ~sec_vars ~univs in (* If the constant was an obligation we need to update the program map *) - match CEphemeron.get pinfo.Proof_info.proof_ending with + match CEphemeron.default pinfo.Proof_info.proof_ending Proof_ending.Regular with | Proof_ending.End_obligation oinfo -> Obls_.obligation_admitted_terminator ~pm oinfo uctx (List.hd cst) | _ -> pm @@ -2083,7 +2077,7 @@ let save ~pm ~proof ~opaque ~idopt = let proof_info = process_idopt_for_save ~idopt proof.pinfo in finalize_proof ~pm proof_obj proof_info -let save_regular ~proof ~opaque ~idopt = +let save_regular ~(proof : t) ~opaque ~idopt = let open Proof_ending in match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with | Regular -> @@ -2094,8 +2088,8 @@ let save_regular ~proof ~opaque ~idopt = (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) -let save_lemma_admitted_delayed ~pm ~proof ~pinfo = - let { entries; uctx } = proof in +let save_lemma_admitted_delayed ~pm ~proof = + let { entries; uctx; pinfo } = proof in if List.length entries <> 1 then CErrors.user_err Pp.(str "Admitted does not support multiple statements"); let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in @@ -2106,16 +2100,10 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo = let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in finish_admitted ~pm ~uctx ~pinfo ~sec_vars ~univs -let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt = - (* vio2vo calls this but with invalid info, we have to workaround - that to add the name to the info structure *) - if CList.is_empty pinfo.Proof_info.cinfo then - let name = get_po_name proof in - let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in - finalize_proof ~pm proof info - else - let info = process_idopt_for_save ~idopt pinfo in - finalize_proof ~pm proof info +let save_lemma_proved_delayed ~pm ~proof ~idopt = + (* vio2vo used to call this with invalid [pinfo], now it should work fine. *) + let pinfo = process_idopt_for_save ~idopt proof.pinfo in + finalize_proof ~pm proof pinfo end (* Proof module *) diff --git a/vernac/declare.mli b/vernac/declare.mli index 0520bf8717..e4c77113af 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -278,14 +278,6 @@ module Proof : sig environment and empty evar_map. *) val get_current_context : t -> Evd.evar_map * Environ.env - (* Internal, don't use *) - module Proof_info : sig - type t - (* Make a dummy value, used in the stm *) - val default : unit -> t - end - val info : t -> Proof_info.t - (** {2 Proof delay API, warning, internal, not stable *) (* Intermediate step necessary to delegate the future. @@ -313,13 +305,11 @@ module Proof : sig val save_lemma_admitted_delayed : pm:OblState.t -> proof:proof_object - -> pinfo:Proof_info.t -> OblState.t val save_lemma_proved_delayed : pm:OblState.t -> proof:proof_object - -> pinfo:Proof_info.t -> idopt:Names.lident option -> OblState.t * GlobRef.t list diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1aff76114b..116cfc6413 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -119,7 +119,8 @@ GRAMMAR EXTEND Gram ] ; attr_value: - [ [ "=" ; v = string -> { VernacFlagLeaf v } + [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) } + | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) } | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } | -> { VernacFlagEmpty } ] ] @@ -136,7 +137,7 @@ GRAMMAR EXTEND Gram | IDENT "Cumulative" -> { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) } | IDENT "NonCumulative" -> - { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) } + { ("universes", VernacFlagList ["cumulative", VernacFlagLeaf (FlagIdent "no")]) } | IDENT "Private" -> { ("private", VernacFlagList ["matching", VernacFlagEmpty]) } | IDENT "Program" -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 442269ebda..4cee4f7a47 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1331,20 +1331,10 @@ let pr_control_flag (p : control_flag) = let pr_vernac_control flags = Pp.prlist pr_control_flag flags -let rec pr_vernac_flag (k, v) = - let k = keyword k in - let open Attributes in - match v with - | VernacFlagEmpty -> k - | VernacFlagLeaf v -> k ++ str " = " ++ qs v - | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )" -and pr_vernac_flags m = - prlist_with_sep (fun () -> str ", ") pr_vernac_flag m - let pr_vernac_attributes = function | [] -> mt () - | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () + | flags -> str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut () let pr_vernac ({v = {control; attrs; expr}} as v) = tag_vernac v diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4e52af7959..0f63dfe5ce 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -674,13 +674,19 @@ let is_polymorphic_inductive_cumulativity = let polymorphic_cumulative = let error_poly_context () = user_err - Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context."); + Pp.(str "The cumulative attribute can only be used in a polymorphic context."); in let open Attributes in let open Notations in + (* EJGA: this seems redudant with code in attributes.ml *) qualify_attribute "universes" - (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" - ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative") + (deprecated_bool_attribute + ~name:"Polymorphism" + ~on:"polymorphic" ~off:"monomorphic" + ++ + deprecated_bool_attribute + ~name:"Cumulativity" + ~on:"cumulative" ~off:"noncumulative") >>= function | Some poly, Some cum -> (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index edf48fef1a..57d9e0ac3c 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -226,24 +226,24 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = *) (* Interpreting a possibly delayed proof *) -let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t = +let interp_qed_delayed ~proof ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t = let stack = st.Vernacstate.lemmas in let pm = st.Vernacstate.program in let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in let pm = match pe with | Admitted -> - Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo + Declare.Proof.save_lemma_admitted_delayed ~pm ~proof | Proved (_,idopt) -> - let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in + let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~idopt in pm in stack, pm -let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } = +let interp_qed_delayed_control ~proof ~st ~control { CAst.loc; v=pe } = let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) control - (fun ~st -> interp_qed_delayed ~proof ~pinfo ~st pe) + (fun ~st -> interp_qed_delayed ~proof ~st pe) ~st (* General interp with management of state *) @@ -273,6 +273,6 @@ let interp_gen ~verbosely ~st ~interp_fn cmd = let interp ?(verbosely=true) ~st cmd = interp_gen ~verbosely ~st ~interp_fn:interp_control cmd -let interp_qed_delayed_proof ~proof ~pinfo ~st ~control pe : Vernacstate.t = +let interp_qed_delayed_proof ~proof ~st ~control pe : Vernacstate.t = interp_gen ~verbosely:false ~st - ~interp_fn:(interp_qed_delayed_control ~proof ~pinfo ~control) pe + ~interp_fn:(interp_qed_delayed_control ~proof ~control) pe diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 84d3256c9f..f31bebf7db 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -15,7 +15,6 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> proof and won't be forced *) val interp_qed_delayed_proof : proof:Declare.Proof.proof_object - -> pinfo:Declare.Proof.Proof_info.t -> st:Vernacstate.t -> control:Vernacexpr.control_flag list -> Vernacexpr.proof_end CAst.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 204008997d..011d943c9b 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -204,18 +204,14 @@ module Declare_ = struct s_lemmas := Some stack; res - type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t - let return_proof () = cc Declare.Proof.return_proof let return_partial_proof () = cc Declare.Proof.return_partial_proof let close_future_proof ~feedback_id pf = - cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf, - Declare.Proof.info pt) + cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf) let close_proof ~opaque ~keep_body_ucst_separate = - cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt, - Declare.Proof.info pt) + cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt) let discard_all () = s_lemmas := None let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index e1b13dcb73..e9e06e6d8e 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -104,13 +104,15 @@ module Declare : sig val return_proof : unit -> Declare.Proof.closed_proof_output val return_partial_proof : unit -> Declare.Proof.closed_proof_output - type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t - - val close_future_proof : - feedback_id:Stateid.t -> - Declare.Proof.closed_proof_output Future.computation -> closed_proof - - val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof + val close_future_proof + : feedback_id:Stateid.t + -> Declare.Proof.closed_proof_output Future.computation + -> Declare.Proof.proof_object + + val close_proof + : opaque:Vernacexpr.opacity_flag + -> keep_body_ucst_separate:bool + -> Declare.Proof.proof_object val discard_all : unit -> unit val update_sigma_univs : UGraph.t -> unit |