drg->brg translation contibued (still bugged though)

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 19f473c6d9f164d48f6be61f754f604dec364751..0aed7ab220f64b3041782dfed4d9e9bc146a807b 100644 (file)
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -1,9 +1,17 @@
+lib/nUri.cmi: 
 lib/nUri.cmo: lib/nUri.cmi 
 lib/nUri.cmx: lib/nUri.cmi 
+lib/cps.cmo: 
+lib/cps.cmx: 
+lib/share.cmo: 
+lib/share.cmx: 
+lib/log.cmi: 
 lib/log.cmo: lib/cps.cmx lib/log.cmi 
 lib/log.cmx: lib/cps.cmx lib/log.cmi 
 lib/time.cmo: lib/log.cmi 
 lib/time.cmx: lib/log.cmx 
+automath/aut.cmo: 
+automath/aut.cmx: 
 automath/autProcess.cmi: automath/aut.cmx 
 automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi 
 automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi 
@@ -17,8 +25,10 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
 automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi 
 automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi 
 automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx 
+common/hierarchy.cmi: 
 common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi 
 common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi 
+common/output.cmi: 
 common/output.cmo: lib/log.cmi common/output.cmi 
 common/output.cmx: lib/log.cmx common/output.cmi 
 common/entity.cmo: lib/nUri.cmi automath/aut.cmx 
@@ -160,19 +170,19 @@ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \
     toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
     toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \
     common/library.cmi common/hierarchy.cmi common/entity.cmx \
-    dual_rg/drgOutput.cmi dual_rg/drgAut.cmi dual_rg/drg.cmx lib/cps.cmx \
-    basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
-    basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \
-    basic_ag/bagType.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \
-    automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \
-    automath/autLexer.cmx 
+    dual_rg/drgOutput.cmi dual_rg/drgBrg.cmi dual_rg/drgAut.cmi \
+    dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \
+    basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \
+    basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \
+    basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \
+    automath/autOutput.cmi automath/autLexer.cmx 
 toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \
     toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
     toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \
     common/library.cmx common/hierarchy.cmx common/entity.cmx \
-    dual_rg/drgOutput.cmx dual_rg/drgAut.cmx dual_rg/drg.cmx lib/cps.cmx \
-    basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
-    basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \
-    basic_ag/bagType.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \
-    automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \
-    automath/autLexer.cmx 
+    dual_rg/drgOutput.cmx dual_rg/drgBrg.cmx dual_rg/drgAut.cmx \
+    dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
+    basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \
+    basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \
+    basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \
+    automath/autOutput.cmx automath/autLexer.cmx 

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

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 3558dc8d00540d064c6bc3f0046ab59501e9e3d0..6e6ccfc288e34b0838232020c82574c32babe7f4 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -24,7 +24,8 @@ module DA   = DrgAut
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
-module DrgO = DrgOutput
+module DO   = DrgOutput
+module DBrg = DrgBrg
 module MBrg = MetaBrg
 module BrgO = BrgOutput
 module BrgR = BrgReduction
@@ -85,6 +86,8 @@ let print_counters st = match !kernel with
    | Bag -> BagO.print_counters C.start st.bagc
 
 let xlate f st entity = match !kernel, entity with
+   | Brg, DrgEntity e  -> 
+      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_drg e
    | Brg, MetaEntity e -> 
       let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
    | Bag, MetaEntity e -> 
@@ -98,7 +101,7 @@ let count_entity st = function
    | _            -> st
 
 let export_entity si g moch = function
-   | DrgEntity e  -> X.export_entity DrgO.export_term si g e
+   | DrgEntity e  -> X.export_entity DO.export_term si g e
    | BrgEntity e  -> X.old_export_entity BrgO.export_term si g e
    | MetaEntity e ->
       begin match moch with