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.

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index ba32fe15dd18f2cb38c6af0dc055fae94d72bbe5..9cff07d8fd0b9e623245f12ab6cdf09d24936bcf 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -41,7 +41,7 @@ type machine = int * environment_item list * NCic.term * stack_item list
 val reduce_machine : 
      delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> 
       machine * bool
-val from_stack : stack_item -> machine
+val from_stack : delta:int -> stack_item -> machine
 val unwind : machine -> NCic.term
 
 val split_prods: