new module "xml" devoted to xml I/O

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 26f2d959c912284f483b64b3e0a76c90a08af315..c6e6ac18927b86758d020ae6d985cf0bd9990d98 100644 (file)
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -1,332 +1,258 @@
-components/lib/cps.cmo: 
-components/lib/cps.cmx: 
-components/lib/share.cmo: 
-components/lib/share.cmx: 
-components/lib/log.cmi: 
-components/lib/log.cmo: components/lib/cps.cmx components/lib/log.cmi 
-components/lib/log.cmx: components/lib/cps.cmx components/lib/log.cmi 
-components/lib/time.cmo: components/lib/log.cmi 
-components/lib/time.cmx: components/lib/log.cmx 
-components/common/options.cmo: components/lib/cps.cmx 
-components/common/options.cmx: components/lib/cps.cmx 
-components/common/hierarchy.cmi: 
-components/common/hierarchy.cmo: components/lib/cps.cmx \
-    components/common/hierarchy.cmi 
-components/common/hierarchy.cmx: components/lib/cps.cmx \
-    components/common/hierarchy.cmi 
-components/common/output.cmi: 
-components/common/output.cmo: components/common/options.cmx \
-    components/lib/log.cmi components/common/output.cmi 
-components/common/output.cmx: components/common/options.cmx \
-    components/lib/log.cmx components/common/output.cmi 
-components/common/entity.cmo: components/common/options.cmx \
-    components/automath/aut.cmx 
-components/common/entity.cmx: components/common/options.cmx \
-    components/automath/aut.cmx 
-components/common/marks.cmo: components/common/entity.cmx 
-components/common/marks.cmx: components/common/entity.cmx 
-components/common/alpha.cmi: components/common/entity.cmx 
-components/common/alpha.cmo: components/common/entity.cmx \
-    components/common/alpha.cmi 
-components/common/alpha.cmx: components/common/entity.cmx \
-    components/common/alpha.cmi 
-components/common/library.cmi: components/common/entity.cmx 
-components/common/library.cmo: components/common/hierarchy.cmi \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/common/library.cmi 
-components/common/library.cmx: components/common/hierarchy.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/common/library.cmi 
-components/text/txt.cmo: 
-components/text/txt.cmx: 
-components/text/txtParser.cmi: components/text/txt.cmx 
-components/text/txtParser.cmo: components/text/txt.cmx \
-    components/common/options.cmx components/text/txtParser.cmi 
-components/text/txtParser.cmx: components/text/txt.cmx \
-    components/common/options.cmx components/text/txtParser.cmi 
-components/text/txtLexer.cmo: components/text/txtParser.cmi \
-    components/common/options.cmx components/lib/log.cmi 
-components/text/txtLexer.cmx: components/text/txtParser.cmx \
-    components/common/options.cmx components/lib/log.cmx 
-components/text/txtTxt.cmi: components/text/txt.cmx 
-components/text/txtTxt.cmo: components/text/txt.cmx components/lib/cps.cmx \
-    components/text/txtTxt.cmi 
-components/text/txtTxt.cmx: components/text/txt.cmx components/lib/cps.cmx \
-    components/text/txtTxt.cmi 
-components/automath/aut.cmo: 
-components/automath/aut.cmx: 
-components/automath/autProcess.cmi: components/automath/aut.cmx 
-components/automath/autProcess.cmo: components/automath/aut.cmx \
-    components/automath/autProcess.cmi 
-components/automath/autProcess.cmx: components/automath/aut.cmx \
-    components/automath/autProcess.cmi 
-components/automath/autOutput.cmi: components/automath/autProcess.cmi \
-    components/automath/aut.cmx 
-components/automath/autOutput.cmo: components/lib/log.cmi \
-    components/lib/cps.cmx components/automath/autProcess.cmi \
-    components/automath/aut.cmx components/automath/autOutput.cmi 
-components/automath/autOutput.cmx: components/lib/log.cmx \
-    components/lib/cps.cmx components/automath/autProcess.cmx \
-    components/automath/aut.cmx components/automath/autOutput.cmi 
-components/automath/autParser.cmi: components/automath/aut.cmx 
-components/automath/autParser.cmo: components/common/options.cmx \
-    components/automath/aut.cmx components/automath/autParser.cmi 
-components/automath/autParser.cmx: components/common/options.cmx \
-    components/automath/aut.cmx components/automath/autParser.cmi 
-components/automath/autLexer.cmo: components/common/options.cmx \
-    components/lib/log.cmi components/automath/autParser.cmi 
-components/automath/autLexer.cmx: components/common/options.cmx \
-    components/lib/log.cmx components/automath/autParser.cmx 
-components/basic_ag/bag.cmo: components/lib/log.cmi \
-    components/common/entity.cmx components/lib/cps.cmx 
-components/basic_ag/bag.cmx: components/lib/log.cmx \
-    components/common/entity.cmx components/lib/cps.cmx 
-components/basic_ag/bagOutput.cmi: components/lib/log.cmi \
-    components/basic_ag/bag.cmx 
-components/basic_ag/bagOutput.cmo: components/common/options.cmx \
-    components/lib/log.cmi components/common/hierarchy.cmi \
-    components/common/entity.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagOutput.cmi 
-components/basic_ag/bagOutput.cmx: components/common/options.cmx \
-    components/lib/log.cmx components/common/hierarchy.cmx \
-    components/common/entity.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagOutput.cmi 
-components/basic_ag/bagEnvironment.cmi: components/basic_ag/bag.cmx 
-components/basic_ag/bagEnvironment.cmo: components/lib/log.cmi \
-    components/common/entity.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagEnvironment.cmi 
-components/basic_ag/bagEnvironment.cmx: components/lib/log.cmx \
-    components/common/entity.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagEnvironment.cmi 
-components/basic_ag/bagSubstitution.cmi: components/basic_ag/bag.cmx 
-components/basic_ag/bagSubstitution.cmo: components/lib/share.cmx \
-    components/basic_ag/bag.cmx components/basic_ag/bagSubstitution.cmi 
-components/basic_ag/bagSubstitution.cmx: components/lib/share.cmx \
-    components/basic_ag/bag.cmx components/basic_ag/bagSubstitution.cmi 
-components/basic_ag/bagReduction.cmi: components/basic_ag/bag.cmx 
-components/basic_ag/bagReduction.cmo: components/lib/log.cmi \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_ag/bagSubstitution.cmi components/basic_ag/bagOutput.cmi \
-    components/basic_ag/bagEnvironment.cmi components/basic_ag/bag.cmx \
-    components/basic_ag/bagReduction.cmi 
-components/basic_ag/bagReduction.cmx: components/lib/log.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_ag/bagSubstitution.cmx components/basic_ag/bagOutput.cmx \
-    components/basic_ag/bagEnvironment.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagReduction.cmi 
-components/basic_ag/bagType.cmi: components/common/entity.cmx \
-    components/basic_ag/bag.cmx 
-components/basic_ag/bagType.cmo: components/lib/share.cmx \
-    components/lib/log.cmi components/common/hierarchy.cmi \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_ag/bagReduction.cmi components/basic_ag/bagOutput.cmi \
-    components/basic_ag/bagEnvironment.cmi components/basic_ag/bag.cmx \
-    components/basic_ag/bagType.cmi 
-components/basic_ag/bagType.cmx: components/lib/share.cmx \
-    components/lib/log.cmx components/common/hierarchy.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_ag/bagReduction.cmx components/basic_ag/bagOutput.cmx \
-    components/basic_ag/bagEnvironment.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagType.cmi 
-components/basic_ag/bagUntrusted.cmi: components/common/entity.cmx \
-    components/basic_ag/bag.cmx 
-components/basic_ag/bagUntrusted.cmo: components/lib/log.cmi \
-    components/common/entity.cmx components/basic_ag/bagType.cmi \
-    components/basic_ag/bagEnvironment.cmi components/basic_ag/bag.cmx \
-    components/basic_ag/bagUntrusted.cmi 
-components/basic_ag/bagUntrusted.cmx: components/lib/log.cmx \
-    components/common/entity.cmx components/basic_ag/bagType.cmx \
-    components/basic_ag/bagEnvironment.cmx components/basic_ag/bag.cmx \
-    components/basic_ag/bagUntrusted.cmi 
-components/basic_rg/brg.cmo: components/common/entity.cmx 
-components/basic_rg/brg.cmx: components/common/entity.cmx 
-components/basic_rg/brgOutput.cmi: components/lib/log.cmi \
-    components/common/library.cmi components/basic_rg/brg.cmx 
-components/basic_rg/brgOutput.cmo: components/common/options.cmx \
-    components/lib/log.cmi components/common/library.cmi \
-    components/common/hierarchy.cmi components/common/entity.cmx \
-    components/lib/cps.cmx components/basic_rg/brg.cmx \
-    components/basic_rg/brgOutput.cmi 
-components/basic_rg/brgOutput.cmx: components/common/options.cmx \
-    components/lib/log.cmx components/common/library.cmx \
-    components/common/hierarchy.cmx components/common/entity.cmx \
-    components/lib/cps.cmx components/basic_rg/brg.cmx \
-    components/basic_rg/brgOutput.cmi 
-components/basic_rg/brgEnvironment.cmi: components/basic_rg/brg.cmx 
-components/basic_rg/brgEnvironment.cmo: components/common/entity.cmx \
-    components/basic_rg/brg.cmx components/basic_rg/brgEnvironment.cmi 
-components/basic_rg/brgEnvironment.cmx: components/common/entity.cmx \
-    components/basic_rg/brg.cmx components/basic_rg/brgEnvironment.cmi 
-components/basic_rg/brgSubstitution.cmi: components/basic_rg/brg.cmx 
-components/basic_rg/brgSubstitution.cmo: components/basic_rg/brg.cmx \
-    components/basic_rg/brgSubstitution.cmi 
-components/basic_rg/brgSubstitution.cmx: components/basic_rg/brg.cmx \
-    components/basic_rg/brgSubstitution.cmi 
-components/basic_rg/brgReduction.cmi: components/lib/log.cmi \
-    components/common/entity.cmx components/basic_rg/brg.cmx 
-components/basic_rg/brgReduction.cmo: components/lib/share.cmx \
-    components/common/output.cmi components/lib/log.cmi \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_rg/brgOutput.cmi components/basic_rg/brgEnvironment.cmi \
-    components/basic_rg/brg.cmx components/basic_rg/brgReduction.cmi 
-components/basic_rg/brgReduction.cmx: components/lib/share.cmx \
-    components/common/output.cmx components/lib/log.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_rg/brgOutput.cmx components/basic_rg/brgEnvironment.cmx \
-    components/basic_rg/brg.cmx components/basic_rg/brgReduction.cmi 
-components/basic_rg/brgType.cmi: components/lib/log.cmi \
-    components/common/entity.cmx components/basic_rg/brgReduction.cmi \
-    components/basic_rg/brg.cmx 
-components/basic_rg/brgType.cmo: components/lib/share.cmx \
-    components/lib/log.cmi components/common/hierarchy.cmi \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_rg/brgSubstitution.cmi \
-    components/basic_rg/brgReduction.cmi components/basic_rg/brgOutput.cmi \
-    components/basic_rg/brgEnvironment.cmi components/basic_rg/brg.cmx \
-    components/basic_rg/brgType.cmi 
-components/basic_rg/brgType.cmx: components/lib/share.cmx \
-    components/lib/log.cmx components/common/hierarchy.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_rg/brgSubstitution.cmx \
-    components/basic_rg/brgReduction.cmx components/basic_rg/brgOutput.cmx \
-    components/basic_rg/brgEnvironment.cmx components/basic_rg/brg.cmx \
-    components/basic_rg/brgType.cmi 
-components/basic_rg/brgUntrusted.cmi: components/common/entity.cmx \
-    components/basic_rg/brgType.cmi components/basic_rg/brg.cmx 
-components/basic_rg/brgUntrusted.cmo: components/lib/log.cmi \
-    components/common/entity.cmx components/basic_rg/brgType.cmi \
-    components/basic_rg/brgReduction.cmi \
-    components/basic_rg/brgEnvironment.cmi components/basic_rg/brg.cmx \
-    components/basic_rg/brgUntrusted.cmi 
-components/basic_rg/brgUntrusted.cmx: components/lib/log.cmx \
-    components/common/entity.cmx components/basic_rg/brgType.cmx \
-    components/basic_rg/brgReduction.cmx \
-    components/basic_rg/brgEnvironment.cmx components/basic_rg/brg.cmx \
-    components/basic_rg/brgUntrusted.cmi 
-components/complete_rg/crg.cmo: components/common/entity.cmx 
-components/complete_rg/crg.cmx: components/common/entity.cmx 
-components/complete_rg/crgOutput.cmi: components/complete_rg/crg.cmx 
-components/complete_rg/crgOutput.cmo: components/common/hierarchy.cmi \
-    components/common/entity.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/complete_rg/crgOutput.cmi 
-components/complete_rg/crgOutput.cmx: components/common/hierarchy.cmx \
-    components/common/entity.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/complete_rg/crgOutput.cmi 
-components/complete_rg/crgXml.cmi: components/common/library.cmi \
-    components/complete_rg/crg.cmx 
-components/complete_rg/crgXml.cmo: components/common/library.cmi \
-    components/common/hierarchy.cmi components/common/entity.cmx \
-    components/complete_rg/crg.cmx components/lib/cps.cmx \
-    components/common/alpha.cmi components/complete_rg/crgXml.cmi 
-components/complete_rg/crgXml.cmx: components/common/library.cmx \
-    components/common/hierarchy.cmx components/common/entity.cmx \
-    components/complete_rg/crg.cmx components/lib/cps.cmx \
-    components/common/alpha.cmx components/complete_rg/crgXml.cmi 
-components/complete_rg/crgTxt.cmi: components/text/txt.cmx \
-    components/complete_rg/crg.cmx 
-components/complete_rg/crgTxt.cmo: components/text/txtTxt.cmi \
-    components/text/txt.cmx components/common/options.cmx \
-    components/common/hierarchy.cmi components/common/entity.cmx \
-    components/complete_rg/crg.cmx components/lib/cps.cmx \
-    components/complete_rg/crgTxt.cmi 
-components/complete_rg/crgTxt.cmx: components/text/txtTxt.cmx \
-    components/text/txt.cmx components/common/options.cmx \
-    components/common/hierarchy.cmx components/common/entity.cmx \
-    components/complete_rg/crg.cmx components/lib/cps.cmx \
-    components/complete_rg/crgTxt.cmi 
-components/complete_rg/crgAut.cmi: components/complete_rg/crg.cmx \
-    components/automath/aut.cmx 
-components/complete_rg/crgAut.cmo: components/common/options.cmx \
-    components/common/entity.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/automath/aut.cmx \
-    components/complete_rg/crgAut.cmi 
-components/complete_rg/crgAut.cmx: components/common/options.cmx \
-    components/common/entity.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/automath/aut.cmx \
-    components/complete_rg/crgAut.cmi 
-components/complete_rg/crgBrg.cmi: components/complete_rg/crg.cmx \
-    components/basic_rg/brg.cmx 
-components/complete_rg/crgBrg.cmo: components/common/marks.cmx \
-    components/common/entity.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/basic_rg/brg.cmx \
-    components/complete_rg/crgBrg.cmi 
-components/complete_rg/crgBrg.cmx: components/common/marks.cmx \
-    components/common/entity.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/basic_rg/brg.cmx \
-    components/complete_rg/crgBrg.cmi 
-components/toplevel/meta.cmo: components/common/entity.cmx 
-components/toplevel/meta.cmx: components/common/entity.cmx 
-components/toplevel/metaOutput.cmi: components/toplevel/meta.cmx 
-components/toplevel/metaOutput.cmo: components/toplevel/meta.cmx \
-    components/lib/log.cmi components/common/entity.cmx \
-    components/lib/cps.cmx components/toplevel/metaOutput.cmi 
-components/toplevel/metaOutput.cmx: components/toplevel/meta.cmx \
-    components/lib/log.cmx components/common/entity.cmx \
-    components/lib/cps.cmx components/toplevel/metaOutput.cmi 
-components/toplevel/metaLibrary.cmi: components/toplevel/meta.cmx 
-components/toplevel/metaLibrary.cmo: components/toplevel/metaOutput.cmi \
-    components/toplevel/metaLibrary.cmi 
-components/toplevel/metaLibrary.cmx: components/toplevel/metaOutput.cmx \
-    components/toplevel/metaLibrary.cmi 
-components/toplevel/metaAut.cmi: components/toplevel/meta.cmx \
-    components/automath/aut.cmx 
-components/toplevel/metaAut.cmo: components/common/options.cmx \
-    components/toplevel/meta.cmx components/common/entity.cmx \
-    components/lib/cps.cmx components/automath/aut.cmx \
-    components/toplevel/metaAut.cmi 
-components/toplevel/metaAut.cmx: components/common/options.cmx \
-    components/toplevel/meta.cmx components/common/entity.cmx \
-    components/lib/cps.cmx components/automath/aut.cmx \
-    components/toplevel/metaAut.cmi 
-components/toplevel/metaBag.cmi: components/toplevel/meta.cmx \
-    components/basic_ag/bag.cmx 
-components/toplevel/metaBag.cmo: components/toplevel/meta.cmx \
-    components/lib/cps.cmx components/basic_ag/bag.cmx \
-    components/toplevel/metaBag.cmi 
-components/toplevel/metaBag.cmx: components/toplevel/meta.cmx \
-    components/lib/cps.cmx components/basic_ag/bag.cmx \
-    components/toplevel/metaBag.cmi 
-components/toplevel/metaBrg.cmi: components/toplevel/meta.cmx \
-    components/basic_rg/brg.cmx 
-components/toplevel/metaBrg.cmo: components/toplevel/meta.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_rg/brg.cmx components/toplevel/metaBrg.cmi 
-components/toplevel/metaBrg.cmx: components/toplevel/meta.cmx \
-    components/common/entity.cmx components/lib/cps.cmx \
-    components/basic_rg/brg.cmx components/toplevel/metaBrg.cmi 
-components/toplevel/top.cmo: components/text/txtParser.cmi \
-    components/text/txtLexer.cmx components/text/txt.cmx \
-    components/lib/time.cmx components/common/output.cmi \
-    components/common/options.cmx components/toplevel/metaOutput.cmi \
-    components/toplevel/metaLibrary.cmi components/toplevel/metaBrg.cmi \
-    components/toplevel/metaBag.cmi components/toplevel/metaAut.cmi \
-    components/toplevel/meta.cmx components/lib/log.cmi \
-    components/common/library.cmi components/common/hierarchy.cmi \
-    components/common/entity.cmx components/complete_rg/crgXml.cmi \
-    components/complete_rg/crgTxt.cmi components/complete_rg/crgBrg.cmi \
-    components/complete_rg/crgAut.cmi components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/basic_rg/brgUntrusted.cmi \
-    components/basic_rg/brgReduction.cmi components/basic_rg/brgOutput.cmi \
-    components/basic_rg/brg.cmx components/basic_ag/bagUntrusted.cmi \
-    components/basic_ag/bagType.cmi components/basic_ag/bagOutput.cmi \
-    components/basic_ag/bag.cmx components/automath/autProcess.cmi \
-    components/automath/autParser.cmi components/automath/autOutput.cmi \
-    components/automath/autLexer.cmx components/automath/aut.cmx 
-components/toplevel/top.cmx: components/text/txtParser.cmx \
-    components/text/txtLexer.cmx components/text/txt.cmx \
-    components/lib/time.cmx components/common/output.cmx \
-    components/common/options.cmx components/toplevel/metaOutput.cmx \
-    components/toplevel/metaLibrary.cmx components/toplevel/metaBrg.cmx \
-    components/toplevel/metaBag.cmx components/toplevel/metaAut.cmx \
-    components/toplevel/meta.cmx components/lib/log.cmx \
-    components/common/library.cmx components/common/hierarchy.cmx \
-    components/common/entity.cmx components/complete_rg/crgXml.cmx \
-    components/complete_rg/crgTxt.cmx components/complete_rg/crgBrg.cmx \
-    components/complete_rg/crgAut.cmx components/complete_rg/crg.cmx \
-    components/lib/cps.cmx components/basic_rg/brgUntrusted.cmx \
-    components/basic_rg/brgReduction.cmx components/basic_rg/brgOutput.cmx \
-    components/basic_rg/brg.cmx components/basic_ag/bagUntrusted.cmx \
-    components/basic_ag/bagType.cmx components/basic_ag/bagOutput.cmx \
-    components/basic_ag/bag.cmx components/automath/autProcess.cmx \
-    components/automath/autParser.cmx components/automath/autOutput.cmx \
-    components/automath/autLexer.cmx components/automath/aut.cmx 
+src/lib/cps.cmo: 
+src/lib/cps.cmx: 
+src/lib/share.cmo: 
+src/lib/share.cmx: 
+src/lib/log.cmi: 
+src/lib/log.cmo: src/lib/cps.cmx src/lib/log.cmi 
+src/lib/log.cmx: src/lib/cps.cmx src/lib/log.cmi 
+src/lib/time.cmo: src/lib/log.cmi 
+src/lib/time.cmx: src/lib/log.cmx 
+src/common/options.cmo: src/lib/cps.cmx 
+src/common/options.cmx: src/lib/cps.cmx 
+src/common/hierarchy.cmi: 
+src/common/hierarchy.cmo: src/lib/cps.cmx src/common/hierarchy.cmi 
+src/common/hierarchy.cmx: src/lib/cps.cmx src/common/hierarchy.cmi 
+src/common/output.cmi: 
+src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \
+    src/common/output.cmi 
+src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \
+    src/common/output.cmi 
+src/common/entity.cmo: src/common/options.cmx src/automath/aut.cmx 
+src/common/entity.cmx: src/common/options.cmx src/automath/aut.cmx 
+src/common/marks.cmo: src/common/entity.cmx 
+src/common/marks.cmx: src/common/entity.cmx 
+src/common/alpha.cmi: src/common/entity.cmx 
+src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi 
+src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi 
+src/common/library.cmi: src/common/entity.cmx 
+src/common/library.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
+    src/lib/cps.cmx src/common/library.cmi 
+src/common/library.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
+    src/lib/cps.cmx src/common/library.cmi 
+src/text/txt.cmo: 
+src/text/txt.cmx: 
+src/text/txtParser.cmi: src/text/txt.cmx 
+src/text/txtParser.cmo: src/text/txt.cmx src/common/options.cmx \
+    src/text/txtParser.cmi 
+src/text/txtParser.cmx: src/text/txt.cmx src/common/options.cmx \
+    src/text/txtParser.cmi 
+src/text/txtLexer.cmo: src/text/txtParser.cmi src/common/options.cmx \
+    src/lib/log.cmi 
+src/text/txtLexer.cmx: src/text/txtParser.cmx src/common/options.cmx \
+    src/lib/log.cmx 
+src/text/txtTxt.cmi: src/text/txt.cmx 
+src/text/txtTxt.cmo: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi 
+src/text/txtTxt.cmx: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi 
+src/automath/aut.cmo: 
+src/automath/aut.cmx: 
+src/automath/autProcess.cmi: src/automath/aut.cmx 
+src/automath/autProcess.cmo: src/automath/aut.cmx src/automath/autProcess.cmi 
+src/automath/autProcess.cmx: src/automath/aut.cmx src/automath/autProcess.cmi 
+src/automath/autOutput.cmi: src/automath/autProcess.cmi src/automath/aut.cmx 
+src/automath/autOutput.cmo: src/lib/log.cmi src/lib/cps.cmx \
+    src/automath/autProcess.cmi src/automath/aut.cmx \
+    src/automath/autOutput.cmi 
+src/automath/autOutput.cmx: src/lib/log.cmx src/lib/cps.cmx \
+    src/automath/autProcess.cmx src/automath/aut.cmx \
+    src/automath/autOutput.cmi 
+src/automath/autParser.cmi: src/automath/aut.cmx 
+src/automath/autParser.cmo: src/common/options.cmx src/automath/aut.cmx \
+    src/automath/autParser.cmi 
+src/automath/autParser.cmx: src/common/options.cmx src/automath/aut.cmx \
+    src/automath/autParser.cmi 
+src/automath/autLexer.cmo: src/common/options.cmx src/lib/log.cmi \
+    src/automath/autParser.cmi 
+src/automath/autLexer.cmx: src/common/options.cmx src/lib/log.cmx \
+    src/automath/autParser.cmx 
+src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx 
+src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx 
+src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx 
+src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \
+    src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagOutput.cmi 
+src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \
+    src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagOutput.cmi 
+src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx 
+src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \
+    src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi 
+src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \
+    src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi 
+src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx 
+src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagSubstitution.cmi 
+src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagSubstitution.cmi 
+src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx 
+src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \
+    src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \
+    src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi 
+src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \
+    src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \
+    src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi 
+src/basic_ag/bagType.cmi: src/common/entity.cmx src/basic_ag/bag.cmx 
+src/basic_ag/bagType.cmo: src/lib/share.cmx src/lib/log.cmi \
+    src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \
+    src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
+    src/basic_ag/bagType.cmi 
+src/basic_ag/bagType.cmx: src/lib/share.cmx src/lib/log.cmx \
+    src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \
+    src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
+    src/basic_ag/bagType.cmi 
+src/basic_ag/bagUntrusted.cmi: src/common/entity.cmx src/basic_ag/bag.cmx 
+src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
+    src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \
+    src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi 
+src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
+    src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \
+    src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi 
+src/basic_rg/brg.cmo: src/common/entity.cmx 
+src/basic_rg/brg.cmx: src/common/entity.cmx 
+src/basic_rg/brgOutput.cmi: src/lib/log.cmi src/common/library.cmi \
+    src/basic_rg/brg.cmx 
+src/basic_rg/brgOutput.cmo: src/common/options.cmx src/lib/log.cmi \
+    src/common/library.cmi src/common/hierarchy.cmi src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi 
+src/basic_rg/brgOutput.cmx: src/common/options.cmx src/lib/log.cmx \
+    src/common/library.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi 
+src/basic_rg/brgEnvironment.cmi: src/basic_rg/brg.cmx 
+src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx src/basic_rg/brg.cmx \
+    src/basic_rg/brgEnvironment.cmi 
+src/basic_rg/brgEnvironment.cmx: src/common/entity.cmx src/basic_rg/brg.cmx \
+    src/basic_rg/brgEnvironment.cmi 
+src/basic_rg/brgSubstitution.cmi: src/basic_rg/brg.cmx 
+src/basic_rg/brgSubstitution.cmo: src/basic_rg/brg.cmx \
+    src/basic_rg/brgSubstitution.cmi 
+src/basic_rg/brgSubstitution.cmx: src/basic_rg/brg.cmx \
+    src/basic_rg/brgSubstitution.cmi 
+src/basic_rg/brgReduction.cmi: src/lib/log.cmi src/common/entity.cmx \
+    src/basic_rg/brg.cmx 
+src/basic_rg/brgReduction.cmo: src/lib/share.cmx src/common/output.cmi \
+    src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \
+    src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi 
+src/basic_rg/brgReduction.cmx: src/lib/share.cmx src/common/output.cmx \
+    src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \
+    src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi 
+src/basic_rg/brgType.cmi: src/lib/log.cmi src/common/entity.cmx \
+    src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx 
+src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \
+    src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \
+    src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \
+    src/basic_rg/brg.cmx src/basic_rg/brgType.cmi 
+src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \
+    src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
+    src/basic_rg/brgSubstitution.cmx src/basic_rg/brgReduction.cmx \
+    src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \
+    src/basic_rg/brg.cmx src/basic_rg/brgType.cmi 
+src/basic_rg/brgUntrusted.cmi: src/common/entity.cmx src/basic_rg/brgType.cmi \
+    src/basic_rg/brg.cmx 
+src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
+    src/basic_rg/brgType.cmi src/basic_rg/brgReduction.cmi \
+    src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
+    src/basic_rg/brgUntrusted.cmi 
+src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
+    src/basic_rg/brgType.cmx src/basic_rg/brgReduction.cmx \
+    src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
+    src/basic_rg/brgUntrusted.cmi 
+src/complete_rg/crg.cmo: src/common/entity.cmx 
+src/complete_rg/crg.cmx: src/common/entity.cmx 
+src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx 
+src/complete_rg/crgOutput.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi 
+src/complete_rg/crgOutput.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgOutput.cmi 
+src/complete_rg/crgXml.cmi: src/common/library.cmi src/complete_rg/crg.cmx 
+src/complete_rg/crgXml.cmo: src/common/library.cmi src/common/hierarchy.cmi \
+    src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/common/alpha.cmi src/complete_rg/crgXml.cmi 
+src/complete_rg/crgXml.cmx: src/common/library.cmx src/common/hierarchy.cmx \
+    src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/common/alpha.cmx src/complete_rg/crgXml.cmi 
+src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx 
+src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
+    src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi 
+src/complete_rg/crgTxt.cmx: src/text/txtTxt.cmx src/text/txt.cmx \
+    src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi 
+src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx 
+src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
+    src/complete_rg/crgAut.cmi 
+src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
+    src/complete_rg/crgAut.cmi 
+src/complete_rg/crgBrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx 
+src/complete_rg/crgBrg.cmo: src/common/marks.cmx src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+    src/complete_rg/crgBrg.cmi 
+src/complete_rg/crgBrg.cmx: src/common/marks.cmx src/common/entity.cmx \
+    src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+    src/complete_rg/crgBrg.cmi 
+src/toplevel/meta.cmo: src/common/entity.cmx 
+src/toplevel/meta.cmx: src/common/entity.cmx 
+src/toplevel/metaOutput.cmi: src/toplevel/meta.cmx 
+src/toplevel/metaOutput.cmo: src/toplevel/meta.cmx src/lib/log.cmi \
+    src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi 
+src/toplevel/metaOutput.cmx: src/toplevel/meta.cmx src/lib/log.cmx \
+    src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi 
+src/toplevel/metaLibrary.cmi: src/toplevel/meta.cmx 
+src/toplevel/metaLibrary.cmo: src/toplevel/metaOutput.cmi \
+    src/toplevel/metaLibrary.cmi 
+src/toplevel/metaLibrary.cmx: src/toplevel/metaOutput.cmx \
+    src/toplevel/metaLibrary.cmi 
+src/toplevel/metaAut.cmi: src/toplevel/meta.cmx src/automath/aut.cmx 
+src/toplevel/metaAut.cmo: src/common/options.cmx src/toplevel/meta.cmx \
+    src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \
+    src/toplevel/metaAut.cmi 
+src/toplevel/metaAut.cmx: src/common/options.cmx src/toplevel/meta.cmx \
+    src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \
+    src/toplevel/metaAut.cmi 
+src/toplevel/metaBag.cmi: src/toplevel/meta.cmx src/basic_ag/bag.cmx 
+src/toplevel/metaBag.cmo: src/toplevel/meta.cmx src/lib/cps.cmx \
+    src/basic_ag/bag.cmx src/toplevel/metaBag.cmi 
+src/toplevel/metaBag.cmx: src/toplevel/meta.cmx src/lib/cps.cmx \
+    src/basic_ag/bag.cmx src/toplevel/metaBag.cmi 
+src/toplevel/metaBrg.cmi: src/toplevel/meta.cmx src/basic_rg/brg.cmx 
+src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi 
+src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/entity.cmx \
+    src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi 
+src/toplevel/top.cmo: src/text/txtParser.cmi src/text/txtLexer.cmx \
+    src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \
+    src/common/options.cmx src/toplevel/metaOutput.cmi \
+    src/toplevel/metaLibrary.cmi src/toplevel/metaBrg.cmi \
+    src/toplevel/metaBag.cmi src/toplevel/metaAut.cmi src/toplevel/meta.cmx \
+    src/lib/log.cmi src/common/library.cmi src/common/hierarchy.cmi \
+    src/common/entity.cmx src/complete_rg/crgXml.cmi \
+    src/complete_rg/crgTxt.cmi src/complete_rg/crgBrg.cmi \
+    src/complete_rg/crgAut.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
+    src/basic_rg/brgOutput.cmi src/basic_rg/brg.cmx \
+    src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \
+    src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \
+    src/automath/autProcess.cmi src/automath/autParser.cmi \
+    src/automath/autOutput.cmi src/automath/autLexer.cmx src/automath/aut.cmx 
+src/toplevel/top.cmx: src/text/txtParser.cmx src/text/txtLexer.cmx \
+    src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \
+    src/common/options.cmx src/toplevel/metaOutput.cmx \
+    src/toplevel/metaLibrary.cmx src/toplevel/metaBrg.cmx \
+    src/toplevel/metaBag.cmx src/toplevel/metaAut.cmx src/toplevel/meta.cmx \
+    src/lib/log.cmx src/common/library.cmx src/common/hierarchy.cmx \
+    src/common/entity.cmx src/complete_rg/crgXml.cmx \
+    src/complete_rg/crgTxt.cmx src/complete_rg/crgBrg.cmx \
+    src/complete_rg/crgAut.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
+    src/basic_rg/brgOutput.cmx src/basic_rg/brg.cmx \
+    src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \
+    src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \
+    src/automath/autProcess.cmx src/automath/autParser.cmx \
+    src/automath/autOutput.cmx src/automath/autLexer.cmx src/automath/aut.cmx 

diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index 17ed69d21720b40cb4ed97ee81d78df71518ac29..a6fcf6c4811aa86a59db6c07dfa723d4253b0381 100644 (file)
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -1,7 +1,11 @@
 MAIN = helena
 
+SRC  = src
+
 REQUIRES = unix str helm-ng_kernel
 
+OCAMLOPTIONS = -rectypes 
+
 KEEP = README
 
 CLEAN = etc/log.txt etc/profile.txt

diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common
index 25e67cc1be2949042799dfc6b30411b68ad2807e..c47540beac9ff2e3c5aed7b0f4ffea6de23517f3 100644 (file)
--- a/helm/software/lambda-delta/Makefile.common
+++ b/helm/software/lambda-delta/Makefile.common
@@ -9,14 +9,13 @@ LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl
 LDDLDIR = /projects/helm/public_html/lambda-delta/static/lddl
 DOWNDIR = /projects/helm/public_html/lambda-delta/download
 XMLDIR  = /projects/helm/public_html/lambda-delta/xml
-SRC     = components
 
 DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make))
 
 INCLUDES = $(DIRECTORIES:%=-I %) 
 
 OCAMLDEP  = $(OCAMLFIND) ocamldep -native $(INCLUDES)
-OCAMLOPT  = $(OCAMLFIND) opt -rectypes -linkpkg -package "$(REQUIRES)" $(INCLUDES)
+OCAMLOPT  = $(OCAMLFIND) opt $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES)
 OCAMLLEX  = ocamllex.opt
 OCAMLYACC = ocamlyacc -v
 XMLLINT   = xmllint --noout

