lambda-delta:

[helm.git] / helm / software / lambda-delta / basic_rg / brgType.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index 8c9996c22a3fbb000cd3a8f7d8717606052bf733..4bf5882a4885a48cf53e1fc4af257e875820bc9e 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -11,12 +11,13 @@
 
 module U = NUri
 module C = Cps
-module S = Share
+module A = Share
 module L = Log
 module H = Hierarchy
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
+module S = BrgSubstitution
 module R = BrgReduction
 
 exception TypeError of B.message
@@ -51,8 +52,10 @@ let rec b_type_of f g c x =
       let f h = f x (B.Sort (a, h)) in H.apply f g h
    | B.LRef (_, i)           ->
       let f _ = function
-         | Some (_, B.Abst w)                  -> f x w
-        | Some (_, B.Abbr (B.Cast (_, w, _))) -> f x w
+         | Some (_, B.Abst w)                  ->
+           S.lift (f x) (succ i) (0) w
+        | Some (_, B.Abbr (B.Cast (_, w, _))) -> 
+           S.lift (f x) (succ i) (0) w
         | Some (_, B.Abbr _)                  -> assert false
         | Some (_, B.Void)                    -> 
            error1 "reference to excluded variable" c x
@@ -71,7 +74,7 @@ let rec b_type_of f g c x =
       E.get_obj f uri   
    | B.Bind (a, B.Abbr v, t) ->
       let f xv xt tt =
-         f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+         f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
       in
       let f xv cc = b_type_of (f xv) g cc t in
       let f xv = B.push (f xv) c a (B.Abbr xv) in
@@ -82,14 +85,14 @@ let rec b_type_of f g c x =
       type_of f g c v
    | B.Bind (a, B.Abst u, t) ->
       let f xu xt tt =
-        f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
+        f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
       in
       let f xu cc = b_type_of (f xu) g cc t in
       let f xu _ = B.push (f xu) c a (B.Abst xu) in
       type_of f g c u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
-         f (S.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
+         f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
       in
       let f cc = b_type_of f g cc t in
       B.push f c a B.Void   
@@ -101,7 +104,7 @@ let rec b_type_of f g c x =
            L.unbox (succ level);
            let f r =
 (*            L.warn (Printf.sprintf "Convertible: %b" a); *)
-              if r then f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt)
+              if r then f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt)
               else error3 c xv vv w
            in
            R.are_convertible f ~si:!si c w vv
@@ -114,7 +117,7 @@ let rec b_type_of f g c x =
    | B.Cast (a, u, t)        ->
       let f xu xt tt r =  
          (* L.warn (Printf.sprintf "Convertible: %b" a); *)
-        if r then f (S.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu
+        if r then f (A.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu
       in
       let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) c xu tt in
       let f xu _ = b_type_of (f xu) g c t in