update in helena

[helm.git] / helm / software / helena / src / basic_rg / brgCrg.ml

diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml
index 8514de641d204c35a1d0d41c1925b38cb3ddac1f..984f84916a26e3ff434c9202d6500b0ca13752bf 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgCrg.ml
+++ b/helm/software/helena/src/basic_rg/brgCrg.ml
@@ -10,78 +10,67 @@
       V_______________________________________________________________ *)
 
 module C = Cps
+module N = Layer
 module E = Entity
-module J = Marks
-module N = Level
 module D = Crg
 module B = Brg
 
 (* internal functions: crg to brg term **************************************)
 
 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 tt uu = f (B.Cast (a, uu, tt)) in
+   | D.TSort k         -> f (B.Sort k)
+   | D.TGRef (a, n)    -> f (B.GRef (a, n))
+   | D.TLRef (a, i)    -> f (B.LRef (a, i))
+   | D.TCast (u, t)    ->
+      let f tt uu = f (B.Cast (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 (_, e, t)  -> 
-      xlate_term f (D.tshift e t)
-   | D.TBind (a, b, t)  ->
-      let f tt = f (xlate_bind tt a b) in xlate_term f t
+   | D.TAppl (a, v, t) ->
+      let f tt vv = f (B.Appl (a, vv, tt)) in
+      let f tt = xlate_term (f tt) v in
+      xlate_term f t 
+   | D.TProj (e, t)    -> 
+      D.shift (xlate_term f) e t
+   | D.TBind (y, b, t)    -> 
+      xlate_term (xlate_bind f y b) t
 
-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 (m, ws) ->
-         let map x n w = 
-           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      ->
-         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 _       ->
-         let map x n = B.Bind (n :: a, B.Void, x) in
-        List.fold_left map x ns
+and xlate_bind f y b t = match b with
+   | D.Abst (r, n, w) ->
+      let f ww = f (B.Bind (y, B.Abst (r, n, ww), t)) in 
+      xlate_term f w
+   | D.Abbr v         ->
+      let f vv = f (B.Bind (y, B.Abbr vv, t)) in 
+      xlate_term f v
+   | D.Void           ->
+      f (B.Bind (y, B.Void, t))
 
 (* internal functions: brg to crg term **************************************)
 
 let rec xlate_bk_term f = function
-   | B.Sort (a, l)     -> f (D.TSort (a, l))
-   | 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 tt uu = f (D.TCast (a, uu, tt)) in
+   | B.Sort k         -> f (D.TSort k)
+   | B.GRef (a, n)    -> f (D.TGRef (a, n))
+   | B.LRef (a, i)    -> f (D.TLRef (a, i))
+   | B.Cast (u, t)    ->
+      let f tt uu = f (D.TCast (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 tt uu = f (D.TAppl (a, [uu], tt)) in
+   | B.Appl (a, u, t) ->
+      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 tt bb = f (D.TBind (a, bb, tt)) in
+   | B.Bind (y, b, t) ->
+      let f tt bb = f (D.TBind (y, 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) ->
-      let f tt = f (D.Abst (n, [tt])) in
+   | B.Abst (r, n, t) ->
+      let f tt = f (D.Abst (r, n, tt)) in
       xlate_bk_term f t
-   | B.Abbr t      ->
-      let f tt = f (D.Abbr [tt]) in
+   | 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
    
 (* interface functions ******************************************************)