diff options
123 files changed, 2182 insertions, 1023 deletions
diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md index aec6cd0a21..c564105c9c 100644 --- a/.github/ISSUE_TEMPLATE.md +++ b/.github/ISSUE_TEMPLATE.md @@ -3,7 +3,9 @@ #### Description of the problem <!-- If you can, it's helpful to provide self-contained example of some code -that reproduces the bug. If not, a link to a larger example is also helpful. --> +that reproduces the bug. If not, a link to a larger example is also helpful. +You can generate a shorter version of your program by following these +instructions: https://github.com/coq/coq/wiki/Coqbot-minimize-feature. --> #### Coq Version diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3b95800f0d..32b05ec746 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-05-24-V1" + CACHEKEY: "bionic_coq-V2020-07-21-V38" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -481,6 +481,8 @@ doc:refman-pdf:dune: - _build/log - _build/default/doc/refman-pdf +# currently bugged: dune cleans up the glob files so no links +# see #12699 doc:stdlib:dune: extends: .dune-ci-template variables: @@ -501,11 +503,11 @@ doc:refman:deploy: dependencies: - doc:ml-api:odoc - doc:refman:dune - - doc:stdlib:dune + - build:base needs: - doc:ml-api:odoc - doc:refman:dune - - doc:stdlib:dune + - build:base script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy @@ -515,7 +517,7 @@ doc:refman:deploy: - mkdir -p _deploy/$CI_COMMIT_REF_NAME - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api - cp -rv _build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman - - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib + - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib - cd _deploy/$CI_COMMIT_REF_NAME/ - git add api refman stdlib - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA" @@ -724,6 +726,9 @@ library:ci-coqprime: - build:edge+flambda - plugin:ci-bignums +library:ci-coqtail: + extends: .ci-template + library:ci-coquelicot: extends: .ci-template diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8a09e43c94..d561ec8a12 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -184,7 +184,7 @@ stream][Zulip-dev] of our Zulip chat. Finally, we strongly encourage authors of plugins to submit their plugins to join Coq's continuous integration (CI) early on. Indeed, -the Coq API gets continously reworked, so this is the best way of +the Coq API gets continuously reworked, so this is the best way of ensuring your plugin stays compatible with new Coq versions, as this means Coq developers will fix your plugin for you. Learn more about this in the [CI README (user part)][CI-README-users]. diff --git a/Makefile.ci b/Makefile.ci index 77d8bda671..85e4b965f9 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -17,6 +17,7 @@ CI_TARGETS= \ ci-color \ ci-compcert \ ci-coq_dpdgraph \ + ci-coqtail \ ci-coquelicot \ ci-corn \ ci-cross_crypto \ diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 305c6a627e..b27d1df39d 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -64,7 +64,8 @@ jobs: set -e brew update (cd $(brew --repository)/Library/Taps/homebrew/homebrew-core/ && git fetch --shallow-since=${HBCORE_DATE} && git checkout ${HBCORE_REF}) - brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme + brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme || true + # || true: workaround #12657, see also #12672 and commit message for this line pip3 install macpack displayName: 'Install system dependencies' env: diff --git a/default.nix b/default.nix index 6b0e396d23..df1c43101b 100644 --- a/default.nix +++ b/default.nix @@ -43,7 +43,7 @@ stdenv.mkDerivation rec { hostname python3 time # coq-makefile timing tools ] - ++ (with ocamlPackages; [ ocaml findlib num ]) + ++ (with ocamlPackages; [ ocaml findlib ]) ++ optionals buildIde [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook @@ -69,6 +69,12 @@ stdenv.mkDerivation rec { ++ [ dune_2 ] # Maybe the next build system ); + # Since #12604, ocamlfind looks for num when building plugins + # This follows a similar change in the nixpkgs repo (cf. NixOS/nixpkgs#94230) + propagatedBuildInputs = [ + ocamlPackages.num + ]; + src = if shell then null else diff --git a/dev/README.md b/dev/README.md index 0c6b8020f1..0a6b196ec0 100644 --- a/dev/README.md +++ b/dev/README.md @@ -22,14 +22,12 @@ | [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source | | [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files | | [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling | -| [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | -| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | -| [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | +| [`dev/doc/universes.md`](doc/universes.md) | Help for debugging universes | | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | +| [`dev/doc/parsing.md`](doc/parsing.md) | Grammar and parsing overview | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | | [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate | -| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 577ce35aae..fd6ea9bb09 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -55,7 +55,7 @@ IF DEFINED HTTP_PROXY ( )
REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
+SET CYGWIN_REPOSITORY=https://mirrors.kernel.org/sourceware/cygwin
REM see -cygcache in ReadMe.txt
SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4973cbb478..2725e6b56c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -380,3 +380,10 @@ : "${sf_CI_REF:=master}" : "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}" : "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}" + +######################################################################## +# Coqtail +######################################################################## +: "${coqtail_CI_REF:=master}" +: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}" +: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}" diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh new file mode 100755 index 0000000000..b8b5c6c724 --- /dev/null +++ b/dev/ci/ci-coqtail.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqtail + +( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 1302065961..27876d68de 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download metacoq -( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8c5696f4f9..7570b17095 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-24-V1" +# CACHEKEY: "bionic_coq-V2020-07-21-V38" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -17,9 +17,10 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of source-doc and coq-makefile texlive-science tipa -# More dependencies of the sphinx doc +# More dependencies of the sphinx doc, pytest for coqtail RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ - antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \ + pytest==5.4.3 # We need to install OPAM 2.0 manually for now. RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh new file mode 100644 index 0000000000..e57f95ef19 --- /dev/null +++ b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then + + coqhammer_CI_REF=factor-class-hint-clenv + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md new file mode 100644 index 0000000000..f8b4537e77 --- /dev/null +++ b/dev/doc/parsing.md @@ -0,0 +1,397 @@ +# Parsing + +Coq's parser is based on Camlp5 using an extensible grammar. Somewhat helpful +Camlp5 documentation is available [here](http://camlp5.github.io/doc/htmlc/grammars.html). +However, the Camlp5 code has been copied into the Coq source tree and may differ +from the Camlp5 release. + +Notable attributes of the parser include: + +* The grammar is extensible at run time. This is essential for supporting notations + and optionally-loaded plugins that extend the grammar. + +* The grammar is split into multiple source files. Nonterminals can be local to a file + or global. + +* While 95% of the nonterminals and almost all the productions are defined in the grammar, + a few are defined directly in OCaml code. Since many developers have worked on the parser + over the years, this code can be idiosyncratic, reflecting various coding styles. + +* The parser is a recursive descent parser that, by default, only looks at the next token + to make a parsing decision. It's possible to hand-code additional lookahead where + necessary by writing OCaml code. + +* There's no code that checks whether a grammar is ambiguous or whether every production + can be recognized. Developers who modify the grammar may, in some cases, need to structure their + added productions in specific ways to ensure that their additions are parsable and that they + don't break existing productions. + +## Contents ## + +- [Grammars: `*.mlg` File Structure](#grammars-mlg-file-structure) +- [Grammars: Nonterminals and Productions](#grammars-nonterminals-and-productions) + - [Alternate production syntax](#alternate-production-syntax) +- [Usage notes](#usage-notes) + - [Other components](#other-components) + - [Parsing productions](#parsing-productions) + - [Lookahead](#lookahead) + +## Grammars: `*.mlg` File Structure ## + +Grammars are defined in `*.mlg` files, which `coqpp` compiles into `*.ml` files at build time. +`coqpp` code is in the `coqpp` directory. `coqpp` uses yacc and lex to parse the grammar files. +You can examine its yacc and lex input files in `coqpp_lex.mll` and `coqpp_parse.mly` for +details not fully covered here. + +In addition, there is a `doc_grammar` build utility that uses the `coqpp` parser to extract the +grammar, then edits and inserts it into the documentation. This is described in +[`doc/tools/docgram/README.md`](../../doc/tools/docgram/README.md). +`doc_grammar` generates +[`doc/tools/docgram/fullGrammar`](../../doc/tools/docgram/fullGrammar), +which has the full grammar for Coq +(not including some optionally-loaded plugins). This may be easier to read since everything is +in one file and the parser action routines and other OCaml code are omitted. + +`*.mlg` files contain the following types of nodes (See `node` in the yacc grammar). This part is +very specific to Coq (not so similar to Camlp5): + +* OCaml code - OCaml code enclosed in curly braces, which is copied verbatim to the generated `*.ml` file + +* Comments - comments in the `*.mlg` file in the form `(* … *)`, which are not copied + to the generated `*.ml` file. Comments in OCaml code are preserved. + +* `DECLARE_PLUGIN "*_plugin"` - associates the file with a specific plugin, for example "ltac_plugin" + +* `GRAMMAR EXTEND` - adds additional nonterminals and productions to the grammar and declares global + nonterminals referenced in the `GRAMMAR EXTEND`: + + ``` + GRAMMAR EXTEND Gram + GLOBAL: + bignat bigint …; + <nonterminal definitions> + END + ``` + + Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "Prim.bignat"`. + All the `*.mlg` files include `open Pcoq` and often its modules, e.g. `open Pcoq.Prim`. + + `GRAMMAR EXTEND` should be used only for large syntax additions. To add new commands + and tactics, use these instead: + + - `VERNAC COMMAND EXTEND` to add new commands + - `TACTIC EXTEND` to add new tactics + - `ARGUMENT EXTEND` to add new nonterminals + + These constructs provide essential semantic information that's provided in a more complex, + less readable way with `GRAMMAR EXTEND`. + +* `VERNAC COMMAND EXTEND` - adds new command syntax by adding productions to the + `command` nonterminal. For example: + + ``` + VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY + | [ "Extraction" "Library" ident(m) ] + -> { extraction_library false m } + END + ``` + + Productions here are represented with alternate syntax, described later. + + New commands should be added using this construct rather than `GRAMMAR EXTEND` so + they are correctly registered, such as having the correct command classifier. + + TODO: explain "ExtractionLibrary", CLASSIFIED AS, CLASSIFIED BY, "{ tactic_mode }", STATE + +* `VERNAC { … } EXTEND` - TODO. A variant. The `{ … }` is a block of OCaml code. + +* `TACTIC EXTEND` - adds new tactic syntax by adding productions to `simple_tactic`. + For example: + + ``` + TACTIC EXTEND btauto + | [ "btauto" ] -> { Refl_btauto.Btauto.tac } + END + ``` + + adds a new nonterminal `btauto`. + + New tactics should be added using this construct rather than `GRAMMAR EXTEND`. + + TODO: explain DEPRECATED, LEVEL (not shown) + +* `ARGUMENT EXTEND` - defines a new nonterminal + + ``` + ARGUMENT EXTEND ast_closure_term + PRINTED BY { pp_ast_closure_term } + INTERPRETED BY { interp_ast_closure_term } + GLOBALIZED BY { glob_ast_closure_term } + SUBSTITUTED BY { subst_ast_closure_term } + RAW_PRINTED BY { pp_ast_closure_term } + GLOB_PRINTED BY { pp_ast_closure_term } + | [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c } + END + ``` + + See comments in `tacentries.mli` for partial information on the various + arguments. + +* `VERNAC ARGUMENT EXTEND` - (part of `argument_extend` in the yacc grammar) defines + productions for a single nonterminal. For example: + + ``` + VERNAC ARGUMENT EXTEND language + PRINTED BY { pr_language } + | [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } + | [ "OCaml" ] -> { Ocaml } + | [ "Haskell" ] -> { Haskell } + | [ "Scheme" ] -> { Scheme } + | [ "JSON" ] -> { JSON } + END + ``` + + TODO: explain PRINTED BY, CODE + +* DOC_GRAMMAR - Used in `doc_grammar`-generated files to permit simplified syntax + +Note that you can reverse engineer many details by comparing the `.mlg` input file with +the `.ml` generated by `coqpp`. + +## Grammars: Nonterminals and Productions + +Here's a simple nonterminal definition in the Camlp5 format: + + ``` + universe: + [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids } + | u = universe_expr -> { [u] } ] ] + ; + ``` + +In which: +* `universe` is the nonterminal being defined +* productions are separated by `|` and, as a group, are enclosed in `[ [ … ] ];` +* `u = universe_expr` refers to the `universe_expr` nonterminal. `u` is bound to + the value returned by that nonterminal's action routine, which can be + referred to in the action routine. For `ids = LIST1 universe_expr SEP ","`, + `ids` is bound to the list of values returned by `universe_expr`. +* `-> { … }` contains the OCaml action routine, which is executed when the production is recognized + and returns a value +* Semicolons separate adjacent grammatical elements (nonterminals, strings or other constructs) + +Grammatical elements that appear in productions are: + +- nonterminal names - identifiers in the form `[a-zA-Z0-9_]*`. These correspond to variables in + the generated `.ml` code. In some cases a qualified name, such as `Prim.name`, is used. +- `"…"` - a literal string that becomes a keyword and cannot be used as an `ident`. + The string doesn't have to be a valid identifier; frequently the string will contain only + punctuation characters. Generally we try to avoid adding new keywords that are also valid + identifiers--though there is an unresolved debate among the developers about whether having more + such keywords in general is good (e.g. it makes it easier to highlight keywords in GUIs) + or bad (more keywords for the user to avoid and new keywords may require changes to existing + proof files). +- `IDENT "…"` - a literal string that has the form of an `ident` that doesn't become + a keyword +- `OPT element` - optionally include `element` (e.g. a nonterminal, IDENT "…" or "…"). + The value is of type `'a option`. +- `LIST1 element` - a list of one or more `element`s. The value is of type `'a list`. +- `LIST0 element` - an optional list of `element`s +- `LIST1 element SEP sep` - a list of `element`s separated by `sep` +- `LIST0 element SEP sep` - an optional list of `element`s separated by `sep` +- `( elements )` - grouping to represent a series of elements as a unit, + useful within `OPT` and `LIST*`. +- `[ elements1 | elements2 | … ]` - alternatives (either `elements1` or `elements2` or …), + actually nested productions, each of which can have its own action routines + +Nonterminals can also be defined with multiple levels to specify precedence and associativity +of its productions. This is described in the Coq documentation under the `Print Grammar` +command. The first square bracket around a nonterminal definition is for grouping +level definitions, which are separated with `|`, for example: + + ``` + tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] + | "4" LEFTA + : + ``` + +Grammar extensions can specify what level they are modifying, for example: + + ``` + tactic_expr: LEVEL "1" [ RIGHTA + [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + ] ]; + ``` + +### Alternate production syntax ### + +Except for `GRAMMAR EXTEND`, the `EXTEND` nodes in the `*.mlg`s use simplified syntax in +productions that's similar to what's used in the `Tactic Notation` and +`Ltac2 Notation` commands. For example: + + ``` + TACTIC EXTEND cc + | [ "congruence" ] -> { congruence_tac 1000 [] } + | [ "congruence" integer(n) ] -> { congruence_tac n [] } + | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } + | [ "congruence" integer(n) "with" ne_constr_list(l) ] -> + { congruence_tac n l } + END + ``` + +Nonterminals appearing in the alternate production syntax are accessed through `wit_*` symbols +defined in the OCaml code. Some commonly used symbols are defined in `stdarg.ml`. +Others are defined in the code generated by `ARGUMENT EXTEND` and `VERNAC ARGUMENT EXTEND` +constructs. References to nonterminals that don't have `wit_*` symbols cause +compilation errors. + +The differences are: +* The outer `: [ … ];` is omitted. Each production is enclosed in `| [ … ]`. +* The action routine is outside the square brackets +* Literal strings that are valid identifiers don't become reserved keywords +* No semicolons separating elements of the production +* `integer(n)` is used to bind a nonterminal value to a variable instead of `n = integer` +* Alternate forms of constructs are used: + * `ne_entry_list` for `LIST1 entry` + * `entry_list` for `LIST0 entry` + * `ne_entry_list_sep(var, sep)` for `LIST1 entry SEP sep` where the list is bound to `var` + * `entry_list_sep(var, sep)` for `LIST0 entry SEP sep` where the list is bound to `var` + * `entry_opt` for OPT entry +* There's no way to define `LEVEL`s +* There's no equivalent to `( elements )` or `[ elements1 | elements2 | … ]`, which may + require repeating similar syntax several times. For example, this single production + is equivalent to 8 productions in `TACTIC EXTEND` representing all possible expansions of + three `OPT`s: + + ``` + | IDENT "Add"; IDENT "Parametric"; IDENT "Relation"; LIST0 binder; ":"; constr; constr; + OPT [ IDENT "reflexivity"; IDENT "proved"; IDENT "by"; constr -> { … } ]; + OPT [ IDENT "symmetry"; IDENT "proved"; IDENT "by"; constr -> { … } ]; + OPT [ IDENT "transitivity"; IDENT "proved"; IDENT "by"; constr -> { … } ]; + IDENT "as"; ident -> { … } + ``` + +## Usage notes + +### Other components + +Coq's lexer is in `clexer.ml`. Its 10 token types are defined in `tok.ml`. + +The parser is in `grammar.ml`. The extensive use of GADT (generalized algebraic datatypes) +makes it harder for the uninitiated to understand it. + +When the parser is invoked, the call tells the parser which nonterminal to parse. `vernac_control` +is the start symbol for commands. `tactic_mode` is the start symbol for tactics. +Tactics give syntax errors if Coq is not in proof mode. There are additional details +not mentioned here. + +### Parsing productions + +Some thoughts, not to be taken as identifying all the issues: + +Since the parser examines only the next token to make a parsing decision (and perhaps +because of other potentially fixable limitations), some productions have to be ordered +or structured in a particular way to parse correctly in all cases. + +For example, consider these productions: + + ``` + command: [ [ + | IDENT "Print"; p = printable -> { VernacPrint p } + | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> { VernacPrint (PrintName (qid,l)) } + | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> + { VernacPrint (PrintModuleType qid) } + | IDENT "Print"; IDENT "Module"; qid = global -> + { VernacPrint (PrintModule qid) } + | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> + { VernacPrint (PrintNamespace ns) } + : + + printable: + [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> { PrintName (qid,l) } + | IDENT "All" -> { PrintFullContext } + | IDENT "Section"; s = global -> { PrintSectionContext s } + : + ``` + +Reversing the order of the first two productions in `command` causes the `All` in `Print All` to +be parsed incorrectly as a `smart_global`, making that command unavailable. `Print Namespace nat.` +still works correctly, though. + +Similarly, the production for `Print Module Type` has to appear before `Print Module <global>` +in order to be reachable. + +Internally, the parser generates a tree that represents the possible prefixes for the +productions of a nonterminal as described in +[the Camlp5 documentation](http://camlp5.github.io/doc/htmlc/grammars.html#b:Rules-insertion). + +Here's another example in which the way the productions are written matters. `OPT` at +the beginning of a production doesn't always work well: + + ``` + command: [ [ + | IDENT "Foo"; n = natural -> { VernacBack 1 } + | OPT (IDENT "ZZ"); IDENT "Foo" -> { VernacBack 1 } + : + ``` + +`Foo.` looks like it should be accepted, but it gives a parse error: + + ``` + Unnamed_thm < Foo. + Toplevel input, characters 3-4: + > Foo. + > ^ + Error: + Syntax error: [prim:natural] expected after 'Foo' (in [vernac:command]). + ``` + +Reversing the order of the productions doesn't help, but splitting +the 'OPT' production into 2 productions works: + + ``` + | IDENT "Foo" -> { VernacBack 1 } + | IDENT "ZZ"; IDENT "Foo" -> { VernacBack 1 } + | IDENT "Foo"; n = natural -> { VernacBack 1 } + + ``` + +On the other hand, `OPT` works just fine when the parser has already found the +right production. For example `Back` and `Back <natural>` can be combined using +an `OPT`: + + ``` + | IDENT "Back"; n = OPT natural -> { VernacBack (Option.default 1 n) } + ``` + +### Lookahead + +It's possible to look ahead more than one symbol using OCaml code. Generally we +avoid doing this unless there's a strong reason to do so. For example, this +code defines a new nonterminal `local_test_lpar_id_colon` that checks that +the next 3 tokens are `"("` `ident` and `":"` without consuming any input: + + ``` + let local_test_lpar_id_colon = + let open Pcoq.Lookahead in + to_entry "lpar_id_colon" begin + lk_kw "(" >> lk_ident >> lk_kw ":" + end + ``` + +This one checks that the next 2 tokens are `"["` and `"|"` with no space between. +This is a special case: intropatterns can have sequences like `"[|]"` that are +3 different tokens with empty nonterminals between them. Making `"[|"` a keyword +would break existing code with "[|]": + + ``` + let test_array_opening = + let open Pcoq.Lookahead in + to_entry "test_array_opening" begin + lk_kw "[" >> lk_kw "|" >> check_no_space + end + ``` + +TODO: how to add a tactic or command diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index aa650fbdc8..ac4972ed0d 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,6 +1,5 @@ open Format open Term -open Constr open Names open Cemitcodes open Vmvalues @@ -8,9 +7,7 @@ open Vmvalues let ppripos (ri,pos) = (match ri with | Reloc_annot a -> - let sp,i = a.ci.ci_ind in - print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + print_string "switch\n" | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> diff --git a/doc/changelog/02-specification-language/10858-stuck-classed.md b/doc/changelog/02-specification-language/10858-stuck-classed.md deleted file mode 100644 index c7186f2c1d..0000000000 --- a/doc/changelog/02-specification-language/10858-stuck-classed.md +++ /dev/null @@ -1,12 +0,0 @@ -- **Changed:** - Typeclass resolution, accessible through :tacn:`typeclasses eauto`, - now suspends constraints according to their modes - instead of failing. If a typeclass constraint does not match - any of the declared modes for its class, the constraint is postponed, and - the proof search continues on other goals. Proof search does a fixed point - computation to try to solve them at a later stage of resolution. It does - not fail if there remain only stuck constraints at the end of resolution. - This makes typeclasses with declared modes more robust with respect to the - order of resolution. - (`#10858 <https://github.com/coq/coq/pull/10858>`_, - fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). diff --git a/doc/changelog/03-notations/12523-term-notation-custom.rst b/doc/changelog/03-notations/12523-term-notation-custom.rst deleted file mode 100644 index 1a611f3fb1..0000000000 --- a/doc/changelog/03-notations/12523-term-notation-custom.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Simultaneous definition of terms and notations now support custom entries. - Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_. - (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès). diff --git a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst deleted file mode 100644 index ab8768a079..0000000000 --- a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Printing bug with notations for n-ary applications used with applied references. - (`#12683 <https://github.com/coq/coq/pull/12683>`_, - fixes `#12682 <https://github.com/coq/coq/pull/12682>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12572-fix-12571.rst b/doc/changelog/04-tactics/12572-fix-12571.rst deleted file mode 100644 index 98b217e86b..0000000000 --- a/doc/changelog/04-tactics/12572-fix-12571.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - typeclasses eauto (and discriminated hint bases) now correctly - classify local variables as being unfoldable - (`#12572 <https://github.com/coq/coq/pull/12572>`_, - fixes `#12571 <https://github.com/coq/coq/issues/12571>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/12541-fix12228.rst b/doc/changelog/05-tactic-language/12541-fix12228.rst deleted file mode 100644 index 286760e008..0000000000 --- a/doc/changelog/05-tactic-language/12541-fix12228.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Excluding occurrences was causing an anomaly in tactics - (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`). - (`#12541 <https://github.com/coq/coq/pull/12541>`_, - fixes `#12228 <https://github.com/coq/coq/issues/12228>`_, - by Pierre Roux). diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst deleted file mode 100644 index 555020d319..0000000000 --- a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Fix the parsing of multi-parameters Ltac2 types - (`#12594 <https://github.com/coq/coq/pull/12594>`_, - fixes `#12595 <https://github.com/coq/coq/issues/12595>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst deleted file mode 100644 index 4df8e97e34..0000000000 --- a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Do not store the full environment inside ssr ast_closure_term - (`#12708 <https://github.com/coq/coq/pull/12708>`_, - fixes `#12707 <https://github.com/coq/coq/issues/12707>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst deleted file mode 100644 index c654ddd69d..0000000000 --- a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Properly report the mismatched magic number of vo files - (`#12677 <https://github.com/coq/coq/pull/12677>`_, - fixes `#12513 <https://github.com/coq/coq/issues/12513>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst new file mode 100644 index 0000000000..a05829b720 --- /dev/null +++ b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Special symbols now escaped in the index produced by coqdoc, + avoiding collision with the syntax of the output format + (`#12754 <https://github.com/coq/coq/pull/12754>`_, + fixes `#12752 <https://github.com/coq/coq/issues/12752>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst new file mode 100644 index 0000000000..67ee061285 --- /dev/null +++ b/doc/changelog/08-tools/12772-fix-details.rst @@ -0,0 +1,5 @@ +- **Fixed:** + The `details` environment added in the 8.12 release can now be used + as advertised in the reference manual + (`#12772 <https://github.com/coq/coq/pull/12772>`_, + by Thomas Letan). diff --git a/doc/changelog/09-coqide/12562-coqide-lax-filename.rst b/doc/changelog/09-coqide/12562-coqide-lax-filename.rst deleted file mode 100644 index ef3160dd99..0000000000 --- a/doc/changelog/09-coqide/12562-coqide-lax-filename.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier - (`#12562 <https://github.com/coq/coq/pull/12562>`_, - fixes `#10988 <https://github.com/coq/coq/issues/10988>`_, - by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst new file mode 100644 index 0000000000..208855b4c8 --- /dev/null +++ b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + Int63 notations now match up with the rest of the standard library: :g:`a \% + m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced + with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. + The old notations are still available as deprecated notations. Additionally, + there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that + users can import to get the ``Int63`` notations without unqualifying the + various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes + `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst new file mode 100644 index 0000000000..1709cf1eae --- /dev/null +++ b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + <? n`, and :g:`m <=? n`. The old notations are still available as deprecated + notations. Additionally, there is now a + ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to + get the ``PrimFloat`` notations without unqualifying the various primitives + (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 + <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst new file mode 100644 index 0000000000..51b59e4a94 --- /dev/null +++ b/doc/changelog/10-standard-library/12716-curry.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12799-list-repeat.rst b/doc/changelog/10-standard-library/12799-list-repeat.rst new file mode 100644 index 0000000000..adfc48f67b --- /dev/null +++ b/doc/changelog/10-standard-library/12799-list-repeat.rst @@ -0,0 +1,4 @@ +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 <https://github.com/coq/coq/pull/12799>`_, + by Olivier Laurent). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12583-fix-remake.rst b/doc/changelog/11-infrastructure-and-dependencies/12583-fix-remake.rst deleted file mode 100644 index d9c8b634d6..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/12583-fix-remake.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer - rebuild the ``modules/`` tests on subsequent runs, if they have not been - modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_, - fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index d4707a04d8..0f501382e7 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -136,6 +136,18 @@ Specification language, type inference :cmd:`Arguments`) has been turned into an error (`#11368 <https://github.com/coq/coq/pull/11368>`_, by SimonBoulier). +- **Changed:** + Typeclass resolution, accessible through :tacn:`typeclasses eauto`, + now suspends constraints according to their modes + instead of failing. If a typeclass constraint does not match + any of the declared modes for its class, the constraint is postponed, and + the proof search continues on other goals. Proof search does a fixed point + computation to try to solve them at a later stage of resolution. It does + not fail if there remain only stuck constraints at the end of resolution. + This makes typeclasses with declared modes more robust with respect to the + order of resolution. + (`#10858 <https://github.com/coq/coq/pull/10858>`_, + fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). - **Added:** Warn when manual implicit arguments are used in unexpected positions of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit @@ -1126,6 +1138,84 @@ Infrastructure and dependencies (`#11245 <https://github.com/coq/coq/pull/11245>`_, by Emilio Jesus Gallego Arias). +Changes in 8.12.0 +~~~~~~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +**Notations** + +- **Added:** + Simultaneous definition of terms and notations now support custom entries. + Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_. + (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès). +- **Fixed:** + Printing bug with notations for n-ary applications used with applied references. + (`#12683 <https://github.com/coq/coq/pull/12683>`_, + fixes `#12682 <https://github.com/coq/coq/pull/12682>`_, + by Hugo Herbelin). + +**Tactics** + +- **Fixed:** + :tacn:`typeclasses eauto` (and discriminated hint bases) now correctly + classify local variables as being unfoldable + (`#12572 <https://github.com/coq/coq/pull/12572>`_, + fixes `#12571 <https://github.com/coq/coq/issues/12571>`_, + by Pierre-Marie Pédrot). + +**Tactic language** + +- **Fixed:** + Excluding occurrences was causing an anomaly in tactics + (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`). + (`#12541 <https://github.com/coq/coq/pull/12541>`_, + fixes `#12228 <https://github.com/coq/coq/issues/12228>`_, + by Pierre Roux). +- **Fixed:** + Parsing of multi-parameters Ltac2 types + (`#12594 <https://github.com/coq/coq/pull/12594>`_, + fixes `#12595 <https://github.com/coq/coq/issues/12595>`_, + by Pierre-Marie Pédrot). + +**SSReflect** + +- **Fixed:** + Do not store the full environment inside ssr ast_closure_term + (`#12708 <https://github.com/coq/coq/pull/12708>`_, + fixes `#12707 <https://github.com/coq/coq/issues/12707>`_, + by Pierre-Marie Pédrot). + +**Commands and options** + +- **Fixed:** + Properly report the mismatched magic number of vo files + (`#12677 <https://github.com/coq/coq/pull/12677>`_, + fixes `#12513 <https://github.com/coq/coq/issues/12513>`_, + by Pierre-Marie Pédrot). +- **Changed:** + Arbitrary hints have been undeprecated, and their definition + now triggers a standard warning instead + (`#12678 <https://github.com/coq/coq/pull/12678>`_, + fixes `#11970 <https://github.com/coq/coq/issues/11970>`_, + by Pierre-Marie Pédrot). + +**CoqIDE** + +- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier + (`#12562 <https://github.com/coq/coq/pull/12562>`_, + fixes `#10988 <https://github.com/coq/coq/issues/10988>`_, + by Vincent Laporte). + +**Infrastructure and dependencies** + +- **Fixed:** + Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer + rebuild the ``modules/`` tests on subsequent runs, if they have not been + modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_, + fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross). + Version 8.11 ------------ diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index f9d24fde0e..c27eb216e8 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules ``Datatypes``, ``Specif``, ``Peano``, -``Wf`` and +``Wf`` and ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. @@ -175,7 +175,7 @@ Quantifiers Then we find first-order quantifiers: .. coqtop:: in - + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := ex_intro (x:A) (_:P x). @@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided. single: f_equal2 ... f_equal5 (term) The theorem ``f_equal`` is extended to functions with two to five -arguments. The theorem are names ``f_equal2``, ``f_equal3``, +arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. .. coqtop:: in abort - + Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), @@ -324,7 +324,7 @@ Programming Note that zero is the letter ``O``, and *not* the numeral ``0``. -The predicate ``identity`` is logically +The predicate ``identity`` is logically equivalent to equality but it lives in sort ``Type``. It is mainly maintained for compatibility. @@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``. Specification ~~~~~~~~~~~~~ -The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. +The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. They are available with the syntax shown in the previous section :ref:`datatypes`. For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct @@ -393,11 +393,11 @@ provided. .. coqtop:: in Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). - Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x). A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, -when the predicate ``P`` is now defined as a +when the predicate ``P`` is now defined as a constructor of types in ``Type``. .. index:: @@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: .. coqdoc:: - + Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := match n with @@ -628,7 +628,7 @@ induction principle. .. coqdoc:: Theorem nat_case : - forall (n:nat) (P:nat -> Prop), + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Theorem nat_double_ind : forall R:nat -> nat -> Prop, @@ -640,7 +640,7 @@ induction principle. Well-founded recursion ~~~~~~~~~~~~~~~~~~~~~~ -The basic library contains the basics of well-founded recursion and +The basic library contains the basics of well-founded recursion and well-founded induction, in module ``Wf.v``. .. index:: @@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``. forall P:A -> Prop, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. -The automatically generated scheme ``Acc_rect`` +The automatically generated scheme ``Acc_rect`` can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the @@ -741,7 +741,7 @@ The standard library Survey ~~~~~~ -The rest of the standard library is structured into the following +The rest of the standard library is structured into the following subdirectories: * **Logic** : Classical logic and dependent equality @@ -751,8 +751,8 @@ subdirectories: * **ZArith** : Basic relative integer arithmetic * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words) * **Bool** : Booleans (basic functions and results) - * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) - * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) + * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) + * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) @@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR :name: discrR - + Proves that two real integer constants are different. .. example:: @@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: split_Rmult :name: split_Rmult - + Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. @@ -963,7 +963,7 @@ List library single: fold_left (term) single: fold_right (term) -Some elementary operations on polymorphic lists are defined here. +Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module ``List``. It defines the following notions: @@ -1052,9 +1052,9 @@ Notation Interpretation ``_ + _`` ``add`` ``_ * _`` ``mul`` ``_ / _`` ``div`` -``_ == _`` ``eqb`` -``_ < _`` ``ltb`` -``_ <= _`` ``leb`` +``_ =? _`` ``eqb`` +``_ <? _`` ``ltb`` +``_ <=? _`` ``leb`` ``_ ?= _`` ``compare`` =========== ============== diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 40e0898871..20f4310d13 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -13,13 +13,13 @@ Existential variables | ?[ ?@ident ] | ?@ident {? @%{ {+; @ident := @term } %} } -|Coq| terms can include existential variables which represents unknown -subterms to eventually be replaced by actual subterms. +|Coq| terms can include existential variables that represent unknown +subterms that are eventually replaced with actual subterms. -Existential variables are generated in place of unsolvable implicit +Existential variables are generated in place of unsolved implicit arguments or “_” placeholders when using commands such as ``Check`` (see Section :ref:`requests-to-the-environment`) or when using tactics such as -:tacn:`refine`, as well as in place of unsolvable instances when using +:tacn:`refine`, as well as in place of unsolved instances when using tactics such that :tacn:`eapply`. An existential variable is defined in a context, which is the context of variables of the placeholder which generated the existential variable, and a type, @@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). In the general case, when an existential variable :n:`?@ident` appears -outside of its context of definition, its instance, written under the -form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +outside its context of definition, its instance, written in the +form :n:`{ {*; @ident := @term} }`, is appended to its name, indicating how the variables of its defining context are instantiated. -The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag -is on (see Section :ref:`explicit-display-existentials`), and this is why an -existential variable used in the same context as its context of definition is written with no instance. +Only the variables that are defined in another context are displayed: +this is why an existential variable used in the same context as its +context of definition is written with no instance. +This behaviour may be changed: see :ref:`explicit-display-existentials`. .. coqtop:: all Check (fun x y => _) 0 1. - Set Printing Existential Instances. - - Check (fun x y => _) 0 1. - Existential variables can be named by the user upon creation using the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. @@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + .. _tactics-in-terms: Solving existential variables using tactics diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index bbd486e3ba..ca69072cb9 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of the type of the context of the current expression. For instance, the only argument of:: - nil : forall A:Set, list A` + nil : forall A:Set, list A is contextual. Similarly, both arguments of a term of type:: @@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are quantified explicitly. Use the :cmd:`Generalizable` command to designate which variables should be generalized. -It is activated for a binder by prefixing a \`, and for terms by +It is activated within a binder by prefixing it with \`, and for terms by surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index b4558ef07f..d6a828521f 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -94,7 +94,7 @@ The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` performs case analysis on :n:`@term__0` whose type must be an inductive type with exactly one constructor. The number of variables :n:`@ident__i` must correspond to the number of arguments of this -contrustor. Then, in :n:`@term__1`, these variables are bound to the +constructor. Then, in :n:`@term__1`, these variables are bound to the arguments of the constructor in :n:`@term__0`. For instance, the definition diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 058b8ccd5c..ec182ce08f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -81,8 +81,7 @@ loading of the resource file with the option ``-q``. By environment variables ~~~~~~~~~~~~~~~~~~~~~~~~~ -Load path can be specified to the |Coq| system by setting up ``$COQPATH`` -environment variable. It is a list of directories separated by +``$COQPATH`` can be used to specify the load path. It is a list of directories separated by ``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and ``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`). @@ -92,7 +91,7 @@ not set, they look for the commands in the executable path. .. _COQ_COLORS: -The ``$COQ_COLORS`` environment variable can be used to specify the set +``$COQ_COLORS`` can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated list of assignments of the form :n:`name={*; attr}` where @@ -108,6 +107,22 @@ sets the highlights for added text in diffs to underlined (the 4) with a backgro color (0, 0, 240) and for removed text in diffs to a red background. Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. +.. _OCAMLRUNPARAM: + +``$OCAMLRUNPARAM``, described +`here <https://caml.inria.fr/pub/docs/manual-ocaml/runtime.html#s:ocamlrun-options>`_, +can be used to specify certain runtime and memory usage parameters. In most cases, +experimenting with these settings will likely not cause a significant performance difference +and should be harmless. + +If the variable is not set, |Coq| uses the +`default values <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEcontrol>`_, +except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 32Mwords +(256MB with 64-bit executables or 128MB with 32-bit executables). + +.. todo: Using the same text "here" for both of the links in the last 2 paragraphs generates + an incorrect warning: coq-commands.rst:4: WARNING: Duplicate explicit target name: "here". + The warning doesn't even have the right line number. :-( .. _command-line-options: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 00aafe1266..4480b10319 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -858,19 +858,28 @@ Controlling the effect of proof editing commands Controlling memory usage ------------------------ +.. cmd:: Print Debug GC + + Prints heap usage statistics, which are values from the `stat` type of the `Gc` module + described + `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ + in the OCaml documentation. + The `live_words`, `heap_words` and `top_heap_words` values give the basic information. + Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. + When experiencing high memory usage the following commands can be used to force |Coq| to optimize some of its internal data structures. - .. cmd:: Optimize Proof - This command forces |Coq| to shrink the data structure used to represent - the ongoing proof. + Shrink the data structure used to represent the current proof. .. cmd:: Optimize Heap - This command forces the |OCaml| runtime to perform a heap compaction. - This is in general an expensive operation. - See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + Perform a heap compaction. This is generally an expensive operation. + See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ There is also an analogous tactic :tacn:`optimize_heap`. + +Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` +environment variable. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7b3670164b..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1211,6 +1211,8 @@ The move tactic. :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. +.. _the_case_tactic_ssr: + The case tactic ``````````````` @@ -1235,7 +1237,17 @@ The case tactic x = 1 -> y = 2 -> G. - Note also that the case of |SSR| performs :g:`False` elimination, even + The :tacn:`case` can generate the following warning: + + .. warn:: SSReflect: cannot obtain new equations out of ... + + The tactic was run on an equation that cannot generate simpler equations, + for example `x = 1`. + + The warning can be silenced or made fatal by using the :opt:`Warnings` option + and the `spurious-ssr-injection` key. + + Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. @@ -2280,7 +2292,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } +.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 25c4de7389..c5fab0983f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2227,9 +2227,6 @@ and an explanation of the underlying technique. then :n:`injection @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - .. exn:: Nothing to do, it is an equality between convertible terms. :undocumented: @@ -2237,7 +2234,8 @@ and an explanation of the underlying technique. :undocumented: .. exn:: Nothing to inject. - :undocumented: + + This error is given when one side of the equality is not a constructor. .. tacv:: injection @num diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fcd5ecc070..9e8e5e5fa5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -425,16 +425,98 @@ Displaying information about notations (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s - The first three of these give the precedence and associativity for each construct. - For example, these lines printed by `Print Grammar tactic` indicates that the `try` construct - is at level 3 and right-associative. `SELF` represents the `tactic_expr` nonterminal - at level 5 (the top level):: - + This command doesn't display all nonterminals of the grammar. For example, + productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` + and `tactic_then_gen` which are not shown and can't be printed. + + The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify + what part of the grammar a nonterminal is from. If you examine nonterminal definitions + in the source code, they are identified only by the name following the colon. + + Most of the grammar in the documentation was updated in 8.12 to make it accurate and + readable. This was done using a new developer tool that extracts the grammar from the + source code, edits it and inserts it into the documentation files. While the + edited grammar is equivalent to the original, for readability some nonterminals + have been renamed and others have been eliminated by substituting the nonterminal + definition where the nonterminal was referenced. This command shows the original grammar, + so it won't exactly match the documentation. + + The |Coq| parser is based on Camlp5. The documentation for + `Extensible grammars <http://camlp5.github.io/doc/htmlc/grammars.html>`_ is the + most relevant but it assumes considerable knowledge. Here are the essentials: + + Productions can contain the following elements: + + - nonterminal names - identifiers in the form `[a-zA-Z0-9_]*` + - `"…"` - a literal string that becomes a keyword and cannot be used as an :token:`ident`. + The string doesn't have to be a valid identifier; frequently the string will contain only + punctuation characters. + - `IDENT "…"` - a literal string that has the form of an :token:`ident` + - `OPT element` - optionally include `element` (e.g. a nonterminal, IDENT "…" or "…") + - `LIST1 element` - a list of one or more `element`\s + - `LIST0 element` - an optional list of `element`\s + - `LIST1 element SEP sep` - a list of `element`\s separated by `sep` + - `LIST0 element SEP sep` - an optional list of `element`\s separated by `sep` + - `[ elements1 | elements2 | … ]` - alternatives (either `elements1` or `elements2` or …) + + Nonterminals can have multiple **levels** to specify precedence and associativity + of its productions. This feature of grammars makes it simple to parse input + such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level. + + For example, this output from `Print Grammar tactic` shows the first 3 levels for + `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, + which applies to the productions within it, such as the `try` construct:: + + Entry tactic:tactic_expr is + [ "5" RIGHTA + [ tactic:binder_tactic ] + | "4" LEFTA + [ SELF; ";"; tactic:binder_tactic + | SELF; ";"; SELF + | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA [ IDENT "try"; SELF + : + + The interpretation of `SELF` depends on its position in the production and the + associativity of the level: + + - At the beginning of a production, `SELF` means the next level. In the + fragment shown above, the next level for `try` is "2". (This is defined by the order + of appearance in the grammar or output; the levels could just as well be + named "foo" and "bar".) + - In the middle of a production, `SELF` means the top level ("5" in the fragment) + - At the end of a production, `SELF` means the next level within + `LEFTA` levels and the current level within `RIGHTA` levels. + + `NEXT` always means the next level. `nonterminal LEVEL "…"` is a reference to the specified level + for `nonterminal`. + + `Associativity <http://camlp5.github.io/doc/htmlc/grammars.html#b:Associativity>`_ + explains `SELF` and `NEXT` in somewhat more detail. + + The output for `Print Grammar constr` includes :cmd:`Notation` definitions, + which are dynamically added to the grammar at run time. + For example, in the definition for `operconstr`, the production on the second line shown + here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: - Note that the productions printed by this command are represented in the form used by - |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation. + | "50" LEFTA + [ SELF; "||"; NEXT + + Similarly, `Print Grammar tactic` includes :cmd:`Tactic Notation`\s, such as :tacn:`dintuition`. + + The file + `doc/tools/docgram/fullGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar>`_ + in the source tree extracts the full grammar for + |Coq| (not including notations and tactic notations defined in `*.v` files nor some optionally-loaded plugins) + in a single file with minor changes to handle nonterminals using multiple levels (described in + `doc/tools/docgram/README.md <http://github.com/coq/coq/blob/master/doc/tools/docgram/README.md>`_). + This is complete and much easier to read than the grammar source files. + `doc/tools/docgram/orderedGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/orderedGrammar>`_ + has the edited grammar that's used in the documentation. + + Developer documentation for parsing is in + `dev/doc/parsing.md <http://github.com/coq/coq/blob/master/dev/doc/parsing.md>`_. .. _locating-notations: @@ -872,7 +954,7 @@ where ``x`` is any expression parsed in entry the given rule) and ``y`` is any expression parsed in entry ``expr`` at level strictly less than ``2``. -Rules associated to an entry can refer different sub-entries. The +Rules associated with an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar of term as in the rule @@ -958,7 +1040,7 @@ up to the insertion of a pair of curly brackets. .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar - This displays the state of the grammar for terms associated to + This displays the state of the grammar for terms associated with the custom entry :token:`ident`. .. _NotationSyntax: @@ -1786,13 +1868,13 @@ Tactic notations allow customizing the syntax of tactics. * - ``reference`` - :token:`qualid` - - a global reference of term - - :tacn:`unfold` + - a qualified identifier + - name of an |Ltac|-defined tactic * - ``smart_global`` - :token:`reference` - a global reference of term - - :tacn:`with_strategy` + - :tacn:`unfold`, :tacn:`with_strategy` * - ``constr`` - :token:`term` diff --git a/engine/evd.ml b/engine/evd.ml index c570f75c6b..e85cbc96b2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -987,11 +987,6 @@ let check_constraints evd csts = let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } -let refresh_undefined_universes evd = - let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in - let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in - evd', subst - let nf_univ_variables evd = let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in diff --git a/engine/evd.mli b/engine/evd.mli index 679173ca72..3f17e63034 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val fix_undefined_variables : evar_map -> evar_map -val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst - (** Universe minimization *) val minimize_universes : evar_map -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index d4cb59da26..ca0a21acf7 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -718,35 +718,6 @@ let fix_undefined_variables uctx = { uctx with univ_variables = vars'; univ_algebraic = algs' } -let refresh_undefined_univ_variables uctx = - let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in - let subst_fn u = subst_univs_level_level subst u in - let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc) - uctx.univ_algebraic LSet.empty - in - let vars = - LMap.fold - (fun u v acc -> - LMap.add (subst_fn u) - (Option.map (subst_univs_level_universe subst) v) acc) - uctx.univ_variables LMap.empty - in - let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in - let lbound = uctx.universes_lbound in - let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g) - (ContextSet.levels ctx') g in - let initial = declare uctx.initial_universes in - let univs = declare UGraph.initial_universes in - let uctx' = {names = uctx.names; - local = ctx'; - seff_univs = uctx.seff_univs; - univ_variables = vars; univ_algebraic = alg; - universes = univs; - universes_lbound = lbound; - initial_universes = initial; - weak_constraints = weak; } in - uctx', subst - let minimize uctx = let open UnivMinim in let lbound = uctx.universes_lbound in diff --git a/engine/uState.mli b/engine/uState.mli index 45a0f9964e..607c6c9452 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t val fix_undefined_variables : t -> t -val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst - (** Universe minimization *) val minimize : t -> t diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 4dd7fe7e70..1c7e716fc2 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -85,12 +85,33 @@ let lower_of_list l = type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap } -exception Found of Level.t * lowermap -let find_inst insts v = - try LMap.iter (fun k {enforce;alg;lbound=v';lower} -> - if not alg && enforce && Universe.equal v' v then raise (Found (k, lower))) - insts; raise Not_found - with Found (f,l) -> (f,l) +module LBMap : +sig + type t = private { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t } + val empty : t + val add : Level.t -> lbound -> t -> t +end = +struct + type t = { lbmap : lbound LMap.t; lbrev : (Level.t * lowermap) Universe.Map.t } + (* lbrev is uniquely given from lbmap as a partial reverse mapping *) + let empty = { lbmap = LMap.empty; lbrev = Universe.Map.empty } + let add u bnd m = + let lbmap = LMap.add u bnd m.lbmap in + let lbrev = + if not bnd.alg && bnd.enforce then + match Universe.Map.find bnd.lbound m.lbrev with + | (v, _) -> + if Level.compare u v <= 0 then + Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev + else m.lbrev + | exception Not_found -> + Universe.Map.add bnd.lbound (u, bnd.lower) m.lbrev + else m.lbrev + in + { lbmap; lbrev } +end + +let find_inst insts v = Universe.Map.find v insts.LBMap.lbrev let compute_lbound left = (* The universe variable was not fixed yet. @@ -114,11 +135,11 @@ let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, let inst = Universe.make u in let cstrs' = enforce_leq lbound inst cstrs in (ctx, us, LSet.remove u algs, - LMap.add u {enforce;alg;lbound;lower} insts, cstrs'), + LBMap.add u {enforce;alg;lbound;lower} insts, cstrs'), {enforce; alg; lbound=inst; lower} else (* Actually instantiate *) (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u {enforce;alg;lbound;lower} insts, cstrs), + LBMap.add u {enforce;alg;lbound;lower} insts, cstrs), {enforce; alg; lbound; lower} type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t @@ -180,10 +201,10 @@ let minimize_univ_variables ctx us algs left right cstrs = let lbounds = match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with | None -> lbounds - | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} + | Some lbound -> LBMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} lbounds in (Univ.LMap.remove r left, lbounds)) - left (left, Univ.LMap.empty) + left (left, LBMap.empty) in let rec instance (ctx, us, algs, insts, cstrs as acc) u = let acc, left, lower = @@ -256,7 +277,7 @@ let minimize_univ_variables ctx us algs left right cstrs = with UpperBoundedAlg -> enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) and aux (ctx, us, algs, seen, cstrs as acc) u = - try acc, LMap.find u seen + try acc, LMap.find u seen.LBMap.lbmap with Not_found -> instance acc u in LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) -> diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 57cdccce6d..0e237b74fe 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -544,6 +544,7 @@ struct let coercions = BoolOpt ["Printing"; "Coercions"] let raw_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] + let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] let existential = BoolOpt ["Printing"; "Existential"; "Instances"] let universes = BoolOpt ["Printing"; "Universes"] @@ -558,7 +559,7 @@ struct { opts = [raw_matching]; init = true; label = "Display raw _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; - { opts = [notations]; init = true; label = "Display _parentheses" }; + { opts = [parentheses]; init = true; label = "Display _parentheses" }; { opts = [all_basic]; init = false; label = "Display _all basic low-level contents" }; { opts = [existential]; init = false; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 9921208e04..15cc451ea8 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1187,7 +1187,7 @@ value coq_interprete if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); - if (Field(*sp, 2) == Val_true) { + if (Is_tailrec_switch(*sp)) { for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; }else{ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 86ae6295fd..a19f9b56c1 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,7 @@ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #define Is_double(v) (Tag_val(v) == Double_tag) +#define Is_tailrec_switch(v) (Field(v,1) == Val_true) /* coq array */ #define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 5e5fad9f04..41b3bff465 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -128,6 +128,7 @@ val prim_ind_to_string : 'a prim_ind -> string (** Can raise [Not_found] *) val op_or_type_of_string : string -> op_or_type + val op_or_type_to_string : op_or_type -> string val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7bff377238..bacc308e1f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont = done; let annot = - {ci = ci; rtbl = rtbl; tailcall = is_tailcall; + {rtbl = rtbl; tailcall = is_tailcall; max_stack_size = !max_stack_size - sz} in diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 6b4daabf0c..ed475dca7e 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,7 +13,6 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Constr open Vmvalues open Cbytecodes open Copcodes @@ -424,12 +423,11 @@ let subst_strcst s sc = | Const_float _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) +let subst_annot _ (a : annot_switch) = a + let subst_reloc s ri = match ri with - | Reloc_annot a -> - let (kn,i) = a.ci.ci_ind in - let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in - Reloc_annot {a with ci = ci} + | Reloc_annot a -> Reloc_annot (subst_annot s a) | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) diff --git a/kernel/primred.ml b/kernel/primred.ml index 10a8da8813..90eeeb9be7 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -5,62 +5,71 @@ open Retroknowledge open Environ open CErrors -let add_retroknowledge env action = +type _ action_kind = + | IncompatTypes : _ prim_type -> Constant.t action_kind + | IncompatInd : _ prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +let check_same_types typ c1 c2 = + if not (Constant.equal c1 c2) + then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2)) + +let check_same_inds ind i1 i2 = + if not (eq_ind i1 i2) + then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2)) + +let add_retroknowledge retro action = match action with - | Register_type(PT_int63,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_int63 with - | None -> { retro with retro_int63 = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro - | Register_type(PT_float64,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_float64 with - | None -> { retro with retro_float64 = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro - | Register_type(PT_array,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_array with - | None -> { retro with retro_array = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro + | Register_type(typ,c) -> + begin match typ with + | PT_int63 -> + (match retro.retro_int63 with + | None -> { retro with retro_int63 = Some c } + | Some c' -> check_same_types typ c c'; retro) + + | PT_float64 -> + (match retro.retro_float64 with + | None -> { retro with retro_float64 = Some c } + | Some c' -> check_same_types typ c c'; retro) + + | PT_array -> + (match retro.retro_array with + | None -> { retro with retro_array = Some c } + | Some c' -> check_same_types typ c c'; retro) + end + | Register_ind(pit,ind) -> - let retro = env.retroknowledge in - let retro = - match pit with + begin match pit with | PIT_bool -> let r = match retro.retro_bool with | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_bool = Some r } | PIT_carry -> let r = match retro.retro_carry with | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_carry = Some r } | PIT_pair -> let r = match retro.retro_pair with | None -> (ind,1) - | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in + | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_pair = Some r } | PIT_cmp -> let r = match retro.retro_cmp with | None -> ((ind,1), (ind,2), (ind,3)) - | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_cmp = Some r } | PIT_f_cmp -> let r = match retro.retro_f_cmp with | None -> ((ind,1), (ind,2), (ind,3), (ind,4)) - | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_f_cmp = Some r } | PIT_f_class -> let r = @@ -69,10 +78,12 @@ let add_retroknowledge env action = (ind,5), (ind,6), (ind,7), (ind,8), (ind,9)) | Some (((ind',_),_,_,_,_,_,_,_,_) as t) -> - assert (eq_ind ind ind'); t in + check_same_inds pit ind ind'; t in { retro with retro_f_class = Some r } - in - set_retroknowledge env retro + end + +let add_retroknowledge env action = + set_retroknowledge env (add_retroknowledge env.retroknowledge action) let get_int_type env = match env.retroknowledge.retro_int63 with diff --git a/kernel/primred.mli b/kernel/primred.mli index 1bfaffaa44..6e9d4e297e 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -2,6 +2,13 @@ open Names open Environ (** {5 Reduction of primitives} *) +type _ action_kind = + | IncompatTypes : _ CPrimitives.prim_type -> Constant.t action_kind + | IncompatInd : _ CPrimitives.prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +(** May raise [IncomtibleDeclarations] *) val add_retroknowledge : env -> Retroknowledge.action -> env val get_int_type : env -> Constant.t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 04e7a81697..48567aa564 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,7 +88,7 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = univs, typ | Some (typ,Monomorphic_entry uctx) -> - assert (AUContext.is_empty auctx); + assert (AUContext.is_empty auctx); (* ensured by ComPrimitive *) let env = push_context_set ~strict:true uctx env in let u = Instance.empty in let typ = @@ -99,12 +99,14 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = Monomorphic uctx, typ | Some (typ,Polymorphic_entry (unames,uctx)) -> - assert (not (AUContext.is_empty auctx)); - (* push_context will check that the universes aren't repeated in the instance - so comparing the sizes works *) - assert (AUContext.size auctx = UContext.size uctx); - (* No polymorphic primitive uses constraints currently *) - assert (Constraint.is_empty (UContext.constraints uctx)); + assert (not (AUContext.is_empty auctx)); (* ensured by ComPrimitive *) + (* [push_context] will check that the universes aren't repeated in + the instance so comparing the sizes works. No polymorphic + primitive uses constraints currently. *) + if not (AUContext.size auctx = UContext.size uctx + && Constraint.is_empty (UContext.constraints uctx)) + then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++ + str (op_or_type_to_string p)); let env = push_context ~strict:false uctx env in (* Now we know that uctx matches the auctx *) let typ = (Typeops.infer_type env typ).utj_val in diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index ec429d5f9e..de604176cb 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names open Univ -open Constr (********************************************) (* Initialization of the abstract machine ***) @@ -61,8 +60,9 @@ type structured_constant = type reloc_table = (tag * int) array +(** When changing this, adapt Is_tailrec_switch in coq_values.h accordingly *) type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } let rec eq_structured_values v1 v2 = v1 == v2 || @@ -123,22 +123,16 @@ let hash_structured_constant c = | Const_float f -> combinesmall 7 (Float64.hash f) let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && CArray.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall + (asw1.tailcall : bool) == asw2.tailcall && + Int.equal asw1.max_stack_size asw2.max_stack_size let hash_annot_switch asw = let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 + let h1 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h2 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 asw.max_stack_size let pp_sort s = let open Sorts in diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index f4070a02a3..f6efd49cfc 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr (** Values *) @@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } val eq_structured_constant : structured_constant -> structured_constant -> bool val hash_structured_constant : structured_constant -> int diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 9eeba614c7..148c1772bf 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1020,10 +1020,11 @@ let lia (can_enum : bool) (prfdepth : int) sys = p) sys end; + let bnd1 = bound_monomials sys in let sys = subst sys in - let bnd = bound_monomials sys in + let bnd2 = bound_monomials sys in (* To deal with non-linear monomials *) - let sys = bnd @ saturate_by_linear_equalities sys @ sys in + let sys = bnd1 @ bnd2 @ saturate_by_linear_equalities sys @ sys in let sys' = List.map (fun ((p, o), prf) -> (cstr_of_poly (p, o), prf)) sys in xlia (List.map fst sys) can_enum reduction_equations sys' diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 4e1f9a66ac..fa29e6080e 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) = let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in try - ignore (get_injection env evd (EConstr.of_constr ty)); - tac id.Context.binder_name (EConstr.of_constr t) - (EConstr.of_constr ty) + let x = id.Context.binder_name in + ignore + (let eq = Lazy.force eq in + find_option + (match_operator env evd eq + [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|]) + (HConstr.find_all eq !table_cache)); + tac x (EConstr.of_constr t) (EConstr.of_constr ty) with Not_found -> Tacticals.New.tclIDTAC) let iter_let_aux tac = diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 1c81fbc10b..1e182b52fa 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -485,17 +485,22 @@ let revtoptac n0 = Logic.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) end -let equality_inj l b id c = - Proofview.V82.tactic begin fun gl -> - let msg = ref "" in - try Proofview.V82.of_tactic (Equality.inj None l b None c) gl - with - | CErrors.UserError (_,s) - when msg := Pp.string_of_ppcmds s; - !msg = "Not a projectable equality but a discriminable one." || - !msg = "Nothing to inject." -> - Feedback.msg_warning (Pp.str !msg); - discharge_hyp (id, (id, "")) gl +let nothing_to_inject = + CWarnings.create ~name:"spurious-ssr-injection" ~category:"ssr" + (fun (sigma, env, ty) -> + Pp.(str "SSReflect: cannot obtain new equations out of" ++ fnl() ++ + str" " ++ Printer.pr_econstr_env env sigma ty ++ fnl() ++ + str "Did you write an extra [] in the intro pattern?")) + +let equality_inj l b id c = Proofview.Goal.enter begin fun gl -> + Proofview.tclORELSE (Equality.inj None l b None c) + (function + | (Equality.NothingToInject,_) -> + let open Proofview.Notations in + Ssrcommon.tacTYPEOF (EConstr.mkVar id) >>= fun ty -> + nothing_to_inject (Proofview.Goal.sigma gl, Proofview.Goal.env gl, ty); + Proofview.V82.tactic (discharge_hyp (id, (id, ""))) + | (e,info) -> Proofview.tclZERO ~info e) end let injectidl2rtac id c = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bbd8fa0434..aeb18ec322 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -499,13 +499,6 @@ let beta_applist sigma (c,l) = (* Iota reduction tools *) -type 'a miota_args = { - mP : constr; (* the result type *) - mconstr : constr; (* the constructor *) - mci : case_info; (* special info to re-build pattern *) - mcargs : 'a list; (* the constructor's arguments *) - mlf : 'a array } (* the branch code vector *) - let reducible_mind_case sigma c = match EConstr.kind sigma c with | Construct _ | CoFix _ -> true | _ -> false @@ -514,10 +507,7 @@ let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in - if Int.equal bodynum ind then mkCoFix (ind,typedbodies) - else - let bd = mkCoFix (ind,typedbodies) in - bd + mkCoFix (ind,typedbodies) in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -530,18 +520,6 @@ let reduce_and_refold_cofix recfun env sigma cofix sk = (fun _ (t,sk') -> recfun (t,sk')) [] sigma raw_answer sk -let reduce_mind_case sigma mia = - match EConstr.kind sigma mia.mconstr with - | Construct ((ind_sp,i),u) -> -(* let ncargs = (fst mia.mci).(i-1) in*) - let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in - applist (mia.mlf.(i-1),real_cargs) - | CoFix cofix -> - let cofix_def = contract_cofix sigma cofix in - (* XXX Is NoInvert OK here? *) - mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) - | _ -> assert false - (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) @@ -549,10 +527,7 @@ let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies) let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in - if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies) - else - let bd = mkFix ((recindices,ind),typedbodies) in - bd + mkFix ((recindices,ind),typedbodies) in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 0f288cdd46..d404a7e414 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -217,22 +217,14 @@ val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr (** Raises [Invalid_argument] *) - -type 'a miota_args = { - mP : constr; (** the result type *) - mconstr : constr; (** the constructor *) - mci : case_info; (** special info to re-build pattern *) - mcargs : 'a list; (** the constructor's arguments *) - mlf : 'a array } (** the branch code vector *) - val reducible_mind_case : evar_map -> constr -> bool -val reduce_mind_case : evar_map -> constr miota_args -> constr val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool val contract_fix : evar_map -> fixpoint -> constr +val contract_cofix : evar_map -> cofixpoint -> constr (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : Environ.env -> Constant.t tableKey -> bool diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index e4b5dc1edf..9d15e98373 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -458,6 +458,25 @@ let contract_cofix_use_function env sigma f substl_checking_arity env (List.rev subbodies) sigma (nf_beta env sigma bodies.(bodynum)) +type 'a miota_args = { + mP : constr; (** the result type *) + mconstr : constr; (** the constructor *) + mci : case_info; (** special info to re-build pattern *) + mcargs : 'a list; (** the constructor's arguments *) + mlf : 'a array } (** the branch code vector *) + +let reduce_mind_case sigma mia = + match EConstr.kind sigma mia.mconstr with + | Construct ((ind_sp,i),u) -> +(* let ncargs = (fst mia.mci).(i-1) in*) + let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in + applist (mia.mlf.(i-1),real_cargs) + | CoFix cofix -> + let cofix_def = contract_cofix sigma cofix in + (* XXX Is NoInvert OK here? *) + mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) + | _ -> assert false + let reduce_mind_case_use_function func env sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((ind_sp,i),u) -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 854a5ff63d..e5fa9bada1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -262,19 +262,14 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> assert (from = 0) ; - let ci = sw.sw_annot.Vmvalues.ci in let ((mind,_ as ind), u), allargs = find_rectype_a env t in - let iv = if Typeops.should_invert_case env ci then - CaseInvert {univs=u; args=allargs} - else NoInvert - in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in + let p, relevance = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params p in (* calcul des branches *) @@ -286,6 +281,11 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in + let ci = Inductiveops.make_case_info env ind relevance RegularStyle in + let iv = if Typeops.should_invert_case env ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -296,17 +296,17 @@ and nf_stk ?from:(from=0) env sigma c t stk = and nf_predicate env sigma ind mip params v pT = match kind (whd_allnolet env pT) with | LetIn (name,b,t,pT) -> - let body = + let body, rel = nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in - mkLetIn (name,b,t,body) + mkLetIn (name,b,t,body), rel | Prod (name,dom,codom) -> begin match whd_val v with | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let body = + let body, rel = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in - mkLambda(name,dom,body) + mkLambda(name,dom,body), rel | _ -> assert false end | _ -> @@ -321,8 +321,10 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let r = Inductive.relevance_of_inductive env (fst ind) in let name = make_annot name r in - let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in - mkLambda(name,dom,body) + let env = push_rel (LocalAssum (name,dom)) env in + let body = nf_vtype env sigma vb in + let rel = Retyping.relevance_of_type env sigma (EConstr.of_constr body) in + mkLambda(name,dom,body), rel | _ -> assert false and nf_args env sigma vargs ?from:(f=0) t = diff --git a/printing/printer.ml b/printing/printer.ml index f8413f3588..c5cb6ffad8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -257,11 +257,12 @@ let pr_puniverses f env sigma (c,u) = then f env c ++ pr_universe_instance sigma u else f env c -let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) -let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind) -let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr) + +let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) +let pr_inductive env ind = pr_global_env (Termops.vars_of_env env) (GlobRef.IndRef ind) +let pr_constructor env cstr = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstructRef cstr) let pr_pconstant = pr_puniverses pr_constant let pr_pinductive = pr_puniverses pr_inductive diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9bd7ccda5d..db76d08736 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp -let refresh_undefined_univs clenv = - match EConstr.kind clenv.evd clenv.templval.rebus with - | Var _ -> clenv, Univ.empty_level_subst - | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst - | _ -> - let evd', subst = Evd.refresh_undefined_universes clenv.evd in - let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in - { clenv with evd = evd'; templval = map_freelisted clenv.templval; - templtyp = map_freelisted clenv.templtyp }, subst - let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c diff --git a/proofs/clenv.mli b/proofs/clenv.mli index fd1e2fe593..43e808dac7 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -45,9 +45,6 @@ val mk_clenv_from_n : Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv -(** Refresh the universes in a clenv *) -val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst - (** {6 linking of clenvs } *) val clenv_fchain : diff --git a/tactics/auto.ml b/tactics/auto.ml index 3287c1c354..0931c3e61e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -12,11 +12,9 @@ open Pp open Util open Names open Termops -open EConstr open Environ open Genredexpr open Tactics -open Clenv open Locus open Proofview.Notations open Hints @@ -69,38 +67,7 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) -let connect_hint_clenv h gl = - let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in - (* [clenv] has been generated by a hint-making function, so the only relevant - data in its evarmap is the set of metas. The [evar_reset_evd] function - below just replaces the metas of sigma by those coming from the clenv. *) - let sigma = Tacmach.New.project gl in - let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in - (* Still, we need to update the universes *) - let clenv, c = - if h.hint_poly then - (* Refresh the instance of the hint *) - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let emap c = Vars.subst_univs_level_constr subst c in - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - (* Only metas are mentioning the old universes. *) - let clenv = { - templval = Evd.map_fl emap clenv.templval; - templtyp = Evd.map_fl emap clenv.templtyp; - evd = Evd.map_metas emap evd; - env = Proofview.Goal.env gl; - } in - clenv, emap c - else - let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - { clenv with evd = evd ; env = Proofview.Goal.env gl }, c - in clenv, c - -let unify_resolve flags (h : hint) = - Proofview.Goal.enter begin fun gl -> - let clenv, c = connect_hint_clenv h gl in - Clenv.res_pf ~flags clenv - end +let unify_resolve flags h = Hints.hint_res_pf ~flags h let unify_resolve_nodelta h = unify_resolve auto_unif_flags h @@ -110,10 +77,10 @@ let unify_resolve_gen = function let exact h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (exact_check c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> exact_check c end (* Util *) diff --git a/tactics/auto.mli b/tactics/auto.mli index 903da143d2..bc2eee0e4c 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -12,7 +12,6 @@ open Names open EConstr -open Clenv open Pattern open Hints open Tactypes @@ -23,9 +22,6 @@ val default_search_depth : int ref val auto_flags_of_state : TransparentState.t -> Unification.unify_flags -val connect_hint_clenv - : hint -> Proofview.Goal.t -> clausenv * constr - (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index bb062bfc11..1f148e01fa 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -151,23 +151,15 @@ struct type t = Dn.t - let empty = Dn.empty + type pattern = Dn.pattern - let add = function - | None -> - (fun dn (c,v) -> - Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> - Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + let pattern st pat = match st with + | None -> Dn.pattern bounded_constr_pat_discr (pat, !dnet_depth) + | Some st -> Dn.pattern (bounded_constr_pat_discr_st st) (pat, !dnet_depth) - let rmv = function - | None -> - (fun dn (c,v) -> - Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) - | Some st -> - (fun dn (c,v) -> - Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + let empty = Dn.empty + let add = Dn.add + let rmv = Dn.rmv let lookup sigma = function | None -> diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 4358e5a8d9..2caa193202 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -28,10 +28,14 @@ module Make : sig type t + type pattern + + val pattern : TransparentState.t option -> constr_pattern -> pattern + val empty : t - val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t - val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t + val add : t -> pattern -> Z.t -> t + val rmv : t -> pattern -> Z.t -> t val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 63cafbf76d..36544883aa 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -144,61 +144,50 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st = } let e_give_exact flags h = - let { hint_term = c; hint_clnv = clenv } = h in let open Tacmach.New in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in - let c, sigma = - if h.hint_poly then - let clenv', subst = Clenv.refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in - let c = Vars.subst_univs_level_constr subst c in - c, evd - else c, sigma - in + let sigma, c = Hints.fresh_hint env sigma h in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> Clenv.unify ~flags t1 <*> exact_no_check c end -let unify_e_resolve flags = begin fun gls (h, _) -> - let clenv', c = connect_hint_clenv h gls in - Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv' - end - -let unify_resolve flags = begin fun gls (h, _) -> - let clenv', _ = connect_hint_clenv h gls in - Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv' +let unify_resolve ~with_evars flags h diff = match diff with +| None -> + Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h +| Some (diff, ty) -> + let () = assert (not h.hint_poly) in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let sigma, c = Hints.fresh_hint env sigma h in + let clenv = mk_clenv_from_env env sigma (Some diff) (c, ty) in + Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv end (** Application of a lemma using [refine] instead of the old [w_unify] *) -let unify_resolve_refine flags gls (h, n) = - let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in +let unify_resolve_refine flags h diff = + let len = match diff with None -> None | Some (diff, _) -> Some diff in + Proofview.Goal.enter begin fun gls -> let open Clenv in let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in Refine.refine ~typecheck:false begin fun sigma -> - let sigma, term, ty = - if h.hint_poly then - let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in - let map c = Vars.subst_univs_level_constr subst c in - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - sigma, map c, map t - else - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - sigma, c, t - in - let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in - let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in - let sigma' = - Evarconv.(unify_leq_delay - ~flags:(default_flags_of flags.core_unify_flags.modulo_delta) - env sigma' cl.cl_concl concl) - in (sigma', term) end - -let unify_resolve_refine flags gl clenv = + let sigma, term = Hints.fresh_hint env sigma h in + let ty = Retyping.get_type_of env sigma term in + let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in + let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in + let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in + let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in + (sigma, term) + end + end + +let unify_resolve_refine flags h diff = Proofview.tclORELSE - (unify_resolve_refine flags gl clenv) + (unify_resolve_refine flags h diff) (fun (exn,info) -> match exn with | Evarconv.UnableToUnify _ -> @@ -211,35 +200,21 @@ let unify_resolve_refine flags gl clenv = (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. *) -let clenv_of_prods nprods h gl = - let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in - if poly || Int.equal nprods 0 then Some (None, clenv) - else - let sigma = Tacmach.New.project gl in - let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in - let diff = nb_prod sigma ty - nprods in - if (>=) diff 0 then - (* Was Some clenv... *) - Some (Some diff, - mk_clenv_from_n gl (Some diff) (c,ty)) - else None - let with_prods nprods h f = if get_typeclasses_limit_intros () then Proofview.Goal.enter begin fun gl -> - try match clenv_of_prods nprods h gl with - | None -> - let info = Exninfo.reify () in - Tacticals.New.tclZEROMSG ~info (str"Not enough premisses") - | Some (diff, clenv') -> - let h = { h with hint_clnv = clenv' } in - f gl (h, diff) - with e when CErrors.noncritical e -> - let e, info = Exninfo.capture e in - Proofview.tclZERO ~info e end + let { hint_term = c; hint_poly = poly } = h in + if poly || Int.equal nprods 0 then f None + else + let sigma = Tacmach.New.project gl in + let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in + let diff = nb_prod sigma ty - nprods in + if (>=) diff 0 then f (Some (diff, ty)) + else Tacticals.New.tclZEROMSG (str"Not enough premisses") + end else Proofview.Goal.enter begin fun gl -> - if Int.equal nprods 0 then f gl (h, None) + if Int.equal nprods 0 then f None else Tacticals.New.tclZEROMSG (str"Not enough premisses") end let matches_pattern concl pat = @@ -347,25 +322,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if get_typeclasses_filtered_unification () then let tac = with_prods nprods h - (fun gl clenv -> + (fun diff -> matches_pattern concl p <*> - unify_resolve_refine flags gl clenv) + unify_resolve_refine flags h diff) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = - with_prods nprods h (unify_resolve flags) in + with_prods nprods h (unify_resolve ~with_evars:false flags h) in Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | ERes_pf h -> if get_typeclasses_filtered_unification () then let tac = (with_prods nprods h - (fun gl clenv -> + (fun diff -> matches_pattern concl p <*> - unify_resolve_refine flags gl clenv)) in + unify_resolve_refine flags h diff)) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = - with_prods nprods h (unify_e_resolve flags) in + with_prods nprods h (unify_resolve ~with_evars:true flags h) in Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | Give_exact h -> @@ -373,12 +348,12 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let tac = matches_pattern concl p <*> Proofview.Goal.enter - (fun gl -> unify_resolve_refine flags gl (h, None)) in + (fun gl -> unify_resolve_refine flags h None) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else e_give_exact flags h | Res_pf_THEN_trivial_fail h -> - let fst = with_prods nprods h (unify_e_resolve flags) in + let fst = with_prods nprods h (unify_resolve ~with_evars:true flags h) in let snd = if complete then Tacticals.New.tclIDTAC else e_trivial_fail_db only_classes db_list local_db secvars in Tacticals.New.tclTHEN fst snd @@ -1235,8 +1210,7 @@ let autoapply c i = (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in - unify_e_resolve flags gl (h, 0) <*> + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*> Proofview.tclEVARMAP >>= (fun sigma -> let sigma = Typeclasses.make_unresolvables (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in diff --git a/tactics/dn.ml b/tactics/dn.ml index e1c9b7c0b5..07eb49442a 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -38,6 +38,8 @@ struct type t = Trie.t + type pattern = (Y.t * int) option list + let empty = Trie.empty (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in @@ -89,11 +91,13 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) in List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm)) - let add tm dna (pat,inf) = - let p = path_of dna pat in Trie.add p (ZSet.singleton inf) tm + let pattern dna pat = path_of dna pat + + let add tm p inf = + Trie.add p (ZSet.singleton inf) tm - let rmv tm dna (pat,inf) = - let p = path_of dna pat in Trie.remove p (ZSet.singleton inf) tm + let rmv tm p inf = + Trie.remove p (ZSet.singleton inf) tm let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm diff --git a/tactics/dn.mli b/tactics/dn.mli index 2a60c3eb82..287aa2b257 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -18,9 +18,13 @@ sig must decompose any tree into a label characterizing its root node and the list of its subtree *) - val add : t -> 'a decompose_fun -> 'a * Z.t -> t + type pattern - val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t + val pattern : 'a decompose_fun -> 'a -> pattern + + val add : t -> pattern -> Z.t -> t + + val rmv : t -> pattern -> Z.t -> t type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 686303a2ab..9a554b117e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -19,7 +19,6 @@ open Tacticals open Tacmach open Evd open Tactics -open Clenv open Auto open Genredexpr open Tactypes @@ -66,10 +65,7 @@ open Auto (***************************************************************************) let unify_e_resolve flags h = - Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv' - end + Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h let hintmap_of sigma secvars concl = (* Warning: for computation sharing, we need to return a closure *) @@ -87,10 +83,10 @@ let hintmap_of sigma secvars concl = let e_exact flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (e_give_exact c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c end let rec e_trivial_fail_db db_list local_db = diff --git a/tactics/equality.ml b/tactics/equality.ml index a2325b69cc..1689b0d3ad 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1416,6 +1416,11 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) +exception NothingToInject +let () = CErrors.register_handler (function + | NothingToInject -> Some (Pp.str "Nothing to inject.") + | _ -> None) + let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in let env = eq_clause.env in @@ -1429,7 +1434,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) | Inr [([],_,_)] -> - tclZEROMSG (str"Nothing to inject.") + Proofview.tclZERO NothingToInject | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) diff --git a/tactics/equality.mli b/tactics/equality.mli index e252eeab28..fdcbbc0e3c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -91,6 +91,7 @@ val discr_tac : evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic (* Below, if flag is [None], it takes the value from the dynamic value of the option *) +exception NothingToInject val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : inj_flags option -> intro_patterns option -> evars_flag -> diff --git a/tactics/hints.ml b/tactics/hints.ml index 386224824f..41b200bb83 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -258,7 +258,7 @@ let empty_se = { let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid -let add_tac pat t st se = +let add_tac pat t se = match pat with | None -> if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se @@ -267,12 +267,14 @@ let add_tac pat t st se = if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se else { se with sentry_pat = List.insert pri_order t se.sentry_pat; - sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); } + sentry_bnet = Bounded_net.add se.sentry_bnet pat t; } let rebuild_dn st se = let dn' = List.fold_left - (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) + (fun dn (id, t) -> + let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in + Bounded_net.add dn pat (id, t)) Bounded_net.empty se.sentry_pat in { se with sentry_bnet = dn' } @@ -636,8 +638,6 @@ struct is_unfold v.code.obj then None else Some gr | None -> None in - let dnst = if db.use_dn then Some db.hintdb_state else None in - let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in match k with | None -> let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in @@ -646,8 +646,14 @@ struct { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } else db | Some gr -> + let pat = + if not db.use_dn && is_exact v.code.obj then None + else + let dnst = if db.use_dn then Some db.hintdb_state else None in + Option.map (fun p -> Bounded_net.pattern dnst p) v.pat + in let oval = find gr db in - { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map } + { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map } let rebuild_db st' db = let db' = @@ -1593,3 +1599,45 @@ struct let repr (h : t) = h.code.obj end + +let connect_hint_clenv h gl = + let { hint_uctx = ctx; hint_clnv = clenv } = h in + (* [clenv] has been generated by a hint-making function, so the only relevant + data in its evarmap is the set of metas. The [evar_reset_evd] function + below just replaces the metas of sigma by those coming from the clenv. *) + let sigma = Tacmach.New.project gl in + let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in + (* Still, we need to update the universes *) + if h.hint_poly then + (* Refresh the instance of the hint *) + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let emap c = Vars.subst_univs_level_constr subst c in + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + (* Only metas are mentioning the old universes. *) + { + templval = Evd.map_fl emap clenv.templval; + templtyp = Evd.map_fl emap clenv.templtyp; + evd = Evd.map_metas emap evd; + env = Proofview.Goal.env gl; + } + else + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + { clenv with evd = evd ; env = Proofview.Goal.env gl } + +let fresh_hint env sigma h = + let { hint_term = c; hint_uctx = ctx } = h in + if h.hint_poly then + (* Refresh the instance of the hint *) + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in + let c = Vars.subst_univs_level_constr subst c in + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + sigma, c + else + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + sigma, c + +let hint_res_pf ?with_evars ?with_classes ?flags h = + Proofview.Goal.enter begin fun gl -> + let clenv = connect_hint_clenv h gl in + Clenv.res_pf ?with_evars ?with_classes ?flags clenv + end diff --git a/tactics/hints.mli b/tactics/hints.mli index 8243716624..f0fed75828 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -39,7 +39,7 @@ type 'a hint_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Genarg.glob_generic_argument (* Hint Extern *) -type hint = { +type hint = private { hint_term : constr; hint_type : types; hint_uctx : Univ.ContextSet.t; @@ -239,6 +239,11 @@ val wrap_hint_warning_fun : env -> evar_map -> (evar_map -> 'a * evar_map) -> 'a * evar_map (** Variant of the above for non-tactics *) +val fresh_hint : env -> evar_map -> hint -> evar_map * constr + +val hint_res_pf : ?with_evars:bool -> ?with_classes:bool -> + ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic + (** Printing hints *) val pr_searchtable : env -> evar_map -> Pp.t diff --git a/tactics/ppred.mli b/tactics/ppred.mli index c68fab5296..3996d7edc8 100644 --- a/tactics/ppred.mli +++ b/tactics/ppred.mli @@ -6,10 +6,15 @@ val pr_with_occurrences : val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t -val pr_red_expr_env : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * +val pr_red_expr : ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> (string -> Pp.t) -> + ('a,'b,'c) red_expr_gen -> Pp.t + +(** Compared to [pr_red_expr], this immediately applied the tuple + elements to the extra arguments. *) +val pr_red_expr_env : 'env -> 'sigma -> + ('env -> 'sigma -> 'a -> Pp.t) * + ('env -> 'sigma -> 'a -> Pp.t) * ('b -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> + ('env -> 'sigma -> 'c -> Pp.t) -> (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t diff --git a/test-suite/Makefile b/test-suite/Makefile index 0935617fbf..f7447d6cec 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -771,8 +771,6 @@ coq-makefile/%.log : coq-makefile/%/run.sh # coqdoc -coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh)) - $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v deleted file mode 100644 index f62f6109e1..0000000000 --- a/test-suite/arithmetic/primitive.v +++ /dev/null @@ -1,12 +0,0 @@ -Section S. - Variable A : Type. - Fail Primitive int : let x := A in Set := #int63_type. - Fail Primitive add := #int63_add. -End S. - -(* [Primitive] should be forbidden in sections, otherwise its type after cooking -will be incorrect: - -Check int. - -*) diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v index 0d034a65eb..ae46117e59 100644 --- a/test-suite/bugs/closed/bug_12483.v +++ b/test-suite/bugs/closed/bug_12483.v @@ -4,7 +4,7 @@ Goal False. Proof. cut (false = true). { intro H; discriminate H. } -change false with (1 <= 0)%float. +change false with (1 <=? 0)%float. rewrite leb_spec. Fail reflexivity. Abort. diff --git a/test-suite/bugs/closed/bug_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v new file mode 100644 index 0000000000..22d95949bb --- /dev/null +++ b/test-suite/bugs/closed/bug_12566_1.v @@ -0,0 +1,16 @@ + +Class C (n:nat) := c{}. + +Instance c0 : C 0 := {}. + +Definition x := 0. + +Opaque x. + +Type _ : C x. +(* this is maybe wrong behaviour, if it changes just update the test *) + +Hint Opaque x : typeclass_instances. +Transparent x. + +Fail Type _ : C x. diff --git a/test-suite/coqdoc/bug12742.html.out b/test-suite/coqdoc/bug12742.html.out new file mode 100644 index 0000000000..75dd185ff9 --- /dev/null +++ b/test-suite/coqdoc/bug12742.html.out @@ -0,0 +1,67 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug12742</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug12742</h1> + +<div class="code"> +</div> + +<div class="doc"> +Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> <i>Xxxxxxxxx xxxxxxx xxxxxxx</i> xxxxxxx "xxxx-xxxxxx" xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx <i>xxxx</i> xx + <i>xxxxx</i> (xx, xxxxxxxxx, <i>xxx'x xxxx: xxx xxx xx xxxx</i>). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + +<div class="paragraph"> </div> + + +</li> +<li> <i>Xxxxx xxxxxxxxxx</i> xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. + +</li> +</ul> + +</div> +<div class="code"> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out new file mode 100644 index 0000000000..d7eba096fc --- /dev/null +++ b/test-suite/coqdoc/bug12742.tex.out @@ -0,0 +1,51 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug12742}{Library }{Coqdoc.bug12742} + +\begin{coqdoccode} +\end{coqdoccode} +Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + + + +\begin{itemize} +\item \textit{Xxxxxxxxx xxxxxxx xxxxxxx} xxxxxxx ``xxxx-xxxxxx'' xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx \textit{xxxx} xx + \textit{xxxxx} (xx, xxxxxxxxx, \textit{xxx'x xxxx: xxx xxx xx xxxx}). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + + + +\item \textit{Xxxxx xxxxxxxxxx} xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. + +\end{itemize} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug12742.v b/test-suite/coqdoc/bug12742.v new file mode 100644 index 0000000000..8ce1faff00 --- /dev/null +++ b/test-suite/coqdoc/bug12742.v @@ -0,0 +1,20 @@ + (** Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + + - _Xxxxxxxxx xxxxxxx xxxxxxx_ xxxxxxx "xxxx-xxxxxx" xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx _xxxx_ xx + _xxxxx_ (xx, xxxxxxxxx, _xxx'x xxxx: xxx xxx xx xxxx_). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + + - _Xxxxx xxxxxxxxxx_ xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. +*) diff --git a/test-suite/coqdoc/details.html.out b/test-suite/coqdoc/details.html.out new file mode 100644 index 0000000000..e1f1ad9867 --- /dev/null +++ b/test-suite/coqdoc/details.html.out @@ -0,0 +1,48 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.details</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.details</h1> + +<div class="code"> +</div> +<details><div class="code"> +<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := 3.<br/> +</div> +</details><div class="code"> + +<br/> +</div> +<details><summary>Foo bar </summary><div class="code"> +<span class="id" title="keyword">Fixpoint</span> <a id="idnat" class="idref" href="#idnat"><span class="id" title="definition">idnat</span></a> (<a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> + | <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Coqdoc.details.html#idnat:2"><span class="id" title="definition">idnat</span></a> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a>)<br/> + | 0 ⇒ 0<br/> + <span class="id" title="keyword">end</span>.<br/> +</div> +</details><div class="code"> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/details.tex.out b/test-suite/coqdoc/details.tex.out new file mode 100644 index 0000000000..37778944ba --- /dev/null +++ b/test-suite/coqdoc/details.tex.out @@ -0,0 +1,44 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.details}{Library }{Coqdoc.details} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol +\coqdocindent{1.00em} +\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/details.v b/test-suite/coqdoc/details.v new file mode 100644 index 0000000000..208e60317d --- /dev/null +++ b/test-suite/coqdoc/details.v @@ -0,0 +1,11 @@ +(* begin details *) +Definition foo : nat := 3. +(* end details *) + +(* begin details : Foo bar *) +Fixpoint idnat (x : nat) : nat := + match x with + | S x => S (idnat x) + | 0 => 0 + end. +(* end details *) diff --git a/test-suite/micromega/bug_12790.v b/test-suite/micromega/bug_12790.v new file mode 100644 index 0000000000..39d640ebd9 --- /dev/null +++ b/test-suite/micromega/bug_12790.v @@ -0,0 +1,8 @@ +Require Import Lia. + +Goal forall (a b c d x: nat), +S c = a - b -> x <= x + (S c) * d. +Proof. +intros a b c d x H. +lia. +Qed. diff --git a/test-suite/micromega/bug_12791.v b/test-suite/micromega/bug_12791.v new file mode 100644 index 0000000000..8aec1904a4 --- /dev/null +++ b/test-suite/micromega/bug_12791.v @@ -0,0 +1,9 @@ +Require Import Lia. + +Definition t := nat. + +Goal forall (a b: t), let c := a in b = a -> b = c. +Proof. + intros a b c H. + lia. +Qed. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9cb019ca56..fa03ec8193 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -119,3 +119,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) +File "stdin", line 297, characters 0-30: +Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] +0 :=: 0 + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b3270d4f92..90d8da2bec 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -290,3 +290,11 @@ Check V tt. Check fun x : nat => V x. End O. + +Module Bug12691. + +Notation "x :=: y" := True (at level 70, no associativity, only parsing). +Notation "x :=: y" := (x = y). +Check (0 :=: 0). + +End Bug12691. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ba316ceb64..b8db52735d 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,7 +7,7 @@ bli : Type Axioms: bli : Type Axioms: -@seq relies on definitional UIP. +seq relies on definitional UIP. Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v index 23d1e5bbae..75fd5c426f 100644 --- a/test-suite/primitive/float/compare.v +++ b/test-suite/primitive/float/compare.v @@ -6,380 +6,380 @@ Definition min_denorm := Eval compute in ldexp one (-1074)%Z. Definition min_norm := Eval compute in ldexp one (-1024)%Z. -Check (eq_refl false : nan == nan = false). -Check (eq_refl false : nan == nan = false). -Check (eq_refl false : nan < nan = false). -Check (eq_refl false : nan < nan = false). -Check (eq_refl false : nan <= nan = false). -Check (eq_refl false : nan <= nan = false). +Check (eq_refl false : nan =? nan = false). +Check (eq_refl false : nan =? nan = false). +Check (eq_refl false : nan <? nan = false). +Check (eq_refl false : nan <? nan = false). +Check (eq_refl false : nan <=? nan = false). +Check (eq_refl false : nan <=? nan = false). Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). Check (eq_refl FNotComparable : nan ?= nan = FNotComparable). -Check (eq_refl false <: nan == nan = false). -Check (eq_refl false <: nan == nan = false). -Check (eq_refl false <: nan < nan = false). -Check (eq_refl false <: nan < nan = false). -Check (eq_refl false <: nan <= nan = false). -Check (eq_refl false <: nan <= nan = false). +Check (eq_refl false <: nan =? nan = false). +Check (eq_refl false <: nan =? nan = false). +Check (eq_refl false <: nan <? nan = false). +Check (eq_refl false <: nan <? nan = false). +Check (eq_refl false <: nan <=? nan = false). +Check (eq_refl false <: nan <=? nan = false). Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable). -Check (eq_refl false <<: nan == nan = false). -Check (eq_refl false <<: nan == nan = false). -Check (eq_refl false <<: nan < nan = false). -Check (eq_refl false <<: nan < nan = false). -Check (eq_refl false <<: nan <= nan = false). -Check (eq_refl false <<: nan <= nan = false). +Check (eq_refl false <<: nan =? nan = false). +Check (eq_refl false <<: nan =? nan = false). +Check (eq_refl false <<: nan <? nan = false). +Check (eq_refl false <<: nan <? nan = false). +Check (eq_refl false <<: nan <=? nan = false). +Check (eq_refl false <<: nan <=? nan = false). Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable). -Check (eq_refl false : nan == - nan = false). -Check (eq_refl false : - nan == nan = false). -Check (eq_refl false : nan < - nan = false). -Check (eq_refl false : - nan < nan = false). -Check (eq_refl false : nan <= - nan = false). -Check (eq_refl false : - nan <= nan = false). +Check (eq_refl false : nan =? - nan = false). +Check (eq_refl false : - nan =? nan = false). +Check (eq_refl false : nan <? - nan = false). +Check (eq_refl false : - nan <? nan = false). +Check (eq_refl false : nan <=? - nan = false). +Check (eq_refl false : - nan <=? nan = false). Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable). -Check (eq_refl false <: nan == - nan = false). -Check (eq_refl false <: - nan == nan = false). -Check (eq_refl false <: nan < - nan = false). -Check (eq_refl false <: - nan < nan = false). -Check (eq_refl false <: nan <= - nan = false). -Check (eq_refl false <: - nan <= nan = false). +Check (eq_refl false <: nan =? - nan = false). +Check (eq_refl false <: - nan =? nan = false). +Check (eq_refl false <: nan <? - nan = false). +Check (eq_refl false <: - nan <? nan = false). +Check (eq_refl false <: nan <=? - nan = false). +Check (eq_refl false <: - nan <=? nan = false). Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable). -Check (eq_refl false <<: nan == - nan = false). -Check (eq_refl false <<: - nan == nan = false). -Check (eq_refl false <<: nan < - nan = false). -Check (eq_refl false <<: - nan < nan = false). -Check (eq_refl false <<: nan <= - nan = false). -Check (eq_refl false <<: - nan <= nan = false). +Check (eq_refl false <<: nan =? - nan = false). +Check (eq_refl false <<: - nan =? nan = false). +Check (eq_refl false <<: nan <? - nan = false). +Check (eq_refl false <<: - nan <? nan = false). +Check (eq_refl false <<: nan <=? - nan = false). +Check (eq_refl false <<: - nan <=? nan = false). Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable). Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable). -Check (eq_refl true : one == one = true). -Check (eq_refl true : one == one = true). -Check (eq_refl false : one < one = false). -Check (eq_refl false : one < one = false). -Check (eq_refl true : one <= one = true). -Check (eq_refl true : one <= one = true). +Check (eq_refl true : one =? one = true). +Check (eq_refl true : one =? one = true). +Check (eq_refl false : one <? one = false). +Check (eq_refl false : one <? one = false). +Check (eq_refl true : one <=? one = true). +Check (eq_refl true : one <=? one = true). Check (eq_refl FEq : one ?= one = FEq). Check (eq_refl FEq : one ?= one = FEq). -Check (eq_refl true <: one == one = true). -Check (eq_refl true <: one == one = true). -Check (eq_refl false <: one < one = false). -Check (eq_refl false <: one < one = false). -Check (eq_refl true <: one <= one = true). -Check (eq_refl true <: one <= one = true). +Check (eq_refl true <: one =? one = true). +Check (eq_refl true <: one =? one = true). +Check (eq_refl false <: one <? one = false). +Check (eq_refl false <: one <? one = false). +Check (eq_refl true <: one <=? one = true). +Check (eq_refl true <: one <=? one = true). Check (eq_refl FEq <: one ?= one = FEq). Check (eq_refl FEq <: one ?= one = FEq). -Check (eq_refl true <<: one == one = true). -Check (eq_refl true <<: one == one = true). -Check (eq_refl false <<: one < one = false). -Check (eq_refl false <<: one < one = false). -Check (eq_refl true <<: one <= one = true). -Check (eq_refl true <<: one <= one = true). +Check (eq_refl true <<: one =? one = true). +Check (eq_refl true <<: one =? one = true). +Check (eq_refl false <<: one <? one = false). +Check (eq_refl false <<: one <? one = false). +Check (eq_refl true <<: one <=? one = true). +Check (eq_refl true <<: one <=? one = true). Check (eq_refl FEq <<: one ?= one = FEq). Check (eq_refl FEq <<: one ?= one = FEq). -Check (eq_refl true : zero == zero = true). -Check (eq_refl true : zero == zero = true). -Check (eq_refl false : zero < zero = false). -Check (eq_refl false : zero < zero = false). -Check (eq_refl true : zero <= zero = true). -Check (eq_refl true : zero <= zero = true). +Check (eq_refl true : zero =? zero = true). +Check (eq_refl true : zero =? zero = true). +Check (eq_refl false : zero <? zero = false). +Check (eq_refl false : zero <? zero = false). +Check (eq_refl true : zero <=? zero = true). +Check (eq_refl true : zero <=? zero = true). Check (eq_refl FEq : zero ?= zero = FEq). Check (eq_refl FEq : zero ?= zero = FEq). -Check (eq_refl true <: zero == zero = true). -Check (eq_refl true <: zero == zero = true). -Check (eq_refl false <: zero < zero = false). -Check (eq_refl false <: zero < zero = false). -Check (eq_refl true <: zero <= zero = true). -Check (eq_refl true <: zero <= zero = true). +Check (eq_refl true <: zero =? zero = true). +Check (eq_refl true <: zero =? zero = true). +Check (eq_refl false <: zero <? zero = false). +Check (eq_refl false <: zero <? zero = false). +Check (eq_refl true <: zero <=? zero = true). +Check (eq_refl true <: zero <=? zero = true). Check (eq_refl FEq <: zero ?= zero = FEq). Check (eq_refl FEq <: zero ?= zero = FEq). -Check (eq_refl true <<: zero == zero = true). -Check (eq_refl true <<: zero == zero = true). -Check (eq_refl false <<: zero < zero = false). -Check (eq_refl false <<: zero < zero = false). -Check (eq_refl true <<: zero <= zero = true). -Check (eq_refl true <<: zero <= zero = true). +Check (eq_refl true <<: zero =? zero = true). +Check (eq_refl true <<: zero =? zero = true). +Check (eq_refl false <<: zero <? zero = false). +Check (eq_refl false <<: zero <? zero = false). +Check (eq_refl true <<: zero <=? zero = true). +Check (eq_refl true <<: zero <=? zero = true). Check (eq_refl FEq <<: zero ?= zero = FEq). Check (eq_refl FEq <<: zero ?= zero = FEq). -Check (eq_refl true : zero == - zero = true). -Check (eq_refl true : - zero == zero = true). -Check (eq_refl false : zero < - zero = false). -Check (eq_refl false : - zero < zero = false). -Check (eq_refl true : zero <= - zero = true). -Check (eq_refl true : - zero <= zero = true). +Check (eq_refl true : zero =? - zero = true). +Check (eq_refl true : - zero =? zero = true). +Check (eq_refl false : zero <? - zero = false). +Check (eq_refl false : - zero <? zero = false). +Check (eq_refl true : zero <=? - zero = true). +Check (eq_refl true : - zero <=? zero = true). Check (eq_refl FEq : zero ?= - zero = FEq). Check (eq_refl FEq : - zero ?= zero = FEq). -Check (eq_refl true <: zero == - zero = true). -Check (eq_refl true <: - zero == zero = true). -Check (eq_refl false <: zero < - zero = false). -Check (eq_refl false <: - zero < zero = false). -Check (eq_refl true <: zero <= - zero = true). -Check (eq_refl true <: - zero <= zero = true). +Check (eq_refl true <: zero =? - zero = true). +Check (eq_refl true <: - zero =? zero = true). +Check (eq_refl false <: zero <? - zero = false). +Check (eq_refl false <: - zero <? zero = false). +Check (eq_refl true <: zero <=? - zero = true). +Check (eq_refl true <: - zero <=? zero = true). Check (eq_refl FEq <: zero ?= - zero = FEq). Check (eq_refl FEq <: - zero ?= zero = FEq). -Check (eq_refl true <<: zero == - zero = true). -Check (eq_refl true <<: - zero == zero = true). -Check (eq_refl false <<: zero < - zero = false). -Check (eq_refl false <<: - zero < zero = false). -Check (eq_refl true <<: zero <= - zero = true). -Check (eq_refl true <<: - zero <= zero = true). +Check (eq_refl true <<: zero =? - zero = true). +Check (eq_refl true <<: - zero =? zero = true). +Check (eq_refl false <<: zero <? - zero = false). +Check (eq_refl false <<: - zero <? zero = false). +Check (eq_refl true <<: zero <=? - zero = true). +Check (eq_refl true <<: - zero <=? zero = true). Check (eq_refl FEq <<: zero ?= - zero = FEq). Check (eq_refl FEq <<: - zero ?= zero = FEq). -Check (eq_refl true : - zero == - zero = true). -Check (eq_refl true : - zero == - zero = true). -Check (eq_refl false : - zero < - zero = false). -Check (eq_refl false : - zero < - zero = false). -Check (eq_refl true : - zero <= - zero = true). -Check (eq_refl true : - zero <= - zero = true). +Check (eq_refl true : - zero =? - zero = true). +Check (eq_refl true : - zero =? - zero = true). +Check (eq_refl false : - zero <? - zero = false). +Check (eq_refl false : - zero <? - zero = false). +Check (eq_refl true : - zero <=? - zero = true). +Check (eq_refl true : - zero <=? - zero = true). Check (eq_refl FEq : - zero ?= - zero = FEq). Check (eq_refl FEq : - zero ?= - zero = FEq). -Check (eq_refl true <: - zero == - zero = true). -Check (eq_refl true <: - zero == - zero = true). -Check (eq_refl false <: - zero < - zero = false). -Check (eq_refl false <: - zero < - zero = false). -Check (eq_refl true <: - zero <= - zero = true). -Check (eq_refl true <: - zero <= - zero = true). +Check (eq_refl true <: - zero =? - zero = true). +Check (eq_refl true <: - zero =? - zero = true). +Check (eq_refl false <: - zero <? - zero = false). +Check (eq_refl false <: - zero <? - zero = false). +Check (eq_refl true <: - zero <=? - zero = true). +Check (eq_refl true <: - zero <=? - zero = true). Check (eq_refl FEq <: - zero ?= - zero = FEq). Check (eq_refl FEq <: - zero ?= - zero = FEq). -Check (eq_refl true <<: - zero == - zero = true). -Check (eq_refl true <<: - zero == - zero = true). -Check (eq_refl false <<: - zero < - zero = false). -Check (eq_refl false <<: - zero < - zero = false). -Check (eq_refl true <<: - zero <= - zero = true). -Check (eq_refl true <<: - zero <= - zero = true). +Check (eq_refl true <<: - zero =? - zero = true). +Check (eq_refl true <<: - zero =? - zero = true). +Check (eq_refl false <<: - zero <? - zero = false). +Check (eq_refl false <<: - zero <? - zero = false). +Check (eq_refl true <<: - zero <=? - zero = true). +Check (eq_refl true <<: - zero <=? - zero = true). Check (eq_refl FEq <<: - zero ?= - zero = FEq). Check (eq_refl FEq <<: - zero ?= - zero = FEq). -Check (eq_refl true : infinity == infinity = true). -Check (eq_refl true : infinity == infinity = true). -Check (eq_refl false : infinity < infinity = false). -Check (eq_refl false : infinity < infinity = false). -Check (eq_refl true : infinity <= infinity = true). -Check (eq_refl true : infinity <= infinity = true). +Check (eq_refl true : infinity =? infinity = true). +Check (eq_refl true : infinity =? infinity = true). +Check (eq_refl false : infinity <? infinity = false). +Check (eq_refl false : infinity <? infinity = false). +Check (eq_refl true : infinity <=? infinity = true). +Check (eq_refl true : infinity <=? infinity = true). Check (eq_refl FEq : infinity ?= infinity = FEq). Check (eq_refl FEq : infinity ?= infinity = FEq). -Check (eq_refl true <: infinity == infinity = true). -Check (eq_refl true <: infinity == infinity = true). -Check (eq_refl false <: infinity < infinity = false). -Check (eq_refl false <: infinity < infinity = false). -Check (eq_refl true <: infinity <= infinity = true). -Check (eq_refl true <: infinity <= infinity = true). +Check (eq_refl true <: infinity =? infinity = true). +Check (eq_refl true <: infinity =? infinity = true). +Check (eq_refl false <: infinity <? infinity = false). +Check (eq_refl false <: infinity <? infinity = false). +Check (eq_refl true <: infinity <=? infinity = true). +Check (eq_refl true <: infinity <=? infinity = true). Check (eq_refl FEq <: infinity ?= infinity = FEq). Check (eq_refl FEq <: infinity ?= infinity = FEq). -Check (eq_refl true <<: infinity == infinity = true). -Check (eq_refl true <<: infinity == infinity = true). -Check (eq_refl false <<: infinity < infinity = false). -Check (eq_refl false <<: infinity < infinity = false). -Check (eq_refl true <<: infinity <= infinity = true). -Check (eq_refl true <<: infinity <= infinity = true). +Check (eq_refl true <<: infinity =? infinity = true). +Check (eq_refl true <<: infinity =? infinity = true). +Check (eq_refl false <<: infinity <? infinity = false). +Check (eq_refl false <<: infinity <? infinity = false). +Check (eq_refl true <<: infinity <=? infinity = true). +Check (eq_refl true <<: infinity <=? infinity = true). Check (eq_refl FEq <<: infinity ?= infinity = FEq). Check (eq_refl FEq <<: infinity ?= infinity = FEq). -Check (eq_refl true : - infinity == - infinity = true). -Check (eq_refl true : - infinity == - infinity = true). -Check (eq_refl false : - infinity < - infinity = false). -Check (eq_refl false : - infinity < - infinity = false). -Check (eq_refl true : - infinity <= - infinity = true). -Check (eq_refl true : - infinity <= - infinity = true). +Check (eq_refl true : - infinity =? - infinity = true). +Check (eq_refl true : - infinity =? - infinity = true). +Check (eq_refl false : - infinity <? - infinity = false). +Check (eq_refl false : - infinity <? - infinity = false). +Check (eq_refl true : - infinity <=? - infinity = true). +Check (eq_refl true : - infinity <=? - infinity = true). Check (eq_refl FEq : - infinity ?= - infinity = FEq). Check (eq_refl FEq : - infinity ?= - infinity = FEq). -Check (eq_refl true <: - infinity == - infinity = true). -Check (eq_refl true <: - infinity == - infinity = true). -Check (eq_refl false <: - infinity < - infinity = false). -Check (eq_refl false <: - infinity < - infinity = false). -Check (eq_refl true <: - infinity <= - infinity = true). -Check (eq_refl true <: - infinity <= - infinity = true). +Check (eq_refl true <: - infinity =? - infinity = true). +Check (eq_refl true <: - infinity =? - infinity = true). +Check (eq_refl false <: - infinity <? - infinity = false). +Check (eq_refl false <: - infinity <? - infinity = false). +Check (eq_refl true <: - infinity <=? - infinity = true). +Check (eq_refl true <: - infinity <=? - infinity = true). Check (eq_refl FEq <: - infinity ?= - infinity = FEq). Check (eq_refl FEq <: - infinity ?= - infinity = FEq). -Check (eq_refl true <<: - infinity == - infinity = true). -Check (eq_refl true <<: - infinity == - infinity = true). -Check (eq_refl false <<: - infinity < - infinity = false). -Check (eq_refl false <<: - infinity < - infinity = false). -Check (eq_refl true <<: - infinity <= - infinity = true). -Check (eq_refl true <<: - infinity <= - infinity = true). +Check (eq_refl true <<: - infinity =? - infinity = true). +Check (eq_refl true <<: - infinity =? - infinity = true). +Check (eq_refl false <<: - infinity <? - infinity = false). +Check (eq_refl false <<: - infinity <? - infinity = false). +Check (eq_refl true <<: - infinity <=? - infinity = true). +Check (eq_refl true <<: - infinity <=? - infinity = true). Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). Check (eq_refl FEq <<: - infinity ?= - infinity = FEq). -Check (eq_refl false : min_denorm == min_norm = false). -Check (eq_refl false : min_norm == min_denorm = false). -Check (eq_refl true : min_denorm < min_norm = true). -Check (eq_refl false : min_norm < min_denorm = false). -Check (eq_refl true : min_denorm <= min_norm = true). -Check (eq_refl false : min_norm <= min_denorm = false). +Check (eq_refl false : min_denorm =? min_norm = false). +Check (eq_refl false : min_norm =? min_denorm = false). +Check (eq_refl true : min_denorm <? min_norm = true). +Check (eq_refl false : min_norm <? min_denorm = false). +Check (eq_refl true : min_denorm <=? min_norm = true). +Check (eq_refl false : min_norm <=? min_denorm = false). Check (eq_refl FLt : min_denorm ?= min_norm = FLt). Check (eq_refl FGt : min_norm ?= min_denorm = FGt). -Check (eq_refl false <: min_denorm == min_norm = false). -Check (eq_refl false <: min_norm == min_denorm = false). -Check (eq_refl true <: min_denorm < min_norm = true). -Check (eq_refl false <: min_norm < min_denorm = false). -Check (eq_refl true <: min_denorm <= min_norm = true). -Check (eq_refl false <: min_norm <= min_denorm = false). +Check (eq_refl false <: min_denorm =? min_norm = false). +Check (eq_refl false <: min_norm =? min_denorm = false). +Check (eq_refl true <: min_denorm <? min_norm = true). +Check (eq_refl false <: min_norm <? min_denorm = false). +Check (eq_refl true <: min_denorm <=? min_norm = true). +Check (eq_refl false <: min_norm <=? min_denorm = false). Check (eq_refl FLt <: min_denorm ?= min_norm = FLt). Check (eq_refl FGt <: min_norm ?= min_denorm = FGt). -Check (eq_refl false <<: min_denorm == min_norm = false). -Check (eq_refl false <<: min_norm == min_denorm = false). -Check (eq_refl true <<: min_denorm < min_norm = true). -Check (eq_refl false <<: min_norm < min_denorm = false). -Check (eq_refl true <<: min_denorm <= min_norm = true). -Check (eq_refl false <<: min_norm <= min_denorm = false). +Check (eq_refl false <<: min_denorm =? min_norm = false). +Check (eq_refl false <<: min_norm =? min_denorm = false). +Check (eq_refl true <<: min_denorm <? min_norm = true). +Check (eq_refl false <<: min_norm <? min_denorm = false). +Check (eq_refl true <<: min_denorm <=? min_norm = true). +Check (eq_refl false <<: min_norm <=? min_denorm = false). Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt). Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt). -Check (eq_refl false : min_denorm == one = false). -Check (eq_refl false : one == min_denorm = false). -Check (eq_refl true : min_denorm < one = true). -Check (eq_refl false : one < min_denorm = false). -Check (eq_refl true : min_denorm <= one = true). -Check (eq_refl false : one <= min_denorm = false). +Check (eq_refl false : min_denorm =? one = false). +Check (eq_refl false : one =? min_denorm = false). +Check (eq_refl true : min_denorm <? one = true). +Check (eq_refl false : one <? min_denorm = false). +Check (eq_refl true : min_denorm <=? one = true). +Check (eq_refl false : one <=? min_denorm = false). Check (eq_refl FLt : min_denorm ?= one = FLt). Check (eq_refl FGt : one ?= min_denorm = FGt). -Check (eq_refl false <: min_denorm == one = false). -Check (eq_refl false <: one == min_denorm = false). -Check (eq_refl true <: min_denorm < one = true). -Check (eq_refl false <: one < min_denorm = false). -Check (eq_refl true <: min_denorm <= one = true). -Check (eq_refl false <: one <= min_denorm = false). +Check (eq_refl false <: min_denorm =? one = false). +Check (eq_refl false <: one =? min_denorm = false). +Check (eq_refl true <: min_denorm <? one = true). +Check (eq_refl false <: one <? min_denorm = false). +Check (eq_refl true <: min_denorm <=? one = true). +Check (eq_refl false <: one <=? min_denorm = false). Check (eq_refl FLt <: min_denorm ?= one = FLt). Check (eq_refl FGt <: one ?= min_denorm = FGt). -Check (eq_refl false <<: min_denorm == one = false). -Check (eq_refl false <<: one == min_denorm = false). -Check (eq_refl true <<: min_denorm < one = true). -Check (eq_refl false <<: one < min_denorm = false). -Check (eq_refl true <<: min_denorm <= one = true). -Check (eq_refl false <<: one <= min_denorm = false). +Check (eq_refl false <<: min_denorm =? one = false). +Check (eq_refl false <<: one =? min_denorm = false). +Check (eq_refl true <<: min_denorm <? one = true). +Check (eq_refl false <<: one <? min_denorm = false). +Check (eq_refl true <<: min_denorm <=? one = true). +Check (eq_refl false <<: one <=? min_denorm = false). Check (eq_refl FLt <<: min_denorm ?= one = FLt). Check (eq_refl FGt <<: one ?= min_denorm = FGt). -Check (eq_refl false : min_norm == one = false). -Check (eq_refl false : one == min_norm = false). -Check (eq_refl true : min_norm < one = true). -Check (eq_refl false : one < min_norm = false). -Check (eq_refl true : min_norm <= one = true). -Check (eq_refl false : one <= min_norm = false). +Check (eq_refl false : min_norm =? one = false). +Check (eq_refl false : one =? min_norm = false). +Check (eq_refl true : min_norm <? one = true). +Check (eq_refl false : one <? min_norm = false). +Check (eq_refl true : min_norm <=? one = true). +Check (eq_refl false : one <=? min_norm = false). Check (eq_refl FLt : min_norm ?= one = FLt). Check (eq_refl FGt : one ?= min_norm = FGt). -Check (eq_refl false <: min_norm == one = false). -Check (eq_refl false <: one == min_norm = false). -Check (eq_refl true <: min_norm < one = true). -Check (eq_refl false <: one < min_norm = false). -Check (eq_refl true <: min_norm <= one = true). -Check (eq_refl false <: one <= min_norm = false). +Check (eq_refl false <: min_norm =? one = false). +Check (eq_refl false <: one =? min_norm = false). +Check (eq_refl true <: min_norm <? one = true). +Check (eq_refl false <: one <? min_norm = false). +Check (eq_refl true <: min_norm <=? one = true). +Check (eq_refl false <: one <=? min_norm = false). Check (eq_refl FLt <: min_norm ?= one = FLt). Check (eq_refl FGt <: one ?= min_norm = FGt). -Check (eq_refl false <<: min_norm == one = false). -Check (eq_refl false <<: one == min_norm = false). -Check (eq_refl true <<: min_norm < one = true). -Check (eq_refl false <<: one < min_norm = false). -Check (eq_refl true <<: min_norm <= one = true). -Check (eq_refl false <<: one <= min_norm = false). +Check (eq_refl false <<: min_norm =? one = false). +Check (eq_refl false <<: one =? min_norm = false). +Check (eq_refl true <<: min_norm <? one = true). +Check (eq_refl false <<: one <? min_norm = false). +Check (eq_refl true <<: min_norm <=? one = true). +Check (eq_refl false <<: one <=? min_norm = false). Check (eq_refl FLt <<: min_norm ?= one = FLt). Check (eq_refl FGt <<: one ?= min_norm = FGt). -Check (eq_refl false : one == infinity = false). -Check (eq_refl false : infinity == one = false). -Check (eq_refl true : one < infinity = true). -Check (eq_refl false : infinity < one = false). -Check (eq_refl true : one <= infinity = true). -Check (eq_refl false : infinity <= one = false). +Check (eq_refl false : one =? infinity = false). +Check (eq_refl false : infinity =? one = false). +Check (eq_refl true : one <? infinity = true). +Check (eq_refl false : infinity <? one = false). +Check (eq_refl true : one <=? infinity = true). +Check (eq_refl false : infinity <=? one = false). Check (eq_refl FLt : one ?= infinity = FLt). Check (eq_refl FGt : infinity ?= one = FGt). -Check (eq_refl false <: one == infinity = false). -Check (eq_refl false <: infinity == one = false). -Check (eq_refl true <: one < infinity = true). -Check (eq_refl false <: infinity < one = false). -Check (eq_refl true <: one <= infinity = true). -Check (eq_refl false <: infinity <= one = false). +Check (eq_refl false <: one =? infinity = false). +Check (eq_refl false <: infinity =? one = false). +Check (eq_refl true <: one <? infinity = true). +Check (eq_refl false <: infinity <? one = false). +Check (eq_refl true <: one <=? infinity = true). +Check (eq_refl false <: infinity <=? one = false). Check (eq_refl FLt <: one ?= infinity = FLt). Check (eq_refl FGt <: infinity ?= one = FGt). -Check (eq_refl false <<: one == infinity = false). -Check (eq_refl false <<: infinity == one = false). -Check (eq_refl true <<: one < infinity = true). -Check (eq_refl false <<: infinity < one = false). -Check (eq_refl true <<: one <= infinity = true). -Check (eq_refl false <<: infinity <= one = false). +Check (eq_refl false <<: one =? infinity = false). +Check (eq_refl false <<: infinity =? one = false). +Check (eq_refl true <<: one <? infinity = true). +Check (eq_refl false <<: infinity <? one = false). +Check (eq_refl true <<: one <=? infinity = true). +Check (eq_refl false <<: infinity <=? one = false). Check (eq_refl FLt <<: one ?= infinity = FLt). Check (eq_refl FGt <<: infinity ?= one = FGt). -Check (eq_refl false : - infinity == infinity = false). -Check (eq_refl false : infinity == - infinity = false). -Check (eq_refl true : - infinity < infinity = true). -Check (eq_refl false : infinity < - infinity = false). -Check (eq_refl true : - infinity <= infinity = true). -Check (eq_refl false : infinity <= - infinity = false). +Check (eq_refl false : - infinity =? infinity = false). +Check (eq_refl false : infinity =? - infinity = false). +Check (eq_refl true : - infinity <? infinity = true). +Check (eq_refl false : infinity <? - infinity = false). +Check (eq_refl true : - infinity <=? infinity = true). +Check (eq_refl false : infinity <=? - infinity = false). Check (eq_refl FLt : - infinity ?= infinity = FLt). Check (eq_refl FGt : infinity ?= - infinity = FGt). -Check (eq_refl false <: - infinity == infinity = false). -Check (eq_refl false <: infinity == - infinity = false). -Check (eq_refl true <: - infinity < infinity = true). -Check (eq_refl false <: infinity < - infinity = false). -Check (eq_refl true <: - infinity <= infinity = true). -Check (eq_refl false <: infinity <= - infinity = false). +Check (eq_refl false <: - infinity =? infinity = false). +Check (eq_refl false <: infinity =? - infinity = false). +Check (eq_refl true <: - infinity <? infinity = true). +Check (eq_refl false <: infinity <? - infinity = false). +Check (eq_refl true <: - infinity <=? infinity = true). +Check (eq_refl false <: infinity <=? - infinity = false). Check (eq_refl FLt <: - infinity ?= infinity = FLt). Check (eq_refl FGt <: infinity ?= - infinity = FGt). -Check (eq_refl false <<: - infinity == infinity = false). -Check (eq_refl false <<: infinity == - infinity = false). -Check (eq_refl true <<: - infinity < infinity = true). -Check (eq_refl false <<: infinity < - infinity = false). -Check (eq_refl true <<: - infinity <= infinity = true). -Check (eq_refl false <<: infinity <= - infinity = false). +Check (eq_refl false <<: - infinity =? infinity = false). +Check (eq_refl false <<: infinity =? - infinity = false). +Check (eq_refl true <<: - infinity <? infinity = true). +Check (eq_refl false <<: infinity <? - infinity = false). +Check (eq_refl true <<: - infinity <=? infinity = true). +Check (eq_refl false <<: infinity <=? - infinity = false). Check (eq_refl FLt <<: - infinity ?= infinity = FLt). Check (eq_refl FGt <<: infinity ?= - infinity = FGt). -Check (eq_refl false : - infinity == one = false). -Check (eq_refl false : one == - infinity = false). -Check (eq_refl true : - infinity < one = true). -Check (eq_refl false : one < - infinity = false). -Check (eq_refl true : - infinity <= one = true). -Check (eq_refl false : one <= - infinity = false). +Check (eq_refl false : - infinity =? one = false). +Check (eq_refl false : one =? - infinity = false). +Check (eq_refl true : - infinity <? one = true). +Check (eq_refl false : one <? - infinity = false). +Check (eq_refl true : - infinity <=? one = true). +Check (eq_refl false : one <=? - infinity = false). Check (eq_refl FLt : - infinity ?= one = FLt). Check (eq_refl FGt : one ?= - infinity = FGt). -Check (eq_refl false <: - infinity == one = false). -Check (eq_refl false <: one == - infinity = false). -Check (eq_refl true <: - infinity < one = true). -Check (eq_refl false <: one < - infinity = false). -Check (eq_refl true <: - infinity <= one = true). -Check (eq_refl false <: one <= - infinity = false). +Check (eq_refl false <: - infinity =? one = false). +Check (eq_refl false <: one =? - infinity = false). +Check (eq_refl true <: - infinity <? one = true). +Check (eq_refl false <: one <? - infinity = false). +Check (eq_refl true <: - infinity <=? one = true). +Check (eq_refl false <: one <=? - infinity = false). Check (eq_refl FLt <: - infinity ?= one = FLt). Check (eq_refl FGt <: one ?= - infinity = FGt). -Check (eq_refl false <<: - infinity == one = false). -Check (eq_refl false <<: one == - infinity = false). -Check (eq_refl true <<: - infinity < one = true). -Check (eq_refl false <<: one < - infinity = false). -Check (eq_refl true <<: - infinity <= one = true). -Check (eq_refl false <<: one <= - infinity = false). +Check (eq_refl false <<: - infinity =? one = false). +Check (eq_refl false <<: one =? - infinity = false). +Check (eq_refl true <<: - infinity <? one = true). +Check (eq_refl false <<: one <? - infinity = false). +Check (eq_refl true <<: - infinity <=? one = true). +Check (eq_refl false <<: one <=? - infinity = false). Check (eq_refl FLt <<: - infinity ?= one = FLt). Check (eq_refl FGt <<: one ?= - infinity = FGt). diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh index cd87eb4e5b..6e3dd6d04b 100755 --- a/test-suite/primitive/float/gen_compare.sh +++ b/test-suite/primitive/float/gen_compare.sh @@ -20,7 +20,7 @@ genTest() { echo >&2 "genTest expects 10 arguments" fi TACTICS=(":" "<:" "<<:") - OPS=("==" "<" "<=" "?=") + OPS=("=?" "<?" "<=?" "?=") x="$1" y="$2" OPS1=("$3" "$4" "$5" "$6") # for x y diff --git a/test-suite/primitive/uint63/eqb.v b/test-suite/primitive/uint63/eqb.v index dcc0b71f6d..43c98e2b6f 100644 --- a/test-suite/primitive/uint63/eqb.v +++ b/test-suite/primitive/uint63/eqb.v @@ -4,14 +4,14 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 == 1 = true). -Check (eq_refl true <: 1 == 1 = true). -Check (eq_refl true <<: 1 == 1 = true). -Definition compute1 := Eval compute in 1 == 1. +Check (eq_refl : 1 =? 1 = true). +Check (eq_refl true <: 1 =? 1 = true). +Check (eq_refl true <<: 1 =? 1 = true). +Definition compute1 := Eval compute in 1 =? 1. Check (eq_refl compute1 : true = true). -Check (eq_refl : 9223372036854775807 == 0 = false). -Check (eq_refl false <: 9223372036854775807 == 0 = false). -Check (eq_refl false <<: 9223372036854775807 == 0 = false). -Definition compute2 := Eval compute in 9223372036854775807 == 0. +Check (eq_refl : 9223372036854775807 =? 0 = false). +Check (eq_refl false <: 9223372036854775807 =? 0 = false). +Check (eq_refl false <<: 9223372036854775807 =? 0 = false). +Definition compute2 := Eval compute in 9223372036854775807 =? 0. Check (eq_refl compute2 : false = false). diff --git a/test-suite/primitive/uint63/leb.v b/test-suite/primitive/uint63/leb.v index 5354919978..e5142282ae 100644 --- a/test-suite/primitive/uint63/leb.v +++ b/test-suite/primitive/uint63/leb.v @@ -4,20 +4,20 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 <= 1 = true). -Check (eq_refl true <: 1 <= 1 = true). -Check (eq_refl true <<: 1 <= 1 = true). -Definition compute1 := Eval compute in 1 <= 1. +Check (eq_refl : 1 <=? 1 = true). +Check (eq_refl true <: 1 <=? 1 = true). +Check (eq_refl true <<: 1 <=? 1 = true). +Definition compute1 := Eval compute in 1 <=? 1. Check (eq_refl compute1 : true = true). -Check (eq_refl : 1 <= 2 = true). -Check (eq_refl true <: 1 <= 2 = true). -Check (eq_refl true <<: 1 <= 2 = true). -Definition compute2 := Eval compute in 1 <= 2. +Check (eq_refl : 1 <=? 2 = true). +Check (eq_refl true <: 1 <=? 2 = true). +Check (eq_refl true <<: 1 <=? 2 = true). +Definition compute2 := Eval compute in 1 <=? 2. Check (eq_refl compute2 : true = true). -Check (eq_refl : 9223372036854775807 <= 0 = false). -Check (eq_refl false <: 9223372036854775807 <= 0 = false). -Check (eq_refl false <<: 9223372036854775807 <= 0 = false). -Definition compute3 := Eval compute in 9223372036854775807 <= 0. +Check (eq_refl : 9223372036854775807 <=? 0 = false). +Check (eq_refl false <: 9223372036854775807 <=? 0 = false). +Check (eq_refl false <<: 9223372036854775807 <=? 0 = false). +Definition compute3 := Eval compute in 9223372036854775807 <=? 0. Check (eq_refl compute3 : false = false). diff --git a/test-suite/primitive/uint63/ltb.v b/test-suite/primitive/uint63/ltb.v index 7ae5ac6493..50cef6be66 100644 --- a/test-suite/primitive/uint63/ltb.v +++ b/test-suite/primitive/uint63/ltb.v @@ -4,20 +4,20 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 1 < 1 = false). -Check (eq_refl false <: 1 < 1 = false). -Check (eq_refl false <<: 1 < 1 = false). -Definition compute1 := Eval compute in 1 < 1. +Check (eq_refl : 1 <? 1 = false). +Check (eq_refl false <: 1 <? 1 = false). +Check (eq_refl false <<: 1 <? 1 = false). +Definition compute1 := Eval compute in 1 <? 1. Check (eq_refl compute1 : false = false). -Check (eq_refl : 1 < 2 = true). -Check (eq_refl true <: 1 < 2 = true). -Check (eq_refl true <<: 1 < 2 = true). -Definition compute2 := Eval compute in 1 < 2. +Check (eq_refl : 1 <? 2 = true). +Check (eq_refl true <: 1 <? 2 = true). +Check (eq_refl true <<: 1 <? 2 = true). +Definition compute2 := Eval compute in 1 <? 2. Check (eq_refl compute2 : true = true). -Check (eq_refl : 9223372036854775807 < 0 = false). -Check (eq_refl false <: 9223372036854775807 < 0 = false). -Check (eq_refl false <<: 9223372036854775807 < 0 = false). -Definition compute3 := Eval compute in 9223372036854775807 < 0. +Check (eq_refl : 9223372036854775807 <? 0 = false). +Check (eq_refl false <: 9223372036854775807 <? 0 = false). +Check (eq_refl false <<: 9223372036854775807 <? 0 = false). +Definition compute3 := Eval compute in 9223372036854775807 <? 0. Check (eq_refl compute3 : false = false). diff --git a/test-suite/primitive/uint63/mod.v b/test-suite/primitive/uint63/mod.v index 5307eed493..3ad6312c2c 100644 --- a/test-suite/primitive/uint63/mod.v +++ b/test-suite/primitive/uint63/mod.v @@ -4,14 +4,14 @@ Set Implicit Arguments. Open Scope int63_scope. -Check (eq_refl : 6 \% 3 = 0). -Check (eq_refl 0 <: 6 \% 3 = 0). -Check (eq_refl 0 <<: 6 \% 3 = 0). -Definition compute1 := Eval compute in 6 \% 3. +Check (eq_refl : 6 mod 3 = 0). +Check (eq_refl 0 <: 6 mod 3 = 0). +Check (eq_refl 0 <<: 6 mod 3 = 0). +Definition compute1 := Eval compute in 6 mod 3. Check (eq_refl compute1 : 0 = 0). -Check (eq_refl : 5 \% 3 = 2). -Check (eq_refl 2 <: 5 \% 3 = 2). -Check (eq_refl 2 <<: 5 \% 3 = 2). -Definition compute2 := Eval compute in 5 \% 3. +Check (eq_refl : 5 mod 3 = 2). +Check (eq_refl 2 <: 5 mod 3 = 2). +Check (eq_refl 2 <<: 5 mod 3 = 2). +Definition compute2 := Eval compute in 5 mod 3. Check (eq_refl compute2 : 2 = 2). diff --git a/test-suite/primitive/uint63/unsigned.v b/test-suite/primitive/uint63/unsigned.v index 82920bd201..6224e9d15b 100644 --- a/test-suite/primitive/uint63/unsigned.v +++ b/test-suite/primitive/uint63/unsigned.v @@ -11,8 +11,8 @@ Check (eq_refl 0 <<: 1/(0-1) = 0). Definition compute1 := Eval compute in 1/(0-1). Check (eq_refl compute1 : 0 = 0). -Check (eq_refl : 3 \% (0-1) = 3). -Check (eq_refl 3 <: 3 \% (0-1) = 3). -Check (eq_refl 3 <<: 3 \% (0-1) = 3). -Definition compute2 := Eval compute in 3 \% (0-1). +Check (eq_refl : 3 mod (0-1) = 3). +Check (eq_refl 3 <: 3 mod (0-1) = 3). +Check (eq_refl 3 <<: 3 mod (0-1) = 3). +Definition compute2 := Eval compute in 3 mod (0-1). Check (eq_refl compute2 : 3 = 3). diff --git a/test-suite/ssr/noting_to_inject.v b/test-suite/ssr/noting_to_inject.v new file mode 100644 index 0000000000..95bbd3e777 --- /dev/null +++ b/test-suite/ssr/noting_to_inject.v @@ -0,0 +1,9 @@ +Require Import ssreflect ssrfun ssrbool. + + +Goal forall b : bool, b -> False. +Set Warnings "+spurious-ssr-injection". +Fail move=> b []. +Set Warnings "-spurious-ssr-injection". +move=> b []. +Abort. diff --git a/test-suite/success/primitive.v b/test-suite/success/primitive.v new file mode 100644 index 0000000000..b2d02a0c49 --- /dev/null +++ b/test-suite/success/primitive.v @@ -0,0 +1,69 @@ +(* This file mostly tests for the error paths in declaring primitives. + Successes are tested in the various test-suite/primitive/* directories *) + +(* [Primitive] should be forbidden in sections, otherwise its type +after cooking will be incorrect. *) +Section S. + Variable A : Type. + Fail Primitive int : let x := A in Set := #int63_type. + Fail Primitive int := #int63_type. (* we fail even if section variable not used *) +End S. +Section S. + Fail Primitive int := #int63_type. (* we fail even if no section variables *) +End S. + +(* can't declare primitives with nonsense types *) +Fail Primitive xx : nat := #int63_type. + +(* non-cumulative conversion *) +Fail Primitive xx : Type := #int63_type. + +(* check evars *) +Fail Primitive xx : let x := _ in Set := #int63_type. + +(* explicit type is unified with expected type, not just converted + + extra universes are OK for monomorphic primitives (even though + their usefulness is questionable, there's no difference compared + with predeclaring them) + *) +Primitive xx : let x := Type in _ := #int63_type. + +(* double declaration *) +Fail Primitive yy := #int63_type. + +Module DoubleCarry. + (* XXX maybe should be an output test: this is the case where the new + declaration is already in the nametab so can be nicely printed *) + Module M. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Register carry as kernel.ind_carry. + End M. + + Module N. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Fail Register carry as kernel.ind_carry. + End N. +End DoubleCarry. + +(* univ polymorphic primitives *) + +(* universe count must be as expected *) +Fail Primitive array@{u v} : Type@{u} -> Type@{v} := #array_type. + +(* use a phantom universe to ensure we check conversion not just the universe count *) +Fail Primitive array@{u} : Set -> Set := #array_type. + +(* no constraints allowed! *) +Fail Primitive array@{u | Set < u} : Type@{u} -> Type@{u} := #array_type. + +(* unification works for polymorphic primitives too (although universe + counts mean it's not enough) *) +Fail Primitive array : let x := Type in _ -> Type := #array_type. +Primitive array : _ -> Type := #array_type. diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v index d3e2749088..3a6dfb1e11 100644 --- a/test-suite/success/sprop.v +++ b/test-suite/success/sprop.v @@ -171,6 +171,10 @@ End sFix. Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0. +(* Check that VM/native properly keep the relevance of the predicate in the case info + (bad-relevance warning as error otherwise) *) +Definition vm_rebuild_case := Eval vm_compute in eq_sind. + Require Import ssreflect. Goal forall T : SProp, T -> True. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 7af09585d0..712cb6a135 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -15,6 +15,7 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. +End toto. (* Check regular failure when statically existing ref does not exist any longer at run time *) @@ -23,4 +24,71 @@ Goal let x := 0 in True. intro x. Fail (clear x; unfold x). Abort. -End toto. + +(* Static analysis of unfold *) + +Module A. + +Opaque id. +Ltac f := unfold id. +Goal id 0 = 0. +Fail f. +Transparent id. +f. +Abort. + +End A. + +Module B. + +Module Type T. Axiom n : nat. End T. + +Module F(X:T). +Ltac f := unfold X.n. +End F. + +Module M. Definition n := 0. End M. +Module N := F M. +Goal match M.n with 0 => 0 | S _ => 1 end = 0. +N.f. +match goal with |- 0=0 => idtac end. +Abort. + +End B. + +Module C. + +(* We reject inductive types and constructors *) + +Fail Ltac g := unfold nat. +Fail Ltac g := unfold S. + +End C. + +Module D. + +(* In interactive mode, we delay the interpretation of short names *) + +Notation x := Nat.add. + +Goal let x := 0 in x = 0+0. +unfold x. +match goal with |- 0 = 0 => idtac end. +Abort. + +Goal let x := 0 in x = 0+0. +intro; unfold x. (* dynamic binding (but is it really the most natural?) *) +match goal with |- 0 = 0+0 => idtac end. +Abort. + +Goal let fst := 0 in fst = Datatypes.fst (0,0). +unfold fst. +match goal with |- 0 = 0 => idtac end. +Abort. + +Goal let fst := 0 in fst = Datatypes.fst (0,0). +intro; unfold fst. (* dynamic binding *) +match goal with |- 0 = Datatypes.fst (0,0) => idtac end. +Abort. + +End D. diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v index 282f56267c..3511ba0918 100644 --- a/theories/Array/PArray.v +++ b/theories/Array/PArray.v @@ -45,19 +45,19 @@ Local Open Scope array_scope. Primitive max_length := #array_max_length. (** Axioms *) -Axiom get_out_of_bounds : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t. +Axiom get_out_of_bounds : forall A (t:array A) i, (i <? length t) = false -> t.[i] = default t. -Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. +Axiom get_set_same : forall A t i (a:A), (i <? length t) = true -> t.[i<-a].[i] = a. Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. Axiom default_set : forall A t i (a:A), default t.[i<-a] = default t. Axiom get_make : forall A (a:A) size i, (make size a).[i] = a. -Axiom leb_length : forall A (t:array A), length t <= max_length = true. +Axiom leb_length : forall A (t:array A), length t <=? max_length = true. Axiom length_make : forall A size (a:A), - length (make size a) = if size <= max_length then size else max_length. + length (make size a) = if size <=? max_length then size else max_length. Axiom length_set : forall A t i (a:A), length t.[i<-a] = length t. @@ -69,7 +69,7 @@ Axiom length_reroot : forall A (t:array A), length (reroot t) = length t. Axiom array_ext : forall A (t1 t2:array A), length t1 = length t2 -> - (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> + (forall i, i <? length t1 = true -> t1.[i] = t2.[i]) -> default t1 = default t2 -> t1 = t2. @@ -77,7 +77,7 @@ Axiom array_ext : forall A (t1 t2:array A), Lemma default_copy A (t:array A) : default (copy t) = default t. Proof. - assert (irr_lt : length t < length t = false). + assert (irr_lt : length t <? length t = false). destruct (Int63.ltbP (length t) (length t)); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. assert (get_copy := get_copy A t (length t)). @@ -87,7 +87,7 @@ Qed. Lemma default_make A (a : A) size : default (make size a) = a. Proof. - assert (irr_lt : length (make size a) < length (make size a) = false). + assert (irr_lt : length (make size a) <? length (make size a) = false). destruct (Int63.ltbP (length (make size a)) (length (make size a))); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. assert (get_make := get_make A a size (length (make size a))). @@ -96,7 +96,7 @@ Qed. Lemma default_reroot A (t:array A) : default (reroot t) = default t. Proof. - assert (irr_lt : length t < length t = false). + assert (irr_lt : length t <? length t = false). destruct (Int63.ltbP (length t) (length t)); try reflexivity. exfalso; eapply BinInt.Z.lt_irrefl; eassumption. assert (get_reroot := get_reroot A t (length t)). @@ -107,16 +107,16 @@ Qed. Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t. Proof. - case_eq (i < length t); intros. + case_eq (i <? length t); intros. rewrite get_set_same; trivial. rewrite get_out_of_bounds, default_set; trivial. rewrite length_set; trivial. Qed. Lemma get_not_default_lt A (t:array A) x : - t.[x] <> default t -> (x < length t) = true. + t.[x] <> default t -> (x <? length t) = true. Proof. intros Hd. - case_eq (x < length t); intros Heq; [trivial | ]. + case_eq (x <? length t); intros Heq; [trivial | ]. elim Hd; rewrite get_out_of_bounds; trivial. Qed. diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v index f4aa1f81c6..78df357c0f 100644 --- a/theories/Floats/FloatAxioms.v +++ b/theories/Floats/FloatAxioms.v @@ -38,9 +38,9 @@ Qed. Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x). Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x). -Axiom eqb_spec : forall x y, (x == y)%float = SFeqb (Prim2SF x) (Prim2SF y). -Axiom ltb_spec : forall x y, (x < y)%float = SFltb (Prim2SF x) (Prim2SF y). -Axiom leb_spec : forall x y, (x <= y)%float = SFleb (Prim2SF x) (Prim2SF y). +Axiom eqb_spec : forall x y, (x =? y)%float = SFeqb (Prim2SF x) (Prim2SF y). +Axiom ltb_spec : forall x y, (x <? y)%float = SFltb (Prim2SF x) (Prim2SF y). +Axiom leb_spec : forall x y, (x <=? y)%float = SFleb (Prim2SF x) (Prim2SF y). Definition flatten_cmp_opt c := match c with diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v index e5a9748481..ed7947aa63 100644 --- a/theories/Floats/PrimFloat.v +++ b/theories/Floats/PrimFloat.v @@ -27,9 +27,11 @@ Register float_class as kernel.ind_f_class. Primitive float := #float64_type. (** ** Syntax support *) +Module Import PrimFloatNotationsInternalA. Declare Scope float_scope. Delimit Scope float_scope with float. Bind Scope float_scope with float. +End PrimFloatNotationsInternalA. Declare ML Module "float_syntax_plugin". @@ -41,31 +43,34 @@ Primitive abs := #float64_abs. Primitive sqrt := #float64_sqrt. Primitive opp := #float64_opp. -Notation "- x" := (opp x) : float_scope. Primitive eqb := #float64_eq. -Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope. Primitive ltb := #float64_lt. -Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope. Primitive leb := #float64_le. -Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope. Primitive compare := #float64_compare. -Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope. Primitive mul := #float64_mul. -Notation "x * y" := (mul x y) : float_scope. Primitive add := #float64_add. -Notation "x + y" := (add x y) : float_scope. Primitive sub := #float64_sub. -Notation "x - y" := (sub x y) : float_scope. Primitive div := #float64_div. + +Module Import PrimFloatNotationsInternalB. +Notation "- x" := (opp x) : float_scope. +Notation "x =? y" := (eqb x y) (at level 70, no associativity) : float_scope. +Notation "x <? y" := (ltb x y) (at level 70, no associativity) : float_scope. +Notation "x <=? y" := (leb x y) (at level 70, no associativity) : float_scope. +Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope. +Notation "x * y" := (mul x y) : float_scope. +Notation "x + y" := (add x y) : float_scope. +Notation "x - y" := (sub x y) : float_scope. Notation "x / y" := (div x y) : float_scope. +End PrimFloatNotationsInternalB. (** ** Conversions *) @@ -114,15 +119,27 @@ Definition neg_zero := Eval compute in (-zero)%float. Definition two := Eval compute in (of_int63 2). (** ** Predicates and helper functions *) -Definition is_nan f := negb (f == f)%float. +Definition is_nan f := negb (f =? f)%float. -Definition is_zero f := (f == zero)%float. (* note: 0 == -0 with floats *) +Definition is_zero f := (f =? zero)%float. (* note: 0 =? -0 with floats *) -Definition is_infinity f := (abs f == infinity)%float. +Definition is_infinity f := (abs f =? infinity)%float. Definition is_finite (x : float) := negb (is_nan x || is_infinity x). (** [get_sign]: return [true] for [-] sign, [false] for [+] sign. *) Definition get_sign f := let f := if is_zero f then (one / f)%float else f in - (f < zero)%float. + (f <? zero)%float. + +Module Export PrimFloatNotations. + Local Open Scope float_scope. + #[deprecated(since="8.13",note="use infix <? instead")] + Notation "x < y" := (x <? y) (at level 70, no associativity) : float_scope. + #[deprecated(since="8.13",note="use infix <=? instead")] + Notation "x <= y" := (x <=? y) (at level 70, no associativity) : float_scope. + #[deprecated(since="8.13",note="use infix =? instead")] + Notation "x == y" := (x =? y) (at level 70, no associativity) : float_scope. + Export PrimFloatNotationsInternalA. + Export PrimFloatNotationsInternalB. +End PrimFloatNotations. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 8ab12ae534..77be679070 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -272,12 +272,18 @@ Proof with auto. - destruct H; subst... Qed. -Definition prod_uncurry (A B C:Type) (f:A * B -> C) +Definition curry {A B C:Type} (f:A * B -> C) (x:A) (y:B) : C := f (x,y). -Definition prod_curry (A B C:Type) (f:A -> B -> C) +Definition uncurry {A B C:Type} (f:A -> B -> C) (p:A * B) : C := match p with (x, y) => f x y end. +#[deprecated(since = "8.13", note = "Use curry instead.")] +Definition prod_uncurry (A B C:Type) : (A * B -> C) -> A -> B -> C := curry. + +#[deprecated(since = "8.13", note = "Use uncurry instead.")] +Definition prod_curry (A B C:Type) : (A -> B -> C) -> A * B -> C := uncurry. + Import EqNotations. Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2), diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c3c69f46f3..e0eae7c287 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -3157,6 +3157,44 @@ Section Repeat. - f_equal; apply IHn. Qed. + Lemma repeat_app x n m : + repeat x (n + m) = repeat x n ++ repeat x m. + Proof. + induction n as [|n IHn]; simpl; auto. + now rewrite IHn. + Qed. + + Lemma repeat_eq_app x n l1 l2 : + repeat x n = l1 ++ l2 -> repeat x (length l1) = l1 /\ repeat x (length l2) = l2. + Proof. + revert n; induction l1 as [|a l1 IHl1]; simpl; intros n Hr; subst. + - repeat split; now rewrite repeat_length. + - destruct n; inversion Hr as [ [Heq Hr0] ]; subst. + now apply IHl1 in Hr0 as [-> ->]. + Qed. + + Lemma repeat_eq_cons x y n l : + repeat x n = y :: l -> x = y /\ repeat x (pred n) = l. + Proof. + intros Hr. + destruct n; inversion_clear Hr; auto. + Qed. + + Lemma repeat_eq_elt x y n l1 l2 : + repeat x n = l1 ++ y :: l2 -> x = y /\ repeat x (length l1) = l1 /\ repeat x (length l2) = l2. + Proof. + intros Hr; apply repeat_eq_app in Hr as [Hr1 Hr2]; subst. + apply repeat_eq_cons in Hr2; intuition. + Qed. + + Lemma Forall_eq_repeat x l : + Forall (eq x) l -> l = repeat x (length l). + Proof. + induction l as [|a l IHl]; simpl; intros HF; auto. + inversion_clear HF as [ | ? ? ? HF']; subst. + now rewrite (IHl HF') at 1. + Qed. + End Repeat. Lemma repeat_to_concat A n (a:A) : diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 5f903c41cb..2a26b6b12a 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -48,7 +48,7 @@ Definition mulc_WW x y := Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : int63_scope. Definition pos_mod p x := - if p <= digits then + if p <=? digits then let p := digits - p in (x << p) >> p else x. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 2c112c3469..383c0aff3a 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -31,56 +31,61 @@ Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. Declare ML Module "int63_syntax_plugin". +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. +End Int63NotationsInternalA. (* Logical operations *) Primitive lsl := #int63_lsl. -Infix "<<" := lsl (at level 30, no associativity) : int63_scope. Primitive lsr := #int63_lsr. -Infix ">>" := lsr (at level 30, no associativity) : int63_scope. Primitive land := #int63_land. -Infix "land" := land (at level 40, left associativity) : int63_scope. Primitive lor := #int63_lor. -Infix "lor" := lor (at level 40, left associativity) : int63_scope. Primitive lxor := #int63_lxor. -Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. (* Arithmetic modulo operations *) Primitive add := #int63_add. -Notation "n + m" := (add n m) : int63_scope. Primitive sub := #int63_sub. -Notation "n - m" := (sub n m) : int63_scope. Primitive mul := #int63_mul. -Notation "n * m" := (mul n m) : int63_scope. Primitive mulc := #int63_mulc. Primitive div := #int63_div. -Notation "n / m" := (div n m) : int63_scope. Primitive mod := #int63_mod. -Notation "n '\%' m" := (mod n m) (at level 40, left associativity) : int63_scope. (* Comparisons *) Primitive eqb := #int63_eq. -Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. Primitive ltb := #int63_lt. -Notation "m < n" := (ltb m n) : int63_scope. Primitive leb := #int63_le. -Notation "m <= n" := (leb m n) : int63_scope. -Notation "m ≤ n" := (leb m n) (at level 70, no associativity) : int63_scope. Local Open Scope int63_scope. +Module Import Int63NotationsInternalB. +Infix "<<" := lsl (at level 30, no associativity) : int63_scope. +Infix ">>" := lsr (at level 30, no associativity) : int63_scope. +Infix "land" := land (at level 40, left associativity) : int63_scope. +Infix "lor" := lor (at level 40, left associativity) : int63_scope. +Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. +Infix "+" := add : int63_scope. +Infix "-" := sub : int63_scope. +Infix "*" := mul : int63_scope. +Infix "/" := div : int63_scope. +Infix "mod" := mod (at level 40, no associativity) : int63_scope. +Infix "=?" := eqb (at level 70, no associativity) : int63_scope. +Infix "<?" := ltb (at level 70, no associativity) : int63_scope. +Infix "<=?" := leb (at level 70, no associativity) : int63_scope. +Infix "≤?" := leb (at level 70, no associativity) : int63_scope. +End Int63NotationsInternalB. + (** The number of digits as a int *) Definition digits := 63. @@ -89,16 +94,16 @@ Definition max_int := Eval vm_compute in 0 - 1. Register Inline max_int. (** Access to the nth digits *) -Definition get_digit x p := (0 < (x land (1 << p))). +Definition get_digit x p := (0 <? (x land (1 << p))). Definition set_digit x p (b:bool) := - if if 0 <= p then p < digits else false then + if if 0 <=? p then p <? digits else false then if b then x lor (1 << p) else x land (max_int lxor (1 << p)) else x. (** Equality to 0 *) -Definition is_zero (i:int) := i == 0. +Definition is_zero (i:int) := i =? 0. Register Inline is_zero. (** Parity *) @@ -113,7 +118,6 @@ Definition bit i n := negb (is_zero ((i >> n) << (digits - 1))). (** Extra modulo operations *) Definition opp (i:int) := 0 - i. Register Inline opp. -Notation "- x" := (opp x) : int63_scope. Definition oppcarry i := max_int - i. Register Inline oppcarry. @@ -134,29 +138,27 @@ Register Inline subcarry. Definition addc_def x y := let r := x + y in - if r < x then C1 r else C0 r. + if r <? x then C1 r else C0 r. (* the same but direct implementation for efficiency *) Primitive addc := #int63_addc. -Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. Definition addcarryc_def x y := let r := addcarry x y in - if r <= x then C1 r else C0 r. + if r <=? x then C1 r else C0 r. (* the same but direct implementation for efficiency *) Primitive addcarryc := #int63_addcarryc. Definition subc_def x y := - if y <= x then C0 (x - y) else C1 (x - y). + if y <=? x then C0 (x - y) else C1 (x - y). (* the same but direct implementation for efficiency *) Primitive subc := #int63_subc. -Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. Definition subcarryc_def x y := - if y < x then C0 (x - y - 1) else C1 (x - y - 1). + if y <? x then C0 (x - y - 1) else C1 (x - y - 1). (* the same but direct implementation for efficiency *) Primitive subcarryc := #int63_subcarryc. -Definition diveucl_def x y := (x/y, x\%y). +Definition diveucl_def x y := (x/y, x mod y). (* the same but direct implementation for efficiency *) Primitive diveucl := #int63_diveucl. @@ -166,6 +168,12 @@ Definition addmuldiv_def p x y := (x << p) lor (y >> (digits - p)). Primitive addmuldiv := #int63_addmuldiv. +Module Import Int63NotationsInternalC. +Notation "- x" := (opp x) : int63_scope. +Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. +Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. +End Int63NotationsInternalC. + Definition oppc (i:int) := 0 -c i. Register Inline oppc. @@ -177,11 +185,10 @@ Register Inline predc. (** Comparison *) Definition compare_def x y := - if x < y then Lt - else if (x == y) then Eq else Gt. + if x <? y then Lt + else if (x =? y) then Eq else Gt. Primitive compare := #int63_compare. -Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. Import Bool ZArith. (** Translation to Z *) @@ -194,8 +201,6 @@ Fixpoint to_Z_rec (n:nat) (i:int) := Definition to_Z := to_Z_rec size. -Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. - Fixpoint of_pos_rec (n:nat) (p:positive) := match n, p with | O, _ => 0 @@ -215,8 +220,12 @@ Definition of_Z z := Definition wB := (2 ^ (Z.of_nat size))%Z. +Module Import Int63NotationsInternalD. +Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. +Notation "'φ' x" := (to_Z x) (at level 0) : int63_scope. Notation "'Φ' x" := (zn2z_to_Z wB to_Z x) (at level 0) : int63_scope. +End Int63NotationsInternalD. Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z. Proof. @@ -347,16 +356,16 @@ Axiom mulc_spec : forall x y, φ x * φ y = φ (fst (mulc x y)) * wB + φ (snd ( Axiom div_spec : forall x y, φ (x / y) = φ x / φ y. -Axiom mod_spec : forall x y, φ (x \% y) = φ x mod φ y. +Axiom mod_spec : forall x y, φ (x mod y) = φ x mod φ y. (* Comparisons *) -Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. +Axiom eqb_correct : forall i j, (i =? j)%int63 = true -> i = j. -Axiom eqb_refl : forall x, (x == x)%int63 = true. +Axiom eqb_refl : forall x, (x =? x)%int63 = true. -Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> φ x < φ y. +Axiom ltb_spec : forall x y, (x <? y)%int63 = true <-> φ x < φ y. -Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> φ x <= φ y. +Axiom leb_spec : forall x y, (x <=? y)%int63 = true <-> φ x <= φ y. (** Exotic operations *) @@ -397,7 +406,7 @@ Local Open Scope int63_scope. Definition sqrt_step (rec: int -> int -> int) (i j: int) := let quo := i / j in - if quo < j then rec i ((j + quo) >> 1) + if quo <? j then rec i ((j + quo) >> 1) else j. Definition iter_sqrt := @@ -421,9 +430,9 @@ Definition high_bit := 1 << (digits - 1). Definition sqrt2_step (rec: int -> int -> int -> int) (ih il j: int) := - if ih < j then + if ih <? j then let (quo,_) := diveucl_21 ih il j in - if quo < j then + if quo <? j then match j +c quo with | C0 m1 => rec ih il (m1 >> 1) | C1 m1 => rec ih il ((m1 >> 1) + high_bit) @@ -448,48 +457,48 @@ Definition sqrt2 ih il := let (ih1, il1) := mulc s s in match il -c il1 with | C0 il2 => - if ih1 < ih then (s, C1 il2) else (s, C0 il2) + if ih1 <? ih then (s, C1 il2) else (s, C0 il2) | C1 il2 => - if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2) + if ih1 <? (ih - 1) then (s, C1 il2) else (s, C0 il2) end. (** Gcd **) Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} := match guard with | O => 1 - | S p => if j == 0 then i else gcd_rec p j (i \% j) + | S p => if j =? 0 then i else gcd_rec p j (i mod j) end. Definition gcd := gcd_rec (2*size). (** equality *) -Lemma eqb_complete : forall x y, x = y -> (x == y) = true. +Lemma eqb_complete : forall x y, x = y -> (x =? y) = true. Proof. intros x y H; rewrite -> H, eqb_refl;trivial. Qed. -Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. +Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y. Proof. split;auto using eqb_correct, eqb_complete. Qed. -Lemma eqb_false_spec : forall x y, (x == y) = false <-> x <> y. +Lemma eqb_false_spec : forall x y, (x =? y) = false <-> x <> y. Proof. intros;rewrite <- not_true_iff_false, eqb_spec;split;trivial. Qed. -Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false. +Lemma eqb_false_complete : forall x y, x <> y -> (x =? y) = false. Proof. intros x y;rewrite eqb_false_spec;trivial. Qed. -Lemma eqb_false_correct : forall x y, (x == y) = false -> x <> y. +Lemma eqb_false_correct : forall x y, (x =? y) = false -> x <> y. Proof. intros x y;rewrite eqb_false_spec;trivial. Qed. Definition eqs (i j : int) : {i = j} + { i <> j } := - (if i == j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) + (if i =? j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true)) else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false))) (eqb_correct i j) @@ -503,7 +512,7 @@ Qed. (* Extra function on equality *) Definition cast i j := - (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) + (if i =? j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) then fun Heq : true = true -> i = j => Some (fun (P : int -> Type) (Hi : P i) => @@ -520,14 +529,14 @@ Proof. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. -Lemma cast_diff : forall i j, i == j = false -> cast i j = None. +Lemma cast_diff : forall i j, i =? j = false -> cast i j = None. Proof. intros;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed. Definition eqo i j := - (if i == j as b return ((b = true -> i = j) -> option (i=j)) + (if i =? j as b return ((b = true -> i = j) -> option (i=j)) then fun Heq : true = true -> i = j => Some (Heq (eq_refl true)) else fun _ : false = true -> i = j => None) (eqb_correct i j). @@ -540,7 +549,7 @@ Proof. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. -Lemma eqo_diff : forall i j, i == j = false -> eqo i j = None. +Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None. Proof. unfold eqo;intros; generalize (eqb_correct i j). rewrite H;trivial. @@ -548,13 +557,13 @@ Qed. (** Comparison *) -Lemma eqbP x y : reflect (φ x = φ y ) (x == y). +Lemma eqbP x y : reflect (φ x = φ y ) (x =? y). Proof. apply iff_reflect; rewrite eqb_spec; split; [ apply to_Z_inj | apply f_equal ]. Qed. -Lemma ltbP x y : reflect (φ x < φ y )%Z (x < y). +Lemma ltbP x y : reflect (φ x < φ y )%Z (x <? y). Proof. apply iff_reflect; symmetry; apply ltb_spec. Qed. -Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤ y). +Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤? y). Proof. apply iff_reflect; symmetry; apply leb_spec. Qed. Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z. @@ -742,7 +751,7 @@ Proof. Qed. Lemma add_le_r m n: - if (n <= m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. + if (n <=? m + n)%int63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. @@ -753,11 +762,11 @@ Proof. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. apply f_equal2 with (f := Zmod); auto with zarith. - case_eq (n <= m + n)%int63; auto. + case_eq (n <=? m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. assert (H1: (φ (m + n) = φ m + φ n)%Z). rewrite add_spec, Zmod_small; auto with zarith. - replace (n <= m + n)%int63 with true; auto. + replace (n <=? m + n)%int63 with true; auto. apply sym_equal; rewrite leb_spec, H1; auto with zarith. Qed. @@ -783,7 +792,7 @@ Proof. apply to_Z_inj; rewrite lsr_spec; reflexivity. Qed. Lemma lsr_0_r i: i >> 0 = i. Proof. apply to_Z_inj; rewrite lsr_spec, Zdiv_1_r; exact eq_refl. Qed. -Lemma lsr_1 n : 1 >> n = (n == 0). +Lemma lsr_1 n : 1 >> n = (n =? 0)%int63. Proof. case eqbP. intros h; rewrite (to_Z_inj _ _ h), lsr_0_r; reflexivity. @@ -798,12 +807,12 @@ Proof. lia. Qed. -Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int63. +Lemma lsr_add i m n: ((i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%int63. Proof. case (to_Z_bounded m); intros H1m H2m. case (to_Z_bounded n); intros H1n H2n. case (to_Z_bounded i); intros H1i H2i. - generalize (add_le_r m n); case (n <= m + n)%int63; intros H. + generalize (add_le_r m n); case (n <=? m + n)%int63; intros H. apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. rewrite add_spec, Zmod_small; auto with zarith. apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. @@ -833,7 +842,7 @@ Proof. apply f_equal2 with (f := Zmod); auto with zarith. Qed. -Lemma lsr_M_r x i (H: (digits <= i = true)%int63) : x >> i = 0%int63. +Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63. Proof. apply to_Z_inj. rewrite lsr_spec, to_Z_0. @@ -889,22 +898,22 @@ Proof. Qed. Lemma bit_lsr x i j : - (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63. + (bit (x >> i) j = if j <=? i + j then bit x (i + j) else false)%int63. Proof. - unfold bit; rewrite lsr_add; case (_ ≤ _); auto. + unfold bit; rewrite lsr_add; case (_ ≤? _); auto. Qed. -Lemma bit_b2i (b: bool) i : bit b i = (i == 0) && b. +Lemma bit_b2i (b: bool) i : bit b i = (i =? 0)%int63 && b. Proof. case b; unfold bit; simpl b2i. - rewrite lsr_1; case (i == 0); auto. + rewrite lsr_1; case (i =? 0)%int63; auto. rewrite lsr0, lsl0, andb_false_r; auto. Qed. -Lemma bit_1 n : bit 1 n = (n == 0). +Lemma bit_1 n : bit 1 n = (n =? 0)%int63. Proof. unfold bit; rewrite lsr_1. - case (_ == _); simpl; auto. + case (_ =? _)%int63; simpl; auto. Qed. Local Hint Resolve Z.lt_gt Z.div_pos : zarith. @@ -929,14 +938,14 @@ Proof. case bit; discriminate. Qed. -Lemma bit_M i n (H: (digits <= n = true)%int63): bit i n = false. +Lemma bit_M i n (H: (digits <=? n = true)%int63): bit i n = false. Proof. unfold bit; rewrite lsr_M_r; auto. Qed. -Lemma bit_half i n (H: (n < digits = true)%int63) : bit (i>>1) n = bit i (n+1). +Lemma bit_half i n (H: (n <? digits = true)%int63) : bit (i>>1) n = bit i (n+1). Proof. unfold bit. rewrite lsr_add. - case_eq (n <= (1 + n))%int63. + case_eq (n <=? (1 + n))%int63. replace (1+n)%int63 with (n+1)%int63; [auto|idtac]. apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto. intros H1; assert (H2: n = max_int). @@ -968,10 +977,10 @@ Proof. Qed. Lemma bit_lsl x i j : bit (x << i) j = -(if (j < i) || (digits <= j) then false else bit x (j - i))%int63. +(if (j <? i) || (digits <=? j) then false else bit x (j - i))%int63. Proof. assert (F1: 1 >= 0) by discriminate. - case_eq (digits <= j)%int63; intros H. + case_eq (digits <=? j)%int63; intros H. rewrite orb_true_r, bit_M; auto. set (d := φ digits). case (Zle_or_lt d (φ j)); intros H1. @@ -1039,10 +1048,10 @@ Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i). Proof. apply bit_ext; intros n. rewrite -> lor_spec, !bit_lsr, lor_spec. - case (_ <= _)%int63; auto. + case (_ <=? _)%int63; auto. Qed. -Lemma lor_le x y : (y <= x lor y)%int63 = true. +Lemma lor_le x y : (y <=? x lor y)%int63 = true. Proof. generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. unfold wB; elim size. @@ -1092,7 +1101,7 @@ Proof. rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. intros m H1 H2. - case_eq (digits <= m)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (digits <=? m)%int63; [idtac | rewrite <- not_true_iff_false]; intros Heq. rewrite bit_M in H1; auto; discriminate. rewrite leb_spec in Heq. @@ -1131,7 +1140,7 @@ Proof. rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. intros _ HH m; case (to_Z_bounded m); intros H1m H2m. - case_eq (digits <= m)%int63. + case_eq (digits <=? m)%int63. intros Hlm; rewrite bit_M; auto; discriminate. rewrite <- not_true_iff_false, leb_spec; intros Hlm. case (Zle_lt_or_eq 0 φ m); auto; intros Hm. @@ -1177,11 +1186,11 @@ Proof. rewrite (fun x y => Zmod_small (x - y)); auto with zarith. intros n; rewrite -> bit_lsl, bit_lsr. generalize (add_le_r (digits - p) n). - case (_ ≤ _); try discriminate. + case (_ ≤? _); try discriminate. rewrite -> sub_spec, Zmod_small; auto with zarith; intros H1. - case_eq (n < p)%int63; try discriminate. + case_eq (n <? p)%int63; try discriminate. rewrite <- not_true_iff_false, ltb_spec; intros H2. - case (_ ≤ _); try discriminate. + case (_ ≤? _); try discriminate. intros _; rewrite bit_M; try discriminate. rewrite -> leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith. rewrite -> sub_spec, Zmod_small; auto with zarith. @@ -1196,7 +1205,7 @@ Proof. apply bit_ext; intros n. rewrite bit_b2i, land_spec, bit_1. generalize (eqb_spec n 0). - case (n == 0); auto. + case (n =? 0)%int63; auto. intros(H,_); rewrite andb_true_r, H; auto. rewrite andb_false_r; auto. Qed. @@ -1373,9 +1382,9 @@ Qed. (* sqrt2 *) Lemma sqrt2_step_def rec ih il j: sqrt2_step rec ih il j = - if (ih < j)%int63 then + if (ih <? j)%int63 then let quo := fst (diveucl_21 ih il j) in - if (quo < j)%int63 then + if (quo <? j)%int63 then let m := match j +c quo with | C0 m1 => m1 >> 1 @@ -1453,7 +1462,7 @@ Proof. apply Zmult_lt_0_compat; auto with zarith. refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } cbv zeta. - case_eq (ih < j)%int63;intros Heq. + case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. 2: rewrite <-not_true_iff_false, ltb_spec in Heq. 2: split; auto. @@ -1462,7 +1471,7 @@ Proof. 2: assert (0 <= φ il/φ j) by (apply Z_div_pos; auto with zarith). 2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. case (Zle_or_lt (2^(Z_of_nat size -1)) φ j); intros Hjj. - case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0. + case_eq (fst (diveucl_21 ih il j) <? j)%int63;intros Heq0. 2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. 2: split; auto; apply sqrt_test_true; auto with zarith. rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. @@ -1557,7 +1566,7 @@ Lemma sqrt2_spec : forall x y, generalize (subc_spec il il1). case subc; intros il2 Hil2. simpl interp_carry in Hil2. - case_eq (ih1 < ih)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (ih1 <? ih)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec; intros Heq. unfold interp_carry; rewrite Zmult_1_l. rewrite -> Z.pow_2_r, Hihl1, Hil2. @@ -1602,7 +1611,7 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded ih); intros H1 H2. split; auto with zarith. apply Z.le_trans with (wB/4 - 1); auto with zarith. - case_eq (ih1 < ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; + case_eq (ih1 <? ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec, Hsih; intros Heq. rewrite Z.pow_2_r, Hihl1. case (Zle_lt_or_eq (φ ih1 + 2) φ ih); auto with zarith. @@ -1927,3 +1936,21 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. + +Module Export Int63Notations. + Local Open Scope int63_scope. + #[deprecated(since="8.13",note="use infix mod instead")] + Notation "a \% m" := (a mod m) (at level 40, left associativity) : int63_scope. + #[deprecated(since="8.13",note="use infix =? instead")] + Notation "m '==' n" := (m =? n) (at level 70, no associativity) : int63_scope. + #[deprecated(since="8.13",note="use infix <? instead")] + Notation "m < n" := (m <? n) : int63_scope. + #[deprecated(since="8.13",note="use infix <=? instead")] + Notation "m <= n" := (m <=? n) : int63_scope. + #[deprecated(since="8.13",note="use infix ≤? instead")] + Notation "m ≤ n" := (m <=? n) (at level 70, no associativity) : int63_scope. + Export Int63NotationsInternalA. + Export Int63NotationsInternalB. + Export Int63NotationsInternalC. + Export Int63NotationsInternalD. +End Int63Notations. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 026cf32ceb..2f445c341a 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -522,6 +522,18 @@ Proof. repeat red; eauto using Permutation_NoDup. Qed. +Lemma Permutation_repeat x n l : + Permutation l (repeat x n) -> l = repeat x n. +Proof. + revert n; induction l as [|y l IHl] ; simpl; intros n HP; auto. + - now apply Permutation_nil in HP; inversion HP. + - assert (y = x) as Heq by (now apply repeat_spec with n, (Permutation_in _ HP); left); subst. + destruct n; simpl; simpl in HP. + + symmetry in HP; apply Permutation_nil in HP; inversion HP. + + f_equal; apply IHl. + now apply Permutation_cons_inv with x. +Qed. + End Permutation_properties. Section Permutation_map. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index aa3c5b9d3b..5d210b2e60 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -504,9 +504,9 @@ rule coq_bol = parse { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf } | space* end_show nl { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf } - | space* begin_details nl - { Lexing.new_line lexbuf; - let s = details_body lexbuf in + | space* begin_details (* At this point, the comment remains open, + and will be closed by [details_body] *) + { let s = details_body lexbuf in Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf } | space* end_details nl { Lexing.new_line lexbuf; @@ -728,7 +728,7 @@ and doc_bol = parse else Output.section lev (fun () -> ignore (doc None (from_string s))); if eol then doc_bol lexbuf else doc None lexbuf } - | (space_nl* as s) ('-'+ as line) + | ((space_nl* nl)? as s) (space* '-'+ as line) { let nl_count = count_newlines s in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index def1cbbcf8..32cf05e1eb 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -838,7 +838,7 @@ module Html = struct printf "<a id=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; List.iter (fun (id,(text,link,t)) -> - let id' = prepare_entry id t in + let id' = escaped (prepare_entry id t) in printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l; printf "<br/><br/>" end diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable deleted file mode 100644 index ffaa7e70f4..0000000000 --- a/vernac/.ocamlformat-enable +++ /dev/null @@ -1 +0,0 @@ -comHints.ml diff --git a/vernac/comHints.ml b/vernac/comHints.ml index b05bf9a675..051560fb63 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -9,6 +9,7 @@ (************************************************************************) open Util +open Names (** (Partial) implementation of the [Hint] command; some more functionality still lives in tactics/hints.ml *) @@ -61,14 +62,24 @@ let project_hint ~poly pri l2r r = cb in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c)) + (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c)) let warn_deprecated_hint_constr = - CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + CWarnings.create ~name:"fragile-hint-constr" ~category:"automation" (fun () -> Pp.strbrk - "Declaring arbitrary terms as hints is deprecated; declare a global \ - reference instead") + "Declaring arbitrary terms as hints is fragile; it is recommended to \ + declare a toplevel constant instead") + +(* Only error when we have to (axioms may be instantiated if from functors) + XXX maybe error if not from a functor argument? + *) +let soft_evaluable = + let open GlobRef in + function + | ConstRef c -> EvalConstRef c + | VarRef id -> EvalVarRef id + | (IndRef _ | ConstructRef _) as r -> Tacred.error_not_evaluable r let interp_hints ~poly h = let env = Global.env () in @@ -88,7 +99,7 @@ let interp_hints ~poly h = Dumpglob.add_glob ?loc:r.CAst.loc gr; gr in - let fr r = Tacred.evaluable_of_global_reference env (fref r) in + let fr r = soft_evaluable (fref r) in let fi c = let open Hints in let open Vernacexpr in @@ -135,7 +146,7 @@ let interp_hints ~poly h = "ind"; List.init (Inductiveops.nconstructors env ind) (fun i -> let c = (ind, i + 1) in - let gr = Names.GlobRef.ConstructRef c in + let gr = GlobRef.ConstructRef c in ( empty_hint_info , Declareops.inductive_is_polymorphic mib , true @@ -147,9 +158,7 @@ let interp_hints ~poly h = let pat = Option.map (fp sigma) patcom in let l = match pat with None -> [] | Some (l, _) -> l in let ltacvars = - List.fold_left - (fun accu x -> Names.Id.Set.add x accu) - Names.Id.Set.empty l + List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in let env = Genintern.{(empty_glob_sign env) with ltacvars} in let _, tacexp = Genintern.generic_intern env tacexp in diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 110dcdc98a..eaa5271a73 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -38,7 +38,13 @@ let do_primitive id udecl prim typopt = Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env) env evd typ in - let evd = Evarconv.unify_delay env evd typ expected_typ in + let evd = try Evarconv.unify_delay env evd typ expected_typ + with Evarconv.UnableToUnify (evd,e) as exn -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (Pretype_errors.( + PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info)) + in + Pretyping.check_evars_are_solved ~program_mode:false env evd; let evd = Evd.minimize_universes evd in let uvars = EConstr.universes_of_constr evd typ in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/declare.ml b/vernac/declare.ml index 12a261517f..eedbee852b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1152,13 +1152,6 @@ let declare_mutual_definition ~pm l = Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) | IsCoFixpoint -> None in - (* In the future we will pack all this in a proper record *) - (* XXX: info refactoring *) - let _kind = - if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) - else Decls.(IsDefinition CoFixpoint) - in - let scope = first.prg_info.Info.scope in (* Declare the recursive definitions *) let kns = declare_mutually_recursive_core ~info:first.prg_info ~ntns:first.prg_notations @@ -1167,6 +1160,7 @@ let declare_mutual_definition ~pm l = in (* Only for the first constant *) let dref = List.hd kns in + let scope = first.prg_info.Info.scope in let s_hook = {Hook.S.uctx = first.prg_uctx; obls; scope; dref} in Hook.call ?hook:first.prg_info.Info.hook s_hook; (* XXX: We call the obligation hook here, by consistency with the @@ -1503,7 +1497,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl = in match cinfo with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { CInfo.name; typ; impargs; _} :: thms -> + | { CInfo.name; typ; _} :: thms -> let pinfo = Proof_info.make ~cinfo ~info ~compute_guard () in (* start_lemma has the responsibility to add (name, impargs, typ) to thms, once Info.t is more refined this won't be necessary *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f9ecf10d1b..762c95fffe 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1252,6 +1252,29 @@ let explain_inductive_error = function error_large_non_prop_inductive_not_in_type () | MissingConstraints csts -> error_inductive_missing_constraints csts +(* Primitive errors *) + +let explain_incompatible_prim_declarations (type a) (act:a Primred.action_kind) (x:a) (y:a) = + let open Primred in + let env = Global.env() in + (* The newer constant/inductive (either coming from Primitive or a + Require) may be absent from the nametab as the error got raised + while adding it to the safe_env. In that case we can't use + nametab printing. + + There are still cases where the constant/inductive is added + separately from its retroknowledge (using Register), so we still + try nametab based printing. *) + match act with + | IncompatTypes typ -> + let px = try pr_constant env x with Not_found -> Constant.print x in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_type_to_string typ) ++ + str ": " ++ pr_constant env y ++ str " is already declared." + | IncompatInd ind -> + let px = try pr_inductive env x with Not_found -> MutInd.print (fst x) in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_ind_to_string ind) ++ + str ": " ++ pr_inductive env y ++ str " is already declared." + (* Recursion schemes errors *) let explain_recursion_scheme_error env = function @@ -1386,6 +1409,8 @@ let rec vernac_interp_error_handler = function explain_typeclass_error env sigma te | InductiveError e -> explain_inductive_error e + | Primred.IncompatibleDeclarations (act,x,y) -> + explain_incompatible_prim_declarations act x y | Modops.ModuleTypingError e -> explain_module_error e | Modintern.ModuleInternalizationError e -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e9b86f323b..6cc48d0e48 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1579,9 +1579,12 @@ let warn_irrelevant_format = 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 { + let format = + if sd.only_parsing && sd.format <> None then (warn_irrelevant_format (); None) + else sd.format in + let pp_rule = make_pp_rule level sd.pp_syntax_data format in + (* We produce a generic rule even if this precise notation is only parsing *) + Some { synext_reserved = reserved; synext_unparsing = (pp_rule,level); synext_extra = sd.extra; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b93c920654..b73e7c7515 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -30,12 +30,34 @@ let tag_vernac = do_not_tag let keyword s = tag_keyword (str s) +let pr_smart_global = Pputils.pr_or_by_notation pr_qualid + +let pr_in_global_env f c : Pp.t = + let env = Global.env () in + let sigma = Evd.from_env env in + f env sigma c + +(* when not !Flags.beautify_file these just ignore the env/sigma *) +let pr_constr_expr = pr_in_global_env pr_constr_expr +let pr_lconstr_expr = pr_in_global_env pr_lconstr_expr +let pr_binders = pr_in_global_env pr_binders +let pr_constr_pattern_expr = pr_in_global_env pr_constr_pattern_expr + +(* In principle this may use the env/sigma, in practice not sure if it + does except through pr_constr_expr in beautify mode. *) +let pr_gen = pr_in_global_env Pputils.pr_raw_generic + +(* No direct Global.env or pr_in_global_env use after this *) + let pr_constr = pr_constr_expr let pr_lconstr = pr_lconstr_expr let pr_spc_lconstr = - let env = Global.env () in - let sigma = Evd.from_env env in - pr_sep_com spc @@ pr_lconstr_expr env sigma + pr_sep_com spc @@ pr_lconstr_expr + +let pr_red_expr = + Ppred.pr_red_expr + (pr_constr_expr, pr_lconstr_expr, pr_smart_global, pr_constr_expr) + keyword let pr_uconstraint (l, d, r) = pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ @@ -80,8 +102,6 @@ let pr_lfqid {CAst.loc;v=fqid} = let pr_lname_decl (n, u) = pr_lname n ++ pr_universe_decl u -let pr_smart_global = Pputils.pr_or_by_notation pr_qualid - let pr_ltac_ref = Libnames.pr_qualid let pr_module = Libnames.pr_qualid @@ -100,11 +120,6 @@ let sep_end = function | VernacEndSubproof -> str"" | _ -> str"." -let pr_gen t = - let env = Global.env () in - let sigma = Evd.from_env env in - Pputils.pr_raw_generic env sigma t - let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() @@ -190,9 +205,7 @@ let pr_search_where = function let pr_search_item = function | SearchSubPattern (where,p) -> - let env = Global.env () in - let sigma = Evd.from_env env in - pr_search_where where ++ pr_constr_pattern_expr env sigma p + pr_search_where where ++ pr_constr_pattern_expr p | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind) @@ -278,10 +291,8 @@ let pr_hints db h pr_c pr_pat = ++ spc() ++ prlist_with_sep spc pr_qualid c | HintsExtern (n,c,tac) -> let pat = match c with None -> mt () | Some pat -> pr_pat pat in - let env = Global.env () in - let sigma = Evd.from_env env in keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ - spc() ++ Pputils.pr_raw_generic env sigma tac + spc() ++ pr_gen tac in hov 2 (keyword "Hint "++ pph ++ opth) @@ -348,9 +359,7 @@ let pr_type_option pr_c = function | _ as c -> brk(0,2) ++ str" :" ++ pr_c c let pr_binders_arg = - let env = Global.env () in - let sigma = Evd.from_env env in - pr_non_empty_arg @@ pr_binders env sigma + pr_non_empty_arg @@ pr_binders let pr_and_type_binders_arg bl = pr_binders_arg bl @@ -470,21 +479,17 @@ let pr_decl_notation prc decl_ntn = ++ pr_opt (fun sc -> str ": " ++ str sc) scopt let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = - let env = Global.env () in - let sigma = Evd.from_env env in let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in - let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in + let annot = pr_guard_annot pr_lconstr_expr binders rec_order in pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot - ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def - ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) rtype + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) body_def + ++ prlist (pr_decl_notation @@ pr_constr) notations let pr_statement head (idpl,(bl,c)) = - let env = Global.env () in - let sigma = Evd.from_env env in hov 2 (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++ - (match bl with [] -> mt() | _ -> pr_binders env sigma bl ++ spc()) ++ + (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_lconstr c) (**************************************) @@ -492,13 +497,9 @@ let pr_statement head (idpl,(bl,c)) = (**************************************) let pr_constrarg c = - let env = Global.env () in - let sigma = Evd.from_env env in - spc () ++ pr_constr env sigma c + spc () ++ pr_constr c let pr_lconstrarg c = - let env = Global.env () in - let sigma = Evd.from_env env in - spc () ++ pr_lconstr env sigma c + spc () ++ pr_lconstr c let pr_intarg n = spc () ++ int n let pr_oc = function @@ -507,23 +508,21 @@ let pr_oc = function | Some false -> str" :>>" let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) = - let env = Global.env () in - let sigma = Evd.from_env env in let prx = match x with | AssumExpr (id,t) -> hov 1 (pr_lname id ++ pr_oc oc ++ spc() ++ - pr_lconstr_expr env sigma t) + pr_lconstr_expr t) | DefExpr(id,b,opt) -> (match opt with | Some t -> hov 1 (pr_lname id ++ pr_oc oc ++ spc() ++ - pr_lconstr_expr env sigma t ++ str" :=" ++ pr_lconstr env sigma b) + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) | None -> hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr env sigma b)) in + pr_lconstr b)) in let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in - prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn + prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn let pr_record_decl c fs = pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ @@ -650,8 +649,6 @@ let pr_extend s cl = let pr_vernac_expr v = let return = tag_vernac v in - let env = Global.env () in - let sigma = Evd.from_env env in match v with | VernacLoad (f,s) -> return ( @@ -783,7 +780,7 @@ let pr_vernac_expr v = | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - Ppred.pr_red_expr_env env sigma (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + pr_red_expr r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -792,7 +789,7 @@ let pr_vernac_expr v = | None -> mt() | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty in - (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr env sigma body)) + (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in @@ -828,7 +825,7 @@ let pr_vernac_expr v = let n = List.length (List.flatten (List.map fst (List.map snd l))) in let pr_params (c, (xl, t)) = hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++ - (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr env sigma t)) in + (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) @@ -854,9 +851,9 @@ let pr_vernac_expr v = (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ pr_and_type_binders_arg indupar ++ pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++ - pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++ + pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++ str" :=") ++ pr_constructor_list lc ++ - prlist (pr_decl_notation @@ pr_constr env sigma) ntn + prlist (pr_decl_notation @@ pr_constr) ntn in let kind = match f with @@ -886,10 +883,10 @@ let pr_vernac_expr v = | NoDischarge -> str "" in let pr_onecorec {fname; univs; binders; rtype; body_def; notations } = - pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr env sigma rtype ++ - pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++ - prlist (pr_decl_notation @@ pr_constr env sigma) notations + pr_ident_decl (fname,univs) ++ spc() ++ pr_binders binders ++ spc() ++ str":" ++ + spc() ++ pr_lconstr_expr rtype ++ + pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) body_def ++ + prlist (pr_decl_notation @@ pr_constr) notations in return ( hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ @@ -968,11 +965,11 @@ let pr_vernac_expr v = | { v = Anonymous }, _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++ + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false - | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr env sigma p + | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) ) @@ -982,7 +979,7 @@ let pr_vernac_expr v = keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ - pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info) + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info) ) | VernacContext l -> @@ -993,7 +990,7 @@ let pr_vernac_expr v = | VernacExistingInstance insts -> let pr_inst (id, info) = - pr_qualid id ++ pr_hint_info (pr_constr_pattern_expr env sigma) info + pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info in return ( hov 1 (keyword "Existing" ++ spc () ++ @@ -1008,25 +1005,25 @@ let pr_vernac_expr v = (* Modules and Module Types *) | VernacDefineModule (export,m,bl,tys,bd) -> - let b = pr_module_binders bl (pr_lconstr env sigma) in + let b = pr_module_binders bl pr_lconstr in return ( hov 2 (keyword "Module" ++ spc() ++ pr_require_token export ++ pr_lident m ++ b ++ - pr_of_module_type (pr_lconstr env sigma) tys ++ + pr_of_module_type pr_lconstr tys ++ (if List.is_empty bd then mt () else str ":= ") ++ prlist_with_sep (fun () -> str " <+") - (pr_module_ast_inl true (pr_lconstr env sigma)) bd) + (pr_module_ast_inl true pr_lconstr) bd) ) | VernacDeclareModule (export,id,bl,m1) -> - let b = pr_module_binders bl (pr_lconstr env sigma) in + let b = pr_module_binders bl pr_lconstr in return ( hov 2 (keyword "Declare Module" ++ spc() ++ pr_require_token export ++ pr_lident id ++ b ++ str " :" ++ - pr_module_ast_inl true (pr_lconstr env sigma) m1) + pr_module_ast_inl true pr_lconstr m1) ) | VernacDeclareModuleType (id,bl,tyl,m) -> - let b = pr_module_binders bl (pr_lconstr env sigma) in - let pr_mt = pr_module_ast_inl true (pr_lconstr env sigma) in + let b = pr_module_binders bl pr_lconstr in + let pr_mt = pr_module_ast_inl true pr_lconstr in return ( hov 2 (keyword "Module Type " ++ pr_lident id ++ b ++ prlist_strict (fun m -> str " <:" ++ pr_mt m) tyl ++ @@ -1034,7 +1031,7 @@ let pr_vernac_expr v = prlist_with_sep (fun () -> str " <+ ") pr_mt m) ) | VernacInclude (mexprs) -> - let pr_m = pr_module_ast_inl false (pr_lconstr env sigma) in + let pr_m = pr_module_ast_inl false pr_lconstr in return ( hov 2 (keyword "Include" ++ spc() ++ prlist_with_sep (fun () -> str " <+ ") pr_m mexprs) @@ -1079,7 +1076,7 @@ let pr_vernac_expr v = pr_opt_hintbases dbnames) ) | VernacHints (dbnames,h) -> - return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma)) + return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) -> return ( hov 2 @@ -1153,7 +1150,7 @@ let pr_vernac_expr v = let n = List.length (List.flatten (List.map fst bl)) in return ( hov 2 (tag_keyword (str"Implicit Type" ++ str (if n > 1 then "s " else " ")) - ++ pr_ne_params_list (pr_lconstr_expr env sigma) (List.map (fun sb -> false,sb) bl)) + ++ pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl)) ) | VernacGeneralizable g -> return ( @@ -1221,9 +1218,9 @@ let pr_vernac_expr v = let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ - spc() ++ keyword "in" ++ spc () ++ pr_lconstr env sigma c) - | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr env sigma c) + pr_red_expr r0 ++ + spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) + | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () | Some i -> Goal_select.pr_goal_selector i ++ str ": " in @@ -1233,12 +1230,12 @@ let pr_vernac_expr v = | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - Ppred.pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + pr_red_expr r ) | VernacPrint p -> return (pr_printable p) | VernacSearch (sea,g,sea_r) -> - return (pr_search sea g sea_r @@ pr_constr_pattern_expr env sigma) + return (pr_search sea g sea_r @@ pr_constr_pattern_expr) | VernacLocate loc -> let pr_locate =function | LocateAny qid -> pr_smart_global qid @@ -1270,7 +1267,7 @@ let pr_vernac_expr v = return ( hov 2 (keyword "Comments" ++ spc() - ++ prlist_with_sep sep (pr_comment (pr_constr env sigma)) l) + ++ prlist_with_sep sep (pr_comment pr_constr) l) ) (* For extension *) @@ -1282,12 +1279,12 @@ let pr_vernac_expr v = return (keyword "Proof " ++ spc () ++ keyword "using" ++ spc() ++ pr_using e) | VernacProof (Some te, None) -> - return (keyword "Proof with" ++ spc() ++ Pputils.pr_raw_generic env sigma te) + return (keyword "Proof with" ++ spc() ++ pr_gen te) | VernacProof (Some te, Some e) -> return ( keyword "Proof" ++ spc () ++ keyword "using" ++ spc() ++ pr_using e ++ spc() ++ - keyword "with" ++ spc() ++ Pputils.pr_raw_generic env sigma te + keyword "with" ++ spc() ++ pr_gen te ) | VernacProofMode s -> return (keyword "Proof Mode" ++ str s) |