Optimization: take advantage that we don't use arrays anymore in substitutions.

7 files changed, 34 insertions, 19 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c9326615dc..d2256720c4 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -759,6 +759,10 @@ let get_nth_arg head n stk =
     | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in
   strip_rec [] head n stk
 
+let rec subs_consn v i n s =
+  if Int.equal i n then s
+  else subs_consn v (i + 1) n (subs_cons v.(i) s)
+
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
 let rec get_args n tys f e = function
@@ -770,14 +774,13 @@ let rec get_args n tys f e = function
         get_args n tys f (subs_shft (k,e)) s
     | Zapp l :: s ->
         let na = Array.length l in
-        if n == na then (Inl (subs_cons(l,e)),s)
+        if n == na then (Inl (subs_consn l 0 na e), s)
         else if n < na then (* more arguments *)
-          let args = Array.sub l 0 n in
           let eargs = Array.sub l n (na-n) in
-          (Inl (subs_cons(args,e)), Zapp eargs :: s)
+          (Inl (subs_consn l 0 n e), Zapp eargs :: s)
         else (* more lambdas *)
           let etys = List.skipn na tys in
-          get_args (n-na) etys f (subs_cons(l,e)) s
+          get_args (n-na) etys f (subs_consn l 0 na e) s
     | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk ->
       (Inr {mark=mark Cstr Unknown;term=FLambda(n,tys,f,e)}, stk)
 
@@ -931,7 +934,11 @@ let contract_fix_vect fix =
            env, Array.length bds)
       | _ -> assert false
   in
-  (subs_cons(Array.init nfix make_body, env), thisbody)
+  let rec mk_subs env i =
+    if Int.equal i nfix then env
+    else mk_subs (subs_cons (make_body i) env) (i + 1)
+  in
+  (mk_subs env 0, thisbody)
 
 let unfold_projection info p =
   if red_projection info.i_flags p
@@ -1367,7 +1374,7 @@ let rec knr info tab m stk =
             knit info tab fxe fxbd (args@stk')
         | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] as s)) -> (m,args@s))
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
-      knit info tab (subs_cons([|v|],e)) bd stk
+      knit info tab (subs_cons v e) bd stk
   | FEvar(ev,env) ->
       (match info.i_cache.i_sigma ev with
           Some c -> knit info tab env c stk
@@ -1417,7 +1424,7 @@ and case_inversion info tab ci (univs,args) v =
     let env = info_env info in
     let ind = ci.ci_ind in
     let params, indices = Array.chop ci.ci_npar args in
-    let psubst = subs_cons (params, subs_id 0) in
+    let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in
     let mib = Environ.lookup_mind (fst ind) env in
     let mip = mib.mind_packets.(snd ind) in
     (* indtyping enforces 1 ctor with no letins in the context *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 97acd698e8..f61dd5a078 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -134,8 +134,7 @@ let is_subs_id = function
 | Nil w -> Int.equal w 0
 | Cons (_, _, _) -> false
 
-let subs_cons (v, s) =
-  Array.fold_left (fun accu x -> cons (Arg x) accu) s v
+let subs_cons v s = cons (Arg v) s
 
 let rec push_vars i s =
   if Int.equal i 0 then s
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 551c6f1732..9ad422275e 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -22,7 +22,7 @@ type 'a subs
 
 (** Derived constructors granting basic invariants *)
 val subs_id : int -> 'a subs
-val subs_cons: 'a array * 'a subs -> 'a subs
+val subs_cons: 'a -> 'a subs -> 'a subs
 val subs_shft: int * 'a subs -> 'a subs
 val subs_lift: 'a subs -> 'a subs
 val subs_liftn: int -> 'a subs -> 'a subs
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 18f16f427d..b27c53ef0f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -102,7 +102,7 @@ let decompose_Llam_Llet lam =
 let subst_id = subs_id 0
 let lift = subs_lift
 let liftn = subs_liftn
-let cons v subst = subs_cons([|v|], subst)
+let cons v subst = subs_cons v subst
 let shift subst = subs_shft (1, subst)
 
 (* Linked code location utilities *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 85e24f87b7..802a32b0e7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -198,7 +198,7 @@ let type_of_apply env func funt argsv argstv =
         let argt = argstv.(i) in
         let c1 = term_of_fconstr c1 in
         begin match conv_leq false env argt c1 with
-        | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2)
+        | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons (inject arg) e) c2)
         | exception NotConvertible ->
           error_cant_apply_bad_type env
             (i+1,c1,argt)
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 9cca204e8c..390fa58883 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -179,7 +179,7 @@ let decompose_Llam lam =
 let subst_id = subs_id 0
 let lift = subs_lift
 let liftn = subs_liftn
-let cons v subst = subs_cons([|v|], subst)
+let cons v subst = subs_cons v subst
 let shift subst = subs_shft (1, subst)
 
 (* A generic map function *)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2661000a39..bada2c3a60 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -111,15 +111,20 @@ let shift_value n v =
  * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
  *    -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
  *)
+
+let rec mk_fix_subs make_body n env i =
+  if Int.equal i n then env
+  else mk_fix_subs make_body n (subs_cons (make_body i) env) (i + 1)
+
 let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
   let make_body j = FIXP(((reci,j),bodies), env, [||]) in
   let n = Array.length bds in
-  subs_cons(Array.init n make_body, env), bds.(i)
+  mk_fix_subs make_body n env 0, bds.(i)
 
 let contract_cofixp env (i,(_,_,bds as bodies)) =
   let make_body j = COFIXP((j,bodies), env, [||]) in
   let n = Array.length bds in
-  subs_cons(Array.init n make_body, env), bds.(i)
+  mk_fix_subs make_body n env 0, bds.(i)
 
 let make_constr_ref n k t =
   match k with
@@ -401,6 +406,10 @@ let rec strip_app = function
   | APP (args,st) -> APP (args,strip_app st)
   | s -> TOP
 
+let rec subs_consn v i n s =
+  if Int.equal i n then s
+  else subs_consn v (i + 1) n (subs_cons v.(i) s)
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack),
@@ -456,7 +465,7 @@ let rec norm_head info env t stack =
         (* New rule: for Cbv, Delta does not apply to locally bound variables
            or red_set info.reds fDELTA
          *)
-        let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
+        let env' = subs_cons (cbv_stack_term info TOP env b) env in
         norm_head info env' c stack
       else
         (CBN(t,env), stack) (* Should we consider a commutative cut ? *)
@@ -526,14 +535,14 @@ and cbv_stack_value info env = function
       when red_set info.reds fBETA ->
     let nargs = Array.length args in
       if nargs == nlams then
-          cbv_stack_term info stk (subs_cons(args,env)) b
+          cbv_stack_term info stk (subs_consn args 0 nargs env) b
         else if nlams < nargs then
-          let env' = subs_cons(Array.sub args 0 nlams, env) in
+          let env' = subs_consn args 0 nlams env in
           let eargs = Array.sub args nlams (nargs-nlams) in
           cbv_stack_term info (APP(eargs,stk)) env' b
         else
           let ctxt' = List.skipn nargs ctxt in
-          LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
+          LAM(nlams-nargs,ctxt', b, subs_consn args 0 nargs env)
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,[||]), stk)