]> 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:43:47 +0000 (15:43 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Sep 2009 15:43:47 +0000 (15:43 +0000)
commit9aaaba04fbd198881aaee42cfc41fdb75db1eeaa
tree0cc5b3e44ecdcbb1fca08d4b8a76fb3db1a9fce0
parentc6ec0dc44c2e592c7b1323304052bc1a523e7c22
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.ml
helm/software/components/ng_refiner/nCicUnification.ml