| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
"simpl at" and "change at".
|
| |
|
|
| |
finite set libraries.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
They should be rather sensible, but de gustibus & coloribus...
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
|
| |
|
|
|
| |
right-hand side of a "change with": the rhs lives in the toplevel
environment.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Stop sharing those references across constants of the same
module, which was triggering some bugs when using native_compute
in interactive mode in a functor declaration.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
where it will eventually stabilize.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
absence of remaining dependent evars when several arguments are given.
For simplicity of implementation, checking instead for every step of
the n-ary "apply in".
|
| |
|
|
| |
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.
|
| | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Xavier Clerc
Enrico Tassi
Maxime Dénès