| Age | Commit message (Collapse) | Author |
|---|
|
|
|
infrastructure.
The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695
|
|
I'd say this is more of a temporary measure than a long-term plan; IMO
we should make the interfaces safe so `Gramlib.Grammar` does provide
only one signature.
|
|
|
|
This makes sense as a step towards a more functional handling of the
state.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
gramlib
This means we don't need to ignore the result of the fold. cf #10471
Using Format.pp_print_list instead of a custom iteri was suggested by
Jean-Christophe Léchenet (eponier)
|
|
|
|
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.
|
|
|
|
There are still minute uses of type-unsafe primitives. Most of them can be
removed if I had a little higher dan in GADTs (or weeks to spare thinking
about how non-interactive proofs can be performed) but one, which is
really a potential source of unsoundness. The latter is not problematic
as all uses in Coq are protected about the unsoundness proof, but the
API is clearly deficient and needs to be fixed at some point.
|
|
|
|
Not fully used yet, we rely on erasure casts for now.
|
|
|
|
Now that we depend on a module argument, we do not have to quantify
over the arguments anymore.
|
|
The old implementation was simply hiding the fact that the functor relied on
a generic data type. If we want to implement the grammar engine in a truly
type-safe way, we need to make the ancilliary datatypes depend on the type
parameters.
|
|
This module was defining unsafe functions and datatypes only relevant to the
grammar engine. We hide them under the API so as to be able to later clean
it up.
|
|
Reviewed-by: ejgallego
|
|
This was dead code, it was never raised ever.
|
|
They didn't seem to be used at all.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
Apart from the fact we did not use it, its semantics was somewhat flaky as
it was looking for any rule containing some token.
|
|
Due to the fact we only export the functorial API, this property is ensured
statically. There is thus no point in checking it.
|
|
|
|
The references error_verbose and strict_parsing were not accessible from
the API, so their value was statically known.
|
|
This is useless in the functorial API.
|
|
|
|
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`
|
|
|
|
- remove duplicate type definitions `gram_assoc`, `gram_position`,
- make global `warning_verbose` variable into a parameter.
|
|
|
|
|
|
No effect on actual code.
|
|
It was full with utility functions and wrappers that are unused in the Coq
codebase.
|
|
|
|
|
|
This constructor only makes sense in the backtracking mode, that has
been removed from our vendored version of camlp5.
|
|
It is just a wrapper around Sopt. I do not really understand why it is
hardwired in the entry AST.
|
|
Used by rule factorisation in theory, but appears to be unused in Coq.
|
|
It is only used in strict mode, which makes no sense for Coq grammar.
|
