From 9aaaba04fbd198881aaee42cfc41fdb75db1eeaa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Sep 2009 15:43:47 +0000 Subject: [PATCH] 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. --- .../components/ng_kernel/nCicReduction.ml | 74 ++++++++++++------- .../components/ng_refiner/nCicUnification.ml | 4 +- 2 files changed, 48 insertions(+), 30 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 2e13a5304..432ea9a45 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -22,41 +22,56 @@ module type Strategy = sig type env_term type config = int * env_term list * C.term * stack_term list val to_env : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> config -> env_term - val from_stack : stack_term -> config + val from_stack : delta:int -> stack_term -> config val from_stack_list_for_unwind : - unwind: (config -> C.term) -> stack_term list -> C.term list - val from_env : env_term -> config + unwind: (config -> C.term) -> stack_term list -> C.term list + val from_env : delta:int -> env_term -> config val from_env_for_unwind : - unwind: (config -> C.term) -> env_term -> C.term + unwind: (config -> C.term) -> env_term -> C.term val stack_to_env : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> stack_term -> env_term val compute_to_env : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> int -> env_term list -> C.term -> env_term val compute_to_stack : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> config -> stack_term end ;; -module CallByValueByNameForUnwind' = struct +module CallByValueByNameForUnwind' : Strategy = struct type config = int * env_term list * C.term * stack_term list - and stack_term = config lazy_t * C.term lazy_t (* cbv, cbn *) - and env_term = config lazy_t * C.term lazy_t (* cbv, cbn *) - let to_env ~reduce ~unwind c = lazy (fst (reduce c)),lazy (unwind c) - let from_stack (c,_) = Lazy.force c + and stack_term = + config Lazy.t * (int -> config) * C.term Lazy.t + and env_term = + config Lazy.t (* cbneed ~delta:0 *) + * (int -> config) (* cbvalue ~delta *) + * C.term Lazy.t (* cbname ~delta:max_int *) + let to_env ~reduce ~unwind c = + lazy (fst (reduce ~delta:0 c)), + (fun delta -> fst (reduce ~delta c)), + lazy (unwind c) + let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta let from_stack_list_for_unwind ~unwind:_ l = - List.map (function (_,c) -> Lazy.force c) l - let from_env (c,_) = Lazy.force c - let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c + List.map (fun (_,_,c) -> Lazy.force c) l + let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta + let from_env_for_unwind ~unwind:_ (_,_,c) = Lazy.force c let stack_to_env ~reduce:_ ~unwind:_ config = config let compute_to_env ~reduce ~unwind k e t = - lazy (fst (reduce (k,e,t,[]))), lazy (unwind (k,e,t,[])) + lazy (fst (reduce ~delta:0 (k,e,t,[]))), + (fun delta -> fst (reduce ~delta (k,e,t,[]))), + lazy (unwind (k,e,t,[])) let compute_to_stack ~reduce ~unwind config = - lazy (fst (reduce config)), lazy (unwind config) + lazy (fst (reduce ~delta:0 config)), + (fun delta -> fst (reduce ~delta config)), + lazy (unwind config) end ;; @@ -87,7 +102,7 @@ module Reduction(RS : Strategy) = struct let rec reduce ~delta ?(subst = []) context : config -> config * bool = let rec aux = function | k, e, C.Rel n, s when n <= k -> - let k',e',t',s' = RS.from_env (list_nth e (n-1)) in + let k',e',t',s' = RS.from_env ~delta (list_nth e (n-1)) in aux (k',e',t',s'@s) | k, _, C.Rel n, s as config (* when n > k *) -> let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in @@ -104,14 +119,15 @@ module Reduction(RS : Strategy) = struct | (_, _, C.Prod _, _) | (_, _, C.Lambda _, []) as config -> config, true | (k, e, C.Lambda (_,_,t), p::s) -> - aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s) + aux (k+1, (RS.stack_to_env ~reduce:(reduce ~subst context) ~unwind p)::e, t,s) | (k, e, C.LetIn (_,_,m,t), s) -> - let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in + let m' = RS.compute_to_env ~reduce:(reduce ~subst context) ~unwind k e m in aux (k+1, m'::e, t, s) | (_, _, C.Appl ([]|[_]), _) -> assert false | (k, e, C.Appl (he::tl), s) -> let tl' = - List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl + List.map (fun t->RS.compute_to_stack + ~reduce:(reduce ~subst context) ~unwind (k,e,t,[])) tl in aux (k, e, he, tl' @ s) | (_, _, C.Const @@ -128,7 +144,7 @@ module Reduction(RS : Strategy) = struct (_,Ref.Fix (fixno,recindex,height)) as refer) as head),s) as config -> (* if delta >= height then config else *) (match - try Some (RS.from_stack (List.nth s recindex)) + try Some (RS.from_stack ~delta (List.nth s recindex)) with Failure _ -> None with | None -> config, true @@ -138,12 +154,14 @@ module Reduction(RS : Strategy) = struct | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ when delta >= height -> let new_s = - replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind c) in (0, [], head, new_s), false | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ -> let new_s = - replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind c) in let _,_,_,_,body = List.nth fixes fixno in aux (0, [], body, new_s) @@ -281,7 +299,7 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 = | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> aux test_eq_only context hd1 hd2 && - let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in + let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in (try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux true context t1 t2) @@ -361,8 +379,8 @@ let are_convertible ~metasenv ~subst = HExtlib.list_forall_default3 (fun t1 t2 b -> not b || - let t1 = RS.from_stack t1 in - let t2 = RS.from_stack t2 in + let t1 = RS.from_stack ~delta:max_int t1 in + let t2 = RS.from_stack ~delta:max_int t2 in convert_machines true (put_in_whd t1 t2)) s1 s2 true relevance with Invalid_argument _ -> false) || (not (norm1 && norm2) && convert_machines test_eq_only (small_delta_step m1 m2)) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index fc6eea759..07eba73b5 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -623,8 +623,8 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); | _ -> [] *) in let unif_from_stack t1 t2 b metasenv subst = try - let t1 = NCicReduction.from_stack t1 in - let t2 = NCicReduction.from_stack t2 in + let t1 = NCicReduction.from_stack ~delta:max_int t1 in + let t2 = NCicReduction.from_stack ~delta:max_int t2 in unif_machines metasenv subst (put_in_whd t1 t2) with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst -- 2.39.2