| Age | Commit message (Collapse) | Author |
|---|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
coercion not being used
Reviewed-by: ejgallego
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
sense
Reviewed-by: Zimmi48
|
|
We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
entries where it already meant "ident".
- "ident" will be made again available (outside situation of
coercions) to mean "ident" at the end of deprecation phase.
Also renaming "as ident" into "as name".
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
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 avoids relying on fragile invariants.
|
|
We at least support a cast at the top of patterns in notations.
|
|
We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
|
|
|
|
between variable and non-qualified global references
Reviewed-by: ejgallego
Ack-by: maximedenes
Ack-by: gares
|
|
|
|
binder
Reviewed-by: herbelin
|
|
then by last imported
Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares
|
|
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
|
|
Reviewed-by: herbelin
|
|
|
|
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
|
|
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot
|
|
The name bound in binders were not checked up to alpha-equivalence,
nor were the names binding the recursive patterns.
|
|
|
|
This allows to know which global references whose basename may be
unexpectedly caught need to be qualified.
Note: the alternative strategy, which is sometimes used, of renaming
the binding variables so as to avoid collisions with the basename of a
global reference is somehow less nice.
|
|
variables.
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: SkySkimmer
|
|
Fix #13249
|
|
reference.
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
This makes it so that we have an application `h a b` with both `a` and
`b` unbound, `a` is the one that is reported (parent commit with my current
compiler setup reports `b` first, and the code does not define which
it should be).
Ideally we would report both but that requires more code.
|
|
It finds "( x , y , .. , z )".
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
E.g. Locate "(x , y , .. , z )" now works while only
Locate "(_ , _ , .. , _ )" was working before.
This also fixes a confusion between a variable and its anonymization
into _, wrongly finding notations mentioning '_'.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
This is a better abstraction barrier (no "symbol" type with
uninterpreted ".." exported out of notation.ml). It also allows to
"browse" notations mentioning a "..".
|
|
|
|
|
|
This allows the following to interpret "0" in the expected scope:
Notation "0" := true : bool_scope.
Axiom f : bool -> bool -> nat.
Record R := { p : bool -> nat }.
Check (@f 0) 0.
Check fun r => r.(@p) 0.
|
|
Reviewed-by: gares
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
naming
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
This will allow for instance to check the status of a variable name
used both as a term and binder in notations.
|
|
Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.
We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.
Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
As noted by Hugo Herbelin, Dec is rather used for "decidable".
|
|
Until now, declaring a number or string notation on some trigger
removed all previous notations on the same scope.
Bug discovered by Jason Gross while reviewing #12218.
|
|
|
|
|
|
This will enable to handle implicit arguments by ignoring them during
preprocessing (before uninterpreting (i.e., printing)) and remplace
them with holes `_` during postprocessing (after interpreting (i.e.,
parsing)).
|
|
This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
|
|
|
