- lambda-delta: some fixes: now the grundlagen type-checkes through dual_rg

[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 1f149a759f9ce2cd621bb82a31991b80b8153e86..9ff63fb7c3f427c7d005d9699aa3cb70cfe48504 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drgBrg.ml
+++ b/helm/software/lambda-delta/dual_rg/drgBrg.ml
@@ -26,16 +26,16 @@ let rec xlate_term f = function
    | 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 t 
+      xlate_term f u 
    | 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 (ap, e, D.TCast (ac, u, t)) ->
-      xlate_term f (D.TCast (ac, D.TProj (ap, e, u), D.TProj (ap, e, 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.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 (a, b, t)  ->
       let f tt = f (xlate_bind tt a b) in xlate_term f t
 
@@ -61,4 +61,7 @@ and xlate_proj x _ e =
    lenv_fold_left xlate_bind xlate_proj x e
 
 let brg_of_drg f t =
+(*   
+   print_newline (); DrgOutput.pp_term print_string t;
+*)
    f (xlate_term C.start t)