From: Ferruccio Guidi Date: Fri, 6 Aug 2010 11:49:10 +0000 (+0000) Subject: new module "xml" devoted to xml I/O X-Git-Tag: make_still_working~2848 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb74956a335a9cc38a6ced92e16256f10c4eed6e;p=helm.git 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 26f2d959c..c6e6ac189 100644 --- 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 17ed69d21..a6fcf6c48 100644 --- 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 25e67cc1b..c47540bea 100644 --- 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 8e332c33b..abc5de2e1 100644 --- 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 ee53ca212..ccbbf5003 100644 --- 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 index 000000000..2b3129339 --- /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 index 000000000..84c7f2368 --- /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 index 8a6801159..000000000 --- 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 "\n\n" - -let doctype out root 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 "\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 index ed3f7bb8f..000000000 --- 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 d7a45f9d2..ccb5b1559 100644 --- 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 index 2b3129339..000000000 --- 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 index 84c7f2368..000000000 --- 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 index 111cfed06..000000000 --- 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 index c326a9822..000000000 --- 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 index 000000000..111cfed06 --- /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 index 000000000..c326a9822 --- /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 index 000000000..8a6801159 --- /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 "\n\n" + +let doctype out root 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 "\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 index 000000000..ed3f7bb8f --- /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