diff --git a/helm/software/lambda-delta/src/Make b/helm/software/lambda-delta/src/Make
index 8e332c33b7453a26d840fcd5c162148b08e61203..abc5de2e17a4e49d35af620ab3e1ea1ea25111d6 100644 (file)
--- a/helm/software/lambda-delta/src/Make
+++ b/helm/software/lambda-delta/src/Make
@@ -1 +1 @@
-lib common text automath basic_ag basic_rg complete_rg toplevel
+lib common text automath basic_ag complete_rg xml basic_rg toplevel

diff --git a/helm/software/lambda-delta/src/basic_rg/Make b/helm/software/lambda-delta/src/basic_rg/Make
index ee53ca212c4a42e4800ff17ea0ce5a1fc257800e..ccbbf500384f852b7810100d47f4a8620baaa143 100644 (file)
--- a/helm/software/lambda-delta/src/basic_rg/Make
+++ b/helm/software/lambda-delta/src/basic_rg/Make
@@ -1,2 +1,2 @@
-brg brgOutput
+brg brgCrg brgOutput
 brgEnvironment brgSubstitution brgReduction brgType brgUntrusted

diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
new file mode 100644 (file)
index 0000000..2b31293
--- /dev/null
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml
@@ -0,0 +1,101 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module C = Cps
+module Y = Entity
+module M = Marks
+module D = Crg
+module B = Brg
+
+(* internal functions: crg to brg term **************************************)
+
+let rec lenv_fold_left map1 map2 x = function
+   | D.ESort            -> x
+   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
+   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
+
+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 Y.apix C.err f a
+   | 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 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 (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
+
+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 (n :: M.new_mark () :: a, B.Abst 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_proj x _ e =
+   lenv_fold_left xlate_bind xlate_proj x e
+
+(* 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 uu tt = f (D.TCast (a, uu, tt)) in
+      let f uu = xlate_bk_term (f uu) t in
+      xlate_bk_term f u 
+   | B.Appl (a, u, t)  ->
+      let f uu tt = f (D.TAppl (a, [uu], tt)) in
+      let f uu = xlate_bk_term (f uu) t in
+      xlate_bk_term f u 
+   | B.Bind (a, b, t)  ->
+      let f bb tt = f (D.TBind (a, bb, tt)) in
+      let f bb = xlate_bk_term (f bb) t in
+      xlate_bk_bind f b
+
+and xlate_bk_bind f = function
+   | B.Abst t ->
+      let f tt = f (D.Abst [tt]) in
+      xlate_bk_term f t
+   | B.Abbr t ->
+      let f tt = f (D.Abbr [tt]) in
+      xlate_bk_term f t
+   | B.Void   -> f (D.Void 1)
+   
+(* interface functions ******************************************************)
+
+let brg_of_crg f t =
+   f (xlate_term C.start t)
+
+let crg_of_brg = xlate_bk_term

diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.mli b/helm/software/lambda-delta/src/basic_rg/brgCrg.mli
new file mode 100644 (file)
index 0000000..84c7f23
--- /dev/null
+++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.mli
@@ -0,0 +1,14 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+val brg_of_crg: (Brg.term -> 'a) -> Crg.term -> 'a
+
+val crg_of_brg: (Crg.term -> 'a) -> Brg.term -> 'a

diff --git a/helm/software/lambda-delta/src/common/library.ml b/helm/software/lambda-delta/src/common/library.ml
deleted file mode 100644 (file)
index 8a68011..0000000
--- a/helm/software/lambda-delta/src/common/library.ml
+++ /dev/null
@@ -1,132 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module F = Filename
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-
-(* internal functions *******************************************************)
-
-let base = "xml"
-
-let obj_ext = ".xml"
-
-let root = "ENTITY"
-
-let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
-
-let path_of_uri xdir uri =
-   let base = F.concat xdir base in 
-   F.concat base (Str.string_after (U.string_of_uri uri) 3)
-
-(* interface functions ******************************************************)
-
-type och = string -> unit
-
-type attr = string * string
-
-type pp = och -> int -> unit
-
-let attribute out (name, contents) =
-   if contents <> "" then begin
-      out " "; out name; out "=\""; out contents; out "\""
-   end
-
-let xml out version encoding =
-   out "<?xml";
-      attribute out ("version", version);
-      attribute out ("encoding", encoding);
-   out "?>\n\n"
-
-let doctype out root system =
-   out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
-
-let tag tag attrs ?contents out indent =
-   let spc = String.make indent ' ' in
-   out spc; out "<"; out tag; List.iter (attribute out) attrs;
-   match contents with
-      | None      -> out "/>\n"
-      | Some cont -> 
-         out ">\n"; cont out (indent + 3); out spc; 
-        out "</"; out tag; out ">\n"
-
-let sort = "Sort"
-
-let lref = "LRef"
-
-let gref = "GRef"
-
-let cast = "Cast"
-
-let appl = "Appl"
-
-let proj = "Proj"
-
-let abst = "Abst"
-
-let abbr = "Abbr"
-
-let void = "Void"
-
-let position i =
-   "position", string_of_int i
-
-let offset j = 
-   let contents = if j > 0 then string_of_int j else "" in
-   "offset", contents
-
-let uri u =
-   "uri", U.string_of_uri u
-
-let arity n =
-   let contents = if n > 1 then string_of_int n else "" in
-   "arity", contents
-
-let name a =
-   let map f i n r s =
-      let n = if r then n else "^" ^ n in 
-      let spc = if i then "" else " " in
-      f (s ^ n ^ spc)
-   in
-   let f s = "name", s in
-   Y.names f map a ""
-
-let mark a =
-   let err () = "mark", "" in
-   let f i = "mark", string_of_int i in
-   Y.mark err f a
-
-(* TODO: the string s must be quoted *)
-let meta a =
-   let err () = "meta", "" in
-   let f s = "meta", s in
-   Y.meta err f a
-
-let export_entity pp_term si xdir (a, u, b) =
-   let path = path_of_uri xdir u in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
-   let och = open_out (path ^ obj_ext) in
-   let out = output_string och in
-   xml out "1.0" "UTF-8"; doctype out root system;
-   let a = Y.Name (U.name_of_uri u, true) :: a in
-   let attrs = [uri u; name a; mark a; meta a] in 
-   let contents = match b with
-      | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) 
-      | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
-      | Y.Void   -> assert false
-   in
-   let opts = if si then "si" else "" in
-   let shp = H.string_of_graph () in
-   let attrs = ["hierarchy", shp; "options", opts] in
-   tag root attrs ~contents out 0;
-   close_out och

diff --git a/helm/software/lambda-delta/src/common/library.mli b/helm/software/lambda-delta/src/common/library.mli
deleted file mode 100644 (file)
index ed3f7bb..0000000
--- a/helm/software/lambda-delta/src/common/library.mli
+++ /dev/null
@@ -1,53 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-type och = string -> unit
-
-type attr = string * string
-
-type pp = och -> int -> unit
-
-val export_entity:
-   ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
-
-val tag: string -> attr list -> ?contents:pp -> pp 
-
-val sort: string
-
-val lref: string
-
-val gref: string
-
-val cast: string
-
-val appl: string
-
-val proj: string
-
-val abst: string
-
-val abbr: string
-
-val void: string
-
-val position: int -> attr
-
-val offset: int -> attr
-
-val uri: Entity.uri -> attr
-
-val arity: int -> attr
-
-val name: Entity.attrs -> attr
-
-val mark: Entity.attrs -> attr
-
-val meta: Entity.attrs -> attr

diff --git a/helm/software/lambda-delta/src/complete_rg/Make b/helm/software/lambda-delta/src/complete_rg/Make
index d7a45f9d29f5e3b47fa5e6110cec688909d73bf4..ccb5b15595aa9be4852979fcb994e69adf88fdc0 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/Make
+++ b/helm/software/lambda-delta/src/complete_rg/Make
@@ -1 +1 @@
-crg crgOutput crgXml crgTxt crgAut crgBrg
+crg crgOutput crgTxt crgAut

diff --git a/helm/software/lambda-delta/src/complete_rg/crgBrg.ml b/helm/software/lambda-delta/src/complete_rg/crgBrg.ml
deleted file mode 100644 (file)
index 2b31293..0000000
--- a/helm/software/lambda-delta/src/complete_rg/crgBrg.ml
+++ /dev/null
@@ -1,101 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module C = Cps
-module Y = Entity
-module M = Marks
-module D = Crg
-module B = Brg
-
-(* internal functions: crg to brg term **************************************)
-
-let rec lenv_fold_left map1 map2 x = function
-   | D.ESort            -> x
-   | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
-   | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
-
-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 Y.apix C.err f a
-   | 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 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 (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
-
-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 (n :: M.new_mark () :: a, B.Abst 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_proj x _ e =
-   lenv_fold_left xlate_bind xlate_proj x e
-
-(* 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 uu tt = f (D.TCast (a, uu, tt)) in
-      let f uu = xlate_bk_term (f uu) t in
-      xlate_bk_term f u 
-   | B.Appl (a, u, t)  ->
-      let f uu tt = f (D.TAppl (a, [uu], tt)) in
-      let f uu = xlate_bk_term (f uu) t in
-      xlate_bk_term f u 
-   | B.Bind (a, b, t)  ->
-      let f bb tt = f (D.TBind (a, bb, tt)) in
-      let f bb = xlate_bk_term (f bb) t in
-      xlate_bk_bind f b
-
-and xlate_bk_bind f = function
-   | B.Abst t ->
-      let f tt = f (D.Abst [tt]) in
-      xlate_bk_term f t
-   | B.Abbr t ->
-      let f tt = f (D.Abbr [tt]) in
-      xlate_bk_term f t
-   | B.Void   -> f (D.Void 1)
-   
-(* interface functions ******************************************************)
-
-let brg_of_crg f t =
-   f (xlate_term C.start t)
-
-let crg_of_brg = xlate_bk_term

diff --git a/helm/software/lambda-delta/src/complete_rg/crgBrg.mli b/helm/software/lambda-delta/src/complete_rg/crgBrg.mli
deleted file mode 100644 (file)
index 84c7f23..0000000
--- a/helm/software/lambda-delta/src/complete_rg/crgBrg.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-val brg_of_crg: (Brg.term -> 'a) -> Crg.term -> 'a
-
-val crg_of_brg: (Crg.term -> 'a) -> Brg.term -> 'a

diff --git a/helm/software/lambda-delta/src/complete_rg/crgXml.ml b/helm/software/lambda-delta/src/complete_rg/crgXml.ml
deleted file mode 100644 (file)
index 111cfed..0000000
--- a/helm/software/lambda-delta/src/complete_rg/crgXml.ml
+++ /dev/null
@@ -1,114 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-module A = Alpha
-module X = Library
-module D = Crg
-
-(* internal functions *******************************************************)
-
-let rec list_iter map l out tab = match l with
-   | []       -> ()
-   | hd :: tl -> map hd out tab; list_iter map tl out tab
-
-let list_rev_iter map e ns l out tab =
-   let rec aux err f e = function
-      | [], []            -> f e
-      | n :: ns, hd :: tl -> 
-        let f e =
-(*     
-           pp_lenv print_string e; print_string " |- "; 
-          pp_term print_string hd; print_newline ();
-*)
-          map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
-       in
-       aux err f e (ns, tl) 
-      | _                 -> err ()
-   in
-   ignore (aux C.err C.start e (ns, l))
-
-let lenv_iter map1 map2 l out tab = 
-   let rec aux f = function
-      | D.ESort              -> f ()
-      | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
-      | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
-   in 
-   aux C.start l
-
-let rec exp_term e t out tab = match t with
-   | D.TSort (a, l)       ->
-      let a =
-         let err _ = a in
-         let f s = Y.Name (s, true) :: a in
-        H.string_of_sort err f l
-      in
-      let attrs = [X.position l; X.name a] in
-      X.tag X.sort attrs out tab
-   | D.TLRef (a, i, j)    ->
-      let a = 
-         let err _ = a in
-        let f n r = Y.Name (n, r) :: a in
-         D.get_name err f i j e
-      in
-      let attrs = [X.position i; X.offset j; X.name a] in
-      X.tag X.lref attrs out tab
-   | D.TGRef (a, n)       ->
-      let a = Y.Name (U.name_of_uri n, true) :: a in
-      let attrs = [X.uri n; X.name a] in
-      X.tag X.gref attrs out tab
-   | D.TCast (a, u, t)    ->
-      let attrs = [] in
-      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
-      exp_term e t out tab
-   | D.TAppl (a, vs, t)   ->
-      let attrs = [X.arity (List.length vs)] in
-      X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
-      exp_term e t out tab
-   | D.TProj (a, lenv, t) ->
-      let attrs = [] in
-      X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
-      exp_term (D.push_proj C.start e a lenv) t out tab
-   | D.TBind (a, b, t) ->
-(* NOTE: the inner binders are alpha-converted first *)
-(*       so undesirable renamings might occur        *)
-(* EX:   we rename [x][x]x to [x][x_]x_              *)
-(*       whereas [x_][x]x would be more desirable    *)
-      let a = A.alpha (D.names_of_lenv [] e) a in
-      exp_bind e a b out tab; 
-      exp_term (D.push_bind C.start e a b) t out tab 
-
-and exp_bind e a b out tab = 
-   let f a ns = a, ns in
-   let a, ns = Y.get_names f a in 
-   match b with
-      | D.Abst ws ->
-        let e = D.push_bind C.start e a (D.Abst []) in
-        let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
-         X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
-      | D.Abbr vs ->
-         let e = D.push_bind C.start e a (D.Abbr []) in
-         let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
-         X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
-      | D.Void n ->
-         let attrs = [X.name a; X.mark a; X.arity n] in
-         X.tag X.void attrs out tab
-
-and exp_eproj e a lenv out tab =
-   let attrs = [] in
-   X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
-
-(* interface functions ******************************************************)
-
-let export_term = exp_term D.empty_lenv

diff --git a/helm/software/lambda-delta/src/complete_rg/crgXml.mli b/helm/software/lambda-delta/src/complete_rg/crgXml.mli
deleted file mode 100644 (file)
index c326a98..0000000
--- a/helm/software/lambda-delta/src/complete_rg/crgXml.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-val export_term: Crg.term -> Library.pp

diff --git a/helm/software/lambda-delta/src/xml/XmlCrg.ml b/helm/software/lambda-delta/src/xml/XmlCrg.ml
new file mode 100644 (file)
index 0000000..111cfed
--- /dev/null
+++ b/helm/software/lambda-delta/src/xml/XmlCrg.ml
@@ -0,0 +1,114 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+module A = Alpha
+module X = Library
+module D = Crg
+
+(* internal functions *******************************************************)
+
+let rec list_iter map l out tab = match l with
+   | []       -> ()
+   | hd :: tl -> map hd out tab; list_iter map tl out tab
+
+let list_rev_iter map e ns l out tab =
+   let rec aux err f e = function
+      | [], []            -> f e
+      | n :: ns, hd :: tl -> 
+        let f e =
+(*     
+           pp_lenv print_string e; print_string " |- "; 
+          pp_term print_string hd; print_newline ();
+*)
+          map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
+       in
+       aux err f e (ns, tl) 
+      | _                 -> err ()
+   in
+   ignore (aux C.err C.start e (ns, l))
+
+let lenv_iter map1 map2 l out tab = 
+   let rec aux f = function
+      | D.ESort              -> f ()
+      | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
+      | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
+   in 
+   aux C.start l
+
+let rec exp_term e t out tab = match t with
+   | D.TSort (a, l)       ->
+      let a =
+         let err _ = a in
+         let f s = Y.Name (s, true) :: a in
+        H.string_of_sort err f l
+      in
+      let attrs = [X.position l; X.name a] in
+      X.tag X.sort attrs out tab
+   | D.TLRef (a, i, j)    ->
+      let a = 
+         let err _ = a in
+        let f n r = Y.Name (n, r) :: a in
+         D.get_name err f i j e
+      in
+      let attrs = [X.position i; X.offset j; X.name a] in
+      X.tag X.lref attrs out tab
+   | D.TGRef (a, n)       ->
+      let a = Y.Name (U.name_of_uri n, true) :: a in
+      let attrs = [X.uri n; X.name a] in
+      X.tag X.gref attrs out tab
+   | D.TCast (a, u, t)    ->
+      let attrs = [] in
+      X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+      exp_term e t out tab
+   | D.TAppl (a, vs, t)   ->
+      let attrs = [X.arity (List.length vs)] in
+      X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+      exp_term e t out tab
+   | D.TProj (a, lenv, t) ->
+      let attrs = [] in
+      X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+      exp_term (D.push_proj C.start e a lenv) t out tab
+   | D.TBind (a, b, t) ->
+(* NOTE: the inner binders are alpha-converted first *)
+(*       so undesirable renamings might occur        *)
+(* EX:   we rename [x][x]x to [x][x_]x_              *)
+(*       whereas [x_][x]x would be more desirable    *)
+      let a = A.alpha (D.names_of_lenv [] e) a in
+      exp_bind e a b out tab; 
+      exp_term (D.push_bind C.start e a b) t out tab 
+
+and exp_bind e a b out tab = 
+   let f a ns = a, ns in
+   let a, ns = Y.get_names f a in 
+   match b with
+      | D.Abst ws ->
+        let e = D.push_bind C.start e a (D.Abst []) in
+        let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+         X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+      | D.Abbr vs ->
+         let e = D.push_bind C.start e a (D.Abbr []) in
+         let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
+         X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+      | D.Void n ->
+         let attrs = [X.name a; X.mark a; X.arity n] in
+         X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+   let attrs = [] in
+   X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+(* interface functions ******************************************************)
+
+let export_term = exp_term D.empty_lenv

diff --git a/helm/software/lambda-delta/src/xml/XmlCrg.mli b/helm/software/lambda-delta/src/xml/XmlCrg.mli
new file mode 100644 (file)
index 0000000..c326a98
--- /dev/null
+++ b/helm/software/lambda-delta/src/xml/XmlCrg.mli
@@ -0,0 +1,12 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+val export_term: Crg.term -> Library.pp

diff --git a/helm/software/lambda-delta/src/xml/XmlLibrary.ml b/helm/software/lambda-delta/src/xml/XmlLibrary.ml
new file mode 100644 (file)
index 0000000..8a68011
--- /dev/null
+++ b/helm/software/lambda-delta/src/xml/XmlLibrary.ml
@@ -0,0 +1,132 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+module F = Filename
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+
+(* internal functions *******************************************************)
+
+let base = "xml"
+
+let obj_ext = ".xml"
+
+let root = "ENTITY"
+
+let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
+
+let path_of_uri xdir uri =
+   let base = F.concat xdir base in 
+   F.concat base (Str.string_after (U.string_of_uri uri) 3)
+
+(* interface functions ******************************************************)
+
+type och = string -> unit
+
+type attr = string * string
+
+type pp = och -> int -> unit
+
+let attribute out (name, contents) =
+   if contents <> "" then begin
+      out " "; out name; out "=\""; out contents; out "\""
+   end
+
+let xml out version encoding =
+   out "<?xml";
+      attribute out ("version", version);
+      attribute out ("encoding", encoding);
+   out "?>\n\n"
+
+let doctype out root system =
+   out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
+
+let tag tag attrs ?contents out indent =
+   let spc = String.make indent ' ' in
+   out spc; out "<"; out tag; List.iter (attribute out) attrs;
+   match contents with
+      | None      -> out "/>\n"
+      | Some cont -> 
+         out ">\n"; cont out (indent + 3); out spc; 
+        out "</"; out tag; out ">\n"
+
+let sort = "Sort"
+
+let lref = "LRef"
+
+let gref = "GRef"
+
+let cast = "Cast"
+
+let appl = "Appl"
+
+let proj = "Proj"
+
+let abst = "Abst"
+
+let abbr = "Abbr"
+
+let void = "Void"
+
+let position i =
+   "position", string_of_int i
+
+let offset j = 
+   let contents = if j > 0 then string_of_int j else "" in
+   "offset", contents
+
+let uri u =
+   "uri", U.string_of_uri u
+
+let arity n =
+   let contents = if n > 1 then string_of_int n else "" in
+   "arity", contents
+
+let name a =
+   let map f i n r s =
+      let n = if r then n else "^" ^ n in 
+      let spc = if i then "" else " " in
+      f (s ^ n ^ spc)
+   in
+   let f s = "name", s in
+   Y.names f map a ""
+
+let mark a =
+   let err () = "mark", "" in
+   let f i = "mark", string_of_int i in
+   Y.mark err f a
+
+(* TODO: the string s must be quoted *)
+let meta a =
+   let err () = "meta", "" in
+   let f s = "meta", s in
+   Y.meta err f a
+
+let export_entity pp_term si xdir (a, u, b) =
+   let path = path_of_uri xdir u in
+   let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
+   let och = open_out (path ^ obj_ext) in
+   let out = output_string och in
+   xml out "1.0" "UTF-8"; doctype out root system;
+   let a = Y.Name (U.name_of_uri u, true) :: a in
+   let attrs = [uri u; name a; mark a; meta a] in 
+   let contents = match b with
+      | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) 
+      | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+      | Y.Void   -> assert false
+   in
+   let opts = if si then "si" else "" in
+   let shp = H.string_of_graph () in
+   let attrs = ["hierarchy", shp; "options", opts] in
+   tag root attrs ~contents out 0;
+   close_out och

diff --git a/helm/software/lambda-delta/src/xml/XmlLibrary.mli b/helm/software/lambda-delta/src/xml/XmlLibrary.mli
new file mode 100644 (file)
index 0000000..ed3f7bb
--- /dev/null
+++ b/helm/software/lambda-delta/src/xml/XmlLibrary.mli
@@ -0,0 +1,53 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
+
+type och = string -> unit
+
+type attr = string * string
+
+type pp = och -> int -> unit
+
+val export_entity:
+   ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
+
+val tag: string -> attr list -> ?contents:pp -> pp 
+
+val sort: string
+
+val lref: string
+
+val gref: string
+
+val cast: string
+
+val appl: string
+
+val proj: string
+
+val abst: string
+
+val abbr: string
+
+val void: string
+
+val position: int -> attr
+
+val offset: int -> attr
+
+val uri: Entity.uri -> attr
+
+val arity: int -> attr
+
+val name: Entity.attrs -> attr
+
+val mark: Entity.attrs -> attr
+
+val meta: Entity.attrs -> attr