summaryrefslogtreecommitdiff
path: root/kernel/esubst.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /kernel/esubst.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'kernel/esubst.ml')
-rw-r--r--kernel/esubst.ml46
1 files changed, 31 insertions, 15 deletions
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 0a3f4578..e32fc963 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: esubst.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: esubst.ml 8799 2006-05-09 21:15:07Z barras $ *)
open Util
@@ -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')))