| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The old implementation did not beta-iota normalize before observing the head of
the term, resulting in stange bugs.
|
|
|
|
convert_concl/convert_hyp. This was actually probably the main source
of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than
nf_enter, as suspected in 3c2723f.
|
|
équation;" which was committed by mistake.
This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
|
|
|
|
(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc).
It may be the case that the new expression lives in a higher sorts and
the context where it is substituted in supports it. So, it is too
strong to expect that, when the substituted objects are types, the
sort of the new one is smaller than the sort of the original
one. Consider e.g.
Goal @eq Type nat nat.
change nat with (@id Type nat).
which is a correct replacement, even if (id Type nat) is in a higher sort.
Introducing typing in "contextually" would be a big change for a
little numbers of uses, so we instead (hackily) recheck the whole term
(even though typing with evars uses evar_conv which accept to unify
Type with Set, leading to wrongly accept "Goal @eq Set nat nat.
change nat with (@id Type nat).". Evar conv is however rejecting
Prop=Type.)
|
|
(Maybe one of the source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)
|
|
|
|
The rest will take more work.
|
|
We are left with the compatibility layer and a handful of primitives which require some thought to move.
|
|
Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.
The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
|
|
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
|
|
|
|
unification.
|
|
new proof engine in e824d4293. Because of the expansion made by "fold"
and possibly by "change", checking the order of hypotheses is
necessary in general in "reduce". Before, it was done by side-effect
on reference "check", now it has to be explicit. To do for
optimization: flag each of the red_expr conversion strategy according
to whether they really need a check.
Also renamed the e_reduce family to e_change to emphasize that some
expansion can occur and that typing has to be rechecked.
This fixes recent failure of CoLoR (and probably Ergo).
|
|
|
|
Thanks to Yves for reporting it!
|
|
|
|
Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
|
|
|
|
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
|
|
|
|
|
|
This code was wrong but luckily unused. It instantiated an evar with an
instance where the let-in bindings were removed.
|
|
term or a type.
Continuation of 9a82982c1eb.
|
|
type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).
|
|
|
|
|
|
not draw Auto.
|
|
(the action is "clear").
Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.
Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
|
|
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
|
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
|
|
(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.
|
|
|
|
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
|
|
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.
|
|
authoritatively erase non-generalized hypotheses dependent on id.
|
|
Most of the code from Goal.Refine and related was moved to the one
file that was using it, wiz. tactics.ml. Some additional care should
be taken to clean up even more the remaining code.
|
|
with existing ML code.
|
|
projections with their eta-expanded constant form.
|
|
as a disjunctive intropattern.
|
|
|
|
under binders. This might incur a significant time penalty.
|
|
two versions of the rewriting lemma, keeping useless evars around. This
can now happen only when the rewrite lemma is used under binders... Fix
to do next.
|
|
This removes a use of Evd.merge.
|
|
The hypinfo state is now refreshed at a proper time, which should reduce the
overall number of calls to [decompose_applied_relation]. The state passing
nature of the program is also more explicit, removing a use of Evd.merge.
This patch should preserve semantics and efficiency.
|
|
|
|
Goals have to be refreshed when observed, because the evarmap may have
changed between the moment where the goal was generated and the moment the
goal is used.
|
|
|
