diff options
| -rw-r--r-- | dev/README.md | 6 | ||||
| -rwxr-xr-x | dev/build/windows/MakeCoq_MinGW.bat | 2 | ||||
| -rw-r--r-- | dev/doc/parsing.md | 397 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 100 | ||||
| -rw-r--r-- | ide/coqide/coq.ml | 3 | ||||
| -rw-r--r-- | plugins/micromega/certificate.ml | 5 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 27 | ||||
| -rw-r--r-- | tactics/equality.ml | 7 | ||||
| -rw-r--r-- | tactics/equality.mli | 1 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12790.v | 8 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12791.v | 9 | ||||
| -rw-r--r-- | test-suite/ssr/noting_to_inject.v | 9 |
15 files changed, 568 insertions, 37 deletions
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/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/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b4b80ca21..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. 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 18149a690a..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`:: + + | "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. - 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. + 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: 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/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/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/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/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. |