X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgType.ml;h=f23da87d09fad4304838ccff99d8c5420756b5ae;hb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;hp=8b119e5e25aa165cabc483a3ad48faf13aa11295;hpb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml
index 8b119e5e2..f23da87d0 100644
--- a/helm/software/lambda-delta/src/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgType.ml
@@ -9,19 +9,19 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module U = NUri
-module C = Cps
-module A = Share
-module L = Log
-module H = Hierarchy
-module Y = Entity
-module B = Brg
-module O = BrgOutput
-module E = BrgEnvironment
-module S = BrgSubstitution
-module R = BrgReduction
+module U  = NUri
+module C  = Cps
+module W  = Share
+module L  = Log
+module H  = Hierarchy
+module E  = Entity
+module N  = Level
+module B  = Brg
+module BE = BrgEnvironment
+module BS = BrgSubstitution
+module BR = BrgReduction
 
-type message = (R.kam, B.term) Log.message
+type message = (BR.kam, B.term) Log.message
 
 (* Internal functions *******************************************************)
 
@@ -32,7 +32,7 @@ let message1 st1 m t1 =
 
 let log1 s m t =
    let s =  s ^ " the term" in
-   L.log R.specs level (message1 s m t) 
+   L.log BR.specs level (message1 s m t) 
 
 let error1 err s m t =
    err (message1 s m t)
@@ -51,16 +51,17 @@ let error3 err m t1 t2 ?mu t3 =
    err (message3 m t1 t2 ?mu t3)
 
 let assert_convertibility err f st m u w v =
-   if R.are_convertible st m u m w then f () else
+   if BR.are_convertible st m u m w then f () else
    error3 err m v w u
 
 let assert_applicability err f st m u w v =
-   match R.xwhd st m u with 
-      | _, B.Sort _                 -> error1 err "not a function type" m u
-      | mu, B.Bind (_, B.Abst u, _) -> 
-         if R.are_convertible st mu u m w then f () else
+   match BR.xwhd st m u with 
+      | _, B.Sort _                      ->
+         error1 err "not a function type" m u
+      | mu, B.Bind (_, B.Abst (_, u), _) -> 
+         if BR.are_convertible st mu u m w then f () else
 	 error3 err m v w ~mu u
-      | _                         -> assert false (**)
+      | _                                -> assert false (**)
 
 let rec b_type_of err f st m x =
    log1 "Now checking" m x;
@@ -68,57 +69,57 @@ let rec b_type_of err f st m x =
    | B.Sort (a, h)           ->
       let h = H.apply h in f x (B.Sort (a, h)) 
    | B.LRef (_, i)           ->
-      begin match R.get m i with
-         | B.Abst w                  ->
-	    f x (S.lift (succ i) (0) w)
+      begin match BR.get m i with
+         | B.Abst (_, w)     ->
+	    f x (BS.lift (succ i) (0) w)
 	 | B.Abbr (B.Cast (_, w, _)) -> 
-	    f x (S.lift (succ i) (0) w)
+	    f x (BS.lift (succ i) (0) w)
 	 | B.Abbr _                  -> assert false
 	 | B.Void                    -> 
 	    error1 err "reference to excluded variable" m x
       end
    | B.GRef (_, uri)         ->
-      begin match E.get_entity uri with
-         | _, _, Y.Abst w                  -> f x w
-	 | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
-	 | _, _, Y.Abbr _                  -> assert false
-	 | _, _, Y.Void                    ->
+      begin match BE.get_entity uri with
+         | _, _, E.Abst (_, w)             -> f x w
+	 | _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
+	 | _, _, E.Abbr _                  -> assert false
+	 | _, _, E.Void                    ->
             error1 err "reference to unknown entry" m x
       end
    | B.Bind (a, B.Abbr v, t) ->
       let f xv xt tt =
-         f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+         f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
       in
       let f xv m = b_type_of err (f xv) st m t in
-      let f xv = f xv (R.push m a (B.abbr xv)) in
+      let f xv = f xv (BR.push m a (B.abbr xv)) in
       let f xv vv = match xv with 
 	 | B.Cast _ -> f xv
          | _        -> f (B.Cast ([], vv, xv))
       in
       type_of err f st m v
-   | B.Bind (a, B.Abst u, t) ->
+   | B.Bind (a, B.Abst (n, u), t) ->
       let f xu xt tt =
-	 f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
+	 f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
       in
       let f xu m = b_type_of err (f xu) st m t in
-      let f xu _ = f xu (R.push m a (B.abst xu)) in
+      let f xu _ = f xu (BR.push m a (B.abst n xu)) in
       type_of err f st m u
    | B.Bind (a, B.Void, t)   ->
       let f xt tt = 
-         f (A.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+         f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
       in
-      b_type_of err f st (R.push m a B.Void) t
+      b_type_of err f st (BR.push m a B.Void) t
          
    | B.Appl (a, v, t)        ->
       let f xv vv xt tt = 
-         let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+         let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
          assert_applicability err f st m tt vv xv
       in
       let f xv vv = b_type_of err (f xv vv) st m t in
       type_of err f st m v
    | B.Cast (a, u, t)        ->
       let f xu xt tt =  
-	 let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in
+	 let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in
          assert_convertibility err f st m xu tt xt
       in
       let f xu _ = b_type_of err (f xu) st m t in