| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
| |
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
| |
|
|
|
|
| |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This was broken by the attempt to use the same algorithm for rewriting
closed subterms than for rewriting subterms with evars: the algorithm
to find subterms (w_unify_to_subterm) did not go through evars. But
what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"?
Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look
in the instance? If we adopt the first approach, then, what to do when
looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the
instance? Is it normal that an evar behaves as a rigid constant when
it cannot be unified with the pattern?
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
| | |
|
| |
|
|
| |
initial segment of the context of the evar.
|
| |
|
|
| |
unification flags (see also temporary revert in d083200ae5b).
|
| | |
|
| |
|
|
|
|
|
|
| |
- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.
|
| |
|
|
|
|
| |
Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags."
This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968.
|
| |
|
|
| |
This fixes current failure of RelationAlgebra.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
- new function set_flags_for_type for setting flags when converting
types of the terms to unify
- it now sets all conversion flags, possibly restricting delta using
modulo_delta_types
- it is now used in w_unify_core_0 too
- fixing/improving documentation of options
- deprecating "Set Tactic Evars Pattern Unification"
|
| |
|
|
|
|
|
|
|
|
|
| |
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
| | |
|
| |
|
|
| |
in tactic unification.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
while before these were supposed to consider only syntactically.
Made the experiment to unify with all delta flags unset. Keeping the
same flags as for non evar/meta free subterms would lead to too much
successes, as e.g. "true && b" matching "b" when the
modulo_conv_on_closed_terms flag is set, which is the case for
rewrite. But maybe should we instead investigate to have the same
flags but with the restrict_conv_on_strict_subterms flag set. This
rules out examples like "true && b" unifying with "b" and this is
another option which is ok for compiling the stdlib without any
changes.
|
| |
|
|
|
| |
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
matching subterm destruct/induction on a partially applied
pattern. AFAICS, there is only such instance of destruct that needs
this in the contrins (in EuclideanGeometry/G3_ParticularAngle.v), but
while a more global decision is taken, I prefer at the current time to
adopt this approximation of 8.4 semantics, even if the flags are not
the same when the pattern is fully applied or not. Only so little
cases are concerned because in most cases, destruct/induction on a
partially applied pattern is of the form "destruct cst"
(e.g. "destruct eq_dec") and no conversion is needed anyway.
Not being uniform whether the pattern is fully applied or not is a bit
unsatisfactory, but hopefully, this is temporary.
|
| |
|
|
|
|
|
|
|
| |
Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
|
| |
|
|
|
|
|
|
|
| |
eager meta substition in w_unify, so as to preserve compatibility
after PMP's move of (setoid) rewrite clauses from metas to
evars (fbbe491cfa).
Hoping it is compatible for non-rewrite uses of the eager meta flag,
and that it is not too costly.
|
| | |
|
| |
|
|
|
|
| |
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.
|
| |
|
|
|
|
|
| |
This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
|
| |
|
|
|
|
| |
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
|
| |
|
|
|
| |
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
|
| | |
|
| |
|
|
| |
unification.
|
| | |
|
| |
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
| |
|
|
|
| |
application case to expand primitive projections at the head of both
applications.
|
| |
|
|
|
|
|
|
|
| |
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.
|
| |
|
|
|
| |
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
| |
|
|
|
| |
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
|
| |
|
|
|
|
|
|
|
|
| |
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
| |
|
|
| |
projections with their eta-expanded constant form.
|
| |
|
|
|
|
|
| |
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
|
| | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Guillaume Melquiond
Matthieu Sozeau
Maxime Dénès
Matthieu Sozeau