- initial support for abstractions with explicit levels

[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 32950e1cf557c5a55a8463752179224b75923d33..f844c2e5114cec00d2cd7685d75f18249e9e2a44 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
@@ -12,6 +12,7 @@
 module C = Cps
 module E = Entity
 module J = Marks
+module N = Level
 module D = Crg
 module B = Brg
 
@@ -37,8 +38,8 @@ let rec xlate_term f = function
    | D.TProj (a, e, t)  ->
       let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
       xlate_term f t
-   | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, 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)  ->
       let f tt = f (xlate_bind tt a b) in xlate_term f t
 
@@ -46,19 +47,19 @@ and xlate_bind x a b =
    let f a ns = a, ns in
    let a, ns = E.get_names f a in 
    match b with
-      | D.Abst ws ->
+      | D.Abst (m, ws) ->
          let map x n w = 
-           let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst ww, x) in 
+           let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in 
            xlate_term f w
         in
         List.fold_left2 map x ns ws 
-      | D.Abbr vs ->
+      | D.Abbr vs      ->
          let map x n v = 
            let f vv = B.Bind (n :: a, B.Abbr vv, x) in 
            xlate_term f v
         in
         List.fold_left2 map x ns vs
-      | D.Void _  ->
+      | D.Void _       ->
          let map x n = B.Bind (n :: a, B.Void, x) in
         List.fold_left map x ns
 
@@ -85,13 +86,13 @@ let rec xlate_bk_term f = function
       xlate_bk_bind f b
 
 and xlate_bk_bind f = function
-   | B.Abst t ->
-      let f tt = f (D.Abst [tt]) in
+   | B.Abst (n, t) ->
+      let f tt = f (D.Abst (n, [tt])) in
       xlate_bk_term f t
-   | B.Abbr t ->
+   | B.Abbr t      ->
       let f tt = f (D.Abbr [tt]) in
       xlate_bk_term f t
-   | B.Void   -> f (D.Void 1)
+   | B.Void        -> f (D.Void 1)
    
 (* interface functions ******************************************************)