]> matita.cs.unibo.it Git - helm.git/commit
Reduction speedup (a.k.a. better sharing):
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Sep 2009 15:44:02 +0000 (15:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Sep 2009 15:44:02 +0000 (15:44 +0000)
commita03741c70a531bdfcc97eddca21e30eb3cd82073
tree6a800faf4b3fa138bbe59b1f52108f2842495eb2
parent9aaaba04fbd198881aaee42cfc41fdb75db1eeaa
Reduction speedup (a.k.a. better sharing):

The ~delta argument was accidentally saved in the closure of aux that was
passed to all functions defined by the reduction strategy. So, most of the
terms where shared by the KAM environment in whd normal form with delta=max_int
(that means, not delta/iota-reduced at all, just beta-normal).
Thus many heavy computations where not shared, completely loosing the point
of having a KM.

The solution was to fix the API so that delta is not hidden anymore, then
really sharing computations with delta=0 (the most common case, I think).

The bad behaviour is still present for other values of delta, and an imperative
cache may be emplyed.
helm/software/components/ng_kernel/nCicReduction.mli