| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This should preserve semantics exactly.
In the compute_implicits family of functions, I changed the
name of the pushed rel to not be fresh, but the env isn't passed
to find_displayed_name_in, and shouldn't affect whd_all.
|
| |/ / / |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Constrextern.explicitize expected that if implicits were declared they
would be declared at least up to the principal argument of the
projection, but Context/discharge of implicits does not preserve this.
Note the anomaly only happens with primitive projections DISABLED in
recent Coqs (>=8.8).
Implicit argument experts may consider whether ensuring enough
implicits are declared would be better.
|
| | |/ / |
|
| |/ / |
|
| |/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
notation to use among several of them"
This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
|
| |\ |
|
| |\ \ |
|
| | |/
|/| |
|
| | | |
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Fix new deprecation warnings in the standard library.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
| |\ \
| | |
| | |
| | | |
infinite eta-expansion)
|
| | |/
|/| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
More precisely when matching
"f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z"
do not allow expansion of f since otherwise, we recursively have to
match "f t" with the same pattern.
|
| |/
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
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
|
| |
|
|
|
|
|
| |
We generalize the possibility to refer to a notation not only by its
"_ U _" form but also using its "a 'U' b".
(Wish from EJGA)
|
| |
|
|
|
|
|
|
| |
We reason up to order, and accept to match a final catch-all clauses
with any other clause.
This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
|
| |
|
|
|
| |
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
|
| |
|
|
|
|
| |
Example which is now reprinted as parsed:
fun '((x,y) as z) => (y,x)=z
|
| |
|
|
|
|
|
|
|
|
|
|
| |
To deal with existing notations starting with a "let" (see notation
"for" in output/Notation2.v) we adopt the pragmatic approach of
glueing only inner let by default.
Ideally, it might be nicer to detect if there is an overlap of
notation, and not to glue only in case of overlap. We could also
decide that a notation starting with a "let" should always be
protected by some constant, say "id", so as to avoid possible
collisions, but this would require changes user side.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.
We let the general case absorb this particular case.
We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).
Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
| |
For instance, the following is now possible:
Check {(x,y)|x+y=0}.
Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
|
| |
|
|
|
|
| |
Reordering the maps for binders and terms while uninterpreting a
notation the same way it will be at the time of interpreting a
notation.
|
| |
|
|
|
| |
Factorizing the place where the different form of extended binders
(i.e. possibly including the 'pat form) are matched.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
(binders shall be substitutable by arbitrary cases patterns).
Giving a proper status to the functions unifying different instance of
the same notation variable (up to alpha-renaming).
Note: The a priori change of semantics in "bind_binding_as_term_env"
which now apply renaming from "unify_id" (as it did in
"bind_bindinglist_as_term_env") should not have an effect since, as
the former comment said, this corresponds to a "Anonymous" case which
should not occur, since the term would have to be bound upwards.
|
| |
|
|
| |
Moving earlier functions which will be needed earlier.
|
| | |
|
| |
|
|
| |
(binders shall be substitutable by arbitrary cases patterns).
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Seizing this opportunity to generalize the possibility for different
associativity into simply reversing the order or not. Also dropping
some dead code.
Example of recursive notation now working:
Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
|
| |
|
|
|
|
|
|
| |
This allows for instance to support recursive notations of the form:
Notation "! x .. y # A #" :=
(((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
(at level 200, x binder).
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.
Example of (artificial) notation that this commit supports:
Notation "! x .. y # A #" :=
(.. (A,(forall x, True)) ..,(forall y, True))
(at level 200, x binder).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- The "terminator" of a recursive notation is now interpreted in the
environment in which it occurs rather than the environment at the
beginning of the recursive patterns.
Note that due to a tolerance in checking unbound variables of
notations, a variable unbound in the environment was still working
ok as long as no user-given variable was shadowing a private
variable of the notation - see the "exists_mixed" example in
test-suite.
Conversely, in a notation such as:
Notation "!! x .. y # A #" :=
((forall x, True), .. ((forall y, True), A) ..)
(at level 200, x binder).
Check !! a b # a=b #.
The unbound "a" was detected only at pretyping and not as expected
at internalizing time, due to "a=b" interpreted in context
containing a and b.
- Similarly, each binder is now interpreted in the environment in
which it occurs rather than as if the sequence of binders was
dependent from the left to the right (such a dependency was ok for
"forall" or "exists" but not in general).
For instance, in:
Notation "!! x .. y # A #" :=
((forall x, True), .. ((forall y, True), A) ..)
(at level 200, x binder).
Check !! (a:nat) (b:a=a) # True #.
The illegal dependency of the type of b in a was detected only at
pretyping time.
- If a let-in occurs in the sequence of binders of a notation with a
recursive pattern, it is now inserted in between the occurrences of
the iterator rather than glued with the forall/fun of the iterator.
For instance, in:
Notation "'exists_true' x .. y , P" :=
(exists x, True /\ .. (exists y, True /\ P) ..)
(at level 200, x binder).
Check exists_true '(x,y) (u:=0), x=y.
We now get
exists '(x, y), True /\ (let u := 0 in True /\ x = y)
while we had before the let-in breaking the repeated pattern:
exists '(x, y), (let u := 0 in True /\ x = y)
This is more compositional, and, in particular, the printer algorithm
now recognizes the pattern which is otherwise broken.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
- renaming lvar into ntnvars when relevant, for consistency
- renaming sometimes genv into env (intern_env) so as to remain
consistent with other parts of the code
|
| |
|
|
| |
This works for contexts in Definition and co, but not yet for "fun" and co.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The motivations are:
- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
before this patch, there is a different treatment of `Definition f
'(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
to interpret `Definition f `pat := c : t`. With the patch, the fix
to avoid seeing a variable named `pat` works for both `fun 'x =>
...` and `Definition f 'x := ...`.
The drawbacks are:
- Counterpart to reflecting the concrete syntax more closerly, there
are more redundancies in the syntax. For instance, the case `CLetIn
(na,b,t,c)` can appears also in the form `CProdN (CLocalDef
(na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
|
Jasper Hugunin
Maxime Dénès
Hugo Herbelin
Gaëtan Gilbert
Emilio Jesus Gallego Arias
mrmr1993
Théo Zimmermann