diff options
99 files changed, 1614 insertions, 729 deletions
diff --git a/.gitignore b/.gitignore index b99d2a0d45..b665b2f86d 100644 --- a/.gitignore +++ b/.gitignore @@ -64,12 +64,9 @@ plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty coqdoc.css -time-of-build.log -time-of-build-pretty.log -time-of-build-before.log -time-of-build-after.log -time-of-build-pretty.log2 -time-of-build-pretty.log3 +time-of-build*.log +time-of-build*.log2 +time-of-build*.log3 .csdp.cache test-suite/.lia.cache test-suite/.nra.cache @@ -118,9 +115,7 @@ doc/stdlib/index-list.html doc/tools/docgram/productionlistGrammar doc/tools/docgram/editedGrammar doc/tools/docgram/prodnGrammar -doc/tutorial/Tutorial.v.out -doc/RecTutorial/RecTutorial.html -doc/RecTutorial/RecTutorial.ps +doc/unreleased.rst # .mll files diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8cff8f66b7..d9adaf5dc7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -17,8 +17,8 @@ well. - [Writing tutorials and blog posts](#writing-tutorials-and-blog-posts) - [Contributing to the wiki](#contributing-to-the-wiki) - [Creating and maintaining Coq packages](#creating-and-maintaining-coq-packages) - - [Distribution](#distribution) - - [Support](#support) + - [Distribution of Coq packages](#distribution-of-coq-packages) + - [Support for plugin and library authors](#support-for-plugin-and-library-authors) - [Standard libraries](#standard-libraries) - [Maintaining existing packages in coq-community](#maintaining-existing-packages-in-coq-community) - [Contributing to the editor support packages](#contributing-to-the-editor-support-packages) @@ -161,14 +161,14 @@ tools is great so that others can start building new things on top. Having an extensive and healthy package ecosystem will be key to the success of Coq. -#### Distribution #### +#### Distribution of Coq packages #### You can distribute your library or plugin through the [Coq package index][Coq-package-index]. Tools can be advertised on the [tools page][tools-website] of the Coq website, or the [tools page][tools-wiki] of the wiki. -#### Support #### +#### Support for plugin and library authors #### You can find advice and best practices about maintaining a Coq project on the [coq-community wiki][coq-community-wiki]. @@ -529,10 +529,20 @@ how you can anticipate the results of the CI before opening a PR. Such a failure can indicate either a bug in your branch, or a breaking change that you introduced voluntarily. All such breaking changes should be properly documented in the [user changelog][user-changelog]. -Furthermore, a backward-compatible fix should be found, and this fix -should be merged in the broken projects *before* your PR to the Coq -repository can be. You can use the same documentation as above to -learn about testing and fixing locally the broken libraries. +Furthermore, a backward-compatible fix should be found, properly +documented in the changelog when non-obvious, and this fix should be +merged in the broken projects *before* your PR to the Coq repository +can be. + +Note that once the breaking change is well understood, it should not +feel like it is your role to fix every project that is affected: as +long as reviewers have approved and are ready to integrate your +breaking change, you are entitled to (politely) request project +authors / maintainers to fix the breakage on their own, or help you +fix it. Obviously, you should leave enough time for this to happen +(you cannot expect a project maintainer to allocate time for this as +soon as you request it) and you should be ready to listen to more +feedback and reconsider the impact of your change. #### Understanding reviewers' feedback #### diff --git a/Makefile.build b/Makefile.build index 8a11d913a9..6590f5f308 100644 --- a/Makefile.build +++ b/Makefile.build @@ -50,6 +50,12 @@ VALIDATE ?= # When non-empty, passed as extra arguments to coqtop/coqc: COQUSERFLAGS ?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -104,6 +110,19 @@ include Makefile.dev ## provides the 'printers' and 'revision' rules ########################################################################### # Timing targets ########################################################################### +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: @@ -111,21 +130,21 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(HIDE)($(MAKE) --no-print-directory $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else ifeq (,$(AFTER)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -858,7 +877,7 @@ endif $(HIDE)$(BOOTCOQC) $< -vio -noglob %.v.timing.diff: %.v.before-timing %.v.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)'PYTHON TIMING-DIFF $*.v.{before,after}-timing' $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/Makefile.dev b/Makefile.dev index b1e142333a..6e9b5356ab 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -140,17 +140,17 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ### 4) plugins ################ -OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) -MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) -NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) -BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) -RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) -EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) +OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO)) +MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO)) +RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO)) +NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO)) +FUNINDVO:=$(filter theories/funind/%, $(THEORIESVO)) +BTAUTOVO:=$(filter theories/btauto/%, $(THEORIESVO)) +RTAUTOVO:=$(filter theories/rtauto/%, $(THEORIESVO)) +EXTRACTIONVO:=$(filter theories/extraction/%, $(THEORIESVO)) CCVO:= -DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) -LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) +DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO)) +LTACVO:=$(filter theories/ltac/%, $(THEORIESVO)) omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 9ed7180807..6a740b9033 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -43,9 +43,10 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab ### Breaking changes When your PR breaks an external project we test in our CI, you must -prepare a patch (or ask someone to prepare a patch) to fix the -project. There is experimental support for an improved workflow, see -[the next section](#experimental-automatic-overlay-creation-and-building), below +prepare a patch (or ask someone—possibly the project author—to +prepare a patch) to fix the project. There is experimental support for +an improved workflow, see [the next +section](#experimental-automatic-overlay-creation-and-building), below are the steps to manually prepare a patch: 1. Fork the external project, create a new branch, push a commit adapting diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 06b617d4c1..6649820f22 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -1,36 +1,40 @@ Information for external library / Coq plugin authors ----------------------------------------------------- -You are encouraged to consider submitting your development for addition to +You are encouraged to consider submitting your project for addition to Coq's CI. This means that: -- Any time that a proposed change is breaking your development, Coq developers - will send you patches to adapt it or, at the very least, will work with you - to see how to adapt it. +- Any time that a proposed change is breaking your project, Coq + developers and contributors will send you patches to adapt it or + will explain how to adapt it and work with you to ensure that you + manage to do it. On the condition that: -- At the time of the submission, your development works with Coq's +- At the time of the submission, your project works with Coq's `master` branch. -- Your development is publicly available in a git repository and we can easily +- Your project is publicly available in a git repository and we can easily send patches to you (e.g. through pull / merge requests). - You react in a timely manner to discuss / integrate those patches. + When seeking your help for preparing such patches, we will accept + that it takes longer than when we are just requesting to integrate a + simple (and already fully prepared) patch. - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. - For that, we recommend setting a CI system for you development, see + For that, we recommend setting a CI system for you project, see [supported CI images for Coq](#supported-ci-images-for-coq) below. -- You maintain a reasonable build time for your development, or you provide +- You maintain a reasonable build time for your project, or you provide a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach -out to you and give you a 30-day grace period during which your development +out to you and give you a 30-day grace period during which your project would be moved into our "allow failure" category. At the end of the grace -period, in the absence of progress, the development would be removed from our +period, in the absence of progress, the project would be removed from our CI. ### Timely merging of overlays @@ -47,7 +51,7 @@ these kind of merges. ### OCaml and plugin-specific considerations -Developments that link against Coq's OCaml API [most of them are known +Projects that link against Coq's OCaml API [most of them are known as "plugins"] do have some special requirements: - Coq's OCaml API is not stable. We hope to improve this in the future @@ -65,7 +69,7 @@ as "plugins"] do have some special requirements: uses. In particular, warnings that are considered fatal by the Coq developers _must_ be also fatal for plugin CI code. -### Add your development by submitting a pull request +### Add your project by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the @@ -75,7 +79,7 @@ Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an example. **Do not hesitate to submit an incomplete pull request if you need help to finish it.** -You may also be interested in having your development tested in our +You may also be interested in having your project tested in our performance benchmark. Currently this is done by providing an OPAM package in https://github.com/coq/opam-coq-archive and opening an issue at https://github.com/coq/coq-bench/issues. @@ -83,13 +87,13 @@ https://github.com/coq/coq-bench/issues. ### Recommended branching policy. It is sometimes the case that you will need to maintain a branch of -your development for particular Coq versions. This is in fact very -likely if your development includes a Coq ML plugin. +your project for particular Coq versions. This is in fact very likely +if your project includes a Coq ML plugin. -We thus recommend a branching convention that mirrors Coq's branching -policy. Then, you would have a `master` branch that follows Coq's -`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so -on. +For such projects, we recommend a branching convention that mirrors +Coq's branching policy. Then, you would have a `master` branch that +follows Coq's `master`, a `v8.8` branch that works with Coq's `v8.8` +branch and so on. This convention will be supported by tools in the future to make some developer commands work more seamlessly. diff --git a/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh b/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh new file mode 100644 index 0000000000..c17fe4fcba --- /dev/null +++ b/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10832" ] || [ "$CI_BRANCH" = "master+fix6082-7766-overriding-notation-format" ]; then + + equations_CI_REF=master+fix-interpretation-notation-format-pr10832 + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + + quickchick_CI_REF=master+fix-interpretation-notation-format-pr10832 + quickchick_CI_GITURL=https://github.com/herbelin/QuickChick + +fi diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md index 3db5d0b14f..f81630c55d 100644 --- a/dev/doc/INSTALL.make.md +++ b/dev/doc/INSTALL.make.md @@ -102,6 +102,14 @@ Detailed Installation Procedure. it is recommended to compile in parallel, via make -jN where N is your number of cores. + If you wish to create timing logs for the standard library, you can + pass `TIMING=1` (for per-line timing files) or `TIMED=1` (for + per-file timing on stdout). Further variables and targets are + available for more detailed timing analysis; see the section of the + reference manual on `coq_makefile`. If there is any timing target + or variable supported by `coq_makefile`-made Makefiles which is not + supported by Coq's own Makefile, please report that as a bug. + 5. You can now install the Coq system. Executables, libraries, and manual pages are copied in some standard places of your system, defined at configuration time (step 3). Just do diff --git a/dev/doc/changes.md b/dev/doc/changes.md index cb6e695865..42dd2dd052 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +Types `precedence`, `parenRelation`, `tolerability` in +`notgram_ops.ml` have been reworked. See `entry_level` and +`entry_relative_level` in `constrexpr.ml`. + +### ML API + Exception handling: - Coq's custom `Backtrace` module has been removed in favor of OCaml's diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst new file mode 100644 index 0000000000..51818c666b --- /dev/null +++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst @@ -0,0 +1,5 @@ +- **Added:** + :cmd:`Implicit Types` are now taken into account for printing. To inhibit it, + unset the :flag:`Printing Use Implicit Types` flag + (`#11261 <https://github.com/coq/coq/pull/11261>`_, + by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_). diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst new file mode 100644 index 0000000000..5393fb3d8c --- /dev/null +++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst @@ -0,0 +1 @@ +- Different interpretations in different scopes of the same notation string can now be associated to different printing formats; this fixes bug #6092 and #7766 (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst new file mode 100644 index 0000000000..1d94cbf21b --- /dev/null +++ b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Notations in onlyprinting mode do not uselessly reserve parsing keywords + (`#11590 <https://github.com/coq/coq/pull/11590>`_, + by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_). diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst new file mode 100644 index 0000000000..49dd0ee2d8 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst @@ -0,0 +1,5 @@ +- **Added:** + New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the + `Coq` library prefix by default + (`#11617 <https://github.com/coq/coq/pull/11617>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst new file mode 100644 index 0000000000..3b20bbf75d --- /dev/null +++ b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst @@ -0,0 +1,35 @@ +- **Added:** + The ``make-both-single-timing-files.py`` script now accepts a + ``--fuzz=N`` parameter on the command line which determines how many + characters two lines may be offset in the "before" and "after" + timing logs while still being considered the same line. When + invoking this script via the ``print-pretty-single-time-diff`` + target in a ``Makefile`` made by ``coq_makefile``, you can set this + argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + The ``make-one-time-file.py`` and ``make-both-time-files.py`` + scripts now accept a ``--real`` parameter on the command line to + print real times rather than user times in the tables. The + ``make-both-single-timing-files.py`` script accepts a ``--user`` + parameter to use user times. When invoking these scripts via the + ``print-pretty-timed`` or ``print-pretty-timed-diff`` or + ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by + ``coq_makefile``, you can set this argument by passing + ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass + ``--user``) to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + Coq's build system now supports both ``TIMING_FUZZ``, + ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` + made by ``coq_makefile`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Fixed:** + The various timing targets for Coq's standard library now correctly + display and label the "before" and "after" columns, rather than + mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ + fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason + Gross). diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst index 90c23d8b76..32a4750b73 100644 --- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst +++ b/doc/changelog/08-tools/11523-coqdep+refactor2.rst @@ -1,7 +1,10 @@ - **Changed:** - Internal options and behavior of ``coqdep`` have changed, in particular - options ``-w``, ``-D``, ``-mldep``, and ``-dumpbox`` have been removed, - and ``-boot`` will not load any path by default, ``-R/-Q`` should be - used instead - (`#11523 <https://github.com/coq/coq/pull/11523>`_, + Internal options and behavior of ``coqdep`` have changed. ``coqdep`` + no longer works as a replacement for ``ocamldep``, thus ``.ml`` + files are not supported as input. Also, several deprecated options + have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``, + ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will + not load any path by default now, ``-R/-Q`` should be used instead. + (`#11523 <https://github.com/coq/coq/pull/11523>`_ and + `#11589 <https://github.com/coq/coq/pull/11589>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst b/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst new file mode 100644 index 0000000000..0a686dd87d --- /dev/null +++ b/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst @@ -0,0 +1,4 @@ +- **Fixed:** + :cmd:`Extraction Implicit` on the constructor of a record was leading to an anomaly + (`#11329 <https://github.com/coq/coq/pull/11329>`_, + by Hugo Herbelin, fixes `#11114 <https://github.com/coq/coq/pull/11114>`_). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f0bbaed8f3..9686500a35 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2208,6 +2208,13 @@ or :g:`m` to the type :g:`nat` of natural numbers). Adds blocks of implicit types with different specifications. +.. flag:: Printing Use Implicit Types + + By default, the type of bound variables is not printed when + the variable name is associated to an implicit type which matches the + actual type of the variable. This feature can be deactivated by + turning this flag off. + .. _implicit-generalization: Implicit generalization diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 3d1fc6d4b9..179dff9959 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -255,14 +255,20 @@ file timing data: one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed TGTS="a.vo b.vo"``. - .. :: + .. note:: This target requires ``python`` to build the table. .. note:: This target will *append* to the timing log; if you want a - fresh start, you must remove the ``filetime-of-build.log`` or + fresh start, you must remove the file ``time-of-build.log`` or ``run make cleanall``. + .. note:: + By default the table displays user times. If the build log + contains real times (which it does by default), passing + ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times + rather than user times in the table. + .. example:: For example, the output of ``make pretty-timed`` may look like this: @@ -310,6 +316,15 @@ file timing data: (which are frequently noise); lexicographic sorting forces an order on files which take effectively no time to compile. + If you prefer a different sorting order, you can pass + ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or + ``TIMING_SORT_BY=diff`` to sort by the signed difference in + time. + + .. note:: + Just like ``pretty-timed``, this table defaults to using user + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. + .. example:: For example, the output table from @@ -349,7 +364,7 @@ line timing data: :: - print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing this target will make a sorted table of the per-line timing differences between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and @@ -364,6 +379,28 @@ line timing data: .. note:: This target requires python to build the table. + .. note:: + This target follows the same sorting order as the + ``print-pretty-timed-diff`` target, and supports the same + options for the ``TIMING_SORT_BY`` variable. + + .. note:: + By default, two lines are only considered the same if the + character offsets and initial code strings are identical. Passing + ``TIMING_FUZZ=N`` relaxes this constraint by allowing the + character locations to differ by up to ``N``, as long + as the total number of characters and initial code strings + continue to match. This is useful when there are small changes + to a file, and you want to match later lines that have not + changed even though the character offsets have changed. + + .. note:: + By default the table picks up real times, under the assumption + that when comparing line-by-line, the real time is a more + accurate representation as it includes disk time and time spent + in the native compiler. Passing ``TIMING_REAL=0`` to ``make`` + will use user times rather than real times in the table. + .. example:: For example, running ``print-pretty-single-time-diff`` might give a table like this: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a8d5ac610f..7c628e534b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: +.. coqtop:: none + + Reset Initial. + .. coqtop:: all Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). @@ -350,6 +354,11 @@ Reserving notations This command declares an infix parsing rule without giving its interpretation. + When a format is attached to a reserved notation, it is used by + default by all subsequent interpretations of the corresponding + notation. A specific interpretation can provide its own format + overriding the default format though. + Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/ide/coq.ml b/ide/coq.ml index 4d6ba55d76..0c6aef0305 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -133,10 +133,10 @@ and asks_for_coqtop args = ~filter:false ~filename:(coqtop_path ()) () in match file with - | Some _ -> - let () = custom_coqtop := file in + | [file] -> + let () = custom_coqtop := Some file in filter_coq_opts args - | None -> exit 0 + | _ -> exit 0 exception WrongExitStatus of string diff --git a/ide/coqide.ml b/ide/coqide.ml index ccf6d40b2b..143a12deeb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -282,9 +282,8 @@ let load ?parent _ = let filename = try notebook#current_term.fileops#filename with Invalid_argument _ -> None in - match select_file_for_open ~title:"Load file" ?parent ?filename () with - | None -> () - | Some f -> FileAux.load_file f + let filenames = select_file_for_open ~title:"Load file" ~multiple:true ?parent ?filename () in + List.iter FileAux.load_file filenames let save ?parent _ = on_current_term (FileAux.check_save ?parent ~saveas:false) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 1cf065cf25..38da229d61 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -259,7 +259,7 @@ let current_dir () = match project_path#get with | None -> "" | Some dir -> dir -let select_file_for_open ~title ?(filter=true) ?parent ?filename () = +let select_file_for_open ~title ?(filter=true) ?(multiple=false) ?parent ?filename () = let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ?parent () in @@ -271,6 +271,7 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () = file_chooser#add_filter (filter_all_files ()) end; file_chooser#set_default_response `OPEN; + file_chooser#set_select_multiple multiple; let dir = match filename with | None -> current_dir () | Some f -> Filename.dirname f in @@ -279,12 +280,12 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () = match file_chooser#run () with | `OPEN -> begin - match file_chooser#filename with - | None -> None - | Some _ as f -> - project_path#set file_chooser#current_folder; f + let filenames = file_chooser#get_filenames in + (if filenames <> [] then + project_path#set file_chooser#current_folder); + filenames end - | `DELETE_EVENT | `CANCEL -> None in + | `DELETE_EVENT | `CANCEL -> [] in file_chooser#destroy (); file diff --git a/ide/ideutils.mli b/ide/ideutils.mli index bacb273657..af30cd2b05 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -31,7 +31,7 @@ val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter val select_file_for_open : - title:string -> ?filter:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string option + title:string -> ?filter:bool -> ?multiple:bool -> ?parent:GWindow.window -> ?filename:string -> unit -> string list val select_file_for_save : title:string -> ?parent:GWindow.window -> ?filename:string -> unit -> string option val try_convert : string -> string diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b96ef7c4e5..4bdacda529 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -19,11 +19,21 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option +type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string + +type entry_level = int +type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome + type notation_entry = InConstrEntry | InCustomEntry of string -type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int +type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level type notation_key = string + +(* A notation associated to a given parsing rule *) type notation = notation_entry_level * notation_key +(* A notation associated to a given interpretation *) +type specific_notation = notation_with_optional_scope * notation + type 'a or_by_notation_r = | AN of 'a | ByNotation of (string * string option) @@ -78,7 +88,7 @@ type cases_pattern_expr_r = (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of qualid option | CPatOr of cases_pattern_expr list - | CPatNotation of notation * cases_pattern_notation_substitution + | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) @@ -119,7 +129,7 @@ and constr_expr_r = | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type - | CNotation of notation * constr_notation_substitution + | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index b4798127f9..401853b625 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -75,7 +75,8 @@ let rec cases_pattern_expr_eq p1 p2 = Option.equal qualid_eq r1 r2 | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 - | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> + | CPatNotation (inscope1, n1, s1, l1), CPatNotation (inscope2, n2, s2, l2) -> + Option.equal notation_with_optional_scope_eq inscope1 inscope2 && notation_eq n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 @@ -160,7 +161,8 @@ let rec constr_expr_eq e1 e2 = Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 - | CNotation(n1, s1), CNotation(n2, s2) -> + | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> + Option.equal notation_with_optional_scope_eq inscope1 inscope2 && notation_eq n1 n2 && constr_notation_substitution_eq s1 s2 | CPrim i1, CPrim i2 -> @@ -271,7 +273,7 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with | CPatCstr (_,patl1,patl2) -> List.fold_left (cases_pattern_fold_names f) (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,(patl,patll),patl') -> + | CPatNotation (_,_,(patl,patll),patl') -> List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat @@ -320,7 +322,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bl,bll)) -> + | CNotation (_,_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in @@ -399,9 +401,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bl,bll)) -> + | CNotation (inscope,n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, + CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) | CDelimiters (s,a) -> CDelimiters (s,f e a) @@ -574,7 +576,7 @@ let mkAppPattern ?loc p lp = CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern" (Pp.str "Nested applications not supported.") | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp) - | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp) + | CPatNotation (inscope, n, s, l) -> CPatNotation (inscope, n , s, l@lp) | _ -> CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern" (Pp.str "Such pattern cannot have arguments.")) @@ -591,8 +593,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v | CAppExpl ((None,r,i),args) -> CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[]) - | CNotation (ntn,(c,cl,[],[])) -> - CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c, + | CNotation (inscope,ntn,(c,cl,[],[])) -> + CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c, List.map (List.map coerce_to_cases_pattern_expr) cl),[]) | CPrim p -> CPatPrim p diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 06232b8e1a..38dc10a9b3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes (* This suppresses printing of primitive tokens (e.g. numeral) and notations *) let print_no_symbol = ref false +(* This tells to skip types if a variable has this type by default *) +let print_use_implicit_types = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Use";"Implicit";"Types"] + ~value:true + +(**********************************************************************) + +let hole = CAst.make @@ CHole (None, IntroAnonymous, None) + +let is_reserved_type na t = + not !Flags.raw_print && print_use_implicit_types () && + match na with + | Anonymous -> false + | Name id -> + try + let pat = Reserve.find_reserved_type id in + let _ = match_notation_constr false t ([],pat) in + true + with Not_found | No_match -> false + (**********************************************************************) (* Turning notations and scopes on and off for printing *) module IRuleSet = Set.Make(struct @@ -75,10 +97,10 @@ let inactive_notations_table = let inactive_scopes_table = Summary.ref ~name:"inactive_scopes_table" CString.Set.empty -let show_scope scopt = - match scopt with - | None -> str "" - | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc +let show_scope inscope = + match inscope with + | LastLonelyNotation -> str "" + | NotationInScope sc -> spc () ++ str "in scope" ++ spc () ++ str sc let _show_inactive_notations () = begin @@ -97,8 +119,8 @@ let _show_inactive_notations () = let _ = Feedback.msg_notice (str "Inactive notations:") in IRuleSet.iter (function - | NotationRule (scopt, ntn) -> - Feedback.msg_notice (pr_notation ntn ++ show_scope scopt) + | NotationRule (inscope, ntn) -> + Feedback.msg_notice (pr_notation ntn ++ show_scope inscope) | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)))) !inactive_notations_table @@ -107,18 +129,19 @@ let deactivate_notation nr = | SynDefRule kn -> (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table - | NotationRule (scopt, ntn) -> - match availability_of_notation (scopt, ntn) (scopt, []) with + | NotationRule (inscope, ntn) -> + let scopt = match inscope with NotationInScope sc -> Some sc | LastLonelyNotation -> None in + match availability_of_notation (inscope, ntn) (scopt, []) with | None -> user_err ~hdr:"Notation" (pr_notation ntn ++ spc () ++ str "does not exist" - ++ (match scopt with - | None -> spc () ++ str "in the empty scope." - | Some _ -> show_scope scopt ++ str ".")) + ++ (match inscope with + | LastLonelyNotation -> spc () ++ str "in the empty scope." + | NotationInScope _ -> show_scope inscope ++ str ".")) | Some _ -> if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () - ++ str "is already inactive" ++ show_scope scopt ++ str ".") + ++ str "is already inactive" ++ show_scope inscope ++ str ".") else inactive_notations_table := IRuleSet.add nr !inactive_notations_table let reactivate_notation nr = @@ -127,9 +150,9 @@ let reactivate_notation nr = IRuleSet.remove nr !inactive_notations_table with Not_found -> match nr with - | NotationRule (scopt, ntn) -> + | NotationRule (inscope, ntn) -> Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () - ++ str "is already active" ++ show_scope scopt ++ + ++ str "is already active" ++ show_scope inscope ++ str ".") | SynDefRule kn -> let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in @@ -157,8 +180,8 @@ let reactivate_scope sc = let is_inactive_rule nr = IRuleSet.mem nr !inactive_notations_table || match nr with - | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table - | NotationRule (None, ntn) -> false + | NotationRule (NotationInScope sc, ntn) -> CString.Set.mem sc !inactive_scopes_table + | NotationRule (LastLonelyNotation, ntn) -> false | SynDefRule _ -> false (* args: notation, scope, activate/deactivate *) @@ -169,10 +192,13 @@ let toggle_scope_printing ~scope ~activate = deactivate_scope scope let toggle_notation_printing ?scope ~notation ~activate = + let inscope = match scope with + | None -> LastLonelyNotation + | Some sc -> NotationInScope sc in if activate then - reactivate_notation (NotationRule (scope, notation)) + reactivate_notation (NotationRule (inscope, notation)) else - deactivate_notation (NotationRule (scope, notation)) + deactivate_notation (NotationRule (inscope, notation)) (* This governs printing of projections using the dot notation symbols *) let print_projections = ref false @@ -254,11 +280,11 @@ let insert_pat_alias ?loc p = function let rec insert_coercion ?loc l c = match l with | [] -> c - | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[])) + | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[])) let rec insert_pat_coercion ?loc l c = match l with | [] -> c - | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) + | (inscope,ntn)::l -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,([insert_pat_coercion ?loc l c],[]),[]) (**********************************************************************) (* conversion of references *) @@ -348,19 +374,19 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl = | None -> mknot (loc,ntn,l,bl) end | _ -> mknot (loc,ntn,l,bl) -let make_notation loc ntn (terms,termlists,binders,binderlists as subst) = +let make_notation loc (inscope,ntn) (terms,termlists,binders,binderlists as subst) = if not (List.is_empty termlists) || not (List.is_empty binderlists) then - CAst.make ?loc @@ CNotation (ntn,subst) + CAst.make ?loc @@ CNotation (Some inscope,ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[]))) + (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (Some inscope,ntn,(l,[],bl,[]))) (fun (loc,p) -> CAst.make ?loc @@ CPrim p) destPrim terms binders -let make_pat_notation ?loc ntn (terms,termlists as subst) args = - if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else +let make_pat_notation ?loc (inscope,ntn) (terms,termlists as subst) args = + if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (Some inscope,ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,(l,[]),args)) (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) destPatPrim terms [] @@ -450,12 +476,12 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (custom, (tmp_scope, scopes) as allscopes) vars = function - | NotationRule (sc,ntn) -> + | NotationRule (_,ntn as specific_ntn) -> begin match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) (tmp_scope,scopes) with + match availability_of_notation specific_ntn (tmp_scope,scopes) with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) @@ -479,7 +505,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in insert_pat_coercion coercion (insert_pat_delimiters ?loc - (make_pat_notation ?loc ntn (l,ll) l2') key) + (make_pat_notation ?loc specific_ntn (l,ll) l2') key) end | SynDefRule kn -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with @@ -786,17 +812,21 @@ let rec flatten_application c = match DAst.get c with end | a -> c +let same_binder_type ty nal c = + match nal, DAst.get c with + | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty' + | [], _ -> true + | _ -> assert false + (**********************************************************************) (* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = let (sc,n) = uninterp_prim_token r in - let coercion = - if entry_has_prim_token n custom then [] else - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> coercion in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> match availability_of_prim_token n sc scopes with | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) @@ -937,12 +967,10 @@ let rec extern inctx scopes vars r = extern inctx scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_prod scopes (add_vname vars na) na bk t c + factorize_prod scopes vars na bk t c | GLambda (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_lambda inctx scopes (add_vname vars na) na bk t c + factorize_lambda inctx scopes vars na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -971,17 +999,19 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in + let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map CAst.make nal, + let inctx = inctx || typopt <> None in + CLetTuple (List.map CAst.make nal, (Option.map (fun _ -> (make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (c,(na,typopt),b1,b2) -> + let inctx = inctx || typopt <> None in CIf (sub_extern false scopes vars c, (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), @@ -1004,7 +1034,7 @@ let rec extern inctx scopes vars r = | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) in ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, - extern false scopes vars1 def)) idv + sub_extern true scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> @@ -1015,7 +1045,7 @@ let rec extern inctx scopes vars r = let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), - sub_extern false scopes vars1 bv.(i))) idv + sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) @@ -1041,7 +1071,10 @@ and extern_typ (subentry,(_,scopes)) = and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) -and factorize_prod scopes vars na bk aty c = +and factorize_prod scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1058,18 +1091,25 @@ and factorize_prod scopes vars na bk aty c = | _ -> CProdN ([binder],b)) | _ -> assert false) | _, _ -> - let c = extern_typ scopes vars c in - match na, c.v with + let c' = extern_typ scopes vars c in + match na, c'.v with | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + when binding_kind_eq bk bk' + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let ty = if implicit_type then ty else aty in + CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b) | _, CProdN (bl,b) -> - CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CProdN (CLocalAssum([make na],Default bk,ty)::bl,b) | _, _ -> - CProdN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CProdN ([CLocalAssum([make na],Default bk,ty)],c') -and factorize_lambda inctx scopes vars na bk aty c = +and factorize_lambda inctx scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1086,16 +1126,20 @@ and factorize_lambda inctx scopes vars na bk aty c = | _ -> CLambdaN ([binder],b)) | _ -> assert false) | _, _ -> - let c = sub_extern inctx scopes vars c in - match c.v with + let c' = sub_extern inctx scopes vars c in + match c'.v with | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + when binding_kind_eq bk bk' + && not (occur_name na ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let aty = if implicit_type then ty else aty in CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) | CLambdaN (bl,b) -> - CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b) | _ -> - CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CLambdaN ([CLocalAssum([make na],Default bk,ty)],c') and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -1109,15 +1153,17 @@ and extern_local_binder scopes vars = function Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> + let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) - when constr_expr_eq ty ty' && + when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> + let ty = if implicit_type then hole else ty in (na::assums,na::ids, CLocalAssum([CAst.make na],Default bk,ty) :: l)) @@ -1185,11 +1231,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) match keyrule with - | NotationRule (sc,ntn) -> + | NotationRule (_,ntn as specific_ntn) -> (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) scopes with + match availability_of_notation specific_ntn scopes with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) @@ -1212,7 +1258,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = List.map (fun (bl,(subentry,(scopt,scl))) -> pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in - let c = make_notation loc ntn (l,ll,bl,bll) in + let c = make_notation loc specific_ntn (l,ll,bl,bll) in let c = insert_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b2c572d290..1cfd50e26e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -226,7 +226,7 @@ let contract_curly_brackets ntn (l,ll,bl,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> + | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -242,7 +242,7 @@ let contract_curly_brackets_pat ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> + | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -1719,13 +1719,13 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> + | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in rcp_of_glob scopes pat - | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> + | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> in_pat top scopes a - | CPatNotation (ntn,fullargs,extrargs) -> + | CPatNotation (_,ntn,fullargs,extrargs) -> let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in @@ -2035,11 +2035,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) - | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> + | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) - | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a - | CNotation (ntn,args) -> + | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a + | CNotation (_,ntn,args) -> intern_notation intern env ntnvars loc ntn args | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c @@ -2070,7 +2070,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref - | CNotation (ntn,([],[],[],[])) -> + | CNotation (_,ntn,([],[],[],[])) -> assert (Option.is_empty isproj); let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index ffbb982ab7..e6f12f7eb2 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (qid,_) when qualid_is_ident qid -> found c.CAst.loc (qualid_basename qid) bdvars l - | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c diff --git a/interp/notation.ml b/interp/notation.ml index 9d6cab550d..2086e08f79 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -49,6 +49,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false +let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with + | LastLonelyNotation, LastLonelyNotation -> true + | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2 + | (LastLonelyNotation | NotationInScope _), _ -> false + let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 @@ -63,6 +68,15 @@ module NotationOrd = module NotationSet = Set.Make(NotationOrd) module NotationMap = CMap.Make(NotationOrd) +module SpecificNotationOrd = + struct + type t = specific_notation + let compare = pervasives_compare + end + +module SpecificNotationSet = Set.Make(SpecificNotationOrd) +module SpecificNotationMap = CMap.Make(SpecificNotationOrd) + (**********************************************************************) (* Scope of symbols *) @@ -148,21 +162,21 @@ let normalize_scope sc = (**********************************************************************) (* The global stack of scopes *) -type scope_elem = Scope of scope_name | SingleNotation of notation -type scopes = scope_elem list +type scope_item = OpenScopeItem of scope_name | LonelyNotationItem of notation +type scopes = scope_item list let scope_eq s1 s2 = match s1, s2 with -| Scope s1, Scope s2 -> String.equal s1 s2 -| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2 -| Scope _, SingleNotation _ -| SingleNotation _, Scope _ -> false +| OpenScopeItem s1, OpenScopeItem s2 -> String.equal s1 s2 +| LonelyNotationItem s1, LonelyNotationItem s2 -> notation_eq s1 s2 +| OpenScopeItem _, LonelyNotationItem _ +| LonelyNotationItem _, OpenScopeItem _ -> false let scope_stack = ref [] let current_scopes () = !scope_stack let scope_is_open_in_scopes sc l = - List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l + List.exists (function OpenScopeItem sc' -> String.equal sc sc' | _ -> false) l let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) @@ -188,7 +202,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_elem -> obj = +let inScope : bool * bool * scope_item -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -197,11 +211,11 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) + Lib.add_anonymous_leaf (inScope (local,opening,OpenScopeItem (normalize_scope sc))) let empty_scope_stack = [] -let push_scope sc scopes = Scope sc :: scopes +let push_scope sc scopes = OpenScopeItem sc :: scopes let push_scopes = List.fold_right push_scope @@ -254,7 +268,7 @@ let find_delimiters_scope ?loc key = (* Uninterpretation tables *) type interp_rule = - | NotationRule of scope_name option * notation + | NotationRule of specific_notation | SynDefRule of KerName.t (* We define keys for glob_constr and aconstr to split the syntax entries @@ -1064,17 +1078,17 @@ let check_required_module ?loc sc (sp,d) = the scope stack [scopes], and if yes, using delimiters or not *) let find_with_delimiters = function - | None -> None - | Some scope -> + | LastLonelyNotation -> None + | NotationInScope scope -> match (String.Map.find scope !scope_map).delimiters with | Some key -> Some (Some scope, Some key) | None -> None let rec find_without_delimiters find (ntn_scope,ntn) = function - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with - | Some scope' when String.equal scope scope' -> + | NotationInScope scope' when String.equal scope scope' -> Some (None,None) | _ -> (* If the most recently open scope has a notation/numeral printer @@ -1084,9 +1098,9 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function else find_without_delimiters find (ntn_scope,ntn) scopes end - | SingleNotation ntn' :: scopes -> + | LonelyNotationItem ntn' :: scopes -> begin match ntn_scope, ntn with - | None, Some ntn when notation_eq ntn ntn' -> + | LastLonelyNotation, Some ntn when notation_eq ntn ntn' -> Some (None, None) | _ -> find_without_delimiters find (ntn_scope,ntn) scopes @@ -1123,7 +1137,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = scope_map := String.Map.add scope sc !scope_map end; begin match scopt with - | None -> scope_stack := SingleNotation ntn :: !scope_stack + | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack | Some _ -> () end @@ -1133,15 +1147,15 @@ let declare_uninterpretation rule (metas,c as pat) = let rec find_interpretation ntn find = function | [] -> raise Not_found - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> (try let n = find scope in (n,Some scope) with Not_found -> find_interpretation ntn find scopes) - | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> + | LonelyNotationItem ntn'::scopes when notation_eq ntn' ntn -> (try let n = find default_scope in (n,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) find_interpretation ntn find scopes) - | SingleNotation _::scopes -> + | LonelyNotationItem _::scopes -> find_interpretation ntn find scopes let find_notation ntn sc = @@ -1244,7 +1258,7 @@ let availability_of_notation (ntn_scope,ntn) scopes = commonly from the lowest level of the source entry to the highest level of the target entry. *) -type entry_coercion = notation list +type entry_coercion = (notation_with_optional_scope * notation) list module EntryCoercionOrd = struct @@ -1295,7 +1309,7 @@ let rec insert_coercion_path path = function else if shorter_path path path' then path::allpaths else path'::insert_coercion_path path paths -let declare_entry_coercion (entry,_ as ntn) entry' = +let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' = let entry, lev = decompose_custom_entry entry in let entry', lev' = decompose_custom_entry entry' in (* Transitive closure *) @@ -1304,19 +1318,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' = List.fold_right (fun ((lev'',lev'''),path) l -> if notation_entry_eq entry entry''' && level_ord lev lev''' && not (notation_entry_eq entry' entry'') - then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l) + then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l) !entry_coercion_map [] in let toaddright = EntryCoercionMap.fold (fun (entry'',entry''') paths l -> List.fold_right (fun ((lev'',lev'''),path) l -> if entry' = entry'' && level_ord lev' lev'' && entry <> entry''' - then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l) + then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l) !entry_coercion_map [] in entry_coercion_map := List.fold_right (fun (pair,path) -> let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in EntryCoercionMap.add pair (insert_coercion_path path olds)) - (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft) + (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft) !entry_coercion_map let entry_has_global_map = ref String.Map.empty @@ -1349,34 +1363,6 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false -let entry_has_numeral_map = ref String.Map.empty -let entry_has_string_map = ref String.Map.empty - -let declare_custom_entry_has_numeral s n = - try - let p = String.Map.find s !entry_has_numeral_map in - user_err (str "Custom entry " ++ str s ++ - str " has already a rule for numerals at level " ++ int p ++ str ".") - with Not_found -> - entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map - -let declare_custom_entry_has_string s n = - try - let p = String.Map.find s !entry_has_string_map in - user_err (str "Custom entry " ++ str s ++ - str " has already a rule for strings at level " ++ int p ++ str ".") - with Not_found -> - entry_has_string_map := String.Map.add s n !entry_has_string_map - -let entry_has_prim_token prim = function - | InConstrEntrySomeLevel -> true - | InCustomEntryLevel (s,n) -> - match prim with - | Numeral _ -> - (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false) - | String _ -> - (try String.Map.find s !entry_has_string_map <= n with Not_found -> false) - let uninterp_prim_token c = match glob_prim_constr_key c with | None -> raise Notation_ops.No_match @@ -1417,7 +1403,7 @@ let availability_of_prim_token n printer_scope local_scopes = with Not_found -> false in let scopes = make_current_scopes local_scopes in - Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) + Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes) (* Miscellaneous *) @@ -1733,11 +1719,11 @@ let pr_scopes prglob = let rec find_default ntn = function | [] -> None - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> if NotationMap.mem ntn (find_scope scope).notations then Some scope else find_default ntn scopes - | SingleNotation ntn' :: scopes -> + | LonelyNotationItem ntn' :: scopes -> if notation_eq ntn ntn' then Some default_scope else find_default ntn scopes @@ -1891,13 +1877,13 @@ let collect_notation_in_scope scope sc known = let collect_notations stack = fst (List.fold_left (fun (all,knownntn as acc) -> function - | Scope scope -> + | OpenScopeItem scope -> if String.List.mem_assoc scope all then acc else let (l,knownntn) = collect_notation_in_scope scope (find_scope scope) knownntn in ((scope,l)::all,knownntn) - | SingleNotation ntn -> + | LonelyNotationItem ntn -> if List.mem_f notation_eq ntn knownntn then (all,knownntn) else try diff --git a/interp/notation.mli b/interp/notation.mli index 707be6cb87..26c45d5896 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -25,11 +25,15 @@ val notation_entry_eq : notation_entry -> notation_entry -> bool val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool (** Equality on [notation_entry_level]. *) +val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_with_optional_scope -> bool + val notation_eq : notation -> notation -> bool (** Equality on [notation]. *) module NotationSet : Set.S with type elt = notation module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet +module SpecificNotationSet : Set.S with type elt = specific_notation +module SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet (** {6 Scopes } *) (** A scope is a set of interpreters for symbols + optional @@ -213,7 +217,7 @@ val availability_of_prim_token : (** Binds a notation in a given scope to an interpretation *) type interp_rule = - | NotationRule of scope_name option * notation + | NotationRule of specific_notation | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> @@ -236,7 +240,7 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) -val availability_of_notation : scope_name option * notation -> subscopes -> +val availability_of_notation : specific_notation -> subscopes -> (scope_name option * delimiters option) option (** {6 Miscellaneous} *) @@ -299,18 +303,15 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -type entry_coercion = notation list -val declare_entry_coercion : notation -> notation_entry_level -> unit +type entry_coercion = (notation_with_optional_scope * notation) list +val declare_entry_coercion : specific_notation -> notation_entry_level -> unit val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option val declare_custom_entry_has_global : string -> int -> unit val declare_custom_entry_has_ident : string -> int -> unit -val declare_custom_entry_has_numeral : string -> int -> unit -val declare_custom_entry_has_string : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool -val entry_has_prim_token : prim_token -> notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 178f7354f2..848861238a 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -29,7 +29,6 @@ type 'a constr_entry_key_gen = | ETIdent | ETGlobal | ETBigint - | ETString | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) @@ -54,7 +53,6 @@ type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) - | ETProdString (* Parsed as a string *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index dcc3a87b11..d6c6c365cb 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -199,11 +199,11 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) (match c.CAst.v with | CPrim (Numeral (SPlus,n)) -> - CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) + CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) | _ -> c) } | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> - { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } + { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> @@ -380,7 +380,7 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) match p.CAst.v with | CPatPrim (Numeral (SPlus,n)) -> - CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 9f133ca9d4..427505c199 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -10,14 +10,11 @@ open Names open Extend +open Constrexpr (** Dealing with precedences *) -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list +type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = @@ -37,7 +34,4 @@ type one_notation_grammar = { notgram_prods : grammar_constr_prod_item list list; } -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} +type notation_grammar = one_notation_grammar list diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index 5c220abeda..b6699493bb 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -12,33 +12,36 @@ open Pp open CErrors open Util open Notation -open Notation_gram +open Constrexpr -(* Uninterpreted notation levels *) +(* Register the level of notation for parsing and printing + (also register the parsing rule if not onlyprinting) *) let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty -let declare_notation_level ?(onlyprint=false) ntn level = +let declare_notation_level ntn parsing_rule level = try - let (level,onlyprint) = NotationMap.find ntn !notation_level_map in - if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") + let _ = NotationMap.find ntn !notation_level_map in + anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") with Not_found -> - notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map + notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map -let level_of_notation ?(onlyprint=false) ntn = - let (level,onlyprint') = NotationMap.find ntn !notation_level_map in - if onlyprint' && not onlyprint then raise Not_found; - level +let level_of_notation ntn = + NotationMap.find ntn !notation_level_map + +let get_defined_notations () = + NotationSet.elements @@ NotationMap.domain !notation_level_map (**********************************************************************) (* Equality *) open Extend -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false +let entry_relative_level_eq t1 t2 = match t1, t2 with +| LevelLt n1, LevelLt n2 -> Int.equal n1 n2 +| LevelLe n1, LevelLe n2 -> Int.equal n1 n2 +| LevelSome, LevelSome -> true +| (LevelLt _ | LevelLe _ | LevelSome), _ -> false let production_position_eq pp1 pp2 = match (pp1,pp2) with | BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2 @@ -55,19 +58,17 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETIdent, ETIdent -> true | ETGlobal, ETGlobal -> true | ETBigint, ETBigint -> true -| ETString, ETString -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) -> notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false +| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in let prod_eq (l1,pp1) (l2,pp2) = not strict || (production_level_eq l1 l2 && production_position_eq pp1 pp2) in - notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2 && List.equal (constr_entry_key_eq prod_eq) u1 u2 let level_eq = level_eq_gen false diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli index c31f4505e7..d8b7e8e4c1 100644 --- a/parsing/notgram_ops.mli +++ b/parsing/notgram_ops.mli @@ -13,8 +13,13 @@ open Constrexpr open Notation_gram val level_eq : level -> level -> bool +val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit -val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) +val declare_notation_level : notation -> notation_grammar option -> level -> unit +val level_of_notation : notation -> notation_grammar option * level + (** raise [Not_found] if not declared *) + +(** Returns notations with defined parsing/printing rules *) +val get_defined_notations : unit -> notation list diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 2154f2f881..12311f9cd9 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -2,8 +2,8 @@ Tok CLexer Extend Notation_gram -Ppextend Notgram_ops +Ppextend Pcoq G_constr G_prim diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index 7368f4109e..393ab8a302 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -12,7 +12,8 @@ open Util open Pp open CErrors open Notation -open Notation_gram +open Constrexpr +open Notgram_ops (*s Pretty-print. *) @@ -37,41 +38,67 @@ let ppcmd_of_cut = function | PpBrk(n1,n2) -> brk(n1,n2) type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut -type unparsing_rule = unparsing list * precedence +type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list -(* Concrete syntax for symbolic-extension table *) -let notation_rules = - Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t) - -let declare_notation_rule ntn ~extra unpl gram = - notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules - -let find_notation_printing_rule ntn = - try pi1 (NotationMap.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".") -let find_notation_extra_printing_rules ntn = - try pi2 (NotationMap.find ntn !notation_rules) - with Not_found -> [] -let find_notation_parsing_rules ntn = - try pi3 (NotationMap.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".") - -let get_defined_notations () = - NotationSet.elements @@ NotationMap.domain !notation_rules + +let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with + | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2 + | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 + | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2 + | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2 + | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2) + | UnpCut p1, UnpCut p2 -> p1 = p2 + | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ | + UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false + +(* Register generic and specific printing rules *) + +let generic_notation_printing_rules = + Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t) + +let specific_notation_printing_rules = + Summary.ref ~name:"specific-notation-printing-rules" (SpecificNotationMap.empty : (unparsing_rule * extra_unparsing_rules) SpecificNotationMap.t) + +let declare_generic_notation_printing_rules ntn ~reserved ~extra unpl = + generic_notation_printing_rules := NotationMap.add ntn (unpl,reserved,extra) !generic_notation_printing_rules +let declare_specific_notation_printing_rules specific_ntn ~extra unpl = + specific_notation_printing_rules := SpecificNotationMap.add specific_ntn (unpl,extra) !specific_notation_printing_rules + +let has_generic_notation_printing_rule ntn = + NotationMap.mem ntn !generic_notation_printing_rules + +let find_generic_notation_printing_rule ntn = + NotationMap.find ntn !generic_notation_printing_rules + +let find_specific_notation_printing_rule specific_ntn = + SpecificNotationMap.find specific_ntn !specific_notation_printing_rules + +let find_notation_printing_rule which ntn = + try match which with + | None -> raise Not_found (* Normally not the case *) + | Some which -> fst (find_specific_notation_printing_rule (which,ntn)) + with Not_found -> pi1 (find_generic_notation_printing_rule ntn) + +let find_notation_extra_printing_rules which ntn = + try match which with + | None -> raise Not_found + | Some which -> snd (find_specific_notation_printing_rule (which,ntn)) + with Not_found -> pi3 (find_generic_notation_printing_rule ntn) let add_notation_extra_printing_rule ntn k v = try - notation_rules := - let p, pp, gr = NotationMap.find ntn !notation_rules in - NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules + generic_notation_printing_rules := + let p, b, pp = NotationMap.find ntn !generic_notation_printing_rules in + NotationMap.add ntn (p, b, (k,v) :: pp) !generic_notation_printing_rules with Not_found -> user_err ~hdr:"add_notation_extra_printing_rule" (str "No such Notation.") diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index be5af75e72..346fc83f5f 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -9,7 +9,6 @@ (************************************************************************) open Constrexpr -open Notation_gram (** {6 Pretty-print. } *) @@ -31,21 +30,24 @@ val ppcmd_of_cut : ppcut -> Pp.t (** Declare and look for the printing rule for symbolic notations *) type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list + | UnpMetaVar of entry_relative_level + | UnpBinderMetaVar of entry_relative_level + | UnpListMetaVar of entry_relative_level * unparsing list + | UnpBinderListMetaVar of bool * unparsing list | UnpTerminal of string | UnpBox of ppbox * unparsing Loc.located list | UnpCut of ppcut -type unparsing_rule = unparsing list * precedence +type unparsing_rule = unparsing list * entry_level type extra_unparsing_rules = (string * string) list -val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit -val find_notation_printing_rule : notation -> unparsing_rule -val find_notation_extra_printing_rules : notation -> extra_unparsing_rules -val find_notation_parsing_rules : notation -> notation_grammar -val add_notation_extra_printing_rule : notation -> string -> string -> unit -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list +val unparsing_eq : unparsing -> unparsing -> bool + +val declare_generic_notation_printing_rules : notation -> reserved:bool -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val declare_specific_notation_printing_rules : specific_notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val has_generic_notation_printing_rule : notation -> bool +val find_generic_notation_printing_rule : notation -> unparsing_rule * bool * extra_unparsing_rules +val find_specific_notation_printing_rule : specific_notation -> unparsing_rule * extra_unparsing_rules +val find_notation_printing_rule : notation_with_optional_scope option -> notation -> unparsing_rule +val find_notation_extra_printing_rules : notation_with_optional_scope option -> notation -> extra_unparsing_rules +val add_notation_extra_printing_rule : notation -> string -> string -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 9b30ddd958..71a3dcfef2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -507,21 +507,22 @@ and extract_really_ind env kn mib = assert (Int.equal (List.length field_names) (List.length typ)); let projs = ref Cset.empty in let mp = MutInd.modpath kn in - let rec select_fields l typs = match l,typs with + let implicits = implicits_of_global (GlobRef.ConstructRef (ip,1)) in + let rec select_fields i l typs = match l,typs with | [],[] -> [] - | _::l, typ::typs when isTdummy (expand env typ) -> - select_fields l typs + | _::l, typ::typs when isTdummy (expand env typ) || Int.Set.mem i implicits -> + select_fields (i+1) l typs | {binder_name=Anonymous}::l, typ::typs -> - None :: (select_fields l typs) + None :: (select_fields (i+1) l typs) | {binder_name=Name id}::l, typ::typs -> let knp = Constant.make2 mp (Label.of_id id) in (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((==) Keep) (type2signature env typ) then projs := Cset.add knp !projs; - Some (GlobRef.ConstRef knp) :: (select_fields l typs) + Some (GlobRef.ConstRef knp) :: (select_fields (i+1) l typs) | _ -> assert false in - let field_glob = select_fields field_names typ + let field_glob = select_fields (1+npar) field_names typ in (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index bab6bfd78e..5835d75c79 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -298,7 +298,7 @@ END let pr_by_arg_tac env sigma _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t) } diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 6dd51e4e01..dd4195f2ef 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,7 +67,7 @@ val wit_by_arg_tac : val pr_by_arg_tac : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Entry.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 7843faaef3..e2b8bcb5a9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Notation_gram open Tactypes open Locus open Genredexpr @@ -73,43 +72,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function @@ -294,7 +293,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg)) + let pr_farg prtac arg = prtac LevelSome (TacArg (CAst.make arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -314,35 +313,35 @@ let string_of_genarg_arg (ArgumentType arg) = let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t = fun prtac symb arg -> match symb with - | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac LevelSome arg | Extend.Ulist1 s | Extend.Ulist0 s -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_sequence (pr_any_arg prtac s) l end | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l end | Extend.Uopt s -> begin match get_opt arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_opt (pr_any_arg prtac s) l end | Extend.Uentry _ | Extend.Uentryl _ -> - str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> - prtac (1, Any) arg - | Extend.Uentryl (_, l) -> prtac (l, Any) arg + prtac LevelSome arg + | Extend.Uentryl (_, l) -> prtac LevelSome arg | _ -> match arg with | TacGeneric arg -> let pr l arg = prtac l (TacGeneric arg) in pr_any_arg pr symb arg - | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_raw_extend_rec prtac = pr_extend_gen (pr_farg prtac) @@ -630,7 +629,7 @@ let pr_goal_selector ~toplevel s = let pr_then () = str ";" - let ltop = (5,E) + let ltop = LevelLe 5 let lseq = 4 let ltactical = 3 let lorelse = 2 @@ -645,13 +644,13 @@ let pr_goal_selector ~toplevel s = let ltatom = 1 let linfo = 5 - let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq + let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels *) type 'a printer = { - pr_tactic : tolerability -> 'tacexpr -> Pp.t; + pr_tactic : entry_relative_level -> 'tacexpr -> Pp.t; pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t; @@ -780,7 +779,7 @@ let pr_goal_selector ~toplevel s = hov 1 ( primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++ - pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacAssert (ev,_,None,ipat,c) -> hov 1 ( @@ -857,7 +856,7 @@ let pr_goal_selector ~toplevel s = pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl - ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( @@ -893,11 +892,11 @@ let pr_goal_selector ~toplevel s = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with | TacAbstract (t,None) -> - keyword "abstract " ++ pr_tac (labstract,L) t, labstract + keyword "abstract " ++ pr_tac (LevelLt labstract) t, labstract | TacAbstract (t,Some s) -> hov 0 ( keyword "abstract" - ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () + ++ str" (" ++ pr_tac (LevelLt labstract) t ++ str")" ++ spc () ++ keyword "using" ++ spc () ++ pr_id s), labstract | TacLetIn (recflag,llc,u) -> @@ -906,7 +905,7 @@ let pr_goal_selector ~toplevel s = (hv 0 ( pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc ++ spc () ++ keyword "in" - ) ++ fnl () ++ pr_tac (llet,E) u), + ) ++ fnl () ++ pr_tac (LevelLe llet) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( @@ -931,17 +930,17 @@ let pr_goal_selector ~toplevel s = hov 2 ( keyword "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () - ++ pr_tac (lfun,E) body), + ++ pr_tac (LevelLe lfun) body), lfun | TacThens (t,tl) -> hov 1 ( - pr_tac (lseq,E) t ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t ++ pr_then () ++ spc () ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl), lseq | TacThen (t1,t2) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () - ++ pr_tac (lseq,L) t2), + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () + ++ pr_tac (LevelLt lseq) t2), lseq | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl, lseq @@ -949,78 +948,78 @@ let pr_goal_selector ~toplevel s = pr_tac_extend (pr_tac ltop) tf t tr , lseq | TacThens3parts (t1,tf,t2,tl) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () ++ pr_then_gen (pr_tac ltop) tf t2 tl), lseq | TacTry t -> hov 1 ( - keyword "try" ++ spc () ++ pr_tac (ltactical,E) t), + keyword "try" ++ spc () ++ pr_tac (LevelLe ltactical) t), ltactical | TacDo (n,t) -> hov 1 ( str "do" ++ spc () ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTimeout (n,t) -> hov 1 ( keyword "timeout " ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTime (s,t) -> hov 1 ( keyword "time" ++ pr_opt qstring s ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacRepeat t -> hov 1 ( keyword "repeat" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacProgress t -> hov 1 ( keyword "progress" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacShowHyps t -> hov 1 ( keyword "infoH" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacInfo t -> hov 1 ( keyword "info" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), linfo | TacOr (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "+" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacOnce t -> hov 1 ( keyword "once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacExactlyOnce t -> hov 1 ( keyword "exactly_once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacIfThenCatch (t,tt,te) -> hov 1 ( - str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ - str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ - str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + str"tryif" ++ spc() ++ pr_tac (LevelLe ltactical) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (LevelLe ltactical) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (LevelLe ltactical) te ++ brk(1,1)), ltactical | TacOrelse (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "||" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacFail (g,n,l) -> let arg = @@ -1042,7 +1041,7 @@ let pr_goal_selector ~toplevel s = | TacSolve tl -> keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - pr_tac (lcomplete,E) t, lcomplete + pr_tac (LevelLe lcomplete) t, lcomplete | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom @@ -1398,10 +1397,10 @@ let () = let () = let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_tactic printer printer printer - ltop (0,E) + ltop (LevelLe 0) let () = let pr_unit _env _sigma _ _ _ _ () = str "()" in let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit - ltop (0,E) + ltop (LevelLe 0) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 9cff3ea1eb..33db933168 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -16,7 +16,6 @@ open Geninterp open Names open Environ open Constrexpr -open Notation_gram open Genintern open Tacexpr open Tactypes @@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level : 'a raw_extra_genarg_printer_with_level -> 'b glob_extra_genarg_printer_with_level -> 'c extra_genarg_printer_with_level -> - (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t +val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t @@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('b, 'a) match_rule -> Pp.t -val pr_value : tolerability -> Val.t -> Pp.t +val pr_value : entry_relative_level -> Val.t -> Pp.t -val ltop : tolerability +val ltop : entry_relative_level -val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) -> +val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) -> 'a Genprint.top_printer diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 21b832a326..3f67d55e73 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -90,7 +90,7 @@ let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Notation_gram.E) +let tacltop = (LevelLe 5) let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index e6b1706b41..53c895f9d9 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -15,12 +15,12 @@ open Ltac_plugin val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> - (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) -> 'c val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> - (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) -> 'c -> 'd val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index e45bae19ca..96f8cb12ba 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -857,7 +857,7 @@ let glob_cpattern gs p = | k, (v, Some t), _ as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else match t.CAst.v with - | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -865,11 +865,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; diff --git a/printing/genprint.ml b/printing/genprint.ml index a04df31d30..a673cbd933 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -19,15 +19,15 @@ open Geninterp (* Printing generic values *) type 'a with_level = - { default_already_surrounded : Notation_gram.tolerability; - default_ensure_surrounded : Notation_gram.tolerability; + { default_already_surrounded : Constrexpr.entry_relative_level; + default_ensure_surrounded : Constrexpr.entry_relative_level; printer : 'a } type printer_result = | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/genprint.mli b/printing/genprint.mli index 21b8417ffa..59e36baeb6 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -13,15 +13,15 @@ open Genarg type 'a with_level = - { default_already_surrounded : Notation_gram.tolerability; - default_ensure_surrounded : Notation_gram.tolerability; + { default_already_surrounded : Constrexpr.entry_relative_level; + default_ensure_surrounded : Constrexpr.entry_relative_level; printer : 'a } type printer_result = | PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f9f46e1ceb..c2d760ae08 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -20,7 +20,6 @@ open Ppextend open Glob_term open Constrexpr open Constrexpr_ops -open Notation_gram open Namegen (*i*) @@ -66,21 +65,16 @@ let tag_var = tag Tag.variable let lapp = 10 let lposint = 0 let lnegint = 35 (* must be consistent with Notation "- x" *) - let ltop = (200,E) + let ltop = LevelLe 200 let lproj = 1 let ldelim = 1 - let lsimpleconstr = (8,E) - let lsimplepatt = (1,E) - - let prec_less child (parent,assoc) = - if parent < 0 && Int.equal child lprod then true - else - let parent = abs parent in - match assoc with - | E -> (<=) child parent - | L -> (<) child parent - | Prec n -> child<=n - | Any -> true + let lsimpleconstr = LevelLe 8 + let lsimplepatt = LevelLe 1 + + let prec_less child = function + | LevelLt parent -> (<) child parent + | LevelLe parent -> if parent < 0 && Int.equal child lprod then true else child <= abs parent + | LevelSome -> true let prec_of_prim_token = function | Numeral (SPlus,_) -> lposint @@ -98,22 +92,22 @@ let tag_var = tag Tag.variable let rec aux = function | [] -> mt () - | UnpMetaVar (_, prec) as unp :: l -> + | UnpMetaVar prec as unp :: l -> let c = pop env in let pp2 = aux l in - let pp1 = pr (n, prec) c in + let pp1 = pr prec c in return unp pp1 pp2 - | UnpBinderMetaVar (_, prec) as unp :: l -> + | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in let pp2 = aux l in - let pp1 = pr_patt (n, prec) c in + let pp1 = pr_patt prec c in return unp pp1 pp2 - | UnpListMetaVar (_, prec, sl) as unp :: l -> + | UnpListMetaVar (prec, sl) as unp :: l -> let cl = pop envlist in - let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in let pp2 = aux l in return unp pp1 pp2 - | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> + | UnpBinderListMetaVar (isopen, sl) as unp :: l -> let cl = pop bll in let pp2 = aux l in let pp1 = pr_binders (fun () -> aux sl) isopen cl in @@ -133,8 +127,8 @@ let tag_var = tag Tag.variable in aux unps - let pr_notation pr pr_patt pr_binders s env = - let unpl, level = find_notation_printing_rule s in + let pr_notation pr pr_patt pr_binders which s env = + let unpl, level = find_notation_printing_rule which s in print_hunks level pr pr_patt pr_binders env unpl, level let pr_delimiters key strm = @@ -216,7 +210,7 @@ let tag_var = tag Tag.variable let pr_expl_args pr (a,expl) = match expl with - | None -> pr (lapp,L) a + | None -> pr (LevelLt lapp) a | Some {v=ExplByPos (n,_id)} -> anomaly (Pp.str "Explicitation by position not implemented.") | Some {v=ExplByName id} -> @@ -243,31 +237,32 @@ let tag_var = tag Tag.variable let las = lapp let lpator = 0 let lpatrec = 0 + let lpattop = LevelLe 200 let rec pr_patt sep inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> let pp (c, p) = - pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p + pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p in (if l = [] then str "{| |}" else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec | CPatAlias (p, na) -> - pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las + pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las | CPatCstr (c, None, []) -> pr_reference c, latom | CPatCstr (c, None, args) -> - pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp | CPatCstr (c, Some args, []) -> - str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp | CPatCstr (c, Some expl_args, extra_args) -> - surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args) - ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp + surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args) + ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp | CPatAtom (None) -> str "_", latom @@ -276,16 +271,16 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - let pp p = hov 0 (pr_patt mt (lpator,Any) p) in + let pp p = hov 0 (pr_patt mt lpattop p) in surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator - | CPatNotation ((_,"( _ )"),([p],[]),[]) -> - pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom + | CPatNotation (_,(_,"( _ )"),([p],[]),[]) -> + pr_patt (fun()->str"(") lpattop p ++ str")", latom - | CPatNotation (s,(l,ll),args) -> - let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) s (l,ll,[],[]) in - (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not) - ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not + | CPatNotation (which,s,(l,ll),args) -> + let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in + (if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not) + ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not | CPatPrim p -> pr_prim_token p, latom @@ -440,7 +435,7 @@ let tag_var = tag Tag.variable | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) let pr_case_item pr (tm,as_clause, in_clause) = - hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause) + hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause) let pr_case_type pr po = match po with @@ -456,17 +451,17 @@ let tag_var = tag Tag.variable pr_case_type pr po let pr_proj pr pr_app a f l = - hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + hov 0 (pr (LevelLe lproj) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") let pr_appexpl pr (f,us) l = hov 2 ( str "@" ++ pr_reference f ++ pr_universe_instance us ++ - prlist (pr_sep_com spc (pr (lapp,L))) l) + prlist (pr_sep_com spc (pr (LevelLt lapp))) l) let pr_app pr a l = hov 2 ( - pr (lapp,L) a ++ + pr (LevelLt lapp) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) let pr_record_body_gen pr l = @@ -483,7 +478,7 @@ let tag_var = tag Tag.variable let pr_dangling_with_for sep pr inherited a = match a.v with | (CFix (_,[_])|CCoFix(_,[_])) -> - pr sep (latom,E) a + pr sep (LevelLe latom) a | _ -> pr sep inherited a @@ -546,14 +541,14 @@ let tag_var = tag Tag.variable let c,l1 = List.sep_last l1 in let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in if not (List.is_empty l2) then - return (p ++ prlist (pr spc (lapp,L)) l2, lapp) + return (p ++ prlist (pr spc (LevelLt lapp)) l2, lapp) else return (p, lproj) | CAppExpl ((None,qid,us),[t]) | CApp ((_, {v = CRef(qid,us)}),[t,None]) when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var -> return ( - hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), + hov 0 (str ".." ++ pr spc (LevelLe latom) t ++ spc () ++ str ".."), larg ) | CAppExpl ((None,f,us),l) -> @@ -642,24 +637,24 @@ let tag_var = tag Tag.variable return (pr_glob_sort s, latom) | CCast (a,b) -> return ( - hv 0 (pr mt (lcast,L) a ++ spc () ++ + hv 0 (pr mt (LevelLt lcast) a ++ spc () ++ match b with - | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b - | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b - | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b + | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b + | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b + | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b | CastCoerce -> str ":>"), lcast ) - | CNotation ((_,"( _ )"),([t],[],[],[])) -> - return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) - | CNotation (s,env) -> - pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env + | CNotation (_,(_,"( _ )"),([t],[],[],[])) -> + return (pr (fun()->str"(") ltop t ++ str")", latom) + | CNotation (which,s,env) -> + pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env | CGeneralization (bk,ak,c) -> return (pr_generalization bk ak (pr mt ltop c), latom) | CPrim p -> return (pr_prim_token p, prec_of_prim_token p) | CDelimiters (sc,a) -> - return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) + return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim) in let loc = constr_loc a in pr_with_comments ?loc diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index c17ca251a8..288fb251c4 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -15,9 +15,8 @@ open Libnames open Constrexpr open Names -open Notation_gram -val prec_less : precedence -> tolerability -> bool +val prec_less : entry_level -> entry_relative_level -> bool val pr_tight_coma : unit -> Pp.t @@ -49,7 +48,7 @@ val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t -val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t +val pr_constr_expr_n : Environ.env -> Evd.evar_map -> entry_relative_level -> constr_expr -> Pp.t type term_pr = { pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t; @@ -76,8 +75,8 @@ val default_term_pr : term_pr Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) -val lsimpleconstr : tolerability -val ltop : tolerability +val lsimpleconstr : entry_relative_level +val ltop : entry_relative_level val modular_constr_pr : - ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) -> - (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t + ((unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index cc83a1dde0..b376616b61 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -278,7 +278,7 @@ let pr_compacted_decl env sigma decl = ids, mt (), typ | CompactedDecl.LocalDef (ids,c,typ) -> (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in + let pb = pr_lconstr_env ~inctx:true env sigma c in let pb = if isCast c then surround pb else pb in ids, (str" := " ++ pb ++ cut ()), typ in @@ -297,7 +297,7 @@ let pr_rel_decl env sigma decl = | RelDecl.LocalAssum _ -> mt () | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in + let pb = pr_lconstr_env ~inctx:true env sigma c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = pr_ltype_env env sigma typ in diff --git a/printing/printer.mli b/printing/printer.mli index cd5151bd8f..24d0a8cf6a 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -51,7 +51,7 @@ val enable_goal_names_printing : bool ref val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t +val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" @@ -63,7 +63,7 @@ val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t val pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t -val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t @@ -100,7 +100,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t -val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index d93dd15f91..c3ee5968dc 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -529,7 +529,7 @@ let match_goals ot nt = constr_expr ogname a a2 | CastCoerce, CastCoerce -> () | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)")) - | CNotation (ntn,args), CNotation (ntn2,args2) -> + | CNotation (_,ntn,args), CNotation (_,ntn2,args2) -> constr_notation_substitution ogname args args2 | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) -> constr_expr ogname c c2 diff --git a/test-suite/bugs/closed/bug_11114.v b/test-suite/bugs/closed/bug_11114.v new file mode 100644 index 0000000000..dd981279db --- /dev/null +++ b/test-suite/bugs/closed/bug_11114.v @@ -0,0 +1,17 @@ +Require Extraction. + +Inductive t (sig: list nat) := +| T (k: nat). + +Record pkg := + { _sig: list nat; + _t : t _sig }. + +Definition map (f: nat -> nat) (p: pkg) := + {| _sig := p.(_sig); + _t := match p.(_t) with + | T _ k => T p.(_sig) (f k) + end |}. + +Extraction Implicit Build_pkg [_sig]. +Extraction TestCompile map. diff --git a/test-suite/bugs/closed/bug_9741.v b/test-suite/bugs/closed/bug_9741.v new file mode 100644 index 0000000000..247155d8b3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9741.v @@ -0,0 +1,21 @@ +(* This was failing at parsing *) + +Notation "'a'" := tt (only printing). +Goal True. let a := constr:(1+1) in idtac a. Abort. + +(* Idem *) + +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Open Scope string_scope. + +Axiom Ox: string -> Z. + +Axiom isMMIOAddr: Z -> Prop. + +Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a"). + +Goal False. + set (f := isMMIOAddr). + set (x := f (Ox "0018")). +Abort. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh index 4a50759bdb..a6f35db17c 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/run.sh @@ -5,6 +5,10 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log +"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-user.log -diff -u time-of-build-both.log.expected time-of-build-both.log || exit $? +diff -u time-of-build-both-user.log.expected time-of-build-both-user.log || exit $? + +"$COQLIB"/tools/make-both-time-files.py --real time-of-build-after.log.in time-of-build-before.log.in time-of-build-both-real.log + +diff -u time-of-build-both-real.log.expected time-of-build-both-real.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected new file mode 100644 index 0000000000..ea600b000e --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-real.log.expected @@ -0,0 +1,26 @@ +After | File Name | Before || Change | % Change +---------------------------------------------------------------------------------------------- +20m46.07s | Total | 23m06.30s || -2m20.23s | -10.11% +---------------------------------------------------------------------------------------------- +4m16.77s | Specific/X25519/C64/ladderstep | 5m16.83s || -1m00.06s | -18.95% +3m01.77s | Specific/solinas32_2e255m765_13limbs/femul | 3m27.94s || -0m26.16s | -12.58% +2m35.79s | Specific/solinas32_2e255m765_12limbs/femul | 2m59.21s || -0m23.42s | -13.06% +3m22.96s | Specific/NISTP256/AMD64/femul | 3m37.80s || -0m14.84s | -6.81% +0m39.72s | Specific/X25519/C64/femul | 0m42.98s || -0m03.25s | -7.58% +0m38.19s | Specific/NISTP256/AMD64/feadd | 0m40.48s || -0m02.28s | -5.65% +0m34.35s | Specific/X25519/C64/freeze | 0m36.42s || -0m02.07s | -5.68% +0m33.08s | Specific/X25519/C64/fesquare | 0m35.23s || -0m02.14s | -6.10% +0m31.00s | Specific/NISTP256/AMD64/feopp | 0m32.08s || -0m01.07s | -3.36% +0m27.81s | Specific/NISTP256/AMD64/fenz | 0m28.91s || -0m01.10s | -3.80% +0m27.11s | Specific/X25519/C64/fecarry | 0m28.85s || -0m01.74s | -6.03% +0m24.71s | Specific/X25519/C64/fesub | 0m26.11s || -0m01.39s | -5.36% +0m49.44s | Specific/solinas32_2e255m765_13limbs/Synthesis | 0m49.50s || -0m00.06s | -0.12% +0m43.34s | Specific/NISTP256/AMD64/fesub | 0m43.78s || -0m00.43s | -1.00% +0m40.13s | Specific/solinas32_2e255m765_12limbs/Synthesis | 0m39.53s || +0m00.60s | +1.51% +0m22.81s | Specific/X25519/C64/feadd | 0m23.43s || -0m00.62s | -2.64% +0m13.45s | Specific/NISTP256/AMD64/Synthesis | 0m13.74s || -0m00.29s | -2.11% +0m11.15s | Specific/X25519/C64/Synthesis | 0m11.23s || -0m00.08s | -0.71% +0m07.33s | Compilers/Z/Bounds/Pipeline/Definition | 0m07.40s || -0m00.07s | -0.94% +0m01.93s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.73s || +0m00.19s | +11.56% +0m01.85s | Specific/Framework/SynthesisFramework | 0m01.95s || -0m00.09s | -5.12% +0m01.38s | Compilers/Z/Bounds/Pipeline | 0m01.18s || +0m00.19s | +16.94%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected index 159e645512..159e645512 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both-user.log.expected diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh index 4f39b3ce7e..d4614749e7 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/run.sh @@ -5,6 +5,10 @@ set -e cd "$(dirname "${BASH_SOURCE[0]}")" -"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty.log +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-user.log -diff -u time-of-build-pretty.log.expected time-of-build-pretty.log || exit $? +diff -u time-of-build-pretty-user.log.expected time-of-build-pretty-user.log || exit $? + +"$COQLIB"/tools/make-one-time-file.py time-of-build.log.in time-of-build-pretty-real.log + +diff -u time-of-build-pretty-real.log.expected time-of-build-pretty-real.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected index b9739ddb1d..b9739ddb1d 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-real.log.expected diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected new file mode 100644 index 0000000000..b9739ddb1d --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty-user.log.expected @@ -0,0 +1,26 @@ +Time | File Name +---------------------------------------------------------- +19m16.04s | Total +---------------------------------------------------------- +4m01.34s | Specific/X25519/C64/ladderstep +3m09.62s | Specific/NISTP256/AMD64/femul +2m48.52s | Specific/solinas32_2e255m765_13limbs/femul +2m23.70s | Specific/solinas32_2e255m765_12limbs/femul +0m45.75s | Specific/solinas32_2e255m765_13limbs/Synthesis +0m39.59s | Specific/NISTP256/AMD64/fesub +0m36.92s | Specific/solinas32_2e255m765_12limbs/Synthesis +0m36.32s | Specific/X25519/C64/femul +0m35.40s | Specific/NISTP256/AMD64/feadd +0m31.50s | Specific/X25519/C64/freeze +0m30.13s | Specific/X25519/C64/fesquare +0m28.51s | Specific/NISTP256/AMD64/feopp +0m25.50s | Specific/NISTP256/AMD64/fenz +0m24.99s | Specific/X25519/C64/fecarry +0m22.65s | Specific/X25519/C64/fesub +0m20.93s | Specific/X25519/C64/feadd +0m12.55s | Specific/NISTP256/AMD64/Synthesis +0m10.37s | Specific/X25519/C64/Synthesis +0m07.18s | Compilers/Z/Bounds/Pipeline/Definition +0m01.72s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics +0m01.67s | Specific/Framework/SynthesisFramework +0m01.19s | Compilers/Z/Bounds/Pipeline
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected new file mode 100644 index 0000000000..726c19a2e2 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-real.v.timing.diff.expected @@ -0,0 +1,29 @@ +After | Code | Before || Change | % Change +----------------------------------------------------------------------------------------------------------- +0m01.23s | Total | 0m01.28s || -0m00.04s | -3.50% +----------------------------------------------------------------------------------------------------------- +0m00.53s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).] | 0m00.566s || -0m00.03s | -6.36% +0m00.4s | Chars 285-289 ~ 305-309 [Qed.] | 0m00.411s || -0m00.01s | -2.67% +0m00.194s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.192s || +0m00.00s | +1.04% +0m00.114s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.] | 0m00.114s || +0m00.00s | +0.00% +0m00.s | Chars 065-075 ~ 065-075 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 078-086 ~ 078-086 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 078-090 ~ 078-090 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 087-091 ~ 091-095 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 092-102 ~ 096-106 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 105-113 ~ 109-117 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 105-117 ~ 109-121 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 114-118 ~ 122-126 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 119-129 ~ 127-137 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 132-140 ~ 140-148 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 132-144 ~ 140-152 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 141-145 ~ 153-157 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 146-156 ~ 158-168 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 159-167 ~ 171-179 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 159-171 ~ 171-183 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 168-172 ~ 184-188 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected new file mode 100644 index 0000000000..f6be1d936d --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo-user.v.timing.diff.expected @@ -0,0 +1,29 @@ +After | Code | Before || Change | % Change +----------------------------------------------------------------------------------------------------------- +0m01.14s | Total | 0m01.15s || -0m00.00s | -0.77% +----------------------------------------------------------------------------------------------------------- +0m00.504s | Chars 260-284 ~ 280-304 [(vm_compute;~reflexivity).] | 0m00.528s || -0m00.02s | -4.54% +0m00.384s | Chars 285-289 ~ 305-309 [Qed.] | 0m00.4s || -0m00.01s | -4.00% +0m00.172s | Chars 031-064 ~ 031-064 [Require~Import~Coq.ZArith.ZArith.] | 0m00.156s || +0m00.01s | +10.25% +0m00.083s | Chars 000-030 ~ 000-030 [Require~Import~Coq.Lists.List.] | 0m00.072s || +0m00.01s | +15.27% +0m00.004s | Chars 200-257 ~ 220-277 [Goal~_~List.repeat~Z.div_eucl~...] | 0m00.s || +0m00.00s | ∞ +0m00.s | Chars 065-075 ~ 065-075 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 078-086 ~ 078-086 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 078-090 ~ 078-090 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 087-091 ~ 091-095 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 092-102 ~ 096-106 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 105-113 ~ 109-117 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 105-117 ~ 109-121 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 114-118 ~ 122-126 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 119-129 ~ 127-137 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 132-140 ~ 140-148 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 132-144 ~ 140-152 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 141-145 ~ 153-157 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 146-156 ~ 158-168 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 159-167 ~ 171-179 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 159-171 ~ 171-183 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 168-172 ~ 184-188 [Qed.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 173-183 ~ 189-199 [Goal~_~True.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 186-194 ~ 202-210 [exact~I.] | N/A || +0m00.00s | N/A + N/A | Chars 186-198 ~ 202-214 [constructor.] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 195-199 ~ 215-219 [Qed.] | 0m00.s || +0m00.00s | N/A
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in new file mode 100644 index 0000000000..c58e7d82d1 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.after-timing.in @@ -0,0 +1,20 @@ +Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.083u,0.032s) +Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.194 secs (0.172u,0.023s) +Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 78 - 86 [exact~I.] 0. secs (0.u,0.s) +Chars 87 - 91 [Qed.] 0. secs (0.u,0.s) +Chars 92 - 102 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 105 - 113 [exact~I.] 0. secs (0.u,0.s) +Chars 114 - 118 [Qed.] 0. secs (0.u,0.s) +Chars 119 - 129 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 132 - 140 [exact~I.] 0. secs (0.u,0.s) +Chars 141 - 145 [Qed.] 0. secs (0.u,0.s) +Chars 146 - 156 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 159 - 167 [exact~I.] 0. secs (0.u,0.s) +Chars 168 - 172 [Qed.] 0. secs (0.u,0.s) +Chars 173 - 183 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 186 - 194 [exact~I.] 0. secs (0.u,0.s) +Chars 195 - 199 [Qed.] 0. secs (0.u,0.s) +Chars 200 - 257 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.004u,0.s) +Chars 260 - 284 [(vm_compute;~reflexivity).] 0.53 secs (0.504u,0.024s) +Chars 285 - 289 [Qed.] 0.4 secs (0.384u,0.016s) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in new file mode 100644 index 0000000000..b49c1b1cb7 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in @@ -0,0 +1,20 @@ +Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.072u,0.044s) +Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.192 secs (0.156u,0.035s) +Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 78 - 90 [constructor.] 0. secs (0.u,0.s) +Chars 91 - 95 [Qed.] 0. secs (0.u,0.s) +Chars 96 - 106 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 109 - 121 [constructor.] 0. secs (0.u,0.s) +Chars 122 - 126 [Qed.] 0. secs (0.u,0.s) +Chars 127 - 137 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 140 - 152 [constructor.] 0. secs (0.u,0.004s) +Chars 153 - 157 [Qed.] 0. secs (0.u,0.s) +Chars 158 - 168 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 171 - 183 [constructor.] 0. secs (0.u,0.s) +Chars 184 - 188 [Qed.] 0. secs (0.u,0.s) +Chars 189 - 199 [Goal~_~True.] 0. secs (0.u,0.s) +Chars 202 - 214 [constructor.] 0. secs (0.u,0.s) +Chars 215 - 219 [Qed.] 0. secs (0.u,0.s) +Chars 220 - 277 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.u,0.s) +Chars 280 - 304 [(vm_compute;~reflexivity).] 0.566 secs (0.528u,0.039s) +Chars 305 - 309 [Qed.] 0.411 secs (0.4u,0.008s) diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v new file mode 100644 index 0000000000..7141065b52 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v @@ -0,0 +1,20 @@ +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal True. + exact I. +Qed. +Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5. + vm_compute; reflexivity. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v new file mode 100644 index 0000000000..e152689ee4 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.v @@ -0,0 +1,20 @@ +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal True. + constructor. +Qed. +Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5. + vm_compute; reflexivity. +Qed. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh new file mode 100755 index 0000000000..980bf9cf01 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/run.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 foo.v.after-timing.in foo.v.before-timing.in foo-real.v.timing.diff || exit $? + +diff -u foo-real.v.timing.diff.expected foo-real.v.timing.diff || exit $? + +"$COQLIB"/tools/make-both-single-timing-files.py --fuzz=20 --user foo.v.after-timing.in foo.v.before-timing.in foo-user.v.timing.diff || exit $? + +diff -u foo-user.v.timing.diff.expected foo-user.v.timing.diff || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index cfacf738a3..4b5acb9168 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -10,3 +10,4 @@ export COQLIB ./001-correct-diff-sorting-order/run.sh ./002-single-file-sorting/run.sh ./003-non-utf8/run.sh +./004-per-file-fuzz/run.sh diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 5f22eb5d7c..ef7667936c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -1,4 +1,4 @@ -compose (C:=nat) S +compose S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) @@ -12,3 +12,8 @@ map id' (1 :: nil) : list nat map (id'' (A:=nat)) (1 :: nil) : list nat +fix f (x : nat) : option nat := match x with + | 0 => None + | S _ => x + end + : nat -> option nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 306532c0df..a7c4399e38 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x. Check map (@id'' nat) (1::nil). +Module MatchBranchesInContext. + +Set Implicit Arguments. +Set Contextual Implicit. + +Inductive option A := None | Some (a:A). +Coercion some_nat := @Some nat. +Check fix f x := match x with 0 => None | n => some_nat n end. + +End MatchBranchesInContext. diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out new file mode 100644 index 0000000000..824c260e92 --- /dev/null +++ b/test-suite/output/ImplicitTypes.out @@ -0,0 +1,26 @@ +forall b, b = b + : Prop +forall b : nat, b = b + : Prop +forall b : bool, @eq bool b b + : Prop +forall b : bool, b = b + : Prop +forall b c : bool, b = c + : Prop +forall c b : bool, b = c + : Prop +forall b1 b2, b1 = b2 + : Prop +fun b => b = b + : bool -> Prop +fix f b (n : nat) {struct n} : bool := + match n with + | 0 => b + | S p => f b p + end + : bool -> nat -> bool +∀ b c : bool, b = c + : Prop +∀ b1 b2, b1 = b2 + : Prop diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v new file mode 100644 index 0000000000..dbc83f9229 --- /dev/null +++ b/test-suite/output/ImplicitTypes.v @@ -0,0 +1,37 @@ +Implicit Types b : bool. +Check forall b, b = b. + +(* Check the type is not used if not the reserved one *) +Check forall b:nat, b = b. + +(* Check full printing *) +Set Printing All. +Check forall b, b = b. +Unset Printing All. + +(* Check printing of type *) +Unset Printing Use Implicit Types. +Check forall b, b = b. +Set Printing Use Implicit Types. + +(* Check factorization: we give priority on factorization over implicit type *) +Check forall b c, b = c. +Check forall c b, b = c. + +(* Check factorization of implicit types *) +Check forall b1 b2, b1 = b2. + +(* Check in "fun" *) +Check fun b => b = b. + +(* Check in binders *) +Check fix f b n := match n with 0 => b | S p => f b p end. + +(* Check in notations *) +Module Notation. + Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + Check forall b c, b = c. + Check forall b1 b2, b1 = b2. +End Notation. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 1c8f237bb8..e121b5e86c 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,8 +14,6 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat -[2 + 3] - : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] @@ -77,3 +75,35 @@ Entry constr:expr is [ "201" RIGHTA [ "{"; constr:operconstr LEVEL "200"; "}" ] ] +fun x : nat => [ x ] + : nat -> nat +fun x : nat => [x] + : nat -> nat +∀ x : nat, x = x + : Prop +File "stdin", line 219, characters 0-160: +Warning: Notation "∀ _ .. _ , _" was already defined with a different format +in scope type_scope. [notation-incompatible-format,parsing] +∀x : nat,x = x + : Prop +File "stdin", line 232, characters 0-60: +Warning: Notation "_ %%% _" was already defined with a different format. +[notation-incompatible-format,parsing] +File "stdin", line 236, characters 0-64: +Warning: Notation "_ %%% _" was already defined with a different format. +[notation-incompatible-format,parsing] +File "stdin", line 241, characters 0-62: +Warning: Lonely notation "_ %%%% _" was already defined with a different +format. [notation-incompatible-format,parsing] +3 %% 4 + : nat +3 %% 4 + : nat +3 %% 4 + : nat +File "stdin", line 269, characters 0-61: +Warning: The format modifier is irrelevant for only parsing rules. +[irrelevant-format-only-parsing,parsing] +File "stdin", line 273, characters 0-63: +Warning: The only parsing modifier has no effect in Reserved Notation. +[irrelevant-reserved-notation-only-parsing,parsing] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4ab800c9ba..1cf0d919b1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,9 +22,6 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9). Check [ << # 0 >> ]. -Notation "n" := n%nat (in custom myconstr at level 0, n bigint). -Check [ 2 + 3 ]. - End A. Module B. @@ -195,3 +192,84 @@ Notation "{ p }" := (p) (in custom expr at level 201, p constr). Print Custom Grammar expr. End Bug11331. + +Module Bug_6082. + +Declare Scope foo. +Notation "[ x ]" := (S x) (format "[ x ]") : foo. +Open Scope foo. +Check fun x => S x. + +Declare Scope bar. +Notation "[ x ]" := (S x) (format "[ x ]") : bar. +Open Scope bar. + +Check fun x => S x. + +End Bug_6082. + +Module Bug_7766. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' ∀ x .. y ']' , P") : type_scope. + +Check forall (x : nat), x = x. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "∀ x .. y , P") : type_scope. + +Check forall (x : nat), x = x. + +End Bug_7766. + +Module N. + +(* Other tests about generic and specific formats *) + +Reserved Notation "x %%% y" (format "x %%% y", at level 35). +Reserved Notation "x %%% y" (format "x %%% y", at level 35). + +(* Not using the reserved format, we warn *) + +Notation "x %%% y" := (x+y) (format "x %%% y", at level 35). + +(* Same scope (here lonely): we warn *) + +Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35). +Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35). + +(* Test if the format for a specific notation becomes the default + generic format or if the generic format, in the absence of a + Reserved Notation, is the one canonically obtained from the + notation *) + +Declare Scope foo_scope. +Declare Scope bar_scope. +Declare Scope bar'_scope. +Notation "x %% y" := (x+y) (at level 47, format "x %% y") : foo_scope. +Open Scope foo_scope. +Check 3 %% 4. + +(* No scope, we inherit the initial format *) + +Notation "x %% y" := (x*y) : bar_scope. (* Inherit the format *) +Open Scope bar_scope. +Check 3 %% 4. + +(* Different scope and no reserved notation, we don't warn *) + +Notation "x %% y" := (x*y) (at level 47, format "x %% y") : bar'_scope. +Open Scope bar'_scope. +Check 3 %% 4. + +(* Warn for combination of "only parsing" and "format" *) + +Notation "###" := 0 (at level 0, only parsing, format "###"). + +(* In reserved notation, warn only for the "only parsing" *) + +Reserved Notation "##" (at level 0, only parsing, format "##"). + +End N. diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index 83dd2f40fb..c5b4d6f291 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -6,13 +6,13 @@ where ?B : [ |- Type] p 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b -p 0 0 (B:=bool) +p 0 0 : forall b : bool, 0 = 0 /\ b = b -p 0 0 (B:=bool) +p 0 0 : forall b : bool, 0 = 0 /\ b = b -p (A:=nat) +p : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b -p (A:=nat) +p : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b @p nat 0 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b @@ -44,16 +44,16 @@ p : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b f x true : 0 = 0 /\ true = true -f x (B:=bool) +f x : forall b : bool, 0 = 0 /\ b = b -f x (B:=bool) +f x : forall b : bool, 0 = 0 /\ b = b @f nat : forall a1 a2 : nat, T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b @f : forall (A : Type) (a1 a2 : A), @@ -62,16 +62,16 @@ f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b x.(f) true : 0 = 0 /\ true = true -x.(f) (B:=bool) +x.(f) : forall b : bool, 0 = 0 /\ b = b -x.(f) (B:=bool) +x.(f) : forall b : bool, 0 = 0 /\ b = b @f nat : forall a1 a2 : nat, T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b -f (a1:=0) (a2:=0) +f : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b @f : forall (A : Type) (a1 a2 : A), @@ -218,7 +218,7 @@ p 0 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -p 0 0 (B:=bool) +p 0 0 : forall b : bool, 0 = 0 /\ b = b p 0 0 true : 0 = 0 /\ true = true diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 505dc52ebe..113384e9cf 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -75,7 +75,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". -File "stdin", line 202, characters 2-72: +File "stdin", line 203, characters 2-72: Warning: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index c306b15ef3..22aff36d67 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -123,6 +123,7 @@ Module Test6. Export Scopes. Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). End Notations. + Set Printing Coercions. Check let v := 0%wnat in v : wnat. Check wrap O. Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index aa439fae12..b26e725d9b 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -172,3 +172,16 @@ Notation "#" := 0 (only printing). Print Visibility. End Bug10750. + +Module M18. + + Module A. + Module B. + Infix "+++" := Nat.add (at level 70). + End B. + End A. +Import A. +(* Check that the notation in module B is not visible *) +Infix "+++" := Nat.add (at level 80). + +End M18. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 8ba17e38c8..9698737d33 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -465,7 +465,7 @@ Module EqNotations. | eq_refl => H' end) (at level 10, H' at level 10, - format "'[' 'rew' 'dependent' H in '/' H' ']'"). + format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). Notation "'rew' 'dependent' -> H 'in' H'" := (match H with | eq_refl => H' @@ -476,7 +476,7 @@ Module EqNotations. | eq_refl => H' end) (at level 10, H' at level 10, - format "'[' 'rew' 'dependent' <- H in '/' H' ']'"). + format "'[' 'rew' 'dependent' <- '/ ' H in '/' H' ']'"). Notation "'rew' 'dependent' [ 'fun' y p => P ] H 'in' H'" := (match H as p in (_ = y) return P with | eq_refl => H' diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index c00f8edcf7..d3e5ddcc8a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -255,12 +255,6 @@ Qed. (** Equality of sigma types *) Import EqNotations. -Local Notation "'rew' 'dependent' H 'in' H'" - := (match H with - | eq_refl => H' - end) - (at level 10, H' at level 10, - format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). (** Equality for [sigT] *) Section sigT. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index 475859fcc2..e2ab812cce 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -437,7 +437,7 @@ Reserved Notation "{ 'on' cd , 'bijective' f }" (at level 0, f at level 8, is | or => . It is important that in other notations a leading square bracket #[# is always followed by an operator symbol or a fixed identifier. **) -Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing). +Reserved Notation "[ /\ P1 & P2 ]" (at level 0). Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format "'[hv' [ /\ '[' P1 , '/' P2 ']' '/ ' & P3 ] ']'"). Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format @@ -445,21 +445,21 @@ Reserved Notation "[ /\ P1 , P2 , P3 & P4 ]" (at level 0, format Reserved Notation "[ /\ P1 , P2 , P3 , P4 & P5 ]" (at level 0, format "'[hv' [ /\ '[' P1 , '/' P2 , '/' P3 , '/' P4 ']' '/ ' & P5 ] ']'"). -Reserved Notation "[ \/ P1 | P2 ]" (at level 0, only parsing). +Reserved Notation "[ \/ P1 | P2 ]" (at level 0). Reserved Notation "[ \/ P1 , P2 | P3 ]" (at level 0, format "'[hv' [ \/ '[' P1 , '/' P2 ']' '/ ' | P3 ] ']'"). Reserved Notation "[ \/ P1 , P2 , P3 | P4 ]" (at level 0, format "'[hv' [ \/ '[' P1 , '/' P2 , '/' P3 ']' '/ ' | P4 ] ']'"). -Reserved Notation "[ && b1 & c ]" (at level 0, only parsing). +Reserved Notation "[ && b1 & c ]" (at level 0). Reserved Notation "[ && b1 , b2 , .. , bn & c ]" (at level 0, format "'[hv' [ && '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' & c ] ']'"). -Reserved Notation "[ || b1 | c ]" (at level 0, only parsing). +Reserved Notation "[ || b1 | c ]" (at level 0). Reserved Notation "[ || b1 , b2 , .. , bn | c ]" (at level 0, format "'[hv' [ || '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/ ' | c ] ']'"). -Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing). +Reserved Notation "[ ==> b1 => c ]" (at level 0). Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'"). diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index bc4a57dedd..701ebcad56 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -97,11 +97,11 @@ Local Notation CoqCast x T := (x : T) (only parsing). (** Reserve notation that introduced in this file. **) Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200, - c, vT, vF at level 200, only parsing). + c, vT, vF at level 200). Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200, - c, R, vT, vF at level 200, only parsing). + c, R, vT, vF at level 200). Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200, - c, R, vT, vF at level 200, x ident, only parsing). + c, R, vT, vF at level 200, x ident). Reserved Notation "x : T" (at level 100, right associativity, format "'[hv' x '/ ' : T ']'"). diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 49fb88cd8c..1d682218b6 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -125,6 +125,10 @@ CAMLPKGS ?= TIMING?= # Option for changing sorting of timing output file TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -335,6 +339,19 @@ all.timing.diff: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all .PHONY: all.timing.diff +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: @@ -342,9 +359,9 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' @@ -356,7 +373,7 @@ print-pretty-single-time-diff:: $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -695,7 +712,7 @@ $(VFILES:.v=.vok): %.vok: %.v $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" $(BEAUTYFILES): %.v.beautified: %.v diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 3d07661d56..210901f8a7 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -4,6 +4,7 @@ from __future__ import unicode_literals from __future__ import print_function import sys import re +import argparse from io import open # This script parses the output of `make TIMED=1` into a dictionary @@ -14,18 +15,76 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\u221e' -def parse_args(argv, USAGE, HELP_STRING): - sort_by = 'auto' - if any(arg.startswith('--sort-by=') for arg in argv[1:]): - sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):] - args = [arg for arg in argv if not arg.startswith('--sort-by=')] - if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'): - print(USAGE) - if '--help' in args[1:] or '-h' in args[1:]: - print(HELP_STRING) - if len(args) == 2: sys.exit(0) - sys.exit(1) - return sort_by, args +def nonnegative(arg): + v = int(arg) + if v < 0: raise argparse.ArgumentTypeError("%s is an invalid non-negative int value" % arg) + return v + +def add_sort_by(parser): + return parser.add_argument( + '--sort-by', type=str, dest='sort_by', choices=('auto', 'absolute', 'diff'), + default='auto', + help=('How to sort the table entries.\n' + + 'The "auto" method sorts by absolute time differences ' + + 'rounded towards zero to a whole-number of seconds, then ' + + 'by times in the "after" column, and finally ' + + 'lexicographically by file name. This will put the ' + + 'biggest changes in either direction first, and will ' + + 'prefer sorting by build-time over subsecond changes in ' + + 'build time (which are frequently noise); lexicographic ' + + 'sorting forces an order on files which take effectively ' + + 'no time to compile.\n' + + 'The "absolute" method sorts by the total time taken.\n' + + 'The "diff" method sorts by the signed difference in time.')) + +def add_fuzz(parser): + return parser.add_argument( + '--fuzz', dest='fuzz', metavar='N', type=nonnegative, default=0, + help=('By default, two lines are only considered the same if ' + + 'the character offsets and initial code strings match. ' + 'This option relaxes this constraint by allowing the ' + + 'character offsets to differ by up to N characters, as long ' + + 'as the total number of characters and initial code strings ' + + 'continue to match. This is useful when there are small changes ' + + 'to a file, and you want to match later lines that have not ' + + 'changed even though the character offsets have changed.')) + +def add_real(parser, single_timing=False): + return parser.add_argument( + '--real', action='store_true', + help=(r'''Use real times rather than user times. + +''' + ('''By default, the input is expected to contain lines in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...) +If --real is passed, then the lines are instead expected in the format: +FILE_NAME (...real: NUMBER_IN_SECONDS...)''' if not single_timing else +'''The input is expected to contain lines in the format: +Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) + +def add_user(parser, single_timing=False): + return parser.add_argument( + '--user', dest='real', action='store_false', + help=(r'''Use user times rather than real times. + +''' + ('''By default, the input is expected to contain lines in the format: +FILE_NAME (...real: NUMBER_IN_SECONDS...) +If --user is passed, then the lines are instead expected in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...)''' if not single_timing else +'''The input is expected to contain lines in the format: +Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) + +# N.B. We need to include default=None for nargs='*', c.f., https://bugs.python.org/issue28609#msg280180 +def add_file_name_gen(parser, prefix='', descr='file containing the build log', stddir='in', defaults=None, **kwargs): + extra = ('' if defaults is None else ' (defaults to %s if no argument is passed)' % defaults) + return parser.add_argument( + prefix + 'FILE_NAME', type=str, + help=('The name of the %s (use "-" for std%s)%s.' % (descr, stddir, extra)), + **kwargs) + +def add_file_name(parser): return add_file_name_gen(parser) +def add_after_file_name(parser): return add_file_name_gen(parser, 'AFTER_', 'file containing the "after" build log') +def add_before_file_name(parser): return add_file_name_gen(parser, 'BEFORE_', 'file containing the "before" build log') +def add_output_file_name(parser): return add_file_name_gen(parser, 'OUTPUT_', 'file to write the output table to', stddir='out', defaults='-', nargs='*', default=None) def reformat_time_string(time): @@ -45,14 +104,16 @@ def get_file_lines(file_name): lines = f.readlines() for line in lines: try: - yield line.decode('utf-8') + # Since we read the files in binary mode, we have to + # normalize Windows line endings from \r\n to \n + yield line.decode('utf-8').replace('\r\n', '\n') except UnicodeDecodeError: # invalid utf-8 pass def get_file(file_name): return ''.join(get_file_lines(file_name)) -def get_times(file_name): +def get_times(file_name, use_real=False): ''' Reads the contents of file_name, which should be the output of 'make TIMED=1', and parses it to construct a dict mapping file @@ -60,28 +121,96 @@ def get_times(file_name): using STRIP_REG and STRIP_REP. ''' lines = get_file(file_name) - reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg_user = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg_real = re.compile(r'^([^\s]+) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg = reg_real if use_real else reg_user times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): - reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg = reg_real times = reg.findall(lines) if all(STRIP_REG.search(name.strip()) for name, time in times): times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times) return dict((name, reformat_time_string(time)) for name, time in times) -def get_single_file_times(file_name): +def get_single_file_times(file_name, use_real=False): ''' Reads the contents of file_name, which should be the output of 'coqc -time', and parses it to construct a dict mapping lines to to compile durations, as strings. ''' lines = get_file(file_name) - reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) + reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs \(([0-9\.]+)u(.*)\)$', re.MULTILINE) times = reg.findall(lines) if len(times) == 0: return dict() - longest = max(max((len(start), len(stop))) for start, stop, name, time, extra in times) + longest = max(max((len(start), len(stop))) for start, stop, name, real, user, extra in times) FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) - return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times) + return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(real if use_real else user)) for start, stop, name, real, user, extra in times) + +def fuzz_merge(l1, l2, fuzz): + '''Takes two iterables of ((start, end, code), times) and a fuzz + parameter, and yields a single iterable of ((start, stop, code), + times1, times2) + + We only give both left and right if (a) the codes are the same, + (b) the number of characters (stop - start) is the same, and (c) + the difference between left and right code locations is <= fuzz. + + We keep a current guess at the overall offset, and prefer drawing + from whichever list is earliest after correcting for current + offset. + + ''' + assert(fuzz >= 0) + cur_fuzz = 0 + l1 = list(l1) + l2 = list(l2) + cur1, cur2 = None, None + while (len(l1) > 0 or cur1 is not None) and (len(l2) > 0 or cur2 is not None): + if cur1 is None: cur1 = l1.pop(0) + if cur2 is None: cur2 = l2.pop(0) + ((s1, e1, c1), t1), ((s2, e2, c2), t2) = cur1, cur2 + assert(t1 is not None) + assert(t2 is not None) + s2_adjusted, e2_adjusted = s2 + cur_fuzz, e2 + cur_fuzz + if cur1[0] == cur2[0]: + yield (cur1, cur2) + cur1, cur2 = None, None + cur_fuzz = 0 + elif c1 == c2 and e1-s1 == e2-s2 and abs(s1 - s2) <= fuzz: + yield (((s1, e1, c1), t1), ((s2, e2, c2), t2)) + cur1, cur2 = None, None + cur_fuzz = s1 - s2 + elif s1 < s2_adjusted or (s1 == s2_adjusted and e1 <= e2): + yield (((s1, e1, c1), t1), ((s1 - cur_fuzz, e1 - cur_fuzz, c1), None)) + cur1 = None + else: + yield (((s2 + cur_fuzz, e2 + cur_fuzz, c2), None), ((s2, e2, c2), t2)) + cur2 = None + if len(l1) > 0: + for i in l1: yield (i, (i[0], None)) + elif len(l2) > 0: + for i in l2: yield ((i[0], None), i) + +def adjust_fuzz(left_dict, right_dict, fuzz): + reg = re.compile(r'Chars ([0-9]+) - ([0-9]+) (.*)$') + left_dict_list = sorted(((int(s), int(e), c), v) for ((s, e, c), v) in ((reg.match(k).groups(), v) for k, v in left_dict.items())) + right_dict_list = sorted(((int(s), int(e), c), v) for ((s, e, c), v) in ((reg.match(k).groups(), v) for k, v in right_dict.items())) + merged = list(fuzz_merge(left_dict_list, right_dict_list, fuzz)) + if len(merged) == 0: + # assert that both left and right dicts are empty + assert(not left_dict) + assert(not right_dict) + return left_dict, right_dict + longest = max(max((len(str(start1)), len(str(stop1)), len(str(start2)), len(str(stop2)))) for ((start1, stop1, code1), t1), ((start2, stop2, code2), t2) in merged) + FORMAT1 = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) + FORMAT2 = 'Chars %%0%dd-%%0%dd ~ %%0%dd-%%0%dd %%s' % (longest, longest, longest, longest) + if fuzz == 0: + left_dict = dict((FORMAT1 % k, t1) for (k, t1), _ in merged if t1 is not None) + right_dict = dict((FORMAT1 % k, t2) for _, (k, t2) in merged if t2 is not None) + else: + left_dict = dict((FORMAT2 % (s1, e1, s2, e2, c1), t1) for ((s1, e1, c1), t1), ((s2, e2, c2), t2) in merged if t1 is not None) + right_dict = dict((FORMAT2 % (s1, e1, s2, e2, c1), t2) for ((s1, e1, c1), t1), ((s2, e2, c2), t2) in merged if t2 is not None) + return left_dict, right_dict def fix_sign_for_sorting(num, descending=True): return -num if descending else num diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index fddf75f39f..a28da43043 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,12 +1,17 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' - sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) - left_dict = get_single_file_times(args[1]) - right_dict = get_single_file_times(args[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) - print_or_write_table(table, args[3:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''') + add_sort_by(parser) + add_user(parser, single_timing=True) + add_fuzz(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_single_file_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_single_file_times(args.BEFORE_FILE_NAME, use_real=args.real) + left_dict, right_dict = adjust_fuzz(left_dict, right_dict, fuzz=args.fuzz) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 8937d63c2f..5d88548bba 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,16 +1,15 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table. - -The input is expected to contain lines in the format: -FILE_NAME (...user: NUMBER_IN_SECONDS...) -''' - sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) - left_dict = get_times(args[1]) - right_dict = get_times(args[2]) - table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by) - print_or_write_table(table, args[3:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table.''') + add_sort_by(parser) + add_real(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_times(args.BEFORE_FILE_NAME, use_real=args.real) + table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index ad0a04ab07..3df7d7e584 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -3,19 +3,11 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output of `make TIMED=1` into a sorted table. - -The input is expected to contain lines in the format: -FILE_NAME (...user: NUMBER_IN_SECONDS...) -''' - if len(sys.argv) < 2 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - times_dict = get_times(sys.argv[1]) - table = make_table_string(times_dict) - print_or_write_table(table, sys.argv[2:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of `make TIMED=1` into a sorted table.''') + add_real(parser) + add_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + times_dict = get_times(args.FILE_NAME, use_real=args.real) + table = make_table_string(times_dict) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 506a8dc5b0..2b79bff1b2 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -64,6 +64,7 @@ type coqargs_config = { } type coqargs_pre = { + boot : bool; load_init : bool; load_rcfile : bool; @@ -131,6 +132,7 @@ let default_config = { } let default_pre = { + boot = false; load_init = true; load_rcfile = true; ml_includes = []; @@ -512,6 +514,7 @@ let parse_args ~help ~init arglist : t * string list = |"-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 }} + |"-boot" -> { oval with pre = { oval.pre with boot = true }} |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} @@ -569,5 +572,5 @@ let cmdline_load_path opts = opts.pre.ml_includes @ opts.pre.vo_includes let build_load_path opts = - Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @ + (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @ cmdline_load_path opts diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 26f22386a0..f38381a086 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -40,6 +40,7 @@ type coqargs_config = { } type coqargs_pre = { + boot : bool; load_init : bool; load_rcfile : bool; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3aa9acfc52..7f3d4b570f 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -52,10 +52,10 @@ let load_rcfile ~rcfile ~state = iraise reraise (* Recursively puts `.v` files in the LoadPath if -nois was not passed *) -let build_stdlib_vo_path ~load_init ~unix_path ~coq_path = +let build_stdlib_vo_path ~unix_path ~coq_path = let open Loadpath in { recursive = true; - path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = load_init } + path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true } } let build_stdlib_ml_path ~dir = @@ -88,7 +88,7 @@ let toplevel_init_load_path () = ml_path_if Coq_config.local [coqlib/"dev"] (* LoadPath for Coq user libraries *) -let libs_init_load_path ~load_init = +let libs_init_load_path () = let open Loadpath in let coqlib = Envars.coqlib () in @@ -107,7 +107,7 @@ let libs_init_load_path ~load_init = (* then standard library *) [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @ - [build_stdlib_vo_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path] @ + [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) (if Sys.file_exists user_contrib then diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index fc53c8b47c..f3a007d987 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -20,4 +20,4 @@ val init_ocaml_path : unit -> unit val toplevel_init_load_path : unit -> Loadpath.coq_path list (* LoadPath for Coq user libraries *) -val libs_init_load_path : load_init:bool -> Loadpath.coq_path list +val libs_init_load_path : unit -> Loadpath.coq_path list diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6848862603..ba3deeb2f6 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -32,7 +32,8 @@ let print_usage_common co command = \n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ -\n -noinit start without loading the Init library\ +\n -boot don't bind the `Coq.` prefix to the default -coqlib dir\ +\n -noinit don't load Coq.Init.Prelude on start \ \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ \n\ diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5e98f5ddc0..72e6d41969 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -249,7 +249,6 @@ type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry -| TTString : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry @@ -370,14 +369,12 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) | TTBigint -> MayRecNo (Aentry Prim.bigint) -| TTString -> MayRecNo (Aentry Prim.string) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint -| ETProdString -> TTAny TTString | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) @@ -417,11 +414,6 @@ match e with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) end -| TTString -> - begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v)) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v)) - end | TTReference -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) @@ -537,10 +529,10 @@ let rec pure_sublevels' assoc from forpat level = function let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in - CAst.make ~loc @@ CNotation (notation, env) + CAst.make ~loc @@ CNotation (None, notation, env) | ForPattern -> fun notation loc env -> let env = (env.constrs, env.constrlists) in - CAst.make ~loc @@ CPatNotation (notation, env, []) + CAst.make ~loc @@ CPatNotation (None, notation, env, []) let extend_constr state forpat ng = let custom,n,_,_ = ng.notgram_level in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 882be6449d..d597707d12 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1235,7 +1235,6 @@ GRAMMAR EXTEND Gram syntax_extension_type: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } - | IDENT "string" -> { ETString } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index dfc4631572..f6f6c4f1eb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -324,11 +324,8 @@ let explain_unification_error env sigma p1 p2 = function strbrk ": cannot ensure that " ++ t ++ strbrk " is a subtype of " ++ u] | UnifUnivInconsistency p -> - if !Constrextern.print_universes then - [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] - else - [str "universe inconsistency"] + [str "universe inconsistency: " ++ + Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] | CannotSolveConstraint ((pb,env,t,u),e) -> let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ @@ -1375,13 +1372,8 @@ let _ = CErrors.register_handler explain_exn_default let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> - let msg = - if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i - else - mt() in - str "Universe inconsistency" ++ msg ++ str "." + str "Universe inconsistency." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d39ee60c25..afff0347f5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -286,32 +286,30 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = let open Gramlib.Gramext in function - | RightA -> (L,E) - | LeftA -> (E,L) - | NonA -> (L,L) - let precedence_of_position_and_level from_level = function - | NumLevel n, BorderProd (_,None) -> n, Prec n | NumLevel n, BorderProd (b,Some a) -> - n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp - | NumLevel n, InternalProd -> n, Prec n - | NextLevel, _ -> from_level, L - | DefaultLevel, _ -> - (* Fake value, waiting for PR#5 at herbelin's fork *) 200, - Any + (let open Gramlib.Gramext in + match a, b with + | RightA, Left -> LevelLt n + | RightA, Right -> LevelLe n + | LeftA, Left -> LevelLe n + | LeftA, Right -> LevelLt n + | NonA, _ -> LevelLt n) + | NumLevel n, _ -> LevelLe n + | NextLevel, _ -> LevelLt from_level + | DefaultLevel, _ -> LevelSome (** Computing precedences of subentries for parsing *) let precedence_of_entry_type (from_custom,from_level) = function | ETConstr (custom,_,x) when notation_entry_eq custom from_custom -> precedence_of_position_and_level from_level x - | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n + | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n | ETConstr (custom,_,(NextLevel,_)) -> user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++ quote (pr_notation_entry custom) ++ strbrk " is different from " ++ quote (pr_notation_entry from_custom) ++ str ").") - | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n - | _ -> 0, E (* should not matter *) + | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n + | _ -> LevelSome (* should not matter *) (** Computing precedences for future insertion of parentheses at the time of printing using hard-wired constr levels *) @@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function (* Possible insertion of parentheses at printing time to deal with precedence in a constr entry is managed using [prec_less] in [ppconstr.ml] *) - snd (precedence_of_position_and_level from_level x) + precedence_of_position_and_level from_level x | ETConstr (custom,_,_) -> (* Precedence of printing for a custom entry is managed using explicit insertion of entry coercions at the time of building a [constr_expr] *) - Any - | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0) - | _ -> Any (* should not matter *) + LevelSome + | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0) + | _ -> LevelSome (* should not matter *) (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) @@ -396,12 +394,12 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint | ETString -> - UnpMetaVar (i,prec) + | ETConstr _ | ETGlobal | ETBigint -> + UnpMetaVar prec | ETPattern _ -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETIdent -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETBinder isopen -> assert false @@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level = (* We add NonTerminal for simulation but remove it afterwards *) else make true sl in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl') + | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl') | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,List.map snd sl') + UnpBinderListMetaVar (isopen,List.map snd sl') | _ -> assert false in (None, hunk) :: make_with_space b prods @@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt = if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); let symbs, l = aux (symbs,rfmt) in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) + | ETConstr _ -> UnpListMetaVar (prec,slfmt) | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,slfmt) + UnpBinderListMetaVar (isopen,slfmt) | _ -> assert false in symbs, hunk :: l | symbs, (_,UnpBox (a,b)) :: fmt -> @@ -686,7 +684,6 @@ let prod_entry_type = function | ETIdent -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint - | ETString -> ETProdString | ETBinder _ -> assert false (* See check_binder_type *) | ETConstr (s,_,p) -> ETProdConstr (s,p) | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) @@ -746,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in let pr_arg_level from (lev,typ) = let pplev = function - | (n,L) when Int.equal n from -> str "at next level" - | (n,E) -> str "at level " ++ int n - | (n,L) -> str "at level below " ++ int n - | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" in - Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ - (match typ with - | ETConstr _ | ETPattern _ -> spc () ++ pplev lev - | _ -> mt ()) + | LevelLt n when Int.equal n from -> spc () ++ str "at next level" + | LevelLe n -> spc () ++ str "at level " ++ int n + | LevelLt n -> spc () ++ str "at level below " ++ int n + | LevelSome -> mt () in + Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev let pr_level ntn (from,fromlevel,args,typs) = (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++ @@ -776,43 +769,97 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec = spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") -type syntax_extension = { +let warn_incompatible_format = + CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing" + (fun (specific,ntn) -> + let head,scope = match specific with + | None -> str "Notation", mt () + | Some LastLonelyNotation -> str "Lonely notation", mt () + | Some (NotationInScope sc) -> str "Notation", strbrk (" in scope " ^ sc) in + head ++ spc () ++ pr_notation ntn ++ + strbrk " was already defined with a different format" ++ scope ++ str ".") + +type syntax_parsing_extension = { synext_level : Notation_gram.level; synext_notation : notation; - synext_notgram : notation_grammar; - synext_unparsing : unparsing list; + synext_notgram : notation_grammar option; +} + +type syntax_printing_extension = { + synext_reserved : bool; + synext_unparsing : unparsing_rule; synext_extra : (string * string) list; } -type syntax_extension_obj = locality_flag * syntax_extension +let generic_format_to_declare ntn {synext_unparsing = (rules,_); synext_extra = extra_rules } = + try + let (generic_rules,_),reserved,generic_extra_rules = + Ppextend.find_generic_notation_printing_rule ntn in + if reserved && + (not (List.for_all2eq unparsing_eq rules generic_rules) + || extra_rules <> generic_extra_rules) + then + (warn_incompatible_format (None,ntn); true) + else + false + with Not_found -> true + +let check_reserved_format ntn = function + | None -> () + | Some sy_pp_rules -> let _ = generic_format_to_declare ntn sy_pp_rules in () + +let specific_format_to_declare (specific,ntn as specific_ntn) + {synext_unparsing = (rules,_); synext_extra = extra_rules } = + try + let (specific_rules,_),specific_extra_rules = + Ppextend.find_specific_notation_printing_rule specific_ntn in + if not (List.for_all2eq unparsing_eq rules specific_rules) + || extra_rules <> specific_extra_rules then + (warn_incompatible_format (Some specific,ntn); true) + else false + with Not_found -> true + +type syntax_extension_obj = + locality_flag * (syntax_parsing_extension * syntax_printing_extension option) let check_and_extend_constr_grammar ntn rule = try let ntn_for_grammar = rule.notgram_notation in if notation_eq ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in - let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in - if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in + if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + if oldparsing = None then raise Not_found with Not_found -> Egramcoq.extend_constr_grammar rule -let cache_one_syntax_extension se = - let ntn = se.synext_notation in - let prec = se.synext_level in - let onlyprint = se.synext_notgram.notgram_onlyprinting in - try - let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in - if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; - with Not_found -> - begin - (* Reserve the notation level *) - Notgram_ops.declare_notation_level ntn prec ~onlyprint; - (* Declare the parsing rule *) - if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; - (* Declare the notation rule *) - declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram - end +let cache_one_syntax_extension (pa_se,pp_se) = + let ntn = pa_se.synext_notation in + let prec = pa_se.synext_level in + (* Check and ensure that the level and the precomputed parsing rule is declared *) + let oldparsing = + try + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in + if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec; + oldparsing + with Not_found -> + (* Declare the level and the precomputed parsing rule *) + let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in + None in + (* Declare the parsing rule *) + begin match oldparsing, pa_se.synext_notgram with + | None, Some grams -> List.iter (check_and_extend_constr_grammar ntn) grams + | _ -> (* The grammars rules are canonically derived from the string and the precedence*) () + end; + (* Printing *) + match pp_se with + | None -> () + | Some pp_se -> + (* Check compatibility of format in case of two Reserved Notation *) + (* and declare or redeclare printing rule *) + if generic_format_to_declare ntn pp_se then + declare_generic_notation_printing_rules ntn + ~extra:pp_se.synext_extra ~reserved:pp_se.synext_reserved pp_se.synext_unparsing let cache_syntax_extension (_, (_, sy)) = cache_one_syntax_extension sy @@ -821,11 +868,11 @@ let subst_parsing_rule subst x = x let subst_printing_rule subst x = x -let subst_syntax_extension (subst, (local, sy)) = - (local, { sy with - synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules }; - synext_unparsing = subst_printing_rule subst sy.synext_unparsing; - }) +let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) = + (local, ({ pa_sy with + synext_notgram = Option.map (List.map (subst_parsing_rule subst)) pa_sy.synext_notgram }, + Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy) + ) let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o @@ -990,7 +1037,7 @@ let set_entry_type from n etyps (x,typ) = | ETConstr (s,bko,n), InternalProd -> ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x + | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> ETConstr (from,None,(make_lev n from,typ)) in (x,typ) @@ -1012,7 +1059,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETBigint | ETString | ETGlobal + | ETConstr _ | ETBigint | ETGlobal | ETIdent | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = @@ -1034,7 +1081,7 @@ let make_interpretation_type isrec isonlybinding = function (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) - | ETBigint | ETString | ETGlobal -> NtnTypeConstr + | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.") @@ -1098,8 +1145,6 @@ type entry_coercion_kind = | IsEntryCoercion of notation_entry_level | IsEntryGlobal of string * int | IsEntryIdent of string * int - | IsEntryNumeral of string * int - | IsEntryString of string * int let is_coercion = function | Some (custom,n,_,[e]) -> @@ -1111,8 +1156,6 @@ let is_coercion = function else Some (IsEntryCoercion subentry) | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) - | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n)) - | ETString, InCustomEntry s -> Some (IsEntryString (s,n)) | _ -> None) | Some _ -> assert false | None -> None @@ -1154,10 +1197,10 @@ let find_precedence custom lev etyps symbols onlyprint = user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () - | (ETIdent | ETBigint | ETString | ETGlobal), _ -> + | (ETIdent | ETBigint | ETGlobal), _ -> begin match lev with | None -> - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0) | Some 0 -> ([],0) | _ -> @@ -1174,7 +1217,7 @@ let find_precedence custom lev etyps symbols onlyprint = else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")], 0) else [],Option.get lev | Some _ -> if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); @@ -1227,7 +1270,7 @@ module SynData = struct extra : (string * string) list; (* XXX: Callback to printing, must remove *) - msgs : ((Pp.t -> unit) * Pp.t) list; + msgs : (unit -> unit) list; (* Fields for internalization *) recvars : (Id.t * Id.t) list; @@ -1325,15 +1368,19 @@ let compute_syntax_data ~local deprecation df modifiers = not_data = sy_fulldata; } +let warn_only_parsing_reserved_notation = + CWarnings.create ~name:"irrelevant-reserved-notation-only-parsing" ~category:"parsing" + (fun () -> strbrk "The only parsing modifier has no effect in Reserved Notation.") + let compute_pure_syntax_data ~local df mods = let open SynData in let sd = compute_syntax_data ~local None df mods in - let msgs = - if sd.only_parsing then - (Feedback.msg_warning ?loc:None, - strbrk "The only parsing modifier has no effect in Reserved Notation.")::sd.msgs - else sd.msgs in - { sd with msgs } + if sd.only_parsing + then + let msgs = (fun () -> warn_only_parsing_reserved_notation ?loc:None ())::sd.msgs in + { sd with msgs; only_parsing = false } + else + sd (**********************************************************************) (* Registration of notations interpretation *) @@ -1347,6 +1394,7 @@ type notation_obj = { notobj_onlyprint : bool; notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; + notobj_specific_pp_rules : syntax_printing_extension option; } let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = @@ -1363,26 +1411,35 @@ let load_notation = load_notation_common true let open_notation i (_, nobj) = - let scope = nobj.notobj_scope in - let (ntn, df) = nobj.notobj_notation in - let pat = nobj.notobj_interp in - let onlyprint = nobj.notobj_onlyprint in - let deprecation = nobj.notobj_deprecation in - let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - if Int.equal i 1 && fresh then begin - (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in - (* Declare the uninterpretation *) - if not nobj.notobj_onlyparse then - Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat; - (* Declare a possible coercion *) - (match nobj.notobj_coercion with - | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry - | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n - | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n - | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n - | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n - | None -> ()) + if Int.equal i 1 then begin + let scope = nobj.notobj_scope in + let (ntn, df) = nobj.notobj_notation in + let pat = nobj.notobj_interp in + let onlyprint = nobj.notobj_onlyprint in + let deprecation = nobj.notobj_deprecation in + let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + let specific_ntn = (specific,ntn) in + let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in + if fresh then begin + (* Declare the interpretation *) + let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in + (* Declare the uninterpretation *) + if not nobj.notobj_onlyparse then + Notation.declare_uninterpretation (NotationRule specific_ntn) pat; + (* Declare a possible coercion *) + (match nobj.notobj_coercion with + | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry + | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n + | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n + | None -> ()) + end; + (* Declare specific format if any *) + match nobj.notobj_specific_pp_rules with + | Some pp_sy -> + if specific_format_to_declare specific_ntn pp_sy then + Ppextend.declare_specific_notation_printing_rules + specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing + | None -> () end let cache_notation o = @@ -1424,23 +1481,30 @@ let with_syntax_protection f x = exception NoSyntaxRule let recover_notation_syntax ntn = - try - let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in - let pp_rule,_ = find_notation_printing_rule ntn in - let pp_extra_rules = find_notation_extra_printing_rules ntn in - let pa_rule = find_notation_parsing_rules ntn in - { synext_level = prec; - synext_notation = ntn; - synext_notgram = pa_rule; - synext_unparsing = pp_rule; - synext_extra = pp_extra_rules; - } - with Not_found -> - raise NoSyntaxRule + let pa = + try + let pa_rule,prec = Notgram_ops.level_of_notation ntn in + { synext_level = prec; + synext_notation = ntn; + synext_notgram = pa_rule } + with Not_found -> + raise NoSyntaxRule in + let pp = + try + let pp_rule,reserved,pp_extra_rules = find_generic_notation_printing_rule ntn in + Some { + synext_reserved = reserved; + synext_unparsing = pp_rule; + synext_extra = pp_extra_rules; + } + with Not_found -> None in + pa,pp let recover_squash_syntax sy = - let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in - sy :: sq.synext_notgram.notgram_rules + let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in + match sq.synext_notgram with + | Some gram -> sy :: gram + | None -> raise NoSyntaxRule (**********************************************************************) (* Main entry point for building parsing and printing rules *) @@ -1471,16 +1535,28 @@ let make_pp_rule level (typs,symbols) fmt = | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) -(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) -let make_syntax_rules (sd : SynData.syn_data) = let open SynData in +let make_parsing_rules (sd : SynData.syn_data) = let open SynData in let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in - let custom,level,_,_ = sd.level in - let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in - let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in { + let pa_rule = + if sd.only_printing then None + else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash) + in { synext_level = sd.level; synext_notation = fst sd.info; - synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; - synext_unparsing = pp_rule; + synext_notgram = pa_rule; + } + +let warn_irrelevant_format = + CWarnings.create ~name:"irrelevant-format-only-parsing" ~category:"parsing" + (fun () -> str "The format modifier is irrelevant for only parsing rules.") + +let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in + let custom,level,_,_ = sd.level in + let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in + if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None) + else Some { + synext_reserved = reserved; + synext_unparsing = (pp_rule,level); synext_extra = sd.extra; } @@ -1494,9 +1570,10 @@ let to_map l = let add_notation_in_scope ~local deprecation df env c mods scope = let open SynData in let sd = compute_syntax_data ~local deprecation df mods in - (* Prepare the interpretation *) (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sd in + let sy_pa_rules = make_parsing_rules sd in + let sy_pp_rules = make_printing_rules false sd in + (* Prepare the interpretation *) let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1516,24 +1593,29 @@ let add_notation_in_scope ~local deprecation df env c mods scope = notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; notobj_notation = sd.info; + notobj_specific_pp_rules = sy_pp_rules; } in + let gen_sy_pp_rules = + if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None + else sy_pp_rules (* We use the format of this notation as the default *) in + let _ = check_reserved_format (fst sd.info) sy_pp_rules in (* Ready to change the global state *) - Flags.if_verbose (List.iter (fun (f,x) -> f x)) sd.msgs; - Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); + List.iter (fun f -> f ()) sd.msgs; + Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules))); Lib.add_anonymous_leaf (inNotation notation); sd.info let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) - let level, i_typs, onlyprint = if not (is_numeral symbs) then begin - let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in + let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin + let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in (* If the only printing flag has been explicitly requested, put it back *) - let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in - let _,_,_,typs = sy.synext_level in - Some sy.synext_level, typs, onlyprint - end else None, [], false in + let onlyprint = onlyprint || pa_sy.synext_notgram = None in + let _,_,_,typs = pa_sy.synext_level in + Some pa_sy.synext_level, typs, onlyprint, pp_sy + end else None, [], false, None in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in @@ -1556,6 +1638,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization notobj_onlyprint = onlyprint; notobj_deprecation = deprecation; notobj_notation = df'; + notobj_specific_pp_rules = pp_sy; } in Lib.add_anonymous_leaf (inNotation notation); df' @@ -1563,10 +1646,11 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization (* Notations without interpretation (Reserved Notation) *) let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in - let psd = compute_pure_syntax_data ~local df mods in - let sy_rules = make_syntax_rules {psd with deprecation = None} in - Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; - Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) + let psd = {(compute_pure_syntax_data ~local df mods) with deprecation = None} in + let pa_rules = make_parsing_rules psd in + let pp_rules = make_printing_rules true psd in + List.iter (fun f -> f ()) psd.msgs; + Lib.add_anonymous_leaf (inSyntaxExtension(local,(pa_rules,pp_rules))) (* Notations with only interpretation *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index c6ba4e2c29..314c423f65 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -126,7 +126,6 @@ open Pputils | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko | ETBigint -> str "bigint" - | ETString -> str "string" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 32c438c724..cdd93db884 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -547,7 +547,7 @@ let print_located_qualid ref = print_located_qualid "object" LocAny ref (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_leconstr_env env sigma trm ++ fnl () ++ + (pr_leconstr_env ~inctx:true env sigma trm ++ fnl () ++ str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the @@ -556,7 +556,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = synthesizes the type nat of the abstraction on u *) let print_named_def env sigma name body typ = - let pbody = pr_lconstr_env env sigma body in + let pbody = pr_lconstr_env ~inctx:true env sigma body in let ptyp = pr_ltype_env env sigma typ in let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ @@ -598,7 +598,7 @@ let gallina_print_section_variable env sigma id = with_line_skip (print_name_infos (GlobRef.VarRef id)) let print_body env evd = function - | Some c -> pr_lconstr_env env evd c + | Some c -> pr_lconstr_env ~inctx:true env evd c | None -> (str"<no body>") let print_typed_body env evd (val_0,typ) = |