| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This was dead code, it was never raised ever.
|
|
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.
|
|
|
|
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.
|
|
This constructor was only used by meta-level macros that are not used and
serve no purpose in the grammar engine.
|
|
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`
|
|
|
