- the connections between the intermediate language and the "bag"

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

diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
index f844c2e5114cec00d2cd7685d75f18249e9e2a44..490125095f62118906403cd28c8fcb146f77b6af 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
@@ -18,26 +18,20 @@ module B = Brg
 
 (* internal functions: crg to brg term **************************************)
 
-let rec lenv_fold_left map1 map2 x = function
-   | D.ESort            -> x
-   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
-   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
-
 let rec xlate_term f = function
    | D.TSort (a, l)     -> f (B.Sort (a, l))
    | D.TGRef (a, n)     -> f (B.GRef (a, n))
    | D.TLRef (a, _, _)  -> let f i = f (B.LRef (a, i)) in E.apix C.err f a
    | D.TCast (a, u, t)  ->
-      let f uu tt = f (B.Cast (a, uu, tt)) in
-      let f uu = xlate_term (f uu) t in
-      xlate_term f u 
+      let f tt uu = f (B.Cast (a, uu, tt)) in
+      let f tt = xlate_term (f tt) u in
+      xlate_term f t 
    | D.TAppl (a, vs, t) ->
       let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in
       let f tt = C.list_fold_right f map vs tt in
       xlate_term f t
-   | D.TProj (a, e, t)  ->
-      let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
-      xlate_term f t
+   | D.TProj (_, e, t)  -> 
+      xlate_term f (D.tshift e t)
    | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
       xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
    | D.TBind (a, b, t)  ->
@@ -63,9 +57,6 @@ and xlate_bind x a b =
          let map x n = B.Bind (n :: a, B.Void, x) in
         List.fold_left map x ns
 
-and xlate_proj x _ e =
-   lenv_fold_left xlate_bind xlate_proj x e
-
 (* internal functions: brg to crg term **************************************)
 
 let rec xlate_bk_term f = function
@@ -73,17 +64,17 @@ let rec xlate_bk_term f = function
    | B.GRef (a, n)     -> f (D.TGRef (a, n))
    | B.LRef (a, i)     -> f (D.TLRef (a, i, 0))
    | B.Cast (a, u, t)  ->
-      let f uu tt = f (D.TCast (a, uu, tt)) in
-      let f uu = xlate_bk_term (f uu) t in
-      xlate_bk_term f u 
+      let f tt uu = f (D.TCast (a, uu, tt)) in
+      let f tt = xlate_bk_term (f tt) u in
+      xlate_bk_term f t 
    | B.Appl (a, u, t)  ->
-      let f uu tt = f (D.TAppl (a, [uu], tt)) in
-      let f uu = xlate_bk_term (f uu) t in
-      xlate_bk_term f u 
+      let f tt uu = f (D.TAppl (a, [uu], tt)) in
+      let f tt = xlate_bk_term (f tt) u in
+      xlate_bk_term f t 
    | B.Bind (a, b, t)  ->
-      let f bb tt = f (D.TBind (a, bb, tt)) in
-      let f bb = xlate_bk_term (f bb) t in
-      xlate_bk_bind f b
+      let f tt bb = f (D.TBind (a, bb, tt)) in
+      let f tt = xlate_bk_bind (f tt) b in
+      xlate_bk_term f t 
 
 and xlate_bk_bind f = function
    | B.Abst (n, t) ->
@@ -96,7 +87,6 @@ and xlate_bk_bind f = function
    
 (* interface functions ******************************************************)
 
-let brg_of_crg f t =
-   f (xlate_term C.start t)
+let brg_of_crg f t = f (xlate_term C.start t)
 
 let crg_of_brg = xlate_bk_term