| Age | Commit message (Collapse) | Author |
|---|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
coercion not being used
Reviewed-by: ejgallego
|
|
|
|
In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".
Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.
Incidentally, we create a dedicated output file for notations and
coercions.
|
|
|
|
This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion
|
|
notations.
This also includes tests for abbreviations.
|
|
|
|
Keep Numeral Notation wit a deprecation warning.
|
|
|
|
This is to anticipate further not-only-parsing uses of the notation.
|
|
|
|
This is due to "global" being a syntactic notation, thus including ident.
Parsing was automatically supporting this. This commit adds support for printing.
|
|
entry.
Parsing was automatically supporting this. This commit adds support for printing.
Note: It would be more delicate to recognize that some given entry
support applicative nodes hence abbreviations with arguments.
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
entries)."
This reverts commit 29919b725262dca76708192bde65ce82860747be.
It was pushed by mistake as part of #11530. Sorry about it.
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
|
|
Ceci est une suite à numeral notation in custom entries, cherchant à
raffiner la compatibilité entre entrées. C'est mélangé avec le "pick"
précédent, et c'est en chantier.
|
|
|
|
There was a collision at the time of interpreting subentries (in
metasyntax.ml) but also at the time of "optimizing" the entries (in
egramcoq.ml).
Also fixes #9517, fixes #9519, fixes #9640 (part 3).
|
|
This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.
The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
We restrict #8890 so that it looks for a notation only for the fully
applied coercion.
|
|
- only one space instead of two when printing "{| |}"
- removing a redundant clause in the grammar of record_patterns
|
|
|
|
|
|
|
|
Parameters had to be removed in cases_pattern_of_glob_constr.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
Thanks to Georges Gonthier for noticing it.
Expanding a few Pervasives.compare at this occasion.
|
|
Namely, it does not explicitly open a scope, but we remember that we
don't need the %type delimiter when in type position.
|
|
This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.
Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
|
|
|
|
|
|
See discussion on coq-club starting on 23 August 2016.
|
|
Preferring a notation which does require a delimiter, depending on
whether the coercion is removed or not, was done for primitive tokens.
We do it for all notations.
|
|
Coercions were missing.
|
|
- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
entries. This typically corresponds to rules of the form
'Notation "[ x ]" := x (x custom myconstr).' but also
'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
are natively recognized.
Incidentally merging ETConstr and ETConstrAsBinder.
Noticed in passing that parsing binder as custom was not done as in
constr.
Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
|
