From: Enrico Tassi Date: Fri, 4 Sep 2009 15:44:02 +0000 (+0000) Subject: Reduction speedup (a.k.a. better sharing): X-Git-Tag: make_still_working~3498 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a03741c70a531bdfcc97eddca21e30eb3cd82073;p=helm.git 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 ba32fe15d..9cff07d8f 100644 --- 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: