| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation
The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.
We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.
|
|
If a term is matched only against variables, it will not introduce a
"match" and thus, even if the term is of an inductive type, its
indices will not be taken into account in the current algorithm
(though one could imagine an algorithm which does an expansion
specially in order to filter on indices).
This allows to tell the unification not to use dependencies which the
pattern-matching algorithm is not able to exploit in practice.
See example in file 2733.v.
|
|
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
|
It seems that lifting a term with a negative index is not equivalent to
strengthening it by applying to a dummy substitution. This looks suspicious
at best.
|
|
This ensures that computations are shared as much as possible, mimicking
the "positive" records computational behavior if possible.
|
|
|
|
to anomaly)
|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
|
|
|
|
|
|
|
|
clear_hyps remain with no alternative
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
This is more efficient in general, because Termops.dependent doesn't take
advantage of the knowledge of its pattern argument.
|
|
|
|
We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]
Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.
Now, grepping for `~abort:false` should return the questionable
parts of the system.
Not a lot of places had to be fixed, some comments:
- problems with the interface due to `Evd/Constr` [`Evd.define` being
the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.
A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.
|
|
Answering to commit about #5500: we don't know in general if the
return predicate T(y1,..,yn,x) in the intermediate step of a nested
pattern-matching is a sort, but we don't even know if it is
well-typed: retyping is not enough, we need full typing.
|
|
For instance, error in "Goal forall a f, f a = 0" is now located.
|
|
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.
|
|
|
|
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.
|
