| Age | Commit message (Collapse) | Author |
|---|
|
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
|
|
|
|
|
|
We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
|
|
|
|
|
|
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
|
|
deprecated.
|
|
|
|
|
|
|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
|
|
If we need more fine-tuning we should manage the warnings with the
standard Coq mechanism.
|
|
Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.
The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.
This PR doesn't solve that but it is a step towards a more functional
solution.
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
This is not needed anymore after the unification.
|
|
We remove Coq's wrapper over gramlib's grammar constructors.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Warning: in notations, the name "bigint" actually meant "bignat". A
clarification will eventually be needed.
|
|
Add headers to a few files which were missing them.
|
|
Reviewed-by: ppedrot
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
|
|
|
|
They were in Ltac2, but they are of general interest
|
|
This is in preparation for making the Gramlib interface the canonical
one; see #11647 .
I tried to implement some of the ideas that were floated around in a
chat with Pierre-Marie, suggestions / comments are welcome.
|
|
This PR is in preparation of #9067 (together with #11647) .
Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
|
|
This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
|
|
|
|
|
|
|
|
|
|
in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
|
|
|
|
Instead of just string (and empty strings for tokens without payload)
|
|
Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals
Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t
Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
|
|
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
The types are identical and we have no more reason for the split. Note
the following TODOS:
- discrepancy of `Ploc.after` with `CLexer.after`
- discrepancy of `Ploc.comments` with `CLexer.comments`
- `Ploc.dummy` vs `Loc.t option`
|
|
|
|
This was done in a bit of redundant way when we removed the camlp4
compat layer; we fix this and make the type flow clearer.
|
|
- remove duplicate type definitions `gram_assoc`, `gram_position`,
- make global `warning_verbose` variable into a parameter.
|
