| Age | Commit message (Collapse) | Author |
|---|
|
This is a continuation of the previous patch.
|
|
As witnessed in the ProjectiveGeometry contrib, some evar normalization were
taking ages because of an exponential behaviour due to a call-by-name
substitution: when normalizing an evar, its arguments were substituted right
away and the resulting term was then normalized, leading to a potential
duplication of normalizations.
Now we normalize evar arguments before substituting them, in a call-by-value
fashion. It makes examples from ProjectiveGeometry compile instanteanously
when they were killing the machine due to excessive memory allocation before
the patch.
Note that there is a tension here: we may be normalizing evar arguments too
eagerly, and try a call-by-need approach instead. To choose which particular
strategy we use, we should do some benchmarks... On stdlib, call-by-value
and call-by-need seem indistinguishable. To be continued?
|
|
I'm afraid this fix is a bit heuristic, but it seems to generate correct code in
all cases.
|
|
|
|
|
|
|
|
|
|
|
|
The Info layer was setting the required evarmap too eagerly, making the
tclWITHHOLE tactical accept terms with holes. The logging facility is
now inside the tclWITHHOLES.
|
|
|
|
|
|
|
|
Pretyping of [if] cases was missing a convertibility check with the ambient
type constraint, and just dropped it. This was making the pretyper construct
ill-typed terms.
|
|
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
|
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).
|
|
One missing evar was making the whole substitution fail.
The bug actually existed a priori also in the case where only metas
are substituted (i.e. before bcba6d1bc9f769da), leading to limit the
number of situations where it could be effectful.
This fixes current failures of RelationAlgebra and CFGV.
|
|
- Do use the flag for_ml for distinguishing coq level and ml level
ltac definitions.
- Skip ML call from the trace.
There are still differences from 8.4 and trunk. For instance on:
Ltac f x := refine x.
Goal False.
f I.
8.4 says:
In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed.
Error: The term "I" has type "True" while it is expected to have type "False".
trunk says:
In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed.
Error: The term "I" has type "True" while it is expected to have type "False".
Maybe we would like a mix of both (besides the printing of a
non-elegant "<genarg:uconstr>)?
|
|
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
|
|
normally, so failure is now detected by removing the "Fail".
|
|
|
|
|
|
for Functional Induction was failing because of minus now an alias).
Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):
"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.
"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
|
|
functional induction).
|
|
|
|
intropattern or a bound ltac variable).
|
|
|
|
|
|
|
|
Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad).
|
|
|
|
|
|
Removing blocking of generalization on destructed hypothesis
introduced on Nov 2. It was a bad idea as shown by bug #3790 on
eliminating v:Vector n, keeping an equality.
|
|
|
|
|
|
by hopefully computing the right position where to reinit an empty
level. Also removing obsolete comment.
|
|
|
|
responsible about.
|
|
printing/RichPrinter: Rename into Richprinter.
printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp.
printing/Richprinter: Cosmetics.
|
|
- The previous version of this module was using a feature of
the Format module of ocaml 4.01.
- Add comments.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
printing/Pptactic: Tag tactics pretty-printing.
printing/Ppvernac: Use the relevent Pptactic pretty-printer.
printing/RichPrinter: Publish two new services.
|
|
- Functorize with respect to the pretty-printer for constr.
- Include the application of Make to Ppconstr at toplevel in order to preserve
previous behavior.
|
|
printing/Pptactic: Use it.
|
