From: Claudio Sacerdoti Coen Date: Sun, 9 Mar 2008 16:53:38 +0000 (+0000) Subject: Potentially (and, at least sometimes, actually) big performance improvement: X-Git-Tag: make_still_working~5553 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=c3f967910eca5648fd69886166c66ddd49d92b54;hp=5c8c7f0ae6fdbba432286c01feac114873a1cfe9;p=helm.git Potentially (and, at least sometimes, actually) big performance improvement: let-in were always zeta-expanded during delifting. As a result, implicit, in a context with definitions, were always refined with a type that was well typed, but only up to (potentially expensive) reduction! --- diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index f082fc230..070a07c93 100644 --- a/helm/software/components/cic_unification/cicMetaSubst.ml +++ b/helm/software/components/cic_unification/cicMetaSubst.ml @@ -653,13 +653,17 @@ let delift n subst context metasenv l t = (try match List.nth context (m-k-1) with Some (_,C.Def (t,_)) -> + (try + C.Rel ((position (m-k) l) + k) + with + NotInTheList -> (*CSC: Hmmm. This bit of reduction is not in the spirit of *) (*CSC: first order unification. Does it help or does it harm? *) (*CSC: ANSWER: it hurts performances since it is possible to *) (*CSC: have an exponential explosion of the size of the proof.*) (*CSC: However, without this bit of reduction some "apply" in *) (*CSC: the library fail (e.g. nat/nth_prime.ma). *) - deliftaux k (S.lift m t) + deliftaux k (S.lift m t)) | Some (_,C.Decl t) -> C.Rel ((position (m-k) l) + k) | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))