| 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).
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
We remove the functional and backtracking parsers as they are not used
in Coq.
|
|
`for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done`
|
|
|
