subst. explicites avec vecteurs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8799 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 61 insertions, 56 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index c5a5b9ffa..ff456b93c 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -645,9 +645,9 @@ and compact_v acc s v k i =
 let optimise_closure env c =
   if is_subs_id env then (env,c) else
     let (c',(_,s)) = compact_constr (0,[]) c 1 in
-    let env' = List.fold_left
-      (fun subs i -> subs_cons (clos_rel env i, subs)) (ESID 0) s in
-    (env',c')
+    let env' =
+      Array.map (fun i -> clos_rel env i) (Array.of_list s) in
+    (subs_cons (env', ESID 0),c')
 
 let mk_lambda env t =
   let (env,t) = optimise_closure env t in
@@ -876,18 +876,14 @@ let rec get_args n tys f e stk =
         get_args n tys f (subs_shft (k,e)) s
     | Zapp l :: s ->
         let na = Array.length l in
-        if n == na then
-          let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e l in
-          (Inl e',s)
+        if n == na then (Inl (subs_cons(l,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
-          let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e args in
-          (Inl e', Zapp eargs :: s)
+          (Inl (subs_cons(args,e)), Zapp eargs :: s)
         else (* more lambdas *)
           let (_,etys) = list_chop na tys in
-          let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e l in
-          get_args (n-na) etys f e' s
+          get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
 
@@ -939,13 +935,7 @@ let contract_fix_vect fix =
 	   env, Array.length bds)
       | _ -> assert false
   in
-  let rec subst_bodies_from_i i env =
-    if i = nfix then
-      (env, thisbody)
-    else
-      subst_bodies_from_i (i+1) (subs_cons (make_body i, env))
-  in       
-  subst_bodies_from_i 0 env
+  (subs_cons(Array.init nfix make_body, env), thisbody)
 
 
 (*********************************************************************)
@@ -1025,7 +1015,7 @@ let rec knr info m stk =
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
-      knit info (subs_cons(v,e)) bd stk
+      knit info (subs_cons([|v|],e)) bd stk
   | _ -> (m,stk)
 
 (* Computes the weak head normal form of a term *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 7662a2f8b..dc29e4e98 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -55,7 +55,10 @@ let rec is_lift_id = function
 (* (bounded) explicit substitutions of type 'a *)
 type 'a subs =
   | ESID of int            (* ESID(n)    = %n END   bounded identity *)
-  | CONS of 'a * 'a subs   (* CONS(t,S)  = (S.t)    parallel substitution *)
+  | CONS of 'a array * 'a subs
+                           (* CONS([|t1..tn|],S)  =
+                              (S.t1...tn)    parallel substitution
+                              beware of the order *)
   | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
                            (*                        with n vars *)
   | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
@@ -64,7 +67,7 @@ type 'a subs =
  * Needn't be recursive if we always use these functions
  *)
 
-let subs_cons(x,s) = CONS(x,s)
+let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s)
 
 let subs_liftn n = function
   | ESID p        -> ESID (p+n) (* bounded identity lifted extends by p *)
@@ -85,11 +88,12 @@ let subs_shift_cons = function
 | (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1))
 | (k, s, t)           -> CONS(t,SHIFT(k, s));;
 
-(* Tests whether a substitution is extensionnaly equal to the identity *)
+(* Tests whether a substitution is equal to the identity *)
 let rec is_subs_id = function
     ESID _     -> true
   | LIFT(_,s)  -> is_subs_id s
   | SHIFT(0,s) -> is_subs_id s
+  | CONS(x,s)  -> Array.length x = 0 && is_subs_id s
   | _          -> false
 
 (* Expands de Bruijn k in the explicit substitution subs
@@ -108,14 +112,15 @@ let rec is_subs_id = function
  * variable points k bindings beyond subs.
  *) 
 let rec exp_rel lams k subs =
-  match (k,subs) with
-    | (1, CONS (def,_))         -> Inl(lams,def)
-    | (_, CONS (_,l))           -> exp_rel lams (pred k) l
-    | (_, LIFT (n,_)) when k<=n -> Inr(lams+k,None)
-    | (_, LIFT (n,l))           -> exp_rel (n+lams) (k-n) l
-    | (_, SHIFT (n,s))          -> exp_rel (n+lams) k s
-    | (_, ESID n) when k<=n     -> Inr(lams+k,None)
-    | (_, ESID n)               -> Inr(lams+k,Some (k-n))
+  match subs with
+    | CONS (def,_) when k <= Array.length def
+                           -> Inl(lams,def.(Array.length def - k))
+    | CONS (v,l)           -> exp_rel lams (k - Array.length v) l
+    | LIFT (n,_) when k<=n -> Inr(lams+k,None)
+    | LIFT (n,l)           -> exp_rel (n+lams) (k-n) l
+    | SHIFT (n,s)          -> exp_rel (n+lams) k s
+    | ESID n when k<=n     -> Inr(lams+k,None)
+    | ESID n               -> Inr(lams+k,Some (k-n))
 
 let expand_rel k subs = exp_rel 0 k subs
 
@@ -124,9 +129,20 @@ let rec comp mk_cl s1 s2 =
     | _, ESID _ -> s1
     | ESID _, _ -> s2
     | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
-    | _, CONS(x,s') -> CONS(mk_cl(s1,x), comp mk_cl s1 s')
-    | CONS(x,s), SHIFT(k,s') -> comp mk_cl s (subs_shft(k-1, s'))
-    | CONS(x,s), LIFT(k,s') -> CONS(x,comp mk_cl s (subs_liftn (k-1) s'))
+    | _, CONS(x,s') ->
+        CONS(Array.map (fun t -> mk_cl(s1,t)) x, comp mk_cl s1 s')
+    | CONS(x,s), SHIFT(k,s') ->
+        let lg = Array.length x in
+        if k == lg then comp mk_cl s s'
+        else if k > lg then comp mk_cl s (SHIFT(k-lg, s'))
+        else comp mk_cl (CONS(Array.sub x 0 (lg-k), s)) s'
+    | CONS(x,s), LIFT(k,s') ->
+        let lg = Array.length x in
+        if k == lg then CONS(x, comp mk_cl s s')
+        else if k > lg then CONS(x, comp mk_cl s (LIFT(k-lg, s')))
+        else
+          CONS(Array.sub x (lg-k) k,
+               comp mk_cl (CONS(Array.sub x 0 (lg-k),s)) s')
     | LIFT(k,s), SHIFT(k',s') ->
         if k<k'
         then subs_shft(k, comp mk_cl s (subs_shft(k'-k, s')))
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index cd9c16907..68f5f2201 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -22,21 +22,22 @@ val el_lift : lift -> lift
 val reloc_rel : int -> lift -> int
 val is_lift_id : lift -> bool
 
-(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. 
-  [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
-  $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
-  [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
+(*s Explicit substitutions of type ['a]. *)
 type 'a subs =
-  | ESID of int
-  | CONS of 'a * 'a subs
-  | SHIFT of int * 'a subs
-  | LIFT of int * 'a subs
+  | ESID of int            (* ESID(n)    = %n END   bounded identity *)
+  | CONS of 'a array * 'a subs
+                           (* CONS([|t1..tn|],S)  =
+                              (S.t1...tn)    parallel substitution
+                              beware of the order *)
+  | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
+                           (*                        with n vars *)
+  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
 
-val subs_cons: 'a * 'a subs -> 'a subs
+val subs_cons: 'a array * '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
-val subs_shift_cons: int * 'a subs * 'a -> 'a subs
+val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
 val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
 val is_subs_id: 'a subs -> bool
-val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
\ No newline at end of file
+val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0e7c819b6..fbb06940d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -724,7 +724,7 @@ let check_one_fix renv recpos def =
       | Const kn -> 
           if evaluable_constant kn renv.env then 
             try List.for_all (check_rec_call renv) l
-            with (FixGuardError _ ) as e ->
+            with (FixGuardError _ ) ->
 	      check_rec_call renv(applist(constant_value renv.env kn, l))
 	  else List.for_all (check_rec_call renv) l
 
diff --git a/kernel/term.ml b/kernel/term.ml
index b082c091e..87c319a1b 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -752,19 +752,17 @@ let rec lift_substituend depth s =
 
 let make_substituend c = { sinfo=Unknown; sit=c }
 
-let substn_many lamv n =
+let substn_many lamv n c =
   let lv = Array.length lamv in 
-  let rec substrec depth c = match kind_of_term c with
-    | Rel k     ->
-        if k<=depth then 
-	  c
-        else if k-depth <= lv then
-          lift_substituend depth lamv.(k-depth-1)
-        else 
-	  mkRel (k-lv)
-    | _ -> map_constr_with_binders succ substrec depth c
-  in 
-  substrec n
+  if lv = 0 then c
+  else 
+    let rec substrec depth c = match kind_of_term c with
+      | Rel k     ->
+          if k<=depth then c
+          else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
+          else mkRel (k-lv)
+      | _ -> map_constr_with_binders succ substrec depth c in 
+    substrec n c
 
 (*
 let substkey = Profile.declare_profile "substn_many";;