subst. explicites avec vecteurs

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

1 files changed, 30 insertions, 14 deletions

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')))