| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
productions.
This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.
The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.
Also exporting less of extend.mli in API.
|
|
|
|
- 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.
|
|
|
|
|
|
|
|
Was apparently forgotten in a67bd7f9.
|
|
We enforce that variables of the notation hide the variables in the
implicit-arguments map.
Will be useful when there will be a special map of single binders
when interpreting notations.
|
|
|
|
|
|
|
|
constraints.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
camlp4
|
|
|
|
|
|
|
|
longer use camlp4.
|
|
|
|
|
|
No using a mutable counter to skip them, instead we keep them in the
environment.
|
|
The only difference is when we have a rel local definition in the
initial environment, which isn't actually possible. However that
depends on the specific way we treat parameters.
|
|
There was no test in the test-suite checking for double with-def constraints
in module typing.
|
|
We defer the computation of the universe quantification to the upper layer,
outside of the kernel.
|
|
|
|
|
|
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
|
|
