From 3b03eb1015f14e04e505b11c27fb38b7db6ebe87 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 9 May 2006 21:15:07 +0000 Subject: subst. explicites avec vecteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8799 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/esubst.ml | 44 ++++++++++++++++++++++++++++++-------------- 1 file changed, 30 insertions(+), 14 deletions(-) (limited to 'kernel/esubst.ml') 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