| Age | Commit message (Collapse) | Author |
|---|
|
See discussion on coq-club starting on 23 August 2016.
An open question: what priority to give to "abbreviations"?
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
|
|
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
|
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
|
|
|
|
|
|
|
|
|
This new function is similar to declare_numeral_interpreter,
but works on a lower level : instead of bigint, numbers are
represented as string of their decimal digits (plus a boolean sign)
|
|
This string contains the base-10 representation of the number (big endian)
Note that some inner parsing stuff still uses bigints, see egramcoq.ml
|
|
|
|
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
|
|
|
|
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
|
|
|
|
|
|
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
|
Now it is a private field, locations are optional.
|
|
|
|
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
|
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).
This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
|
|
The ML side lacks a method to query Coq for notations with defined
parsing/printing rules. This commit adds a method
`get_defined_notations` to that purpose.
This is very useful for instance in plugins like SerAPI.
In the medium-term, the `Notation` interface may benefit from a bit of
refactoring to allow programmatic access and manipulation of notations.
|
|
|
|
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
|
more cleanups
|
|
Suggested by @ppedrot
|
|
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
|
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
See 4865.v for details.
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
|
|
|
|
This mechanism relied on functions that are deprecated in recent versions
of ocaml. It was incorrectly used for the most part anyway. The only place
that was using tabulations correctly is "print_loadpath", so there is a
minor regression there: physical paths of short logical paths are no longer
aligned.
|
|
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|
|
|
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
