| Age | Commit message (Collapse) | Author |
|---|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
sort elimination constraints
Reviewed-by: gares
|
|
This was deactivated in fb1c2a017e but it seems useful (e.g. in
contribs containers).
It seems to be useful
|
|
Ideally, if equations t <= ?x were preserving subtyping that could be
simpler. Currently we need however to put a rigid universe as
constraint on the return predicate so that one branch does not force
the return sort to be lower by unification than what another branch
would have needed.
|
|
If the result is in SProp, Prop or (impredicative) Set, we preserve
this information since the elimination sort might be restricted by the
sort of the destructed type.
If the result is in Type, we use a fresh sort upper bound so that we
are sure not having residual algebraic universes which would raise
problems in a type constraint (e.g. in define_evar_as_product).
This fixes the part of #13278 posted on discourse.
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
An identifier starting with _ deactivates the warning.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
Add headers to a few files which were missing them.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
It goes in an error message so should be fine.
|
|
We thread explicitly the evar map everywhere for this purpose.
|
|
We typecheck arguments like previously, using bidirectionality hints,
but ultimately replace them with user-provided arguments on which we
replay coercion traces.
This is a fix which should be easy to backport, but there are two
directions of future work:
- Coercion traces for `Program` coercions (in these cases, we currently
use the inferred arguments)
- Separate the Coercion API in two phases: inference and application of
coercions. It will make the approach taken here cleaner, and probably
make it easier to interleave typing steps with coercion inference.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
|
|
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
See #9616
|
|
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
|
|
|
|
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
|
|
|
|
There are a couple left which seem OK.
|
|
This avoids all the side effects associated with the manipulation of an
unresolvable flag. In the new design:
- The evar_map stores a set of evars that are candidates for typeclass
resolution, which can be retrieved and set.
We maintain the invariant that it always contains only undefined
evars.
- At the creation time of an evar (new_evar), we classify it as a
potential candidate of resolution.
- This uses a hook to test if the conclusion ends in a typeclass
application. (hook set in typeclasses.ml)
- This is an approximation if the conclusion is an existential (i.e.
not yet determined). In that case we register the evar as
potentially a typeclass instance, and later phases must consider
that case, dropping the evar if it is not a typeclass.
- One can pass the ~typeclass_candidate:false flag to new_evar to
prevent classification entirely. Typically this is for new goals
which should not ever be considered to be typeclass resolution
candidates.
- One can mark a subset of evars unresolvable later if
needed. Typically for clausenv, and marking future goals as
unresolvable even if they are typeclass goals. For clausenv for
example, after turing metas into evars we first (optionally) try a
typeclass resolution on the newly created evars and only then mark
the remaining newly created evars as subgoals. The intent of the
code looks clearer now.
This should prevent keeping testing if undefined evars are classes
all the time and crawling large sets when no typeclasses are present.
- Typeclass candidate evars stay candidates through
restriction/evar-evar solutions.
- Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new
evar is a candidate. There's a deficiency in the API, in most use
cases of Evd.add we should rather use a:
`Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info)
-> evar_map`
Usually it is only about nf_evar'ing the evar_info's contents, which
doesn't change the evar candidate status.
- Typeclass resolution can now handle the set of candidates
functionally: it always starts from the set of candidates (and not the
whole undefined_map) and a filter on it, potentially splitting it in
connected components, does proof search for each component in an
evar_map with an empty set of typeclass evars (allowing clean
reentrancy), then reinstates the potential remaining unsolved
components and filtered out typeclass evars at the end of
resolution.
This means no more marking of resolvability/unresolvability
everywhere, and hopefully a more efficient implementation in general.
- This is on top of the cleanup of evar_info's currently but can
be made independent.
[typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates
Solve bug in inheritance of flags in evar-evar solutions.
Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook
|
|
|
|
All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the
combinators to discourage this style of programming.
Still a few places do use imperative style, but they are pretty
localized and should be cleaned up separately.
As these are the last bits of `e_` API remaining this PR closes #6342.
|
|
|
|
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 refines even further c24bcae8 (PR #924) and 6304c843:
- c24bcae8 fixed the order in the heuristic
- 6304c843 improved the order by preferring projections
There remained a dependency in the alphabetic order in selecting
unification candidates. The current commit fixes it.
We radically change the representation of the substitution to invert
by using a map indexed on the rank in the signature rather than on the
name of the variable.
More could be done to use numbers further, e.g. for representing
aliases.
Note that this has consequences on the test-suite (in
output/Notations.v) as some problems now infer a dependent return
clause.
|
|
|
|
The parts of pattern-matching compilation which generated names may
generate names which collided with names of the Ltac environment.
We fix it by avoiding the names of the Ltac environment.
|
