| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
|
|
|
|
|
|
|
|
| |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
|
|
| |
We move the last 3 types to more adequate places.
|
|
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| |
|
|
|
|
|
|
|
|
| |
Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.
We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
|
|
|
|
|
|
| |
The extension mechanism is specific to metasyntax and vernacinterp,
thus it makes sense to place them next to each other.
We also fix the META entry for the `grammar` camlp5 plugin.
|
|
|
|
|
|
| |
There were a few spurious dependencies on the `Vernac` AST in the
pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing,
where they do belong more.
|
|
|
|
|
|
|
| |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.
Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.
This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
|/
|
|
|
|
| |
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
|
|
|
|
|
|
|
|
|
| |
Morally, `library` should not depend on the vernacular
definition. This will also create problems when trying to modularize
the codebase due to the cycle [vernacs depend for example on
constrexprs].
The fix is fortunately easy.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | | |
This command is legacy, equivalent to `EditAt` and only used by
Emacs. We move it to the toplevel so we can kill some legacy code and
in particular the `part_of_script` hack.
|
|/ / |
|
| | |
|
| | |
|
|/
|
|
|
|
| |
This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
|
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
|
|
|
|
|
|
| |
This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.
This supersedes the well-numbered cursed PR #313.
|
|\ |
|
|\ \ |
|
| | | |
|
| | | |
|
|\ \ \
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \
| |_|_|/
|/| | | |
|
| | | | |
|
| |/ /
|/| | |
|
|\ \ \ |
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
|
|\ \ \
| | | |
| | | |
| | | | |
get_lexer_state.
|
| |/ /
|/| | |
|
| |/
|/| |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.
We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).
Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.
Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.
Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
|
| |
| |
| |
| | |
For compatibility, the default is to parse as ident and not as pattern.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
|
| |
| |
| |
| |
| |
| | |
- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions
|
| |
| |
| |
| | |
Renaming it register_grammars_by_name.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This allows in particular to define notations with 'pat style binders.
E.g.:
A non-trivial change in this commit is storing binders and patterns
separately from terms.
This is not strictly necessary but has some advantages.
However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).
So, it is as simple to always store idents (and eventually patterns)
as terms.
|