drg->brg translation contibued (still bugged though)

[helm.git] / helm / software / lambda-delta / dual_rg / drgBrg.ml

diff --git a/helm/software/lambda-delta/dual_rg/drgBrg.ml b/helm/software/lambda-delta/dual_rg/drgBrg.ml
index 2510f892056bc14a6c6c2a00aaa375e7d6f235cc..1f149a759f9ce2cd621bb82a31991b80b8153e86 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drgBrg.ml
+++ b/helm/software/lambda-delta/dual_rg/drgBrg.ml
@@ -39,7 +39,23 @@ let rec xlate_term f = function
    | D.TBind (a, b, t)  ->
       let f tt = f (xlate_bind tt a b) in xlate_term f t
 
-and xlate_bind x a b = assert false
+and xlate_bind x a b =
+   let f a ns = a, ns in
+   let a, ns = Y.get_names f a in 
+   match b with
+      | D.Abst ws ->
+         let map x n w = 
+           let f ww = B.Bind (B.Abst (n :: a, 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 (B.Abbr (n :: a, vv), x) in xlate_term f v
+        in
+        List.fold_left2 map x ns vs
+      | D.Void _  ->
+         let map x n = B.Bind (B.Void (n :: a), x) in
+        List.fold_left map x ns
 
 and xlate_proj x _ e =
    lenv_fold_left xlate_bind xlate_proj x e