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.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 2e13a5304b23b5adca91ef71dcb9c7d2f4349781..432ea9a45bd4c79e599181da2db0cd9038a06463 100644 (file)
--- 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 fc6eea759313223b30c57a7b6215470ea12c24d5..07eba73b564385b6742ada4848bcb16be7f255fd 100644 (file)
--- 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