diff options
148 files changed, 2549 insertions, 665 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3582d18cf6..525ced7fee 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -828,7 +828,12 @@ organization, because of a limitation of GitHub). - the overlays that are backward-compatible (normally the case for overlays fixing Coq code) should have been merged *before* the PR - can be merged; + can be merged; it might be a good idea to ask the PR author to + remove the overlay information from the PR to get a fresh CI run + and ensure that all the overlays have been merged; the PR assignee + may also push a commit removing the overlay information (in that + case the assignee is not considered a co-author, hence no need to + change the assignee) - the overlays that are not backward-compatible (normally only the case for overlays fixing OCaml code) should be merged *just after* diff --git a/checker/check.ml b/checker/check.ml index 31bfebc3d5..6d307b3c5e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -263,6 +263,7 @@ let raw_intern_library f = type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } module Dyn = Dyn.Make () @@ -345,6 +346,7 @@ let intern_from_file ~intern_mode (dir, f) = let () = close_in ch in let ch = open_in_bin f in let () = close_in ch in + let () = System.check_caml_version ~caml:sd.md_ocaml ~file:f in if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); diff --git a/checker/values.ml b/checker/values.ml index 76e3ab0d45..cce0ce7203 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -435,7 +435,7 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) let v_libsum = - Tuple ("summary", [|v_dp;v_deps|]) + Tuple ("summary", [|v_dp;v_deps;String|]) let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index b87a9c0392..5f7d0b5789 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -351,3 +351,10 @@ : "${metacoq_CI_REF:=master}" : "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" : "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" + +######################################################################## +# SF suite +######################################################################## +: "${sf_CI_REF:=master}" +: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}" +: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}" diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index b9d6215e60..d46e53717f 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,22 +3,9 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2 +git_download sf -# "latest" is disabled due to lack of build credits upstream, thus artifacts fail -# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) -data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) - -mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" - -sf_lf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "lf.tgz") | .url') -sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url') -sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url') - -wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz -wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz -wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz - -( cd lf && make clean && make ) -( cd plf && make clean && make ) -( cd vfa && make clean && make ) +( cd lf-current && make clean && make ) +( cd plf-current && make clean && make ) +( cd vfa-current && make clean && make ) +# ( cd qc-current && make clean && make ) diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh new file mode 100644 index 0000000000..50eaf0b109 --- /dev/null +++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then + + elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst new file mode 100644 index 0000000000..e1fcfb78c4 --- /dev/null +++ b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst @@ -0,0 +1,4 @@ +- **Added:** + Abbreviations support arguments occurring both in term and binder position + (`#8808 <https://github.com/coq/coq/pull/8808>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12129-add-with-strategy.rst b/doc/changelog/04-tactics/12129-add-with-strategy.rst new file mode 100644 index 0000000000..68558c0cf4 --- /dev/null +++ b/doc/changelog/04-tactics/12129-add-with-strategy.rst @@ -0,0 +1,4 @@ +- **Added:** + New tactical :tacn:`with_strategy` added which behaves like the + command :cmd:`Strategy`, with effects local to the given tactic + (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst new file mode 100644 index 0000000000..055006d3b4 --- /dev/null +++ b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is + indirectly dependent in the goal; the incompatibility can generally + be fixed by first clearing the hypotheses causing an indirect + dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` + instead; similarly, :tacn:`subst` has no more effect on such variables + (`#12146 <https://github.com/coq/coq/pull/12146>`_, + by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; + fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). diff --git a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst new file mode 100644 index 0000000000..dc438f151e --- /dev/null +++ b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Loss of location of some tactic errors + (`#12223 <https://github.com/coq/coq/pull/12223>`_, + by Hugo Herbelin; fixes + `#12152 <https://github.com/coq/coq/pull/12152>`_ and + `#12255 <https://github.com/coq/coq/pull/12255>`_). diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst new file mode 100644 index 0000000000..0dd0fed4e2 --- /dev/null +++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 <https://github.com/coq/coq/pull/11503>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst b/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst new file mode 100644 index 0000000000..69632fd202 --- /dev/null +++ b/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst @@ -0,0 +1,5 @@ +- **Changed:** + The "reference" tactic generic argument now accepts arbitrary + variables of the goal context + (`#12254 <https://github.com/coq/coq/pull/12254>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst new file mode 100644 index 0000000000..5ab2941446 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst @@ -0,0 +1,9 @@ +- **Deprecated:** + Option :flag:`Hide Obligations` has been deprecated + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). + +- **Removed:** + Deprecated option ``Shrink Obligations`` has been removed + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst index a07e48d2d8..ff736641b4 100644 --- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst +++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst @@ -1,6 +1,9 @@ - **Changed:** - The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc. - and the option set flags `-set`, `-unset` are processed have been reversed. - In the new behavior, require/load flags are processed before option flags. - (`#11851 <https://github.com/coq/coq/pull/11851>`_, + The order in which the require flags `-ri`, `-re`, `-rfrom`, etc. + and the option flags `-set`, `-unset` are given now matters. In + particular, it is now possible to interleave the loading of plugins + and the setting of options by choosing the right order for these + flags. The load flags `-l` and `-lv` are still processed afterward + for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and + `#12097 <https://github.com/coq/coq/pull/12097>`_, by Lasse Blaauwbroek). diff --git a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst index be15fbf8f5..be54e45808 100644 --- a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst +++ b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst @@ -7,11 +7,12 @@ - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt`` - properties of ``concat``: ``in_concat``, ``remove_concat`` - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map`` - - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl`` + - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff`` + - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl`` - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall`` - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat`` - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt`` - - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``NoDup_rev``, ``nodup_incl``, ``cons_seq``, ``seq_S`` + - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S`` - (`#11249 <https://github.com/coq/coq/pull/11249>`_, + (`#11249 <https://github.com/coq/coq/pull/11249>`_, `#12237 <https://github.com/coq/coq/pull/12237>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst index 7c10d261a7..42e5eb96eb 100644 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -1,5 +1,5 @@ - **Added:** - Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` (`#12008 <https://github.com/coq/coq/pull/12008>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst new file mode 100644 index 0000000000..6a4070a82e --- /dev/null +++ b/doc/changelog/10-standard-library/12162-bool-leb.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst deleted file mode 100644 index 37aaf697b5..0000000000 --- a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``, ``incl_Forall_in_iff`` - (`#12237 <https://github.com/coq/coq/pull/12237>`_, - by Olivier Laurent). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 52862dea47..b5618c5721 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -342,17 +342,11 @@ optional tactic is replaced by the default one if not specified. .. flag:: Hide Obligations + .. deprecated:: 8.12 + Controls whether obligations appearing in the term should be hidden as implicit arguments of the special - constantProgram.Tactics.obligation. - -.. flag:: Shrink Obligations - - .. deprecated:: 8.7 - - This flag (on by default) controls whether obligations should have - their context minimized to the set of variables used in the proof of - the obligation, to avoid unnecessary dependencies. + constant ``Program.Tactics.obligation``. The module :g:`Coq.Program.Tactics` defines the default tactic for solving obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index acdd4408ed..899173a83a 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -9,11 +9,11 @@ The |Coq| library The |Coq| library has two parts: - * **The basic library**: definitions and theorems for + * The :gdef:`prelude`: definitions and theorems for the most commonly used elementary logical notions and data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries with + * The :gdef:`standard library`: general-purpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the ``Require`` command (see :ref:`compiled-files`) @@ -28,8 +28,8 @@ also be browsed at http://coq.inria.fr/stdlib/. -The basic library ------------------ +The prelude +----------- This section lists the basic notions and results which are directly available in the standard |Coq| system. Most of these constructions diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9473cc5a15..aa93b4d21f 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -130,30 +130,37 @@ Strings identified with :production:`string`. Keywords - The following character sequences are reserved keywords that cannot be - used as identifiers:: + The following character sequences are keywords defined in the main Coq grammar + that cannot be used as identifiers (even when starting Coq with the `-noinit` + command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop - SProp Set Theorem Type Variable as at cofix discriminated else end + SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with - Note that notations and plugins may define additional keywords. + The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: -Other tokens - The set of - tokens defined at any given time can vary because the :cmd:`Notation` - command can define new tokens. A :cmd:`Require` command may load more notation definitions, - while the end of a :cmd:`Section` may remove notations. Some notations - are defined in the standard library (see :ref:`thecoqlibrary`) and are generally - loaded automatically at startup time. + IF by exists exists2 using + + Note that loading additional modules or plugins may expand the set of reserved + keywords. - Here are the character sequences that |Coq| directly defines as tokens - without using :cmd:`Notation`:: +Other tokens + The following character sequences are tokens defined in the main Coq grammar + (even when starting Coq with the `-noinit` command-line flag):: - ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: - <<: <= = => > >-> >= ? @ @{ [ [= ] _ - `( `{ { {| | |- || } + <<: <= = => > >-> >= ? @ @{ [ ] _ + `( `{ { {| | } + + The following character sequences are tokens defined in notations or plugins + loaded in the :term:`prelude`:: + + ** [= |- || -> + + Note that loading additional modules or plugins may expand the set of defined + tokens. When multiple tokens match the beginning of a sequence of characters, the longest matching token is used. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 545bba4930..d4ceffac9f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -151,7 +151,7 @@ and ``coqtop``, unless stated otherwise: while processing options such as -R and -Q. By default, only the conventional version control management directories named CVS and_darcs are excluded. -:-nois: Start from an empty state instead of loading the Init.Prelude +:-nois, -noinit: Start from an empty state instead of loading the `Init.Prelude` module. :-init-file *file*: Load *file* as the resource file instead of loading the default resource file from the standard configuration @@ -163,32 +163,53 @@ and ``coqtop``, unless stated otherwise: |Coq| script from *file.v*. Write its contents to the standard output as it is executed. :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This - is equivalent to running :cmd:`Require` :n:`qualid`. + is equivalent to running :cmd:`Require` :n:`@qualid`. + + .. _interleave-command-line: + + .. note:: + + Note that the relative order of this command-line option and its + variants (`-rfrom`, `-ri`, `-re`, etc.) and of the `-set` and + `-unset` options matters since the various :cmd:`Require`, + :cmd:`Require Import`, :cmd:`Require Export`, :cmd:`Set` and + :cmd:`Unset` commands will be executed in the order specified on + the command-line. + :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. - This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. + This is equivalent to running :cmd:`From <From ... Require>` + :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is equivalent to running :cmd:`Require Import` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :cmd:`Require Export` :n:`@qualid`. -:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. - This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. -:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. - This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. +:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: + Load |Coq| compiled library :n:`@qualid` and import it. This is + equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath` + :cmd:`Require Import <From ... Require>` :n:`@qualid`. See the + :ref:`note above <interleave-command-line>` regarding the order of + command-line options. +:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: + Load |Coq| compiled library :n:`@qualid` and transitively import it. + This is equivalent to running :cmd:`From <From ... Require>` + :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the + order of command-line options. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. -:-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option - implies -batch (exit just after argument parsing). It is available only - for `coqtop`, as this behavior is the purpose of ``coqc``. -:-compile-verbose *file.v*: Deprecated. Use ``coqc -verbose``. Same as -compile but also output the - content of *file.v* as it is compiled. :-verbose: Output the content of the input file as it is compiled. - This option is available for ``coqc`` only; it is the counterpart of - -compile-verbose. + This option is available for ``coqc`` only. :-vos: Indicate |Coq| to skip the processing of opaque proofs - (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files + (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files - when interpreting ``Require`` commands. + when interpreting :cmd:`Require` commands. :-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead - of ``.vo`` files when interpreting ``Require`` commands, and to output an empty + of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty ``.vok`` files upon success instead of writing a ``.vo`` file. :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or @@ -198,7 +219,7 @@ and ``coqtop``, unless stated otherwise: the output channel supports ANSI escape sequences. :-diffs (on|off|removed): *Coqtop only*. Controls highlighting of differences between proof steps. ``on`` highlights added tokens, ``removed`` highlights both added and - removed tokens. Requires that ``–color`` is enabled. (see Section + removed tokens. Requires that ``-color`` is enabled. (see Section :ref:`showing_diffs`). :-beautify: Pretty-print each command to *file.beautified* when compiling *file.v*, in order to get old-fashioned @@ -224,17 +245,25 @@ and ``coqtop``, unless stated otherwise: changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. :-set *string*: Enable flags and set options. *string* should be - ``Option Name=value``, the value is interpreted according to the - type of the option. For flags ``Option Name`` is equivalent to - ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` + :n:`@setting_name=value`, the value is interpreted according to the + type of the option. For flags :n:`@setting_name` is equivalent to + :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. Flags are processed after initialization - of the document. This includes the `Prelude` if loaded and any libraries loaded - through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` - options. + shell syntax, Coq does not see them. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. :-unset *string*: As ``-set`` but used to disable options and flags. -:-compat *version*: Attempt to maintain some backward-compatibility - with a previous version. + *string* must be :n:`"@setting_name"`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. +:-compat *version*: Load a file that sets a few options to maintain + partial backward-compatibility with a previous version. This is + equivalent to :cmd:`Require Import` `Coq.Compat.CoqXXX` with `XXX` + one of the last three released versions (including the current + version). Note that the :ref:`explanations above + <interleave-command-line>` regarding the order of command-line + options apply, and this could be relevant if you are resetting some + of the compatibility options. :-dump-glob *file*: Dump references for global names in file *file* (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being compiled, *file.glob* is used. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b184311bef..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,6 +57,8 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: + - The grammar reserves the token ``||``. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. .. example:: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..1e35160205 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,25 +213,63 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. + + .. example:: Dynamic nature of mutable cells + + .. coqtop:: all + + Ltac2 mutable x := true. + Ltac2 y := x. + Ltac2 Eval y. + Ltac2 Set x := false. + Ltac2 Eval y. + + .. example:: Interaction with recursive calls + + + .. coqtop:: all + + Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. + Ltac2 Set f := fun b => + match b with true => 1 | _ => f true end. + Ltac2 Eval (f false). + Ltac2 Set f as oldf := fun b => + match b with true => 2 | _ => oldf false end. + Ltac2 Eval (f false). + + In the definition, the `f` in the body is resolved statically + because the definition is marked recursive. In the first re-definition, + the `f` in the body is resolved dynamically. This is witnessed by + the second re-definition. + Reduction ~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8989dd29ab..127e4c6dbe 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -36,6 +36,18 @@ language will be described in Chapter :ref:`ltac`. Common elements of tactics -------------------------- +Reserved keywords +~~~~~~~~~~~~~~~~~ + +The tactics described in this chapter reserve the following keywords:: + + by using + +Thus, these keywords cannot be used as identifiers. It also declares +the following character sequences as tokens:: + + ** [= |- + .. _invocation-of-tactics: Invocation of tactics @@ -2832,6 +2844,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also unfolded and cleared. + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + .. note:: + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the first one is used. @@ -2845,9 +2862,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: subst - This applies subst repeatedly from top to bottom to all identifiers of the + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. .. flag:: Regular Subst Tactic @@ -2873,6 +2892,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. hypotheses, which without the flag it may break. default. + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + .. tacn:: stepl @term :name: stepl @@ -3355,6 +3383,128 @@ the conversion in hypotheses :n:`{+ @ident}`. This is the most general syntax that combines the different variants. +.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. note:: + + This tactic unfortunately does not yet play well with tactic + internalization, resulting in interpretation-time errors when + you try to use it directly with opaque identifiers, as seen in + the first (failing) use of :tacn:`with_strategy` in the + following example. This can be worked around by binding the + identifier to an |Ltac| variable, and this issue should + disappear in a future version of |Coq|; see `#12179 + <https://github.com/coq/coq/issues/12179>`_. + + .. example:: + + .. coqtop:: all reset abort + + Opaque id. + Goal id 10 = 10. + Fail unfold id. + Fail with_strategy transparent [id] unfold id. + let id' := id in with_strategy transparent [id] unfold id'. + + .. warning:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful either in + combination with :tacn:`abstract`, which will check the proof + early while the fine-tuning is still in effect, or to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + + This can be illustrated with the following example involving the + factorial function. + + .. coqtop:: in reset + + Fixpoint fact (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * fact n' + end. + + Suppose now that, for whatever reason, we want in general to + unfold the :g:`id` function very late during conversion: + + .. coqtop:: in + + Strategy 1000 [id]. + + If we try to prove :g:`id (fact n) = fact n` by + :tacn:`reflexivity`, it will now take time proportional to + :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full + computation of :g:`fact n` (in unary, because we are using + :g:`nat`), which takes time :math:`n!`. We can see this cross + the relevant threshold at around :math:`n = 9`: + + .. coqtop:: all abort + + Goal True. + Time assert (id (fact 8) = fact 8) by reflexivity. + Time assert (id (fact 9) = fact 9) by reflexivity. + + Note that behavior will be the same if you mark :g:`id` as + :g:`Opaque` because while most reduction tactics refuse to + unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as + merely a hint to unfold this constant last. + + We can get around this issue by using :tacn:`with_strategy`: + + .. coqtop:: all + + Goal True. + Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. + + However, when we go to close the proof, we will run into + trouble, because the reduction strategy changes are local to the + tactic passed to :tacn:`with_strategy`. + + .. coqtop:: all abort fail + + exact I. + Timeout 1 Defined. + + We can fix this issue by using :tacn:`abstract`: + + .. coqtop:: all + + Goal True. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. + exact I. + Time Defined. + + On small examples this sort of behavior doesn't matter, but + because |Coq| is a super-linear performance domain in so many + places, unless great care is taken, tactic automation using + :tacn:`with_strategy` may not be robustly performant when + scaling the size of the input. + + .. warning:: + + In much the same way this tactic does not play well with + :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as + an intermediary, this tactic does not play well with ``coqchk``, + even when used with :tacn:`abstract`, due to the inability of + tactics to persist information about conversion hints in the + proof term. See `#12200 + <https://github.com/coq/coq/issues/12200>`_ for more details. + Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 1759264e87..7191444bac 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -817,13 +817,15 @@ described first. .. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - .. insertprodn strategy_level strategy_level + .. insertprodn strategy_level strategy_level_or_var .. prodn:: strategy_level ::= opaque | @int | expand | transparent + strategy_level_or_var ::= @strategy_level + | @ident This command accepts the :attr:`local` attribute, which limits its effect to the current section or module, in which case the section and module diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d72409e0d9..c5ec636d5f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -618,6 +618,41 @@ the next command fails because p does not bind in the instance of n. Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). +Notations with expressions used both as binder and term ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +It is possible to use parameters of the notation both in term and +binding position. Here is an example: + +.. coqtop:: in + + Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. + Notation "▢_ n P" := (force n (fun n => P)) + (at level 0, n ident, P at level 9, format "▢_ n P"). + +.. coqtop:: all + + Check exists p, ▢_p (p >= 1). + +More generally, the parameter can be a pattern, as in the following +variant: + +.. coqtop:: in reset + + Definition force2 q (P:nat*nat -> Prop) := + (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + + Notation "▢_ p P" := (force2 p (fun p => P)) + (at level 0, p pattern at level 0, P at level 9, format "▢_ p P"). + +.. coqtop:: all + + Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2). + +This support is experimental. For instance, the notation is used for +printing only if the occurrence of the parameter in term position +comes in the right-hand side before the occurrence in binding position. + .. _RecursiveNotations: Notations with recursive patterns @@ -1383,6 +1418,17 @@ Abbreviations exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments. + Like for notations, it is possible to bind binders in + abbreviations. Here is an example: + + .. coqtop:: in reset + + Definition force2 q (P:nat*nat -> Prop) := + (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + + Notation F p P := (force2 p (fun p => P)). + Check exists x y, F (x,y) (x >= 1 /\ y >= 2). + .. _numeral-notations: Numeral notations @@ -1714,6 +1760,11 @@ Tactic notations allow customizing the syntax of tactics. - a global reference of term - :tacn:`unfold` + * - ``smart_global`` + - :token:`smart_qualid` + - a global reference of term + - :tacn:`with_strategy` + * - ``constr`` - :token:`term` - a term @@ -1734,6 +1785,16 @@ Tactic notations allow customizing the syntax of tactics. - an integer - :tacn:`do` + * - ``strategy_level`` + - :token:`strategy_level` + - a strategy level + - + + * - ``strategy_level_or_var`` + - :token:`strategy_level_or_var` + - a strategy level + - :tacn:`with_strategy` + * - ``tactic`` - :token:`ltac_expr` - a tactic @@ -1766,18 +1827,24 @@ Tactic notations allow customizing the syntax of tactics. .. todo: notation doesn't support italics - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of a simple |Ltac| - identifier as part of what it parses. This is naturally the case for - ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. - This is the reason for introducing a special entry ``int_or_var`` which - evaluates to integers only but which syntactically includes + .. note:: In order to be bound in tactic definitions, each + syntactic entry for argument type must include the case + of a simple |Ltac| identifier as part of what it + parses. This is naturally the case for ``ident``, + ``simple_intropattern``, ``reference``, ``constr``, ... + but not for ``integer`` nor for ``strategy_level``. This + is the reason for introducing special entries + ``int_or_var`` and ``strategy_level_or_var`` which + evaluate to integers or strategy levels only, + respectively, but which syntactically includes identifiers in order to be usable in tactic definitions. - .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` entries can be used in - primitive tactics or in other notations at places where a list of the - underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer`` - or ``int_or_var``. + .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` + entries can be used in primitive tactics or in other + notations at places where a list of the underlying entry + can be used: entry is either ``constr``, ``hyp``, + ``integer``, ``smart_qualid``, ``strategy_level``, + ``strategy_level_or_var``, or ``int_or_var``. .. rubric:: Footnotes diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index c7e3ee18ad..62cc8ea86b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1839,3 +1839,7 @@ sentence: [ document: [ | LIST0 sentence ] + +strategy_level: [ +| DELETE strategy_level0 +] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 4274dccb40..92e9df51d5 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -451,6 +451,14 @@ bar_cbrace: [ | test_pipe_closedcurly "|" "}" ] +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +| strategy_level0 +] + vernac_toplevel: [ | "Drop" "." | "Quit" "." @@ -1213,13 +1221,6 @@ more_implicits_block: [ | "{" LIST1 name "}" ] -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" -] - instance_name: [ | ident_decl binders | @@ -1598,6 +1599,7 @@ simple_tactic: [ | "guard" test | "decompose" "[" LIST1 constr "]" constr | "optimize_heap" +| "with_strategy" strategy_level_or_var "[" LIST1 smart_global "]" tactic3 | "eassumption" | "eexact" constr | "trivial" auto_using hintbases @@ -1855,6 +1857,11 @@ test_lpar_id_colon: [ | local_test_lpar_id_colon ] +strategy_level_or_var: [ +| strategy_level +| identref +] + comparison: [ | "=" | "<" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index df4e5a22e3..11f06b7b8a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -659,6 +659,11 @@ strategy_level: [ | "transparent" ] +strategy_level_or_var: [ +| strategy_level +| ident +] + reserv_list: [ | LIST1 ( "(" simple_reserv ")" ) | simple_reserv @@ -1234,6 +1239,7 @@ simple_tactic: [ | "guard" int_or_var comparison int_or_var | "decompose" "[" LIST1 one_term "]" one_term | "optimize_heap" +| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3 | "start" "ltac" "profiling" | "stop" "ltac" "profiling" | "reset" "ltac" "profile" diff --git a/engine/termops.ml b/engine/termops.ml index 6d779e6a35..c51e753d46 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -803,23 +803,29 @@ let occur_evar sigma n c = let occur_in_global env id constr = let vars = vars_of_global env constr in - if Id.Set.mem id vars then raise Occur + Id.Set.mem id vars let occur_var env sigma id c = let rec occur_rec c = match EConstr.destRef sigma c with - | gr, _ -> occur_in_global env id gr + | gr, _ -> if occur_in_global env id gr then raise Occur | exception DestKO -> EConstr.iter sigma occur_rec c in try occur_rec c; false with Occur -> true +exception OccurInGlobal of GlobRef.t + +let occur_var_indirectly env sigma id c = + let var = GlobRef.VarRef id in + let rec occur_rec c = + match EConstr.destRef sigma c with + | gr, _ -> if not (GlobRef.equal gr var) && occur_in_global env id gr then raise (OccurInGlobal gr) + | exception DestKO -> EConstr.iter sigma occur_rec c + in + try occur_rec c; None with OccurInGlobal gr -> Some gr + let occur_var_in_decl env sigma hyp decl = - let open NamedDecl in - match decl with - | LocalAssum (_,typ) -> occur_var env sigma hyp typ - | LocalDef (_, body, typ) -> - occur_var env sigma hyp typ || - occur_var env sigma hyp body + NamedDecl.exists (occur_var env sigma hyp) decl let local_occur_var sigma id c = let rec occur c = match EConstr.kind sigma c with @@ -828,6 +834,9 @@ let local_occur_var sigma id c = in try occur c; false with Occur -> true +let local_occur_var_in_decl sigma hyp decl = + NamedDecl.exists (local_occur_var sigma hyp) decl + (* returns the list of free debruijn indices in a term *) let free_rels sigma m = diff --git a/engine/termops.mli b/engine/termops.mli index 4e77aa9b3b..709fa361a9 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool +val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool +val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool val free_rels : Evd.evar_map -> constr -> Int.Set.t diff --git a/engine/uState.ml b/engine/uState.ml index 00649ce042..99ac5f2ce8 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -34,7 +34,7 @@ type t = (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) - uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *) + uctx_universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) uctx_weak_constraints : UPairSet.t } @@ -48,7 +48,7 @@ let empty = uctx_univ_variables = LMap.empty; uctx_univ_algebraic = LSet.empty; uctx_universes = initial_sprop_cumulative; - uctx_universes_lbound = Univ.Level.set; + uctx_universes_lbound = UGraph.Bound.Set; uctx_initial_universes = initial_sprop_cumulative; uctx_weak_constraints = UPairSet.empty; } @@ -443,6 +443,10 @@ let check_univ_decl ~poly uctx decl = (ContextSet.constraints uctx.uctx_local); ctx +let is_bound l lbound = match lbound with +| UGraph.Bound.Prop -> Level.is_prop l +| UGraph.Bound.Set -> Level.is_set l + let restrict_universe_context ~lbound (univs, csts) keep = let removed = LSet.diff univs keep in if LSet.is_empty removed then univs, csts @@ -455,7 +459,7 @@ let restrict_universe_context ~lbound (univs, csts) keep = let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in let csts = UGraph.constraints_for ~kept:allkept g in let csts = Constraint.filter (fun (l,d,r) -> - not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in + not ((is_bound l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in (LSet.inter univs keep, csts) let restrict ctx vars = @@ -600,10 +604,10 @@ let make_with_initial_binders ~lbound e us = let add_global_univ uctx u = let initial = - UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes + UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_initial_universes in let univs = - UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes + UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_universes in { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local; uctx_initial_universes = initial; diff --git a/engine/uState.mli b/engine/uState.mli index 6707826aae..533a501b59 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -25,9 +25,9 @@ type t val empty : t -val make : lbound:Univ.Level.t -> UGraph.t -> t +val make : lbound:UGraph.Bound.t -> UGraph.t -> t -val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t +val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t val is_empty : t -> bool @@ -90,7 +90,7 @@ val universe_of_name : t -> Id.t -> Univ.Level.t the universes in [keep]. The constraints [csts] are adjusted so that transitive constraints between remaining universes (those in [keep] and those not in [univs]) are preserved. *) -val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t (** [restrict uctx ctx] restricts the local universes of [uctx] to [ctx] extended by local named universes and side effect universes diff --git a/engine/univMinim.ml b/engine/univMinim.ml index c05a7a800d..4dd7fe7e70 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -267,12 +267,16 @@ let minimize_univ_variables ctx us algs left right cstrs = module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) +let is_bound l lbound = match lbound with +| UGraph.Bound.Prop -> Level.is_prop l +| UGraph.Bound.Set -> Level.is_set l + (* TODO check is_small/sprop *) let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts + Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles @@ -299,7 +303,7 @@ let normalize_context_set ~lbound g ctx us algs weak = (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) || + (fun (l,d,r) -> not ((d == Le && is_bound l lbound) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 2a46d87609..58853e47b8 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> diff --git a/engine/univops.mli b/engine/univops.mli index 02a731ad49..d0145f5643 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -15,5 +15,5 @@ open Univ val universes_of_constr : constr -> LSet.t [@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t +val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t [@@ocaml.deprecated "Use [UState.restrict_universe_context]"] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a1aac60b35..5ad8af6d57 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -976,10 +976,6 @@ let split_by_type_pat ?loc ids subst = assert (terms = [] && termlists = []); subst -let make_subst ids l = - let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in - List.fold_left2 fold Id.Map.empty ids l - let intern_notation intern env ntnvars loc ntn fullargs = (* Adjust to parsing of { } *) let ntn,fullargs = contract_curly_brackets ntn fullargs in @@ -1113,8 +1109,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in check_no_explicitation args1; - let terms = make_subst ids (List.map fst args1) in - let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in + let subst = split_by_type ids (List.map fst args1,[],[],[]) in let infos = (Id.Map.empty, env) in let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.loc in @@ -1624,8 +1619,8 @@ let drop_notations_pattern looked_for genv = let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; let pats1,pats2 = List.chop nvars pats in - let subst = make_subst vars pats1 in - let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in + let subst = split_by_type_pat vars (pats1,[]) in + let idspl1 = List.map (in_not false qid.loc scopes subst []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) | _ -> raise Not_found diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 492671fff0..d5f104b7f8 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -42,6 +42,8 @@ let wit_var = let wit_ref = make0 "ref" +let wit_smart_global = make0 ~dyn:(val_tag (topwit wit_ref)) "smart_global" + let wit_sort_family = make0 "sort_family" let wit_constr = diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 35de3693cb..89bdd78c70 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -39,6 +39,8 @@ val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_smart_global : (qualid or_by_notation, GlobRef.t located or_var, GlobRef.t) genarg_type + val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 7184f5ea29..bd3e234a91 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Pp open CErrors open Names @@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -type syndef_interpretation = (Id.t * subscopes) list * notation_constr - -(* Coercions to the general format of notation that also supports - variables bound to list of expressions *) -let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) -let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) - let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = let syndef = - { syndef_pattern = in_pat pat; + { syndef_pattern = pat; syndef_onlyparsing = onlyparsing; syndef_deprecation = deprecation; } @@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition = let search_syntactic_definition ?loc kn = let syndef = KNmap.find kn !syntax_table in - let def = out_pat syndef.syndef_pattern in Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; - def + syndef.syndef_pattern let search_filtered_syntactic_definition ?loc filter kn = let syndef = KNmap.find kn !syntax_table in - let def = out_pat syndef.syndef_pattern in - let res = filter def in + let res = filter syndef.syndef_pattern in if Option.has_some res then Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 8b323462a1..66a3132f2a 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,12 +13,10 @@ open Notation_term (** Syntactic definitions. *) -type syndef_interpretation = (Id.t * subscopes) list * notation_constr - val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> - onlyparsing:bool -> syndef_interpretation -> unit + onlyparsing:bool -> interpretation -> unit -val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation val search_filtered_syntactic_definition : ?loc:Loc.t -> - (syndef_interpretation -> 'a option) -> KerName.t -> 'a option + (interpretation -> 'a option) -> KerName.t -> 'a option diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 9b87c194c5..3ee1d2fb1f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -19,6 +19,12 @@ open Names * The default value is [Level 100]. *) type level = Expand | Level of int | Opaque +let pr_level = function + | Expand -> Pp.str "expand" + | Level 0 -> Pp.str "transparent" + | Level n -> Pp.int n + | Opaque -> Pp.str "opaque" + let default = Level 0 let is_default = function | Level 0 -> true diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index b25488d94a..930edf6c49 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -27,6 +27,7 @@ val oracle_order : ('a -> Constant.t) -> oracle -> bool -> * The default value (transparent constants) is [Level 0]. *) type level = Expand | Level of int | Opaque +val pr_level : level -> Pp.t val transparent : level (** Check whether a level is transparent *) @@ -42,4 +43,3 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a val get_transp_state : oracle -> TransparentState.t - diff --git a/kernel/environ.ml b/kernel/environ.ml index d6d52dbc2b..182ed55d0e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -67,7 +67,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -129,7 +129,7 @@ let empty_env = { env_stratification = { env_universes = UGraph.initial_universes; env_sprop_allowed = true; - env_universes_lbound = Univ.Level.set; + env_universes_lbound = UGraph.Bound.Set; env_engagement = PredicativeSet }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; diff --git a/kernel/environ.mli b/kernel/environ.mli index 7a46538772..79e632daa0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -62,7 +62,7 @@ end type stratification = { env_universes : UGraph.t; env_sprop_allowed : bool; - env_universes_lbound : Univ.Level.t; + env_universes_lbound : UGraph.Bound.t; env_engagement : engagement } @@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val universes_lbound : env -> Univ.Level.t -val set_universes_lbound : env -> Univ.Level.t -> env +val universes_lbound : env -> UGraph.Bound.t +val set_universes_lbound : env -> UGraph.Bound.t -> env val rel_context : env -> Constr.rel_context val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 8ac96a6481..e9687991c0 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = if has_template_poly then (* For that particular case, we typecheck the inductive in an environment where the universes introduced by the definition are only [>= Prop] *) - let env = set_universes_lbound env Univ.Level.prop in + let env = set_universes_lbound env UGraph.Bound.Prop in push_context_set ~strict:false ctx env else (* In the regular case, all universes are [> Set] *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 5f5f0ef8cd..927db9e9e6 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -148,8 +148,14 @@ let enforce_leq_alg u v g = assert (check_leq g u v); cg +module Bound = +struct + type t = Prop | Set +end + exception AlreadyDeclared = G.AlreadyDeclared let add_universe u ~lbound ~strict g = + let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in let graph = G.add u g.graph in let d = if strict then Lt else Le in enforce_constraint (lbound,d,u) {g with graph} diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8d9afb0990..c9fbd7f694 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t +module Bound : +sig + type t = Prop | Set + (** The [Prop] bound is only used for template polymorphic inductive types. *) +end + +val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : lbound:Level.t -> AUContext.t check_function +val check_subtype : lbound:Bound.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) diff --git a/lib/system.ml b/lib/system.ml index 4e98651d6e..e25f758865 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -168,6 +168,15 @@ let try_remove filename = let error_corrupted file s = CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") +let check_caml_version ~caml:s ~file:f = + if not (String.equal Coq_config.caml_version s) then + CErrors.user_err (str ("The file " ^ f ^ " was compiled with OCaml") ++ + spc () ++ str s ++ spc () ++ str "while this instance of Coq was compiled \ + with OCaml" ++ spc() ++ str Coq_config.caml_version ++ str "." ++ spc () ++ + str "Coq object files need to be compiled with the same OCaml toolchain to \ + be compatible.") + else () + let input_binary_int f ch = try input_binary_int ch with diff --git a/lib/system.mli b/lib/system.mli index 4a8c35b6ea..1e2f519327 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -88,6 +88,8 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val marshal_out : out_channel -> 'a -> unit val marshal_in : string -> in_channel -> 'a +val check_caml_version : caml:string -> file:string -> unit + (** {6 Time stamps.} *) type time diff --git a/library/global.mli b/library/global.mli index 2acd7e2a67..2767594171 100644 --- a/library/global.mli +++ b/library/global.mli @@ -22,7 +22,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool val universes : unit -> UGraph.t -val universes_lbound : unit -> Univ.Level.t +val universes_lbound : unit -> UGraph.Bound.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Constr.named_context diff --git a/man/coq-tex.1 b/man/coq-tex.1 index 7e0a2f81e2..e4cea24c55 100644 --- a/man/coq-tex.1 +++ b/man/coq-tex.1 @@ -1,4 +1,4 @@ -.TH COQ-TEX 1 "29 March 1995" +.TH COQ-TEX 1 .SH NAME coq-tex \- Process Coq phrases embedded in LaTeX files @@ -66,7 +66,7 @@ with `.v.tex' appended. The files produced by .B coq-tex -can be directly processed by LaTeX. +can be directly processed by LaTeX. Both the Coq phrases and the toplevel output are typeset in typewriter font. @@ -86,7 +86,7 @@ folding is performed on the Coq input text. Cause the file .IR coq-image to be executed to evaluate the Coq phrases. By default, -this is the command +this is the command .IR coqtop without specifying any path which is used to evaluate the Coq phrases. .TP diff --git a/man/coq_makefile.1 b/man/coq_makefile.1 index b5de6d367d..0f5912a4bb 100644 --- a/man/coq_makefile.1 +++ b/man/coq_makefile.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coq_makefile \- The Coq Proof Assistant makefile generator diff --git a/man/coqc.1 b/man/coqc.1 index 1e597afd99..a7be343fa0 100644 --- a/man/coqc.1 +++ b/man/coqc.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coqc \- The Coq Proof Assistant compiler @@ -19,14 +19,14 @@ is the batch compiler for the Coq Proof Assistant. The options are basically the same as coqtop(1). .IR file.v \& is the vernacular file to compile. -.IR file \& +.IR file \& must be formed only with the characters `a` to `Z`, `0`-`9` or `_` and must begin with a letter. The compiler produces an object file .IR file.vo \&. -For interactive use of Coq, see +For interactive use of Coq, see .BR coqtop(1). @@ -35,7 +35,7 @@ For interactive use of Coq, see .B coqc is a script that simply runs .B coqtop -with option +with option .B \-compile it accepts the same options as .B coqtop. diff --git a/man/coqchk.1 b/man/coqchk.1 index f9241c0d47..2f9e1fd84d 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "July 7, 201" +.TH COQ 1 .SH NAME coqchk \- The Coq Proof Checker compiled libraries verifier @@ -29,7 +29,7 @@ short or qualified logical name, or by their filename. .TP .BI \-I \ dir, \ \-\-include \ dir -add directory +add directory .I dir in the include path diff --git a/man/coqdep.1 b/man/coqdep.1 index 0770ce88c8..b0d9606969 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "28 March 1995" "Coq tools" +.TH COQ 1 .SH NAME coqdep \- Compute inter-module dependencies for Coq and Caml programs @@ -31,13 +31,13 @@ When a directory is given as argument, it is recursively looked at. Dependencies of Coq modules are computed by looking at .IR Require \& commands (Require, Require Export, Require Import), -.IR Declare \& -.IR ML \& +.IR Declare \& +.IR ML \& .IR Module \& commands and .IR Load \& commands. Dependencies relative to modules from the Coq library are not -printed except if +printed except if .BR \-boot \& is given. @@ -51,27 +51,27 @@ directives and the dot notation .TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. -.TP +.TP .BI \-I/\-Q/\-R \ options Have the same effects on load path and modules names as for other coq commands (coqtop, coqc). -.TP +.TP .BI \-coqlib \ directory Indicates where is the Coq library. The default value has been determined at installation time, and therefore this option should not be used under normal circumstances. -.TP +.TP .BI \-exclude-dir \ dir Skips subdirectory .IR dir \ during .BR -R/-Q \ search. -.TP +.TP .B \-sort Output the given file name ordered by dependencies. .TP .B \-vos Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode) -.TP +.TP .B \-boot For coq developers, prints dependencies over coq library files (omitted by default). @@ -106,7 +106,7 @@ Consider the files (in the same directory): where .TP -.BI \+ +.BI \+ D.ml contains the commands `open A', `open B' and `type t = C.t' ; .TP .BI \+ diff --git a/man/coqdoc.1 b/man/coqdoc.1 index 8d71a8746d..e8a58611f0 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -1,4 +1,4 @@ -.TH coqdoc 1 "April, 2006" +.TH coqdoc 1 .SH NAME coqdoc \- A documentation tool for the Coq proof assistant @@ -47,12 +47,12 @@ Select a TeXmacs output. Redirect the output to stdout .TP .BI \-o \ file, \-\-output \ file -Redirect the output into the file +Redirect the output into the file .I file. .TP .BI \-d \ dir, \ \-\-directory \ dir -Output files into directory -.I dir +Output files into directory +.I dir instead of current directory (option \-d does not change the filename specified with option \-o, if any). .TP @@ -102,7 +102,7 @@ Generate one page for each category and each letter in the index, together with a top page index.html. .SS Table of contents option - + .TP .B \-toc, \ \-\-table\-of\-contents Insert a table of contents. For a LATEX output, it inserts a @@ -136,7 +136,7 @@ Set the base path where the Coq files are installed, especially style files coqd .BI \-R \ dir \ coqdir Map physical directory dir to Coq logical directory coqdir (similarly to Coq option \-R). -.B Note: +.B Note: option \-R only has effect on the files following it on the command line, so you will probably need to put this option first. @@ -155,26 +155,26 @@ Light mode. Suppress proofs (as with \-g) and the following commands: * Require * Transparent / Opaque * Implicit Argument / Implicits - * Section / Variable / Hypothesis / End + * Section / Variable / Hypothesis / End The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). .SS Language options - + Default behavior is to assume ASCII 7 bits input files. -.TP +.TP .B \-latin1, \ \-\-latin1 Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1 \-\-charset iso\-8859\-1. -.TP +.TP .B \-utf8, \ \-\-utf8 Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/. -.TP +.TP .BI \-\-inputenc \ string Give a LATEX input encoding, as an option to LATEX package inputenc. @@ -187,4 +187,3 @@ Specify the HTML character set, to be inserted in the HTML header. .I The Coq Reference Manual from http://coq.inria.fr/ - diff --git a/man/coqide.1 b/man/coqide.1 index c1af046019..267f8a8d4b 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -1,4 +1,4 @@ -.TH COQIDE 1 "July 16, 2004" +.TH COQIDE 1 .SH NAME coqide \- The Coq Proof Assistant graphical interface @@ -17,7 +17,7 @@ is a gtk graphical interface for the Coq proof assistant. For command-line-oriented use of Coq, see .BR coqtop (1) -; for batch-oriented use of Coq, see +; for batch-oriented use of Coq, see .BR coqc (1). diff --git a/man/coqtop.1 b/man/coqtop.1 index e799bc7748..74380f9679 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "October 11, 2006" +.TH COQ 1 .SH NAME coqtop \- The Coq Proof Assistant toplevel system @@ -17,7 +17,7 @@ is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. -For batch-oriented use of Coq, see +For batch-oriented use of Coq, see .BR coqc(1). @@ -29,12 +29,12 @@ Help. Will give you the complete list of options accepted by coqtop. .TP .BI \-I \ dir, \ \-\-include \ dir -add directory +add directory .I dir in the include path .TP -.BI \-R \ dir\ coqdir +.BI \-R \ dir\ coqdir recursively map physical .I dir to logical @@ -67,7 +67,7 @@ load Coq file (Load filename.) .TP -.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename +.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename load verbosely Coq file .I filename.v (Load Verbose filename.) diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1 index ad1a358c32..4ef317749d 100644 --- a/man/coqtop.byte.1 +++ b/man/coqtop.byte.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coqtop.byte \- The bytecode Coq toplevel @@ -31,5 +31,3 @@ and The Coq Reference Manual. .I The Coq web site: http://coq.inria.fr - - diff --git a/man/coqtop.opt.1 b/man/coqtop.opt.1 index 17c763da33..fc097a2ecf 100644 --- a/man/coqtop.opt.1 +++ b/man/coqtop.opt.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "April 25, 2001" +.TH COQ 1 .SH NAME coqtop.opt \- The native-code Coq toplevel @@ -31,5 +31,3 @@ and The Coq Reference Manual. .I The Coq web site: http://coq.inria.fr - - diff --git a/man/coqwc.1 b/man/coqwc.1 index eee37f3d1f..344b1fecc5 100644 --- a/man/coqwc.1 +++ b/man/coqwc.1 @@ -1,4 +1,4 @@ -.TH COQ 1 "16 March 2004" "Coq tools" +.TH COQ 1 .SH NAME coqwc \- print the number of specification, proof and comment lines in diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 963f029766..c19dd00b38 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -26,16 +26,6 @@ open Pcoq.Constr (* TODO: avoid this redefinition without an extra dep to Notation_ops *) let ldots_var = Id.of_string ".." -let constr_kw = - [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; - "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "SProp"; "Prop"; "Set"; "Type"; - ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>"; - ".("; "()"; "`{"; "`("; "@{"; "{|"; - "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ] - -let _ = List.iter CLexer.add_keyword constr_kw - let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 9c50109bb3..cc59b2175b 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -15,10 +15,6 @@ open Libnames open Pcoq.Prim -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"] -let _ = List.iter CLexer.add_keyword prim_kw - - let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string ?loc s = @@ -53,7 +49,7 @@ GRAMMAR EXTEND Gram bignat bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring ne_string string lstring pattern_ident pattern_identref by_notation - smart_global bar_cbrace; + smart_global bar_cbrace strategy_level; preident: [ [ s = IDENT -> { s } ] ] ; @@ -140,4 +136,10 @@ GRAMMAR EXTEND Gram bar_cbrace: [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] ; + strategy_level: + [ [ IDENT "expand" -> { Conv_oracle.Expand } + | IDENT "opaque" -> { Conv_oracle.Opaque } + | n=integer -> { Conv_oracle.Level n } + | IDENT "transparent" -> { Conv_oracle.transparent } ] ] + ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 5b0562fb0d..2cc16f85d5 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -276,6 +276,7 @@ module Prim = let reference = make_gen_entry uprim "reference" let by_notation = Entry.create "by_notation" let smart_global = Entry.create "smart_global" + let strategy_level = gec_gen "strategy_level" (* parsed like ident but interpreted as a term *) let var = gec_gen "var" @@ -505,6 +506,7 @@ let () = Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 90088be307..bd64d21518 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -170,6 +170,7 @@ module Prim : val ne_lstring : lstring Entry.t val var : lident Entry.t val bar_cbrace : unit Entry.t + val strategy_level : Conv_oracle.level Entry.t end module Constr : diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0c305d09e8..c485c38009 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) | SymAx c -> @@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic = app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHEN injt (proof_tac prf)))) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = @@ -508,11 +506,9 @@ let f_equal = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = - try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match EConstr.kind sigma concl with diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f0457acd68..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -243,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type = let new_ctxt, new_end_of_type = decompose_prod_n_assum sigma ctxt_size new_type_of_hyp in - let prove_new_hyp : tactic = - tclTHEN - (tclDO ctxt_size (Proofview.V82.of_tactic intro)) - (fun g -> - let all_ids = pf_ids_of_hyps g in - let new_ids, _ = list_chop ctxt_size all_ids in - let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.type_of g to_refine in - tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g) + let prove_new_hyp = + let open Tacticals.New in + let open Tacmach.New in + tclTHEN (tclDO ctxt_size intro) + (Proofview.Goal.enter (fun g -> + let all_ids = pf_ids_of_hyps g in + let new_ids, _ = list_chop ctxt_size all_ids in + let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in + let evm, _ = + Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g) + to_refine + in + tclTHEN + (Proofview.Unsafe.tclEVARS evm) + (Proofview.V82.tactic (refine to_refine)))) in let simpl_eq_tac = change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp - prove_new_hyp + (Proofview.V82.of_tactic prove_new_hyp) in (* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) (* str "removing an equation " ++ fnl ()++ *) @@ -534,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id = let prov_hid = pf_get_new_id hid g in let c = mkApp (mkVar hid, args) in let evm, _ = pf_apply Typing.type_of g c in - tclTHENLIST - [ Refiner.tclEVARS evm - ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c) - ; thin [hid] - ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ] + let open Tacticals.New in + Proofview.V82.of_tactic + (tclTHENLIST + [ Proofview.Unsafe.tclEVARS evm + ; pose_proof (Name prov_hid) c + ; clear [hid] + ; rename_hyp [(prov_hid, hid)] ]) g) (fun (* if not then we are in a mutual function block diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e83fe56cc9..af53f16e1f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -2,7 +2,7 @@ open Names open Pp open Constr open Libnames -open Refiner +open Tacmach let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id) let mk_rel_id = mk_prefix "R_" @@ -395,7 +395,8 @@ let jmeq_refl () = with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = - tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l + Proofview.V82.of_tactic + (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l) let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" @@ -427,15 +428,16 @@ let evaluable_of_global_reference r = | _ -> assert false let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) = - tclREPEAT - (List.fold_right - (fun (eq, b) i -> - tclORELSE - (Proofview.V82.of_tactic - ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) - i) - (if rev then List.rev eqs else eqs) - (tclFAIL 0 (mt ()))) + let open Tacticals in + (tclREPEAT + (List.fold_right + (fun (eq, b) i -> + tclORELSE + (Proofview.V82.of_tactic + ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) + i) + (if rev then List.rev eqs else eqs) + (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"]) let decompose_lam_n sigma n = if n < 0 then diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5c82ed38bb..9b2d9c4815 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g = in continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g -let pf_type c tac gl = - let evars, ty = Typing.type_of (pf_env gl) (project gl) c in - tclTHEN (Refiner.tclEVARS evars) (tac ty) gl +let pf_type c tac = + let open Tacticals.New in + Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let evars, ty = Typing.type_of env sigma c in + tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty)) + +let pf_type c tac = + Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty))) let pf_typel l tac = let rec aux tys l = diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 17a7121a3f..f867a47c08 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -14,10 +14,7 @@ open Constr open Context open CErrors open Evar_refiner -open Tacmach open Tacexpr -open Refiner -open Evd open Locus open Context.Named.Declaration open Ltac_pretype @@ -26,7 +23,11 @@ module NamedDecl = Context.Named.Declaration (* The instantiate tactic *) -let instantiate_evar evk (ist,rawc) env sigma = +let instantiate_evar evk (ist,rawc) = + let open Proofview.Notations in + Proofview.tclENV >>= fun env -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let evi = Evd.find sigma evk in let filtered = Evd.evar_filtered_env env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in @@ -37,7 +38,8 @@ let instantiate_evar evk (ist,rawc) env sigma = ltac_genargs = ist.Geninterp.lfun; } in let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in - tclEVARS sigma' + Proofview.Unsafe.tclEVARS sigma' + end let evar_list sigma c = let rec evrec acc c = @@ -47,14 +49,15 @@ let evar_list sigma c = evrec [] c let instantiate_tac n c ido = - Proofview.V82.tactic begin fun gl -> - let env = Global.env () in - let sigma = gl.sigma in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in let evl = match ido with - ConclLocation () -> evar_list sigma (pf_concl gl) + ConclLocation () -> evar_list sigma concl | HypLocation (id,hloc) -> - let decl = Environ.lookup_named id (pf_env gl) in + let decl = Environ.lookup_named id env in match hloc with InHyp -> (match decl with @@ -70,17 +73,16 @@ let instantiate_tac n c ido = user_err Pp.(str "Not enough uninstantiated existential variables."); if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in - instantiate_evar evk c env sigma gl + instantiate_evar evk c end let instantiate_tac_by_name id c = - Proofview.V82.tactic begin fun gl -> - let env = Global.env () in - let sigma = gl.sigma in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in let evk = try Evd.evar_key id sigma with Not_found -> user_err Pp.(str "Unknown existential variable.") in - instantiate_evar evk c env sigma gl + instantiate_evar evk c end let let_evar name typ = diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index c4731e5c34..eb53fd45d0 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -31,6 +31,8 @@ let create_generic_quotation name e wit = let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string +let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global + let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr @@ -342,3 +344,55 @@ let pr_lpar_id_colon _ _ _ _ = mt () ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon } | [ local_test_lpar_id_colon(x) ] -> { () } END + +{ + +(* Work around a limitation of the macro system *) +let strategy_level0 = Pcoq.Prim.strategy_level + +let pr_strategy _ _ _ v = Conv_oracle.pr_level v + +} + +ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy } +| [ strategy_level0(n) ] -> { n } +END + +{ + +let intern_strategy ist v = match v with +| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id) +| ArgArg v -> ArgArg v + +let subst_strategy _ v = v + +let interp_strategy ist gl = function +| ArgArg n -> gl.Evd.sigma, n +| ArgVar { CAst.v = id; CAst.loc } -> + let v = + try Id.Map.find id ist.lfun + with Not_found -> + CErrors.user_err ?loc + (str "Unbound variable " ++ Id.print id ++ str".") + in + let v = + try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v + with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level" + in + gl.Evd.sigma, v + +let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v + +} + +ARGUMENT EXTEND strategy_level_or_var + TYPED AS strategy_level + PRINTED BY { pr_strategy } + INTERPRETED BY { interp_strategy } + GLOBALIZED BY { intern_strategy } + SUBSTITUTED BY { subst_strategy } + RAW_PRINTED BY { pr_loc_strategy } + GLOB_PRINTED BY { pr_loc_strategy } +| [ strategy_level(n) ] -> { ArgArg n } +| [ identref(id) ] -> { ArgVar id } +END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fbdb7c0032..e52bf55f71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -78,3 +78,7 @@ val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Id.t Locus.clause_expr) Genarg.genarg_type + +val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type + +val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0bad3cbe5b..ffb597d4cb 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP = TACTIC EXTEND optimize_heap | [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP } END + +(** Tactic analogous to [Strategy] vernacular *) + +TACTIC EXTEND with_strategy +| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> { + with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac) +} +END diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0f0341f123..81e745b714 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -54,16 +54,23 @@ END { +let pr_search_strategy_name _prc _prlc _prt = function + | Dfs -> Pp.str "dfs" + | Bfs -> Pp.str "bfs" + let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" + | Some s -> pr_search_strategy_name _prc _prlc _prt s | None -> Pp.mt () } +ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name } +| [ "bfs" ] -> { Bfs } +| [ "dfs" ] -> { Dfs } +END + ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } -| [ "(bfs)" ] -> { Some Bfs } -| [ "(dfs)" ] -> { Some Dfs } +| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s } | [ ] -> { None } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index aef5f645f4..0e661543db 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 6a158bde17..e51b1f051d 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -30,9 +30,6 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] -let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw - let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 09f1fc371a..d74e981c6d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1325,6 +1325,8 @@ let () = register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref pr_qualid (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_smart_global + (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 04d85ed390..91d26519b8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v = | VarRef var -> EvalVarRef var | ConstRef c -> EvalConstRef c | IndRef _ | ConstructRef _ -> fail () + else if has_type v (topwit wit_smart_global) then + let open GlobRef in + let r = out_gen (topwit wit_smart_global) v in + match r with + | VarRef var -> EvalVarRef var + | ConstRef c -> EvalConstRef c + | IndRef _ | ConstructRef _ -> fail () else match Value.to_constr v with | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c)) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 597c3fdaac..1aa3af0087 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -95,9 +95,16 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) - else - try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> Nametab.error_global_not_found qid + else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then + let id = qualid_basename qid in + ArgArg (qid.CAst.loc, GlobRef.VarRef id) + else match locate_global_with_alias qid with + | r -> ArgArg (qid.CAst.loc, r) + | exception Not_found -> + if not !strict_check && qualid_is_ident qid then + let id = qualid_basename qid in + ArgArg (qid.CAst.loc, GlobRef.VarRef id) + else Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -305,6 +312,12 @@ let intern_evaluable_reference_or_by_notation ist = function (Notation.interp_notation_as_global_reference ?loc GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) +let intern_smart_global ist = function + | {v=AN r} -> intern_global_reference ist r + | {v=ByNotation (ntn,sc);loc} -> + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc + GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) + (* Globalize a reduction expression *) let intern_evaluable ist r = let f ist r = @@ -813,6 +826,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); + Genintern.register_intern0 wit_smart_global (lift intern_smart_global); Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6debc7d9b9..6d350ade8d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -162,17 +162,27 @@ let catching_error call_trace fail (e, info) = fail located_exc end -let catch_error call_trace f x = +let update_loc ?loc (e, info) = + (e, Option.cata (Loc.add_loc info) info loc) + +let catch_error ?loc call_trace f x = try f x with e when CErrors.noncritical e -> let e = Exninfo.capture e in + let e = update_loc ?loc e in catching_error call_trace Exninfo.iraise e -let wrap_error tac k = - if is_traced () then Proofview.tclORELSE tac k else tac +let catch_error_loc ?loc tac = + Proofview.tclOR tac (fun exn -> + let (e, info) = update_loc ?loc exn in + Proofview.tclZERO ~info e) + +let wrap_error ?loc tac k = + if is_traced () then Proofview.tclORELSE tac k + else catch_error_loc ?loc tac -let catch_error_tac call_trace tac = - wrap_error +let catch_error_tac ?loc call_trace tac = + wrap_error ?loc tac (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) @@ -535,9 +545,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = ltac_idents = constrvars.idents; ltac_genargs = ist.lfun; } in - let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in + let loc = loc_of_glob_constr term in + let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in let (evd,c) = - catch_error trace (understand_ltac flags env sigma vars kind) term + catch_error ?loc trace (understand_ltac flags env sigma vars kind) term in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess @@ -1059,7 +1070,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let call = LtacAtomCall t in let trace = push_trace(loc,call) ist in Profile_ltac.do_profile "eval_tactic:2" trace - (catch_error_tac trace (interp_atomic ist t)) + (catch_error_tac ?loc trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) | TacId s -> @@ -1087,7 +1098,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacShowHyps tac -> Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) - end + end [@ocaml.warning "-3"] | TacAbstract (t,ido) -> let call = LtacMLCall tac in let trace = push_trace(None,call) ist in @@ -1149,7 +1160,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with ; poly ; extra = TacStore.set ist.extra f_trace trace } in val_interp ist alias.Tacenv.alias_body >>= fun v -> - Ftactic.lift (tactic_of_value ist v) + Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v)) in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> @@ -1175,7 +1186,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in let tac args = let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in - Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) + Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist)) in Ftactic.run args tac @@ -1278,7 +1289,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace [] } in Profile_ltac.do_profile "interp_app" trace ~count_call:false - (catch_error_tac trace (val_interp ist body)) >>= fun v -> + (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -2022,6 +2033,7 @@ let interp_pre_ident ist env sigma s = let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); + register_interp0 wit_smart_global (lift interp_reference); register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 600c30b403..ed298b7e66 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ee2c87d19a..0f8d941b41 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1897,8 +1897,6 @@ type provername = string * int option * The caching mechanism. *) -open Persistent_cache - module MakeCache (T : sig type prover_option type coeff @@ -1922,7 +1920,7 @@ struct Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0) end - include PHashtable (E) + include Persistent_cache.PHashtable (E) let memo_opt use_cache cache_file f = let memof = memo cache_file f in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 633cdbd735..e7c75e029e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - try (* find_ring_strucure can raise an exception *) - 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 ring = ltac_ring_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + 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 ring = ltac_ring_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl])) end (***********************************************************************) @@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - try - 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 field = ltac_field_structure e in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + 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 field = ltac_field_structure e in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl])) end diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 62d4adca43..01e8daf82d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -22,7 +22,7 @@ open Locusops open Ltac_plugin open Tacmach -open Refiner +open Tacticals open Libnames open Ssrmatching_plugin open Ssrmatching @@ -81,6 +81,9 @@ let nohint = false, [] type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma +let project gl = gl.Evd.sigma +let re_sig it sigma = { Evd.it = it; Evd.sigma = sigma } + let push_ctx a gl = re_sig (sig_it gl, a) (project gl) let push_ctxs a gl = re_sig (List.map (fun x -> x,a) (sig_it gl)) (project gl) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c7110d7a91..e77c5082dd 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -614,7 +614,7 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf = let set_names env sigma n brty = let open EConstr in let (ctxt,cl) = decompose_prod_n_assum sigma n brty in - EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt) + Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -631,11 +631,12 @@ let type_case_branches_with_names env sigma indspec p c = let nparams = mib.mind_nparams in let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in + let lbrty = Array.map EConstr.of_constr lbrty in (* Build case type *) let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then - (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty) + (set_pattern_names env sigma (fst ind) lbrty, conclty) else (lbrty, conclty) (* Type of Case predicates *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index ab69629595..2bec86599e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,7 +194,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : - env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> EConstr.types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2f0e472095..87b4255b88 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -321,10 +321,6 @@ let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = clenv_unify CUMUL ~flags (meta_reducible_instance clenv.env clenv.evd clenv.templtyp) concl clenv -let old_clenv_unique_resolver ?flags clenv gl = - let concl = Goal.V82.concl clenv.evd (sig_it gl) in - clenv_unique_resolver_gen ?flags clenv concl - let clenv_unique_resolver ?flags clenv gl = let concl = Proofview.Goal.concl gl in clenv_unique_resolver_gen ?flags clenv concl diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 1adfdb885a..4279ab4768 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -63,9 +63,6 @@ val clenv_unify : ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv (** unifies the concl of the goal with the type of the clenv *) -val old_clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv - val clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 6f24310cdb..0257a6f204 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -13,7 +13,6 @@ open Constr open Termops open Evd open EConstr -open Refiner open Logic open Reduction open Clenv diff --git a/proofs/logic.ml b/proofs/logic.ml index 406e71aafc..c7a1c32e7c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -28,16 +28,14 @@ module NamedDecl = Context.Named.Declaration type refiner_error = (* Errors raised by the refiner *) - | BadType of constr * constr * constr + | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * Evd.evar_map * refiner_error @@ -73,13 +71,11 @@ let catchable_exception = function let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) -(* Tells if the refiner should check that the submitted rules do not - produce invalid subgoals *) -let check = ref false -let with_check = Flags.with_option check +(* The check flag tells if the refiner should check that the submitted rules do + not produce invalid subgoals *) -let check_typability env sigma c = - if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma +let check_typability ~check env sigma c = + if check then fst (type_of env sigma (EConstr.of_constr c)) else sigma (************************************************************************) (************************************************************************) @@ -316,9 +312,9 @@ let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then raise (RefinerError (env, sigma, NonLinearProof c)) -let check_conv_leq_goal env sigma arg ty conclty = - if !check then - let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in +let check_conv_leq_goal ~check env sigma arg ty conclty = + if check then + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) conclty in match ans with | Some evm -> evm | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) @@ -334,28 +330,27 @@ let meta_free_prefix sigma a = in a with Stop acc -> Array.rev_of_list acc -let goal_type_of env sigma c = - if !check then +let goal_type_of ~check env sigma c = + if check then let (sigma,t) = type_of env sigma (EConstr.of_constr c) in (sigma, EConstr.Unsafe.to_constr t) else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) -let rec mk_refgoals sigma goal goalacc conclty trm = - let env = Goal.V82.env sigma goal in - let hyps = Goal.V82.hyps sigma goal in +let rec mk_refgoals ~check env sigma goalacc conclty trm = + let hyps = Environ.named_context_val env in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in - if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then + if (not check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in let t'ty = EConstr.Unsafe.to_constr t'ty in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else match kind trm with | Meta _ -> - let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in - if !check && occur_meta sigma conclty then + let conclty = nf_betaiota env sigma conclty in + if check && occur_meta sigma conclty then raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in let ev = EConstr.Unsafe.to_constr ev in @@ -363,9 +358,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> - let sigma = check_typability env sigma ty in - let sigma = check_conv_leq_goal env sigma trm ty conclty in - let res = mk_refgoals sigma goal goalacc ty t in + let sigma = check_typability ~check env sigma ty in + let sigma = check_conv_leq_goal ~check env sigma trm ty conclty in + let res = mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t in (* we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin @@ -388,24 +383,24 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let ty = EConstr.Unsafe.to_constr ty in goalacc, ty, sigma, f else - mk_hdgoals sigma goal goalacc f + mk_hdgoals ~check env sigma goalacc f in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in - let sigma = check_conv_leq_goal env sigma trm conclty' conclty in + let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in + let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in + let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in + let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -416,28 +411,27 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm."); - let (sigma, t'ty) = goal_type_of env sigma trm in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + let (sigma, t'ty) = goal_type_of ~check env sigma trm in + let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) (* Same as mkREFGOALS but without knowing the type of the term. Therefore, * Metas should be casted. *) -and mk_hdgoals sigma goal goalacc trm = - let env = Goal.V82.env sigma goal in - let hyps = Goal.V82.hyps sigma goal in +and mk_hdgoals ~check env sigma goalacc trm = + let hyps = Environ.named_context_val env in let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> - let sigma = check_typability env sigma ty in + let sigma = check_typability ~check env sigma ty in let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> - let sigma = check_typability env sigma ty in - mk_refgoals sigma goal goalacc ty t + let sigma = check_typability ~check env sigma ty in + mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t | App (f,l) -> let (acc',hdty,sigma,applicand) = @@ -445,15 +439,15 @@ and mk_hdgoals sigma goal goalacc trm = then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) - else mk_hdgoals sigma goal goalacc f + else mk_hdgoals ~check env sigma goalacc f in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in + let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -462,21 +456,21 @@ and mk_hdgoals sigma goal goalacc trm = (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | _ -> - if !check && occur_meta sigma (EConstr.of_constr trm) then + if check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta."); - let (sigma, ty) = goal_type_of env sigma trm in + let (sigma, ty) = goal_type_of env ~check sigma trm in goalacc, ty, sigma, trm -and mk_arggoals sigma goal goalacc funty allargs = +and mk_arggoals ~check env sigma goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = whd_all env sigma (EConstr.of_constr funty) in let t = EConstr.Unsafe.to_constr t in let rec collapse t = match kind t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) @@ -485,19 +479,17 @@ and mk_arggoals sigma goal goalacc funty allargs = let t = collapse t in match kind t with | Prod (_, c1, b) -> - let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in + let (acc, hargty, sigma, arg) = mk_refgoals ~check env sigma goalacc (EConstr.of_constr c1) harg in (acc, subst1 harg b, sigma), arg | _ -> - let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs -and mk_casegoals sigma goal goalacc p c = - let env = Goal.V82.env sigma goal in - let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in +and mk_casegoals ~check env sigma goalacc p c = + let (acc',ct,sigma,c') = mk_hdgoals ~check env sigma goalacc c in let ct = EConstr.of_constr ct in - let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in + let (acc'',pt,sigma,p') = mk_hdgoals ~check env sigma acc' p in let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals.") in @@ -505,20 +497,19 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') -and treat_case sigma goal ci lbrty lf acc' = +and treat_case ~check env sigma ci lbrty lf acc' = let rec strip_outer_cast c = match kind c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c in let decompose_app_vect c = match kind c with | App (f,cl) -> (f, cl) | _ -> (c,[||]) in - let env = Goal.V82.env sigma goal in Array.fold_left3 (fun (lacc,sigma,bacc) ty fi l -> if isMeta (strip_outer_cast fi) then (* Support for non-eta-let-expanded Meta as found in *) (* destruct/case with an non eta-let expanded elimination scheme *) - let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in + let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in r,s,(fi'::bacc) else (* Deal with a branch in expanded form of the form @@ -539,14 +530,14 @@ and treat_case sigma goal ci lbrty lf acc' = if isMeta head then begin assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); let head' = lift (-n) head in - let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in + let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in (r,s,fi'::bacc) end else (* Supposed to be meta-free *) - let sigma, t'ty = goal_type_of env sigma fi in - let sigma = check_conv_leq_goal env sigma fi t'ty ty in + let sigma, t'ty = goal_type_of ~check env sigma fi in + let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags @@ -574,18 +565,18 @@ let convert_hyp ~check ~reorder env sigma d = (************************************************************************) (* Primitive tactics are handled here *) -let prim_refiner r sigma goal = - let env = Goal.V82.env sigma goal in - let cl = Goal.V82.concl sigma goal in - let cl = EConstr.Unsafe.to_constr cl in +let refiner ~check r = + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let st = Proofview.Goal.state gl in + let cl = Proofview.Goal.concl gl in check_meta_variables env sigma r; - let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in - let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in - (sgl, sigma) - -let prim_refiner ~check r sigma goal = - if check then - with_check (prim_refiner r sigma) goal - else - prim_refiner r sigma goal + let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in + let map gl = Proofview.goal_with_state gl st in + let sgl = List.rev_map map sgl in + let sigma = Goal.V82.partial_solution env sigma (Proofview.Goal.goal gl) (EConstr.of_constr oterm) in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS sgl + end diff --git a/proofs/logic.mli b/proofs/logic.mli index ef8b2731b2..9dc75000a1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -26,23 +26,21 @@ open Evd (** The primitive refiner. *) -val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map +val refiner : check:bool -> constr -> unit Proofview.tactic (** {6 Refiner errors. } *) type refiner_error = (*i Errors raised by the refiner i*) - | BadType of constr * constr * constr + | BadType of constr * constr * EConstr.t | UnresolvedBindings of Name.t list | CannotApply of constr * constr - | NotWellTyped of constr | NonLinearProof of constr | MetaInType of EConstr.constr (*i Errors raised by the tactics i*) | IntroNeedsProduct - | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t exception RefinerError of Environ.env * evar_map * refiner_error diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 29a47c5acd..874bab277d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -12,7 +12,6 @@ open Pp open CErrors open Util open Evd -open Logic type tactic = Proofview.V82.tac @@ -26,18 +25,7 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let refiner ~check pr goal_sigma = - let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in - { it = sgl; sigma = sigma'; } - -(* Profiling refiner *) -let refiner ~check = - if Flags.profile then - let refiner_key = CProfile.declare_profile "refiner" in - CProfile.profile2 refiner_key (refiner ~check) - else refiner ~check - -let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c) +let refiner = Logic.refiner (*********************) (* Tacticals *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 3471f38e9e..a3cbfb5d5d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -28,42 +28,53 @@ val refiner : check:bool -> Constr.t -> unit Proofview.tactic (** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic +[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"] val tclIDTAC_MESSAGE : Pp.t -> tactic +[@@ocaml.deprecated] (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic +[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"] (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) val tclTHEN : tactic -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHEN"] (** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More convenient than [tclTHEN] when [n] is large *) val tclTHENLIST : tactic list -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"] (** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) val tclMAP : ('a -> tactic) -> 'a list -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclMAP"] (** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *) val tclTHEN_i : tactic -> (int -> tactic) -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"] (** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the last resulting subgoal (previously called [tclTHENL]) *) val tclTHENLAST : tactic -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"] (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : tactic -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"] (** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises an error if the number of resulting subgoals is not [n] *) val tclTHENSV : tactic -> tactic array -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"] (** Same with a list of tactics *) val tclTHENS : tactic -> tactic list -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENS"] (** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to @@ -71,15 +82,18 @@ val tclTHENS : tactic -> tactic list -> tactic subgoals and [tac2] to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less than [n+m] *) val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"] (** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the last [n] resulting subgoals and [tac2] on the remaining first subgoals *) val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"] (** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then applies [t1],...,[tn] on the first [n] resulting subgoals and [tac2] for the remaining last subgoals (previously called tclTHENST) *) val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"] (** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t @@ -89,15 +103,28 @@ exception FailError of int * Pp.t Lazy.t val catch_failerror : Exninfo.iexn -> unit val tclORELSE0 : tactic -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"] val tclORELSE : tactic -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclORELSE"] val tclREPEAT : tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"] val tclFIRST : tactic list -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclFIRST"] val tclTRY : tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTRY"] val tclTHENTRY : tactic -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"] val tclCOMPLETE : tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"] val tclAT_LEAST_ONCE : tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"] val tclFAIL : int -> Pp.t -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclFAIL"] val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"] val tclDO : int -> tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclDO"] val tclPROGRESS : tactic -> tactic +[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"] val tclSHOWHYPS : tactic -> tactic +[@@ocaml.deprecated "Internal tactic. Do not use."] diff --git a/stm/stm.ml b/stm/stm.ml index 5790bfc07e..b296f8f08f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2576,6 +2576,21 @@ end (* }}} *) (******************************************************************************) (** STM initialization options: *) + +type option_command = OptionSet of string option | OptionUnset + +type injection_command = + | OptionInjection of (Goptions.option_name * option_command) + (** Set flags or options before the initial state is ready. *) + | RequireInjection of (string * string option * bool option) + (** Require libraries before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) + (* -load-vernac-source interleaving is not supported yet *) + (* | LoadInjection of (string * bool) *) + type stm_init_options = { doc_type : stm_doc_type (** The STM does set some internal flags differently depending on @@ -2589,12 +2604,9 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; require_libs : (string * string option * bool option) list - (** Require [require_libs] before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) + ; injections : injection_command list + (** Injects Require and Set/Unset commands before the initial + state is ready *) ; stm_options : AsyncOpts.stm_opt (** Low-level STM options *) @@ -2625,13 +2637,51 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } = +let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = let require_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in + let interp_set_option opt v old = + let open Goptions in + let err expect = + let opt = String.concat " " opt in + let got = v in (* avoid colliding with Pp.v *) + CErrors.user_err + Pp.(str "-set: " ++ str opt ++ + str" expects " ++ str expect ++ + str" but got " ++ str got) + in + match old with + | BoolValue _ -> + let v = match String.trim v with + | "true" -> true + | "false" | "" -> false + | _ -> err "a boolean" + in + BoolValue v + | IntValue _ -> + let v = String.trim v in + let v = match int_of_string_opt v with + | Some _ as v -> v + | None -> if v = "" then None else err "an int" + in + IntValue v + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) in + + let set_option = let open Goptions in function + | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt + | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in + + let handle_injection = function + | RequireInjection r -> require_file r + (* | LoadInjection l -> *) + | OptionInjection o -> set_option o in + (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2670,7 +2720,7 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } end; (* Import initial libraries. *) - List.iter require_file require_libs; + List.iter handle_injection injections; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; diff --git a/stm/stm.mli b/stm/stm.mli index 2c27d63b82..9780c96512 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,6 +52,20 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) +type option_command = OptionSet of string option | OptionUnset + +type injection_command = + | OptionInjection of (Goptions.option_name * option_command) + (** Set flags or options before the initial state is ready. *) + | RequireInjection of (string * string option * bool option) + (** Require libraries before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) + (* -load-vernac-source interleaving is not supported yet *) + (* | LoadInjection of (string * bool) *) + (** STM initialization options: *) type stm_init_options = { doc_type : stm_doc_type @@ -66,12 +80,9 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; require_libs : (string * string option * bool option) list - (** Require [require_libs] before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) + ; injections : injection_command list + (** Injects Require and Set/Unset commands before the initial + state is ready *) ; stm_options : AsyncOpts.stm_opt (** Low-level STM options *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 31384a353c..58345ac253 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1708,12 +1708,42 @@ let is_eq_x gl x d = with Constr_matching.PatternMatchingFailure -> () +exception FoundDepInGlobal of Id.t option * GlobRef.t + +let test_non_indirectly_dependent_section_variable gl x = + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + List.iter (fun decl -> + NamedDecl.iter_constr (fun c -> + match occur_var_indirectly env sigma x c with + | Some gr -> raise (FoundDepInGlobal (Some (NamedDecl.get_id decl), gr)) + | None -> ()) decl) hyps; + match occur_var_indirectly env sigma x concl with + | Some gr -> raise (FoundDepInGlobal (None, gr)) + | None -> () + +let check_non_indirectly_dependent_section_variable gl x = + try test_non_indirectly_dependent_section_variable gl x + with FoundDepInGlobal (pos,gr) -> + let where = match pos with + | Some id -> str "hypothesis " ++ Id.print id + | None -> str "the conclusion of the goal" in + user_err ~hdr:"Subst" + (strbrk "Section variable " ++ Id.print x ++ + strbrk " occurs implicitly in global declaration " ++ Printer.pr_global gr ++ + strbrk " present in " ++ where ++ strbrk ".") + +let is_non_indirectly_dependent_section_variable gl z = + try test_non_indirectly_dependent_section_variable gl z; true + with FoundDepInGlobal (pos,gr) -> false + (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -1722,7 +1752,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) - && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps + && List.exists (fun y -> local_occur_var_in_decl sigma y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in (dest,id::deps,(id_dest,id)::allhyps) @@ -1731,7 +1761,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = hyps (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) - let depconcl = occur_var env sigma x concl in + let depconcl = local_occur_var sigma x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then @@ -1762,6 +1792,8 @@ let subst_one_var dep_proof_ok x = (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in + if is_section_variable x then + check_non_indirectly_dependent_section_variable gl x; subst_one dep_proof_ok x res end @@ -1795,53 +1827,37 @@ let subst_all ?(flags=default_subst_tactic_flags) () = if !regular_subst_tactic then - (* First step: find hypotheses to treat in linear time *) - let find_equations gl = - let env = Proofview.Goal.env gl in - let sigma = project gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let select_equation_name decl = + (* Find hypotheses to treat in linear time *) + let process hyp = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = project gl in + let c = pf_get_hyp hyp gl |> NamedDecl.get_type in try - let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in + let lbeq,u,(_,x,y) = pf_apply find_eq_data_decompose gl c in let u = EInstance.kind sigma u in let eq = Constr.mkRef (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with - | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) - | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) + | Var x, Var y when Id.equal x y -> + Proofview.tclUNIT () + | Var x', _ when not (Termops.local_occur_var sigma x' y) && + not (is_evaluable env (EvalVarRef x')) && + is_non_indirectly_dependent_section_variable gl x' -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (Termops.local_occur_var sigma y' x) && + not (is_evaluable env (EvalVarRef y')) && + is_non_indirectly_dependent_section_variable gl y' -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> - None - with Constr_matching.PatternMatchingFailure -> None + Proofview.tclUNIT () + with Constr_matching.PatternMatchingFailure -> + Proofview.tclUNIT () + end in - let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter select_equation_name hyps) - in - - (* Second step: treat equations *) - let process hyp = Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let env = Proofview.Goal.env gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let c = pf_get_hyp hyp gl |> NamedDecl.get_type in - let _,_,(_,x,y) = find_eq_data_decompose c in - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else - match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) -> - subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) -> - subst_one flags.rewrite_dependent_proof y' (hyp,x,false) - | _ -> - Proofview.tclUNIT () + tclMAP process (List.rev (List.map NamedDecl.get_id (Proofview.Goal.hyps gl))) end - in - Proofview.Goal.enter begin fun gl -> - let ids = find_equations gl in - tclMAP process ids - end else diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 07f9def2c8..374706c8f9 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -29,6 +29,8 @@ module NamedDecl = Context.Named.Declaration type tactic = Proofview.V82.tac +[@@@ocaml.warning "-3"] + let tclIDTAC = Refiner.tclIDTAC let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE let tclORELSE0 = Refiner.tclORELSE0 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d0a13a8a40..378b6c7418 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5045,6 +5045,80 @@ let unify ?(state=TransparentState.full) x y = Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None))) end +(** [tclWRAPFINALLY before tac finally] runs [before] before each + entry-point of [tac] and passes the result of [before] to + [finally], which is then run at each exit-point of [tac], + regardless of whether it succeeds or fails. Said another way, if + [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun + ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with + [e], it behaves as [before >>= fun v -> finally v <*> tclZERO + e]. Note that if [tac] succeeds [n] times before finally failing, + [before] and [finally] are both run [n+1] times (once around each + succuess, and once more around the final failure). *) +(* We should probably export this somewhere, but it's not clear + where. As per + https://github.com/coq/coq/pull/12197#discussion_r418480525 and + https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't + export it from Proofview, because it seems somehow not primitive + enough. We don't export it from this file because it is more of a + tactical than a tactic. But we also don't export it from Tacticals + because all of the non-New tacticals there operate on `tactic`, not + `Proofview.tactic`, and all of the `New` tacticals that deal with + multi-success things are focussing, i.e., apply their arguments on + each goal separately (and it even says so in the comment on `New`), + whereas it's important that `tclWRAPFINALLY` doesn't introduce + extra focussing. *) +let rec tclWRAPFINALLY before tac finally = + let open Proofview in + let open Proofview.Notations in + before >>= fun v -> tclCASE tac >>= function + | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e + | Next (ret, tac') -> tclOR + (finally v >>= fun () -> tclUNIT ret) + (fun e -> tclWRAPFINALLY before (tac' e) finally) + +let with_set_strategy lvl_ql k = + let glob_key r = + match r with + | GlobRef.ConstRef sp -> ConstKey sp + | GlobRef.VarRef id -> VarKey id + | _ -> user_err Pp.(str + "cannot set an inductive type or a constructor as transparent") in + let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in + tclWRAPFINALLY + (Proofview.tclENV >>= fun env -> + let orig_kl = List.map (fun (_lvl, k) -> + (Conv_oracle.get_strategy (Environ.oracle env) k, k)) + kl in + (* Because the global env might be desynchronized from the + proof-local env, we need to update the global env to have this + tactic play nicely with abstract. + TODO: When abstract no longer depends on Global, delete this + let orig_kl_global = ... in *) + let orig_kl_global = List.map (fun (_lvl, k) -> + (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k)) + kl in + let env = List.fold_left (fun env (lvl, k) -> + Environ.set_oracle env + (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in + Proofview.Unsafe.tclSETENV env <*> + (* TODO: When abstract no longer depends on Global, remove this + [Proofview.tclLIFT] block *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*> + Proofview.tclUNIT (orig_kl, orig_kl_global)) + k + (fun (orig_kl, orig_kl_global) -> + (* TODO: When abstract no longer depends on Global, remove this + [Proofview.tclLIFT] block *) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global)) <*> + Proofview.tclENV >>= fun env -> + let env = List.fold_left (fun env (lvl, k) -> + Environ.set_oracle env + (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in + Proofview.Unsafe.tclSETENV env) + module Simple = struct (** Simplified version of some of the above tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c84ba17f23..b6eb48a3d9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -435,6 +435,12 @@ val declare_intro_decomp_eq : (types * constr * constr) -> constr * types -> unit Proofview.tactic) -> unit +(** Tactic analogous to the [Strategy] vernacular, but only applied + locally to the tactic argument *) +val with_set_strategy : + (Conv_oracle.level * Names.GlobRef.t list) list -> + 'a Proofview.tactic -> 'a Proofview.tactic + (** {6 Simple form of basic tactics. } *) module Simple : sig diff --git a/test-suite/bugs/closed/bug_10812.v b/test-suite/bugs/closed/bug_10812.v new file mode 100644 index 0000000000..68f3814781 --- /dev/null +++ b/test-suite/bugs/closed/bug_10812.v @@ -0,0 +1,28 @@ +(* subst with indirectly dependent section variables *) + +Section A. + +Variable a:nat. +Definition b := a. + +Goal a=1 -> a+a=1 -> b=1. +intros. +Fail subst a. (* was working; we make it failing *) +rewrite H in H0. +discriminate. +Qed. + +Goal a=1 -> a+a=1 -> b=1. +intros. +subst. (* should not apply to a *) +rewrite H in H0. +discriminate. +Qed. + +Goal forall t, a=t -> b=t. +intros. +subst. +reflexivity. +Qed. + +End A. diff --git a/test-suite/bugs/closed/bug_7903.v b/test-suite/bugs/closed/bug_7903.v index 55c7ee99a7..18e1884ca7 100644 --- a/test-suite/bugs/closed/bug_7903.v +++ b/test-suite/bugs/closed/bug_7903.v @@ -1,4 +1,4 @@ (* Slightly improving interpretation of Ltac subterms in notations *) Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). -Check bar x (x + x). +Check fun x => bar x (x + x). diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v new file mode 100644 index 0000000000..14232e8578 --- /dev/null +++ b/test-suite/bugs/closed/bug_9583.v @@ -0,0 +1,7 @@ +(* Was causing a stack overflow before #11613 *) +Declare Custom Entry bla. +Notation "[ t ]" := (t) (at level 0, t custom bla at level 0). +Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0). +Notation "t" := (t) (in custom bla at level 0, t constr at level 9). +Notation "0" := (0) (in custom bla at level 0). +Check fun x => [ ] x [ ]. diff --git a/test-suite/bugs/closed/bug_9679.v b/test-suite/bugs/closed/bug_9679.v new file mode 100644 index 0000000000..24e69d23f9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9679.v @@ -0,0 +1,6 @@ +(* Was raising an anomaly *) +Notation "'[#' ] f '|' x .. z '=n>' b" := + (fun x => .. (fun z => f b) ..) + (at level 201, x binder, z binder, + format "'[ ' [# ] '[' f | ']' x .. z =n> '[' b ']' ']'" + ). diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index e1c20a2059..7b3a460c8c 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -15,6 +15,39 @@ Fail foo (). constructor. Qed. + +(** Bindings are dynamic *) + +Ltac2 Type rec nat := [O | S (nat)]. + +Ltac2 rec nat_eq n m := + match n with + | O => match m with | O => true | S _ => false end + | S n => match m with | O => false | S m => nat_eq n m end + end. + +Ltac2 Type exn ::= [ Assertion_failed ]. + +Ltac2 assert_eq n m := + match nat_eq n m with + | true => () + | false => Control.throw Assertion_failed end. + +Ltac2 mutable x := O. +Ltac2 y := x. +Ltac2 Eval (assert_eq y O). +Ltac2 Set x := (S O). +Ltac2 Eval (assert_eq y (S O)). + +Ltac2 mutable quw := fun (n : nat) => O. +Ltac2 Set quw := fun n => + match n with + | O => O + | S n => S (S (quw n)) + end. + +Ltac2 Eval (quw (S (S O))). + (** Not the right type *) Fail Ltac2 Set foo := 0. @@ -25,10 +58,46 @@ Fail Ltac2 Set bar := fun _ => (). (** Subtype check *) -Ltac2 mutable rec f x := f x. +Ltac2 rec h x := h x. +Ltac2 mutable f x := h x. Fail Ltac2 Set f := fun x => x. Ltac2 mutable g x := x. +Ltac2 Set g := h. + +(** Rebinding with old values *) + + + +Ltac2 mutable qux n := S n. + +Ltac2 Set qux as self := fun n => self (self n). + +Ltac2 Eval assert_eq (qux O) (S (S O)). + +Ltac2 mutable quz := O. + +Ltac2 Set quz as self := S self. + +Ltac2 Eval (assert_eq quz (S O)). + +Ltac2 rec addn n := + match n with + | O => fun m => m + | S n => fun m => S (addn n m) + + end. +Ltac2 mutable rec quy n := + match n with + | O => S O + | S n => S (quy n) + end. -Ltac2 Set g := f. +Ltac2 Set quy as self := fun n => + match n with + | O => O + | S n => addn (self n) (quy n) + end. +Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))). +Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))). diff --git a/test-suite/output/ErrorLocation_12152_1.out b/test-suite/output/ErrorLocation_12152_1.out new file mode 100644 index 0000000000..b7b600d53d --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-7: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v new file mode 100644 index 0000000000..e63ab1cd48 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intro H; auto. diff --git a/test-suite/output/ErrorLocation_12152_2.out b/test-suite/output/ErrorLocation_12152_2.out new file mode 100644 index 0000000000..bdfd0a050f --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-8: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v new file mode 100644 index 0000000000..5df6bec939 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intros H; auto. diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out new file mode 100644 index 0000000000..ed5e183427 --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 0-16: +Error: Ltac variable x is bound to i > 0 which cannot be coerced to +an evaluable reference. + diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v new file mode 100644 index 0000000000..347424b2fc --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.v @@ -0,0 +1,4 @@ +Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. +Definition i := O. +Goal False. +can_unfold (i>0). diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f48eaac4c9..9cb019ca56 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -111,3 +111,11 @@ Warning: The format modifier is irrelevant for only parsing rules. File "stdin", line 280, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] +fun x : nat => U (S x) + : nat -> nat +V tt + : unit * (unit -> unit) +fun x : nat => V x + : forall x : nat, nat * (?T -> ?T) +where +?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4d4b37a8b2..b3270d4f92 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -280,3 +280,13 @@ Notation "###" := 0 (at level 0, only parsing, format "###"). Reserved Notation "##" (at level 0, only parsing, format "##"). End N. + +Module O. + +Notation U t := (match t with 0 => 0 | S t => t | _ => 0 end). +Check fun x => U (S x). +Notation V t := (t,fun t => t). +Check V tt. +Check fun x : nat => V x. + +End O. diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out new file mode 100644 index 0000000000..68dbaeb7b3 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.out @@ -0,0 +1,4 @@ +While loading initial state: +Warning: There is no flag or option with this name: "Extraction Optimize". +[unknown-option,option] +Extraction Optimize is on diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v new file mode 100644 index 0000000000..9a70674b02 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *) + +Test Extraction Optimize. diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out new file mode 100644 index 0000000000..76bb2016eb --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.out @@ -0,0 +1 @@ +Extraction Optimize is off diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v new file mode 100644 index 0000000000..7622d6ff52 --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *) + +Test Extraction Optimize. diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out index 952761acca..58931c4b82 100644 --- a/test-suite/output/print_ltac.out +++ b/test-suite/output/print_ltac.out @@ -6,3 +6,340 @@ Ltac t3 := idtacstr "my tactic" Ltac t4 x := match x with | ?A => (A, A) end +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +Ltac FE.withstrategy l x := + let idx := smart_global:(FE.id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + FE.id + FE.id + ] + with_strategy + l + [ + FE.id + FE.id + ] + with_strategy + tl + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + opaque + [ + FE.id + FE.id + ] + with_strategy + expand + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + x + FE.id + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + idtac diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v index a992846791..d0883e32e4 100644 --- a/test-suite/output/print_ltac.v +++ b/test-suite/output/print_ltac.v @@ -10,3 +10,73 @@ Print Ltac t3. (* https://github.com/coq/coq/issues/9716 *) Ltac t4 x := match x with ?A => constr:((A, A)) end. Print Ltac t4. + +Notation idnat := (@id nat). +Notation idn := id. +Notation idan := (@id). +Fail Strategy transparent [idnat]. +Strategy transparent [idn]. +Strategy transparent [idan]. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). +Print Ltac withstrategy. + +Module Type Empty. End Empty. +Module E. End E. +Module F (E : Empty). + Definition id {T} := @id T. + Notation idnat := (@id nat). + Notation idn := id. + Notation idan := (@id). + Fail Strategy transparent [idnat]. + Strategy transparent [idn]. + Strategy transparent [idan]. + Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). + Print Ltac withstrategy. +End F. + +Module FE := F E. +Print Ltac FE.withstrategy. diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v index 676b97878f..032fcaac6d 100644 --- a/test-suite/success/shrink_obligations.v +++ b/test-suite/success/shrink_obligations.v @@ -2,8 +2,6 @@ Require Program. Obligation Tactic := idtac. -Set Shrink Obligations. - Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit := let bar : {r | n < r} := _ in let qux : {r | p < r} := _ in diff --git a/test-suite/success/strategy.v b/test-suite/success/strategy.v new file mode 100644 index 0000000000..926ba54342 --- /dev/null +++ b/test-suite/success/strategy.v @@ -0,0 +1,87 @@ +Notation aid := (@id) (only parsing). +Notation idn := id (only parsing). +Ltac unfold_id := unfold id. + +Fixpoint fact (n : nat) + := match n with + | 0 => 1 + | S n => (S n) * fact n + end. + +Opaque id. +Goal id (fact 100) = fact 100. + Strategy expand [id]. + Time Timeout 5 reflexivity. (* should be instant *) + (* Finished transaction in 0. secs (0.u,0.s) (successful) *) +Time Timeout 5 Defined. +(* Finished transaction in 0.001 secs (0.u,0.s) (successful) *) + +Goal True. + let x := smart_global:(id) in unfold x. + let x := smart_global:(aid) in unfold x. + let x := smart_global:(idn) in unfold x. +Abort. + +Goal id 0 = 0. + Opaque id. + assert_fails unfold_id. + Transparent id. + assert_succeeds unfold_id. + Opaque id. + Strategy 0 [id]. + assert_succeeds unfold_id. + Strategy 1 [id]. + assert_succeeds unfold_id. + Strategy -1 [id]. + assert_succeeds unfold_id. + Strategy opaque [id]. + assert_fails unfold_id. + Strategy transparent [id]. + assert_succeeds unfold_id. + Opaque id. + Strategy expand [id]. + assert_succeeds unfold_id. + reflexivity. +Qed. +Goal id 0 = 0. + Opaque aid. + assert_fails unfold_id. + Transparent aid. + assert_succeeds unfold_id. + Opaque aid. + Strategy 0 [aid]. + assert_succeeds unfold_id. + Strategy 1 [aid]. + assert_succeeds unfold_id. + Strategy -1 [aid]. + assert_succeeds unfold_id. + Strategy opaque [aid]. + assert_fails unfold_id. + Strategy transparent [aid]. + assert_succeeds unfold_id. + Opaque aid. + Strategy expand [aid]. + assert_succeeds unfold_id. + reflexivity. +Qed. +Goal id 0 = 0. + Opaque idn. + assert_fails unfold_id. + Transparent idn. + assert_succeeds unfold_id. + Opaque idn. + Strategy 0 [idn]. + assert_succeeds unfold_id. + Strategy 1 [idn]. + assert_succeeds unfold_id. + Strategy -1 [idn]. + assert_succeeds unfold_id. + Strategy opaque [idn]. + assert_fails unfold_id. + Strategy transparent [idn]. + assert_succeeds unfold_id. + Opaque idn. + Strategy expand [idn]. + assert_succeeds unfold_id. + reflexivity. +Qed. diff --git a/test-suite/success/tac_wit_ref.v b/test-suite/success/tac_wit_ref.v new file mode 100644 index 0000000000..8bde31858e --- /dev/null +++ b/test-suite/success/tac_wit_ref.v @@ -0,0 +1,8 @@ +Tactic Notation "foo" reference(n) := idtac n. + +Goal forall n : nat, n = 0. +Proof. +intros n. +foo nat. +foo n. +Abort. diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v new file mode 100644 index 0000000000..077b57c87f --- /dev/null +++ b/test-suite/success/with_strategy.v @@ -0,0 +1,577 @@ +Notation aid := (@id) (only parsing). +Notation idn := id (only parsing). +Ltac unfold_id := unfold id. + +Fixpoint fact (n : nat) + := match n with + | 0 => 1 + | S n => (S n) * fact n + end. + +Opaque id. +Goal id 0 = 0. + with_strategy + opaque [id] + (with_strategy + opaque [id id] + (assert_fails unfold_id; + with_strategy + transparent [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (with_strategy + 0 [id] + (assert_succeeds unfold_id; + with_strategy + 1 [id] + (assert_succeeds unfold_id; + with_strategy + -1 [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (assert_fails unfold_id; + with_strategy + transparent [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (with_strategy + expand [id] + (assert_succeeds unfold_id; + let l := strategy_level:(expand) in + with_strategy + l [id] + (let idx := smart_global:(id) in + cbv [idx]; + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + assert_fails + (let idx := smart_global:(id) in + with_strategy + expand [idx] + idtac); + reflexivity)))))))))))). +Qed. +Goal id 0 = 0. + with_strategy + opaque [aid] + (assert_fails unfold_id; + with_strategy + transparent [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (with_strategy + 0 [aid] + (assert_succeeds unfold_id; + with_strategy + 1 [aid] + (assert_succeeds unfold_id; + with_strategy + -1 [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (assert_fails unfold_id; + with_strategy + transparent [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (with_strategy + expand [aid] + (assert_succeeds unfold_id; + reflexivity)))))))))). +Qed. +Goal id 0 = 0. + with_strategy + opaque [idn] + (assert_fails unfold_id; + with_strategy + transparent [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (with_strategy + 0 [idn] + (assert_succeeds unfold_id; + with_strategy + 1 [idn] + (assert_succeeds unfold_id; + with_strategy + -1 [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (assert_fails unfold_id; + with_strategy + transparent [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (with_strategy + expand [idn] + (assert_succeeds unfold_id; + reflexivity)))))))))). +Qed. + +(* test that strategy tactic does not persist after the execution of the tactic *) +Opaque id. +Goal id 0 = 0. + assert_fails unfold_id; + (with_strategy transparent [id] assert_succeeds unfold_id); + assert_fails unfold_id. + assert_fails unfold_id. + with_strategy transparent [id] assert_succeeds unfold_id. + assert_fails unfold_id. + reflexivity. +Qed. + +(* test that the strategy tactic does persist through abstract *) +Opaque id. +Goal id 0 = 0. + Time Timeout 5 + with_strategy + expand [id] + assert (id (fact 100) = fact 100) by abstract reflexivity. + reflexivity. +Time Timeout 5 Defined. + +(* test that it works even with [Qed] *) +Goal id 0 = 0. +Proof using Type. + Time Timeout 5 + abstract + (with_strategy + expand [id] + assert (id (fact 100) = fact 100) by abstract reflexivity; + reflexivity). +Time Timeout 5 Qed. + +(* test that the strategy is correctly reverted after closing the goal completely *) +Goal id 0 = 0. + assert (id 0 = 0) by with_strategy expand [id] reflexivity. + Fail unfold id. + reflexivity. +Qed. + +(* test that the strategy is correctly reverted after failure *) +Goal id 0 = 0. + let id' := id in + (try with_strategy expand [id] fail); assert_fails unfold id'. + Fail unfold id. + (* a more complicated test involving a success and then a failure after backtracking *) + let id' := id in + ((with_strategy expand [id] (unfold id' + fail)) + idtac); + lazymatch goal with |- id 0 = 0 => idtac end; + assert_fails unfold id'. + Fail unfold id. + reflexivity. +Qed. + +(* test multi-success *) +Goal id (fact 100) = fact 100. + Timeout 1 + (with_strategy -1 [id] (((idtac + (abstract reflexivity))); fail)). + Undo. + Timeout 1 + let id' := id in + (with_strategy -1 [id] (((idtac + (unfold id'; reflexivity))); fail)). + Undo. + Timeout 1 + (with_strategy -1 [id] (idtac + (abstract reflexivity))); fail. (* should not time out *) + Undo. + with_strategy -1 [id] abstract reflexivity. +Defined. + +(* check that module substitutions happen correctly *) +Module F. + Definition id {T} := @id T. + Opaque id. + Ltac with_transparent_id tac := with_strategy transparent [id] tac. +End F. +Opaque F.id. + +Goal F.id 0 = F.id 0. + Fail unfold F.id. + (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *) + Fail F.with_transparent_id ltac:(progress unfold F.id). + F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x). +Abort. + +Module Type Empty. End Empty. +Module E. End E. +Module F2F (E : Empty). + Definition id {T} := @id T. + Opaque id. + Ltac with_transparent_id tac := with_strategy transparent [id] tac. +End F2F. +Module F2 := F2F E. +Opaque F2.id. + +Goal F2.id 0 = F2.id 0. + Fail unfold F2.id. + (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *) + Fail F2.with_transparent_id ltac:(progress unfold F2.id). + F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x). +Abort. + +(* test the tactic notation entries *) +Tactic Notation "with_strategy0" strategy_level(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy1" strategy_level_or_var(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy2" strategy_level(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy3" strategy_level_or_var(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac. + +(* [with_strategy0] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *) +Opaque id. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy0 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. + +(* [with_strategy1] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *) +Opaque id. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) let l := strategy_level:(expand) in + with_strategy1 l [id] idtac. + (* This should succeed, but doesn't, basically due to https://github idtac.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy1 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. + +Opaque id. +Goal id 0 = 0. + with_strategy2 + opaque [id] + (with_strategy2 + opaque [id] + (assert_fails unfold_id; + with_strategy2 + transparent [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (with_strategy2 + 0 [id] + (assert_succeeds unfold_id; + with_strategy2 + 1 [id] + (assert_succeeds unfold_id; + with_strategy2 + -1 [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (assert_fails unfold_id; + with_strategy2 + transparent [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (with_strategy2 + expand [id] + (assert_succeeds unfold_id))))))))))). + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy2 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy2 + opaque [aid] + (with_strategy2 + opaque [aid] + (assert_fails unfold_id; + with_strategy2 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (with_strategy2 + 0 [aid] + (assert_succeeds unfold_id; + with_strategy2 + 1 [aid] + (assert_succeeds unfold_id; + with_strategy2 + -1 [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (assert_fails unfold_id; + with_strategy2 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (with_strategy2 + expand [aid] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy2 + opaque [idn] + (with_strategy2 + opaque [idn] + (assert_fails unfold_id; + with_strategy2 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (with_strategy2 + 0 [idn] + (assert_succeeds unfold_id; + with_strategy2 + 1 [idn] + (assert_succeeds unfold_id; + with_strategy2 + -1 [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (assert_fails unfold_id; + with_strategy2 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (with_strategy2 + expand [idn] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. + +Opaque id. +Goal id 0 = 0. + with_strategy3 + opaque [id] + (with_strategy3 + opaque [id] + (assert_fails unfold_id; + with_strategy3 + transparent [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (with_strategy3 + 0 [id] + (assert_succeeds unfold_id; + with_strategy3 + 1 [id] + (assert_succeeds unfold_id; + with_strategy3 + -1 [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (assert_fails unfold_id; + with_strategy3 + transparent [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (with_strategy3 + expand [id] + (assert_succeeds unfold_id))))))))))). + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy3 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy3 + opaque [aid] + (with_strategy3 + opaque [aid] + (assert_fails unfold_id; + with_strategy3 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (with_strategy3 + 0 [aid] + (assert_succeeds unfold_id; + with_strategy3 + 1 [aid] + (assert_succeeds unfold_id; + with_strategy3 + -1 [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (assert_fails unfold_id; + with_strategy3 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (with_strategy3 + expand [aid] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy3 + opaque [idn] + (with_strategy3 + opaque [idn] + (assert_fails unfold_id; + with_strategy3 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (with_strategy3 + 0 [idn] + (assert_succeeds unfold_id; + with_strategy3 + 1 [idn] + (assert_succeeds unfold_id; + with_strategy3 + -1 [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (assert_fails unfold_id; + with_strategy3 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (with_strategy3 + expand [idn] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. + +(* Fake out coqchk to work around what is essentially COQBUG(https://github.com/coq/coq/issues/12200) *) +Reset Initial. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 57cc8c4e90..d70978fabe 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -82,34 +82,39 @@ Qed. (** * Order on booleans *) (************************) -Definition leb (b1 b2:bool) := +#[ local ] Definition le (b1 b2:bool) := match b1 with | true => b2 = true | false => True end. -Hint Unfold leb: bool. +Hint Unfold le: bool. -Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true. +Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true. Proof. destr_bool; intuition. Qed. -Definition ltb (b1 b2:bool) := +#[deprecated(since="8.12",note="Use Bool.le instead.")] +Notation leb := le (only parsing). +#[deprecated(since="8.12",note="Use Bool.le_implb instead.")] +Notation leb_implb := le_implb (only parsing). + +#[ local ] Definition lt (b1 b2:bool) := match b1 with | true => False | false => b2 = true end. -Hint Unfold ltb: bool. +Hint Unfold lt: bool. -Definition compareb (b1 b2 : bool) := +#[ local ] Definition compare (b1 b2 : bool) := match b1, b2 with | false, true => Lt | true, false => Gt | _, _ => Eq end. -Lemma compareb_spec : forall b1 b2, - CompareSpec (b1 = b2) (ltb b1 b2) (ltb b2 b1) (compareb b1 b2). +Lemma compare_spec : forall b1 b2, + CompareSpec (b1 = b2) (lt b1 b2) (lt b2 b1) (compare b1 b2). Proof. destr_bool; auto. Qed. @@ -935,8 +940,8 @@ Defined. (** Notations *) Module BoolNotations. -Infix "<=" := leb : bool_scope. -Infix "<" := ltb : bool_scope. -Infix "?=" := compareb (at level 70) : bool_scope. +Infix "<=" := le : bool_scope. +Infix "<" := lt : bool_scope. +Infix "?=" := compare (at level 70) : bool_scope. Infix "=?" := eqb (at level 70) : bool_scope. End BoolNotations. diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v index 61aab607a9..aaa7321bfc 100644 --- a/theories/Bool/BoolOrder.v +++ b/theories/Bool/BoolOrder.v @@ -14,69 +14,65 @@ Require Export Bool. Require Import Orders. - -Local Notation le := Bool.leb. -Local Notation lt := Bool.ltb. -Local Notation compare := Bool.compareb. -Local Notation compare_spec := Bool.compareb_spec. +Import BoolNotations. (** * Order [le] *) -Lemma le_refl : forall b, le b b. +Lemma le_refl : forall b, b <= b. Proof. destr_bool. Qed. Lemma le_trans : forall b1 b2 b3, - le b1 b2 -> le b2 b3 -> le b1 b3. + b1 <= b2 -> b2 <= b3 -> b1 <= b3. Proof. destr_bool. Qed. -Lemma le_true : forall b, le b true. +Lemma le_true : forall b, b <= true. Proof. destr_bool. Qed. -Lemma false_le : forall b, le false b. +Lemma false_le : forall b, false <= b. Proof. intros; constructor. Qed. -Instance le_compat : Proper (eq ==> eq ==> iff) le. +Instance le_compat : Proper (eq ==> eq ==> iff) Bool.le. Proof. intuition. Qed. (** * Strict order [lt] *) -Lemma lt_irrefl : forall b, ~ lt b b. +Lemma lt_irrefl : forall b, ~ b < b. Proof. destr_bool; auto. Qed. Lemma lt_trans : forall b1 b2 b3, - lt b1 b2 -> lt b2 b3 -> lt b1 b3. + b1 < b2 -> b2 < b3 -> b1 < b3. Proof. destr_bool; auto. Qed. -Instance lt_compat : Proper (eq ==> eq ==> iff) lt. +Instance lt_compat : Proper (eq ==> eq ==> iff) Bool.lt. Proof. intuition. Qed. -Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }. +Lemma lt_trichotomy : forall b1 b2, { b1 < b2 } + { b1 = b2 } + { b2 < b1 }. Proof. destr_bool; auto. Qed. -Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1. +Lemma lt_total : forall b1 b2, b1 < b2 \/ b1 = b2 \/ b2 < b1. Proof. destr_bool; auto. Qed. -Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2. +Lemma lt_le_incl : forall b1 b2, b1 < b2 -> b1 <= b2. Proof. destr_bool; auto. Qed. -Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }. +Lemma le_lteq_dec : forall b1 b2, b1 <= b2 -> { b1 < b2 } + { b1 = b2 }. Proof. destr_bool; auto. Qed. -Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2. +Lemma le_lteq : forall b1 b2, b1 <= b2 <-> b1 < b2 \/ b1 = b2. Proof. destr_bool; intuition. Qed. (** * Order structures *) (* Class structure *) -Instance le_preorder : PreOrder le. +Instance le_preorder : PreOrder Bool.le. Proof. split. - intros b; apply le_refl. - intros b1 b2 b3; apply le_trans. Qed. -Instance lt_strorder : StrictOrder lt. +Instance lt_strorder : StrictOrder Bool.lt. Proof. split. - intros b; apply lt_irrefl. @@ -88,13 +84,13 @@ Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. Definition t := bool. Definition eq := @eq bool. Definition eq_equiv := @eq_equivalence bool. - Definition lt := lt. + Definition lt := Bool.lt. Definition lt_strorder := lt_strorder. Definition lt_compat := lt_compat. - Definition le := le. + Definition le := Bool.le. Definition le_lteq := le_lteq. Definition lt_total := lt_total. - Definition compare := compare. + Definition compare := Bool.compare. Definition compare_spec := compare_spec. Definition eq_dec := bool_dec. Definition eq_refl := @eq_Reflexive bool. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 9f77221d5a..b094f81dc6 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -21,6 +21,8 @@ Require Import Logic. Inductive Empty_set : Set :=. +Register Empty_set as core.Empty_set.type. + (** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := @@ -141,6 +143,9 @@ Inductive BoolSpec (P Q : Prop) : bool -> Prop := | BoolSpecF : Q -> BoolSpec P Q false. Hint Constructors BoolSpec : core. +Register BoolSpec as core.BoolSpec.type. +Register BoolSpecT as core.BoolSpec.BoolSpecT. +Register BoolSpecF as core.BoolSpec.BoolSpecF. (********************************************************************) (** * Peano natural numbers *) @@ -370,6 +375,11 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. Hint Constructors CompareSpec : core. +Register CompareSpec as core.CompareSpec.type. +Register CompEq as core.CompareSpec.CompEq. +Register CompLt as core.CompareSpec.CompLt. +Register CompGt as core.CompareSpec.CompGt. + (** For having clean interfaces after extraction, [CompareSpec] is declared in Prop. For some situations, it is nonetheless useful to have a version in Type. Interestingly, these two versions are equivalent. *) @@ -380,6 +390,11 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. Hint Constructors CompareSpecT : core. +Register CompareSpecT as core.CompareSpecT.type. +Register CompEqT as core.CompareSpecT.CompEqT. +Register CompLtT as core.CompareSpecT.CompLtT. +Register CompGtT as core.CompareSpecT.CompGtT. + Lemma CompareSpec2Type : forall Peq Plt Pgt c, CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. Proof. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 31e8cf463e..474b417e8e 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -44,18 +44,18 @@ Definition In (s:uniset) (a:A) : Prop := charac s a = true. Hint Unfold In : core. (** uniset inclusion *) -Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). +Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a). Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. Hint Unfold seq : core. -Lemma leb_refl : forall b:bool, leb b b. +Lemma le_refl : forall b, Bool.le b b. Proof. destruct b; simpl; auto. Qed. -Hint Resolve leb_refl : core. +Hint Resolve le_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 1dd9285412..026cf32ceb 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -273,8 +273,8 @@ Proof. exact Permutation_length. Qed. -Instance Permutation_Forall (P : A -> Prop) : - Proper ((@Permutation A) ==> Basics.impl) (Forall P). +Global Instance Permutation_Forall (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Forall P) | 10. Proof. intros l1 l2 HP. induction HP; intro HF; auto. @@ -283,8 +283,8 @@ Proof. inversion_clear HF2; auto. Qed. -Instance Permutation_Exists (P : A -> Prop) : - Proper ((@Permutation A) ==> Basics.impl) (Exists P). +Global Instance Permutation_Exists (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Exists P) | 10. Proof. intros l1 l2 HP. induction HP; intro HF; auto. @@ -581,8 +581,8 @@ Proof. now contradiction (Hf x). Qed. -Instance Permutation_flat_map (g : A -> list B) : - Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g). +Global Instance Permutation_flat_map (g : A -> list B) : + Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g) | 10. Proof. intros l1; induction l1; intros l2 HP. - now apply Permutation_nil in HP; subst. @@ -773,7 +773,7 @@ Qed. End Permutation_alt. -Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum. +Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum | 10. Proof. intros l1 l2 HP; induction HP; simpl; intuition. - rewrite 2 (Nat.add_comm x). @@ -781,7 +781,7 @@ Proof. - now transitivity (list_sum l'). Qed. -Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max. +Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max | 10. Proof. intros l1 l2 HP; induction HP; simpl; intuition. - rewrite 2 (Nat.max_comm x). @@ -806,7 +806,7 @@ Proof. now apply (perm_t_trans IHHP2). Qed. -Instance Permutation_transp_equiv : Equivalence Permutation_transp. +Global Instance Permutation_transp_equiv : Equivalence Permutation_transp | 100. Proof. split. - intros l; apply perm_t_refl. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index c8b8660b92..524f818523 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -92,41 +92,6 @@ let create_empty_file filename = let f = open_out filename in close_out f -let interp_set_option opt v old = - let open Goptions in - let err expect = - let opt = String.concat " " opt in - let got = v in (* avoid colliding with Pp.v *) - CErrors.user_err - Pp.(str "-set: " ++ str opt ++ - str" expects " ++ str expect ++ - str" but got " ++ str got) - in - match old with - | BoolValue _ -> - let v = match String.trim v with - | "true" -> true - | "false" | "" -> false - | _ -> err "a boolean" - in - BoolValue v - | IntValue _ -> - let v = String.trim v in - let v = match int_of_string_opt v with - | Some _ as v -> v - | None -> if v = "" then None else err "an int" - in - IntValue v - | StringValue _ -> StringValue v - | StringOptValue _ -> StringOptValue (Some v) - -let set_option = let open Goptions in function - | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt - | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true - | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v - -let set_options = List.iter set_option - (* Compile a vernac file *) let compile opts copts ~echo ~f_in ~f_out = let open Vernac.State in @@ -140,7 +105,7 @@ let compile opts copts ~echo ~f_in ~f_out = ++ str ".") in let ml_load_path, vo_load_path = build_load_path opts in - let require_libs = require_libs opts in + let injections = injection_commands opts in let stm_options = opts.config.stm_flags in let output_native_objects = match opts.config.native_compiler with | NativeOff -> false | NativeOn {ondemand} -> not ondemand @@ -165,11 +130,10 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path; - vo_load_path; require_libs; stm_options; + vo_load_path; injections; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in - set_options opts.config.set_options; let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_out) @@ -218,12 +182,11 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path; - vo_load_path; require_libs; stm_options; + vo_load_path; injections; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in - set_options opts.config.set_options; let ldir = Stm.get_ldir ~doc:state.doc in let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in let doc = Stm.finish ~doc:state.doc in diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index eb66dbaafc..8c154488d0 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -17,5 +17,3 @@ val compile_files : Coqargs.t -> Coqcargs.t -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> unit - -val set_options : (Goptions.option_name * Coqargs.option_command) list -> unit diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 17435c051e..c7ad5edb1f 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -38,8 +38,6 @@ type color = [`ON | `AUTO | `EMACS | `OFF] type native_compiler = NativeOff | NativeOn of { ondemand : bool } -type option_command = OptionSet of string option | OptionUnset - type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; @@ -59,7 +57,6 @@ type coqargs_config = { debug : bool; time : bool; print_emacs : bool; - set_options : (Goptions.option_name * option_command) list; } type coqargs_pre = { @@ -69,10 +66,9 @@ type coqargs_pre = { ml_includes : string list; vo_includes : Loadpath.vo_path list; - vo_requires : (string * string option * bool option) list; - (* None = No Import; Some false = Import; Some true = Export *) load_vernacular_list : (string * bool) list; + injections : Stm.injection_command list; inputstate : string option; } @@ -124,7 +120,6 @@ let default_config = { debug = false; time = false; print_emacs = false; - set_options = []; (* Quiet / verbosity options should be here *) } @@ -135,8 +130,8 @@ let default_pre = { load_rcfile = true; ml_includes = []; vo_includes = []; - vo_requires = []; load_vernacular_list = []; + injections = []; inputstate = None; } @@ -167,13 +162,13 @@ let add_vo_include opts unix_path coq_path implicit = unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }} let add_vo_require opts d p export = - { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }} + { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }} let add_load_vernacular opts verb s = - { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} + { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} let add_set_option opts opt_name value = - { opts with config = { opts.config with set_options = (opt_name, value) :: opts.config.set_options }} + { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }} (** Options for proof general *) let set_emacs opts = @@ -486,10 +481,10 @@ let parse_args ~help ~init arglist : t * string list = | "-set" -> let opt, v = parse_option_set @@ next() in - add_set_option oval opt (OptionSet v) + add_set_option oval opt (Stm.OptionSet v) | "-unset" -> - add_set_option oval (to_opt_key @@ next ()) OptionUnset + add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset |"-native-output-dir" -> let native_output_dir = next () in @@ -513,18 +508,18 @@ let parse_args ~help ~init arglist : t * string list = |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval |"-diffs" -> - add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) + add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval |"-impredicative-set" -> set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval |"-allow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) + add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None) |"-disallow-sprop" -> - add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset + add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset |"-sprop-cumulative" -> warn_deprecated_sprop_cumul(); - add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) + add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None) |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} @@ -564,12 +559,9 @@ let parse_args ~help ~init args = pre = { opts.pre with ml_includes = List.rev opts.pre.ml_includes ; vo_includes = List.rev opts.pre.vo_includes - ; vo_requires = List.rev opts.pre.vo_requires ; load_vernacular_list = List.rev opts.pre.load_vernacular_list + ; injections = List.rev opts.pre.injections } - ; config = { opts.config with - set_options = List.rev opts.config.set_options - } ; } in opts, extra @@ -579,8 +571,8 @@ let parse_args ~help ~init args = (* prelude_data == From Coq Require Import Prelude. *) let prelude_data = "Prelude", Some "Coq", Some false -let require_libs opts = - if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires +let injection_commands opts = + if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections let build_load_path opts = let ml_path, vo_path = diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index a51ed6766a..c8634b7847 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -14,8 +14,6 @@ val default_toplevel : Names.DirPath.t type native_compiler = NativeOff | NativeOn of { ondemand : bool } -type option_command = OptionSet of string option | OptionUnset - type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; @@ -35,7 +33,6 @@ type coqargs_config = { debug : bool; time : bool; print_emacs : bool; - set_options : (Goptions.option_name * option_command) list; } type coqargs_pre = { @@ -45,10 +42,10 @@ type coqargs_pre = { ml_includes : CUnix.physical_path list; vo_includes : Loadpath.vo_path list; - vo_requires : (string * string option * bool option) list; - (* None = No Import; Some false = Import; Some true = Export *) load_vernacular_list : (string * bool) list; + injections : Stm.injection_command list; + inputstate : string option; } @@ -79,5 +76,5 @@ val default : t val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list val error_wrong_arg : string -> unit -val require_libs : t -> (string * string option * bool option) list +val injection_commands : t -> Stm.injection_command list val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7aad856d0a..2d450d430a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -243,13 +243,13 @@ let init_document opts = (* Next line allows loading .vos files when in interactive mode *) Flags.load_vos_libraries := true; let ml_load_path, vo_load_path = build_load_path opts in - let require_libs = require_libs opts in + let injections = injection_commands opts in let stm_options = opts.config.stm_flags in let open Vernac.State in let doc, sid = Stm.(new_doc { doc_type = Interactive opts.config.logic.toplevel_name; - ml_load_path; vo_load_path; require_libs; stm_options; + ml_load_path; vo_load_path; injections; stm_options; }) in { doc; sid; proof = None; time = opts.config.time } @@ -273,7 +273,6 @@ type run_mode = Interactive | Batch let init_toploop opts = let state = init_document opts in let state = Ccompile.load_init_vernaculars opts ~state in - Ccompile.set_options opts.config.set_options; state let coqtop_init run_mode ~opts = diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 13c4d667a0..8979170026 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -289,7 +289,7 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_mut: - [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ] + [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ] ; tac2typ_knd: [ [ t = tac2type -> { CTydDef (Some t) } diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 28e877491e..987cd8c1b8 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -336,7 +336,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics = if isrec then inline_rec_tactic tactics else tactics in let map ({loc;v=id}, e) = - let (e, t) = intern ~strict:true e in + let (e, t) = intern ~strict:true [] e in let () = if not (is_value e) then user_err ?loc (str "Tactic definition must be a syntactical value") @@ -728,19 +728,26 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with type redefinition = { redef_kn : ltac_constant; redef_body : glb_tacexpr; + redef_old : Id.t option; } let perform_redefinition (_, redef) = let kn = redef.redef_kn in let data = Tac2env.interp_global kn in - let data = { data with Tac2env.gdata_expr = redef.redef_body } in + let body = match redef.redef_old with + | None -> redef.redef_body + | Some id -> + (* Rebind the old value with a let-binding *) + GTacLet (false, [Name id, data.Tac2env.gdata_expr], redef.redef_body) + in + let data = { data with Tac2env.gdata_expr = body } in Tac2env.define_global kn data let subst_redefinition (subst, redef) = let kn = Mod_subst.subst_kn subst redef.redef_kn in let body = Tac2intern.subst_expr subst redef.redef_body in if kn == redef.redef_kn && body == redef.redef_body then redef - else { redef_kn = kn; redef_body = body } + else { redef_kn = kn; redef_body = body; redef_old = redef.redef_old } let classify_redefinition o = Substitute o @@ -751,7 +758,7 @@ let inTac2Redefinition : redefinition -> obj = subst_function = subst_redefinition; classify_function = classify_redefinition } -let register_redefinition ?(local = false) qid e = +let register_redefinition ?(local = false) qid old e = let kn = try Tac2env.locate_ltac qid with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown tactic " ++ pr_qualid qid) @@ -766,7 +773,11 @@ let register_redefinition ?(local = false) qid e = if not (data.Tac2env.gdata_mutable) then user_err ?loc:qid.CAst.loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable") in - let (e, t) = intern ~strict:true e in + let ctx = match old with + | None -> [] + | Some { CAst.v = id } -> [id, data.Tac2env.gdata_type] + in + let (e, t) = intern ~strict:true ctx e in let () = if not (is_value e) then user_err ?loc:qid.CAst.loc (str "Tactic definition must be a syntactical value") @@ -777,15 +788,17 @@ let register_redefinition ?(local = false) qid e = user_err ?loc:qid.CAst.loc (str "Type " ++ pr_glbtype name (snd t) ++ str " is not a subtype of " ++ pr_glbtype name (snd data.Tac2env.gdata_type)) in + let old = Option.map (fun { CAst.v = id } -> id) old in let def = { redef_kn = kn; redef_body = e; + redef_old = old; } in Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = let env = Global.env () in - let (e, ty) = Tac2intern.intern ~strict:false e in + let (e, ty) = Tac2intern.intern ~strict:false [] e in let v = Tac2interp.interp Tac2interp.empty_environment e in let selector, proof = match pstate with @@ -818,7 +831,7 @@ let register_struct ?local str = match str with | StrTyp (isrec, t) -> register_type ?local isrec t | StrPrm (id, t, ml) -> register_primitive ?local id t ml | StrSyn (tok, lev, e) -> register_notation ?local tok lev e -| StrMut (qid, e) -> register_redefinition ?local qid e +| StrMut (qid, old, e) -> register_redefinition ?local qid old e (** Toplevel exception *) @@ -913,7 +926,7 @@ let solve ~pstate default tac = let call ~pstate ~default e = let loc = e.loc in - let (e, t) = intern ~strict:false e in + let (e, t) = intern ~strict:false [] e in let () = check_unit ?loc t in let tac = Tac2interp.interp Tac2interp.empty_environment e in solve ~pstate default (Proofview.tclIGNORE tac) diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index a95d8cc49f..548655f561 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -168,7 +168,7 @@ type strexpr = (** External definition *) | StrSyn of sexpr list * int option * raw_tacexpr (** Syntactic extensions *) -| StrMut of qualid * raw_tacexpr +| StrMut of qualid * Names.lident option * raw_tacexpr (** Redefinition of mutable globals *) (** {5 Dynamic semantics} *) diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index a4f385d432..797f72702d 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -396,11 +396,13 @@ let is_pure_constructor kn = let rec is_value = function | GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true -| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false +| GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false | GTacCst (Tuple _, _, el) -> List.for_all is_value el | GTacCst (_, _, []) -> true | GTacOpn (_, el) -> List.for_all is_value el | GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el +| GTacLet (false, bnd, e) -> + is_value e && List.for_all (fun (_, e) -> is_value e) bnd | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ | GTacWth _ -> false @@ -458,6 +460,10 @@ let monomorphic (t : UF.elt glb_typexpr) : mix_type_scheme = let subst id = GTypVar (GVar id) in (0, subst_type subst t) +let polymorphic ((n, t) : type_scheme) : mix_type_scheme = + let subst id = GTypVar (LVar id) in + (n, subst_type subst t) + let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" (fun () -> strbrk "The following expression should have type unit.") @@ -1138,9 +1144,13 @@ let normalize env (count, vars) (t : UF.elt glb_typexpr) = in subst_type subst t -let intern ~strict e = +type context = (Id.t * type_scheme) list + +let intern ~strict ctx e = let env = empty_env () in let env = if strict then env else { env with env_str = false } in + let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in + let env = List.fold_left fold env ctx in let (e, t) = intern_rec env e in let count = ref 0 in let vars = ref UF.Map.empty in diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli index 8b09ecbcf7..ed251d6201 100644 --- a/user-contrib/Ltac2/tac2intern.mli +++ b/user-contrib/Ltac2/tac2intern.mli @@ -12,7 +12,9 @@ open Names open Mod_subst open Tac2expr -val intern : strict:bool -> raw_tacexpr -> glb_tacexpr * type_scheme +type context = (Id.t * type_scheme) list + +val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef val intern_open_type : raw_typexpr -> type_scheme diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml index 54f2da0621..ed783afce7 100644 --- a/user-contrib/Ltac2/tac2interp.ml +++ b/user-contrib/Ltac2/tac2interp.ml @@ -86,7 +86,7 @@ let rec interp (ist : environment) = function | GTacVar id -> return (get_var ist id) | GTacRef kn -> let data = get_ref ist kn in - return (eval_pure (Some kn) data) + return (eval_pure Id.Map.empty (Some kn) data) | GTacFun (ids, e) -> let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in let f = interp_app cls in @@ -187,26 +187,41 @@ and interp_set ist e p r = let () = Valexpr.set_field e p r in return (Valexpr.make_int 0) -and eval_pure kn = function +and eval_pure bnd kn = function +| GTacVar id -> Id.Map.get id bnd | GTacAtm (AtmInt n) -> Valexpr.make_int n | GTacRef kn -> let { Tac2env.gdata_expr = e } = try Tac2env.interp_global kn with Not_found -> assert false in - eval_pure (Some kn) e + eval_pure bnd (Some kn) e | GTacFun (na, e) -> - let cls = { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e } in + let cls = { clos_ref = kn; clos_env = bnd; clos_var = na; clos_exp = e } in let f = interp_app cls in Tac2ffi.of_closure f | GTacCst (_, n, []) -> Valexpr.make_int n -| GTacCst (_, n, el) -> Valexpr.make_block n (Array.map_of_list eval_unnamed el) -| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, Array.map_of_list eval_unnamed el) -| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _ +| GTacCst (_, n, el) -> Valexpr.make_block n (eval_pure_args bnd el) +| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, eval_pure_args bnd el) +| GTacLet (isrec, vals, body) -> + let () = assert (not isrec) in + let fold accu (na, e) = match na with + | Anonymous -> + (* No need to evaluate, we know this is a value *) + accu + | Name id -> + let v = eval_pure bnd None e in + Id.Map.add id v accu + in + let bnd = List.fold_left fold bnd vals in + eval_pure bnd kn body +| GTacAtm (AtmStr _) | GTacSet _ | GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ -> anomaly (Pp.str "Term is not a syntactical value") -and eval_unnamed e = eval_pure None e +and eval_pure_args bnd args = + let map e = eval_pure bnd None e in + Array.map_of_list map args (** Cross-boundary hacks. *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index cc9b840bed..4242f06844 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let indnames = List.map (fun ind -> ind.ind_name) indl in (* In case of template polymorphism, we need to compute more constraints *) - let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in + let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) = interp_params env0 udecl uparamsl paramsl diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index ab11472dec..9ea54f5d8f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -111,11 +111,6 @@ open ProgramDecl (* Saving an obligation *) -let get_shrink_obligations = - Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) - ~key:["Shrink"; "Obligations"] - ~value:true - (* XXX: Is this the right place for this? *) let it_mkLambda_or_LetIn_or_clean t ctx = let open Context.Rel.Declaration in @@ -190,7 +185,7 @@ let add_hint local prg cst = (* true = hide obligations *) let get_hide_obligations = Goptions.declare_bool_option_and_ref - ~depr:false + ~depr:true ~key:["Hide"; "Obligations"] ~value:false @@ -203,7 +198,7 @@ let declare_obligation prg obl body ty uctx = let opaque = (not force) && opaque in let poly = prg.prg_poly in let ctx, body, ty, args = - if get_shrink_obligations () && not poly then shrink_body body ty + if not poly then shrink_body body ty else ([], body, ty, [||]) in let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 058fa691ee..80a4de472c 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -97,7 +97,7 @@ GRAMMAR EXTEND Gram | IDENT "Guarded" -> { VernacCheckGuard } (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; - id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] -> + id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] -> { VernacCreateHintDb (id, b) } | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> { VernacRemoveHints (dbnames, ids) } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3cb10364b5..42259cee10 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,9 +30,6 @@ open Pcoq.Module open Pvernac.Vernac_ open Attributes -let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw - (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) @@ -790,12 +787,6 @@ GRAMMAR EXTEND Gram { List.map (fun name -> (name.CAst.v, MaxImplicit)) items } ] ]; - strategy_level: - [ [ IDENT "expand" -> { Conv_oracle.Expand } - | IDENT "opaque" -> { Conv_oracle.Opaque } - | n=integer -> { Conv_oracle.Level n } - | IDENT "transparent" -> { Conv_oracle.transparent } ] ] - ; instance_name: [ [ name = ident_decl; bl = binders -> { (CAst.map (fun id -> Name id) (fst name), snd name), bl } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 41f2ab9c63..9d67ce3757 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function (* Refiner errors *) let explain_refiner_bad_type env sigma arg ty conclty = - let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in + let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in str "Refiner was given an argument" ++ brk(1,1) ++ pr_lconstr_env env sigma arg ++ spc () ++ str "of type" ++ brk(1,1) ++ pm ++ spc () ++ @@ -1112,16 +1112,9 @@ let explain_refiner_cannot_apply env sigma t harg = pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ pr_lconstr_env env sigma harg ++ str "." -let explain_refiner_not_well_typed env sigma c = - str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed." - let explain_intro_needs_product () = str "Introduction tactics needs products." -let explain_does_not_occur_in env sigma c hyp = - str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ - str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." - let explain_non_linear_proof env sigma c = str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++ spc () ++ str "because a metavariable has several occurrences." @@ -1137,9 +1130,7 @@ let explain_refiner_error env sigma = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg - | NotWellTyped c -> explain_refiner_not_well_typed env sigma c | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp | NonLinearProof c -> explain_non_linear_proof env sigma c | MetaInType c -> explain_meta_in_type env sigma c | NoSuchHyp id -> explain_no_such_hyp id diff --git a/vernac/library.ml b/vernac/library.ml index 85db501e84..c30331b221 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -89,6 +89,7 @@ type library_disk = { type summary_disk = { md_name : compilation_unit_name; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; + md_ocaml : string; } (*s Modules loaded in memory contain the following informations. They are @@ -251,6 +252,7 @@ let intern_from_file f = let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in ObjFile.close_in ch; + System.check_caml_version ~caml:lsd.md_ocaml ~file:f; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in @@ -401,6 +403,7 @@ let load_library_todo f = let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in ObjFile.close_in ch; + System.check_caml_version ~caml:s0.md_ocaml ~file:f; if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); @@ -486,6 +489,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); + md_ocaml = Coq_config.caml_version; } in let md = { md_compiled = cenv; diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 53f3c8408b..8435612abd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1073,12 +1073,12 @@ let make_internalization_vars recvars mainvars typs = let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in maintyps @ extratyps -let make_interpretation_type isrec isonlybinding = function +let make_interpretation_type isrec isonlybinding default_if_binding = function (* Parsed as constr list *) | ETConstr (_,None,_) when isrec -> NtnTypeConstrList - (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *) + (* Parsed as constr, but interpreted as a binder *) | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk) - | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent) + | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr default_if_binding) (* Parsed as constr, interpreted as constr *) | ETConstr (_,None,_) -> NtnTypeConstr (* Others *) @@ -1096,7 +1096,9 @@ let subentry_of_constr_prod_entry = function | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel | _ -> InConstrEntrySomeLevel -let make_interpretation_vars recvars allvars typs = +let make_interpretation_vars + (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent) + recvars allvars typs = let eq_subscope (sc1, l1) (sc2, l2) = Option.equal String.equal sc1 sc2 && List.equal String.equal l1 l2 @@ -1113,7 +1115,7 @@ let make_interpretation_vars recvars allvars typs = Id.Map.mapi (fun x (isonlybinding, sc) -> let typ = Id.List.assoc x typs in ((subentry_of_constr_prod_entry typ,sc), - make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars + make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding default_if_binding typ)) mainvars let check_rule_productivity l = if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then @@ -1793,8 +1795,8 @@ let try_interp_name_alias = function | _ -> raise Not_found let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } = - let vars,reversibility,pat = - try [], APrioriReversible, NRef (try_interp_name_alias (vars,c)) + let acvars,pat,reversibility = + try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible with Not_found -> let fold accu id = Id.Map.add id NtnInternTypeAny accu in let i_vars = List.fold_left fold Id.Map.empty vars in @@ -1802,10 +1804,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing ninterp_var_type = i_vars; ninterp_rec_vars = Id.Map.empty; } in - let nvars, pat, reversibility = interp_notation_constr env nenv c in - let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in - List.map map vars, reversibility, pat + interp_notation_constr env nenv c in + let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in + let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in + let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) diff --git a/vernac/record.ml b/vernac/record.ml index 9fda98d08e..36254780cd 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records = any Set <= i constraint for universes that might actually be instantiated with Prop. *) let is_template = List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in - let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in + let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let () = let error bk {CAst.loc; v=name} = |