From be1700416b160f793c0368a39600b7f81bfb2e44 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 28 Oct 2009 00:21:36 +0000 Subject: [PATCH] drg->brg translation contibued (still bugged though) --- helm/software/lambda-delta/.depend.opt | 34 +++++++++++++------- helm/software/lambda-delta/dual_rg/drgBrg.ml | 18 ++++++++++- helm/software/lambda-delta/toplevel/top.ml | 7 ++-- 3 files changed, 44 insertions(+), 15 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 19f473c6d..0aed7ab22 100644 --- 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 2510f8920..1f149a759 100644 --- 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 3558dc8d0..6e6ccfc28 100644 --- 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 -- 2.39.2