| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
This constructor was only used by meta-level macros that are not used and
serve no purpose in the grammar engine.
|
|
|
|
This introduces a bit of noise in the Dune files but for now I think
it is the best way to do it.
|
|
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`
|
|
|
