| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
|
|
|
|
|
|
|
|
|
|
compat updates to do as part of a release.
|
|
Also test that the compat updating script hasn't become outdated on the
CI.
|
|
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
|
|
All changes done with
```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```
As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497
|
|
Fixes #6764: Printing Notation regressed compared to 8.7
|
|
|
|
|
|
return clause
|
|
|
|
The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".
By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".
See antepenultimate commit for discussion.
|
|
even when no type constraint is given.
This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.
By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.
See penultimate commit for discussion.
|
|
The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.
See previous commit for discussion.
|
|
As noted by Jason Gross on coq-club (Aug 18, 2016), the "small
inversion" heuristic is not used consistently depending on whether the
variables in the type constraint are Rel or Var.
This commit simply gives uniformly preference to the inversion of the
predicate along the indices of the type over other heuristics.
The next three commits will improve further a uniform use of the
different heuristics.
----------------------------------------------------------------------
Here are some extra comments on how to go further with the inference
of the return predicate:
The "small inversion" heuristic build_inversion_problem (1) is
characterized by two features:
- small inversion properly speaking (a), i.e. that is for a match on
t:I params p1(u11..u1p1) ... pn(un1..unpn) with pi exposing the
constructor structure of the indices of the type of t, a return
clause of the form "fun x1..xn (y:I params x1..xn) => match x1..xn y with
| p1(z11..z1p1) ... pn(zn1..znpn) => ?T@{z11..znpn}
| _ => IDProp
end" is used,
- the dependent subterms in the external type constraint U are replaced
by existential variables (b) which can be filled either by projecting
(i.e. installing a dependency) or imitating (i.e. no dependency);
this is obtained by solving the constraint ?T@{u11..unpn} == U by
setting ?T@{z11..znpn} := U'(...?wij@{zij:=uij}...) where U has been
written under the form U'(...uij...) highlighting all occurrences of
each of the uij occurring in U; otherwise said the problem is reduced to
the question of instantiating each wij, deciding whether wij@{zij} := zij
(projection) or wij@{zij} := uij (imitation) [There may be different
way to expose the uij in U, e.g. in the presence of overlapping, or of
evars in U; this is left undetermined].
The two other heuristics used are:
- prepare_predicate_from_arsign_tycon (2): takes the external type
constraint U and decides that each subterm of the form xi or y for a
match on "y:I params x1 ... xn" is dependent; otherwise said, it
corresponds to the degenerated form of (1) where
- no constructor structure is exposed (i.e. each pi is trivial)
- only uij that are Rel are replaced by an evar ?wij and this evar is
directly instantiated by projection (hence creating a dependency),
- simple use of of an evar in case no type constraint is given (3):
this evar is not dependent on the indices nor on the term to match.
Heuristic (1) is not strictly more powerful than other heuristics
because of (at least) two weaknesses.
- The first weakness is due to feature (b), i.e. to letting
unification decide whether these evars have to create a dependency
(projection) or not (imitation).
In particular, the heuristic (2) gives priority to systematic
abstraction over the dependencies (i.e. giving priority to
projection over imitation) and it can then be better as the
following example (from RelationClasses.v) shows:
Fixpoint arrows (l : Tlist) (r : Type) : Type :=
match l with
| Tnil => r
| A :: l' => A -> arrows l' r
end.
Fixpoint predicate_all (l : Tlist) : arrows l Prop -> Prop :=
match l with
| Tnil => fun f => f
| A :: tl => fun f => forall x : A, predicate_all tl (f x)
end.
Using (1) fails. It proposes the predicate
"fun l' => arrows ?l[l':=l'] Prop" so that typing the first branch
leads to unify "arrows ?l[l:=Tnil] Prop == Prop", a problem about
which evarconv unification is not able (yet!) to see what are the
two possible solutions. Using (2) works. It instead directly
suggests that the predicate is "fun l => arrows l Prop" is used, so
that unification is not needed.
Even if in practice the (2) is good (and hence could be added to
(1)), it is not universally better. Consider e.g.
y:bool,H1:P y,H2:P y,f:forall y, P y -> Q y |-
match y as z return Q y with
| true => f y H1
| false => f y H2
end : Q y
There is no way to type it with clause "as z return Q z" even if
trying to generalize H1 and H2 so that they get type P z.
- A second weakness is due to the interaction between small inversion
and constructors having a type whose indices havex a less refined
constructor structure than in the term to match, as in:
Inductive I : nat -> Set :=
| C1 : forall n : nat, listn n -> I n
| C2 : forall n : nat, I n -> I n.
Check (fun x : I 0 => match x with
| C1 n l => 0
| C2 n c => 0
end).
where the inverted predicate is "in I n return match n with 0 => ?T | _ => IDProp end"
but neither C1 nor C2 have fine enough types so that n becomes
constructed. There is a generic solution to that kind of situation which
is to compile the above into
Check (fun x : I 0 => match x with
| C1 n l => match n with 0 => 0 | _ -> id end
| C2 n c => match n with 0 => 0 | _ -> id end
end).
but this is not implemented yet.
In the absence of this refinement, heuristic (3) can here work
better.
So, the current status of the claim is that for (1) to be strictly
more powerful than other current heuristics, work has to be done
- (A) at the unification level (by either being able to reduce problems of
the form "match ?x[constructor] with ... end = a-rigid-term", or, at
worst, by being able to use the heuristic favoring projecting for such
a problem), so that it is better than (2),
- (B) at the match compilation level, by enforcing that, in each branch,
the corresponding constructor is refined so has to match (or
discriminate) the constraints given by the type of the term to
match, and hence being better than (3).
Moreover, (2) and (3) are disjoint. Here is an example which (3) can
solve but not (2) (and (1) cannot because of (B)). [To be fixed in
next commit.]
Inductive I : bool -> bool -> Type := C : I true true | D x : I x x.
Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
match y with
| C => f y H1
| D _ => f y H2
end : Q y z.
Indeed, (2) infers "as y' in I b z return Q y z" which does not work.
Here is an example which (2) can solve but not (3) (and (1) cannot
because of (B) again). [To be fixed in 2nd next commit].
Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
match y with
| C => f y true H1
| D b => f y b H2
end : Q y z.
fix
|
|
This is actually a bit ad hoc at this stage in the sense that this is
specifically to prefer an informative first-order unification failure
over the currently always uninformative failure coming from
second-order unification.
When second-order unification shall be able to give more information,
one may consider alternative strategies, even maybe reporting not just
one but the list of failures in all (interesting) branches.
|
|
It was working in very specific context of section variables. We make
it work similarly in the same kind of specific context of
Parameters. See test file SchemeEquality.v for the expected form. See
discussion at PR #8509.
|
|
|
|
We raise a normal error instead of an anomaly.
|
|
We raise a normal error instead of an anomaly.
This fixes also #2550, #8492.
Note in passing: While the case of a type "Inductive I := list I -> I"
is difficult, the case of a "Inductive I := list nat -> I" should be
easily doable.
|
|
Instead of looking into the name-oriented structure we look into the
actual section structures.
Note: together with #8475 this lets us remove UnivNames.add_global_universe.
|
|
|
|
|
|
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml
version so it makes sense we bump our dependency to 4.05.0 as we can
use some newer compiler features.
|
|
|
|
|
|
|
|
variables.
|
|
|
|
|
|
And update documentation.
|
|
evars by name
|
|
|
|
The regression was introduced in 1522b989 (PR #7193) which itself was
fixing bug #7192. (Note another regression of the same commit which is
fixed in #8416.)
|
|
|
|
When interpreting an existential variable "?n@{inst}" in the current
context, check that variables bound to local definitions are replaced
by variables with convertible body.
Also give a message explaining the type error or non-convertibility
error rather than wrongly saying that there is no binding for the
variable.
|
|
|
|
In particular we check if really used for internal debugging purpose
or to display a message to the user. In the latter case, we replace it
(when possible) by a higher-level printer (e.g. printing foo instead
of Top.foo). In the former case, we clarify that the use is a
debugging use.
Still not perfect (see a few FIXME).
|
|
Zify: replace local definitions by equations
|
|
|
|
|
|
This used to print Var (before #8475, even with explicit binders) but
now doesn't.
|
|
Comes with minor cleanups in exception catching and unnecessary mapi.
|
|
This restores the old behaviour that was printing qualified global names as
a representation of anonymous bound universes, at the cost of a ugly hack.
Ideally this should be handled by the callers, but for the time being the
trade-off is probably OK.
|
|
We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.
This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
|
