From: Ferruccio Guidi Date: Sat, 4 Jul 2015 13:37:33 +0000 (+0000) Subject: - conditional compilation continues ... X-Git-Tag: make_still_working~711 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=586c361209ac14e8c2b1da3509041c0c82a86c92;p=helm.git - conditional compilation continues ... - current run times for helena and managers in profile.txt --- diff --git a/helm/software/helena/.depend.byte b/helm/software/helena/.depend.byte deleted file mode 100644 index 3ca9da5a8..000000000 --- a/helm/software/helena/.depend.byte +++ /dev/null @@ -1,295 +0,0 @@ -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/log.cmi -src/lib/log.cmx : src/lib/log.cmi -src/lib/time.cmo : src/lib/log.cmi -src/lib/time.cmx : src/lib/log.cmx -src/lib/marks.cmi : -src/lib/marks.cmo : src/lib/marks.cmi -src/lib/marks.cmx : src/lib/marks.cmi -src/common/options.cmo : src/lib/cps.cmo -src/common/options.cmx : src/lib/cps.cmx -src/common/hierarchy.cmi : -src/common/hierarchy.cmo : src/lib/cps.cmo src/common/hierarchy.cmi -src/common/hierarchy.cmx : src/lib/cps.cmx src/common/hierarchy.cmi -src/common/layer.cmi : -src/common/layer.cmo : src/common/options.cmo src/lib/marks.cmi \ - src/lib/log.cmi src/common/layer.cmi -src/common/layer.cmx : src/common/options.cmx src/lib/marks.cmx \ - src/lib/log.cmx src/common/layer.cmi -src/common/entity.cmo : src/common/layer.cmi -src/common/entity.cmx : src/common/layer.cmx -src/common/output.cmi : -src/common/output.cmo : src/common/options.cmo 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/alpha.cmi : src/common/entity.cmo -src/common/alpha.cmo : src/common/entity.cmo src/common/alpha.cmi -src/common/alpha.cmx : src/common/entity.cmx src/common/alpha.cmi -src/complete_rg/crg.cmo : src/common/layer.cmi src/common/entity.cmo \ - src/lib/cps.cmo -src/complete_rg/crg.cmx : src/common/layer.cmx src/common/entity.cmx \ - src/lib/cps.cmx -src/complete_rg/crgOutput.cmi : src/common/layer.cmi src/complete_rg/crg.cmo -src/complete_rg/crgOutput.cmo : src/lib/marks.cmi src/lib/log.cmi \ - src/common/layer.cmi src/common/entity.cmo src/complete_rg/crg.cmo \ - src/lib/cps.cmo src/complete_rg/crgOutput.cmi -src/complete_rg/crgOutput.cmx : src/lib/marks.cmx src/lib/log.cmx \ - src/common/layer.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/complete_rg/crgOutput.cmi -src/text/txt.cmo : src/common/layer.cmi -src/text/txt.cmx : src/common/layer.cmx -src/text/txtParser.cmi : src/text/txt.cmo -src/text/txtParser.cmo : src/text/txt.cmo src/common/options.cmo \ - src/common/layer.cmi src/text/txtParser.cmi -src/text/txtParser.cmx : src/text/txt.cmx src/common/options.cmx \ - src/common/layer.cmx src/text/txtParser.cmi -src/text/txtLexer.cmo : src/text/txtParser.cmi src/common/options.cmo \ - src/lib/log.cmi -src/text/txtLexer.cmx : src/text/txtParser.cmx src/common/options.cmx \ - src/lib/log.cmx -src/text/txtCrg.cmi : src/text/txt.cmo src/complete_rg/crg.cmo -src/text/txtCrg.cmo : src/text/txt.cmo src/common/options.cmo \ - src/common/hierarchy.cmi src/common/entity.cmo src/complete_rg/crg.cmo \ - src/lib/cps.cmo src/text/txtCrg.cmi -src/text/txtCrg.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/text/txtCrg.cmi -src/automath/aut.cmo : src/common/entity.cmo -src/automath/aut.cmx : src/common/entity.cmx -src/automath/autProcess.cmi : src/automath/aut.cmo -src/automath/autProcess.cmo : src/automath/aut.cmo \ - 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.cmo -src/automath/autOutput.cmo : src/lib/log.cmi src/lib/cps.cmo \ - src/automath/autProcess.cmi src/automath/aut.cmo \ - 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.cmo -src/automath/autParser.cmo : src/common/options.cmo src/automath/aut.cmo \ - 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.cmo 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/automath/autCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmo \ - src/automath/aut.cmo -src/automath/autCrg.cmo : src/common/options.cmo src/common/layer.cmi \ - src/common/entity.cmo src/complete_rg/crg.cmo src/lib/cps.cmo \ - src/automath/aut.cmo src/automath/autCrg.cmi -src/automath/autCrg.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/automath/autCrg.cmi -src/xml/xmlLibrary.cmi : src/common/layer.cmi src/common/entity.cmo -src/xml/xmlLibrary.cmo : src/common/options.cmo src/common/layer.cmi \ - src/common/hierarchy.cmi src/common/entity.cmo src/lib/cps.cmo \ - src/xml/xmlLibrary.cmi -src/xml/xmlLibrary.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ - src/xml/xmlLibrary.cmi -src/xml/xmlCrg.cmi : src/xml/xmlLibrary.cmi src/common/layer.cmi \ - src/complete_rg/crg.cmo -src/xml/xmlCrg.cmo : src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \ - src/common/entity.cmo src/complete_rg/crg.cmo src/lib/cps.cmo \ - src/common/alpha.cmi src/xml/xmlCrg.cmi -src/xml/xmlCrg.cmx : src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/common/alpha.cmx src/xml/xmlCrg.cmi -src/basic_rg/brg.cmo : src/common/layer.cmi src/common/entity.cmo -src/basic_rg/brg.cmx : src/common/layer.cmx src/common/entity.cmx -src/basic_rg/brgCrg.cmi : src/complete_rg/crg.cmo src/basic_rg/brg.cmo -src/basic_rg/brgCrg.cmo : src/common/layer.cmi src/common/entity.cmo \ - src/complete_rg/crg.cmo src/lib/cps.cmo src/basic_rg/brg.cmo \ - src/basic_rg/brgCrg.cmi -src/basic_rg/brgCrg.cmx : src/common/layer.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgCrg.cmi -src/basic_rg/brgOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ - src/common/layer.cmi src/basic_rg/brg.cmo -src/basic_rg/brgOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmo \ - src/lib/log.cmi src/common/layer.cmi src/common/hierarchy.cmi \ - src/common/entity.cmo src/lib/cps.cmo src/basic_rg/brgCrg.cmi \ - src/basic_rg/brg.cmo src/common/alpha.cmi src/basic_rg/brgOutput.cmi -src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ - src/lib/log.cmx src/common/layer.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \ - src/basic_rg/brg.cmx src/common/alpha.cmx src/basic_rg/brgOutput.cmi -src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmo -src/basic_rg/brgEnvironment.cmo : src/common/options.cmo \ - src/common/entity.cmo src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgEnvironment.cmx : src/common/options.cmx \ - src/common/entity.cmx src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgSubstitution.cmi : src/basic_rg/brg.cmo -src/basic_rg/brgSubstitution.cmo : src/common/options.cmo \ - src/basic_rg/brg.cmo src/basic_rg/brgSubstitution.cmi -src/basic_rg/brgSubstitution.cmx : src/common/options.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi -src/basic_rg/brgReduction.cmi : src/lib/log.cmi src/common/layer.cmi \ - src/common/entity.cmo src/basic_rg/brg.cmo -src/basic_rg/brgReduction.cmo : src/lib/share.cmo src/common/output.cmi \ - src/common/options.cmo src/lib/log.cmi src/common/layer.cmi \ - src/common/hierarchy.cmi src/common/entity.cmo src/basic_rg/brgOutput.cmi \ - src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmo \ - src/basic_rg/brgReduction.cmi -src/basic_rg/brgReduction.cmx : src/lib/share.cmx src/common/output.cmx \ - src/common/options.cmx src/lib/log.cmx src/common/layer.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/basic_rg/brgOutput.cmx \ - src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgReduction.cmi -src/basic_rg/brgValidity.cmi : src/common/layer.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmo -src/basic_rg/brgValidity.cmo : src/common/options.cmo src/lib/log.cmi \ - src/common/layer.cmi src/common/entity.cmo src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmo \ - src/basic_rg/brgValidity.cmi -src/basic_rg/brgValidity.cmx : src/common/options.cmx src/lib/log.cmx \ - src/common/layer.cmx src/common/entity.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgValidity.cmi -src/basic_rg/brgType.cmi : src/common/layer.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmo -src/basic_rg/brgType.cmo : src/lib/share.cmo src/common/options.cmo \ - src/lib/log.cmi src/common/layer.cmi src/common/hierarchy.cmi \ - src/common/entity.cmo src/lib/cps.cmo src/basic_rg/brgSubstitution.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmo src/basic_rg/brgType.cmi -src/basic_rg/brgType.cmx : src/lib/share.cmx src/common/options.cmx \ - src/lib/log.cmx src/common/layer.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/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi -src/basic_rg/brgUntrusted.cmi : src/common/layer.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmo -src/basic_rg/brgUntrusted.cmo : src/lib/log.cmi src/common/entity.cmo \ - src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmo src/basic_rg/brgUntrusted.cmi -src/basic_rg/brgUntrusted.cmx : src/lib/log.cmx src/common/entity.cmx \ - src/basic_rg/brgValidity.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/basic_rg/brgGrafite.cmi : -src/basic_rg/brgGrafite.cmo : src/common/options.cmo src/common/layer.cmi \ - src/common/entity.cmo src/lib/cps.cmo src/basic_rg/brg.cmo \ - src/common/alpha.cmi src/basic_rg/brgGrafite.cmi -src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgGrafite.cmi -src/basic_rg/brgGallina.cmi : -src/basic_rg/brgGallina.cmo : src/common/options.cmo src/common/layer.cmi \ - src/common/entity.cmo src/lib/cps.cmo src/basic_rg/brg.cmo \ - src/common/alpha.cmi src/basic_rg/brgGallina.cmi -src/basic_rg/brgGallina.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgGallina.cmi -src/basic_rg/brgLP.cmi : -src/basic_rg/brgLP.cmo : src/common/options.cmo src/common/layer.cmi \ - src/common/entity.cmo src/lib/cps.cmo src/basic_rg/brg.cmo \ - src/common/alpha.cmi src/basic_rg/brgLP.cmi -src/basic_rg/brgLP.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgLP.cmi -src/basic_ag/bag.cmo : src/lib/marks.cmi src/lib/log.cmi \ - src/common/entity.cmo src/lib/cps.cmo -src/basic_ag/bag.cmx : src/lib/marks.cmx src/lib/log.cmx \ - src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bagCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmo \ - src/basic_ag/bag.cmo -src/basic_ag/bagCrg.cmo : src/lib/marks.cmi src/common/layer.cmi \ - src/common/entity.cmo src/complete_rg/crg.cmo src/lib/cps.cmo \ - src/basic_ag/bag.cmo src/basic_ag/bagCrg.cmi -src/basic_ag/bagCrg.cmx : src/lib/marks.cmx src/common/layer.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi -src/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ - src/common/layer.cmi src/basic_ag/bag.cmo -src/basic_ag/bagOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmo \ - src/lib/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \ - src/common/entity.cmo src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmo \ - src/basic_ag/bagOutput.cmi -src/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ - src/lib/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagOutput.cmi -src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmo -src/basic_ag/bagEnvironment.cmo : src/common/options.cmo src/lib/log.cmi \ - src/common/entity.cmo src/basic_ag/bag.cmo \ - src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagEnvironment.cmx : src/common/options.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/lib/marks.cmi src/basic_ag/bag.cmo -src/basic_ag/bagSubstitution.cmo : src/lib/share.cmo src/basic_ag/bag.cmo \ - 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/common/layer.cmi src/basic_ag/bag.cmo -src/basic_ag/bagReduction.cmo : src/common/options.cmo src/lib/marks.cmi \ - src/lib/log.cmi src/common/entity.cmo src/lib/cps.cmo \ - src/basic_ag/bagSubstitution.cmi src/basic_ag/bagOutput.cmi \ - src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmo \ - src/basic_ag/bagReduction.cmi -src/basic_ag/bagReduction.cmx : src/common/options.cmx src/lib/marks.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/layer.cmi src/basic_ag/bag.cmo -src/basic_ag/bagType.cmo : src/lib/share.cmo src/common/options.cmo \ - src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmo \ - src/lib/cps.cmo src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \ - src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmo \ - src/basic_ag/bagType.cmi -src/basic_ag/bagType.cmx : src/lib/share.cmx src/common/options.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/layer.cmi src/basic_ag/bag.cmo -src/basic_ag/bagUntrusted.cmo : src/lib/log.cmi src/common/entity.cmo \ - src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \ - src/basic_ag/bag.cmo 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/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ - src/text/txtParser.cmi src/text/txtLexer.cmo src/text/txtCrg.cmi \ - src/text/txt.cmo src/lib/time.cmo src/common/output.cmi \ - src/common/options.cmo src/lib/marks.cmi src/lib/log.cmi \ - src/common/layer.cmi src/common/hierarchy.cmi src/common/entity.cmo \ - src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmo src/lib/cps.cmo \ - src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgOutput.cmi src/basic_rg/brgLP.cmi \ - src/basic_rg/brgGrafite.cmi src/basic_rg/brgGallina.cmi \ - src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmo \ - src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ - src/basic_ag/bagOutput.cmi src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmo \ - src/automath/autProcess.cmi src/automath/autParser.cmi \ - src/automath/autOutput.cmi src/automath/autLexer.cmo \ - src/automath/autCrg.cmi src/automath/aut.cmo -src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ - src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \ - src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \ - src/common/options.cmx src/lib/marks.cmx src/lib/log.cmx \ - src/common/layer.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/complete_rg/crgOutput.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/brgLP.cmx \ - src/basic_rg/brgGrafite.cmx src/basic_rg/brgGallina.cmx \ - src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ - src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ - src/basic_ag/bagOutput.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ - src/automath/autProcess.cmx src/automath/autParser.cmx \ - src/automath/autOutput.cmx src/automath/autLexer.cmx \ - src/automath/autCrg.cmx src/automath/aut.cmx diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt deleted file mode 100644 index dfad373a1..000000000 --- a/helm/software/helena/.depend.opt +++ /dev/null @@ -1,295 +0,0 @@ -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/log.cmi -src/lib/log.cmx : src/lib/log.cmi -src/lib/time.cmo : src/lib/log.cmi -src/lib/time.cmx : src/lib/log.cmx -src/lib/marks.cmi : -src/lib/marks.cmo : src/lib/marks.cmi -src/lib/marks.cmx : src/lib/marks.cmi -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/layer.cmi : -src/common/layer.cmo : src/common/options.cmx src/lib/marks.cmi \ - src/lib/log.cmi src/common/layer.cmi -src/common/layer.cmx : src/common/options.cmx src/lib/marks.cmx \ - src/lib/log.cmx src/common/layer.cmi -src/common/entity.cmo : src/common/layer.cmi -src/common/entity.cmx : src/common/layer.cmx -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/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/complete_rg/crg.cmo : src/common/layer.cmi src/common/entity.cmx \ - src/lib/cps.cmx -src/complete_rg/crg.cmx : src/common/layer.cmx src/common/entity.cmx \ - src/lib/cps.cmx -src/complete_rg/crgOutput.cmi : src/common/layer.cmi src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo : src/lib/marks.cmi src/lib/log.cmi \ - src/common/layer.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/lib/marks.cmx src/lib/log.cmx \ - src/common/layer.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/complete_rg/crgOutput.cmi -src/text/txt.cmo : src/common/layer.cmi -src/text/txt.cmx : src/common/layer.cmx -src/text/txtParser.cmi : src/text/txt.cmx -src/text/txtParser.cmo : src/text/txt.cmx src/common/options.cmx \ - src/common/layer.cmi src/text/txtParser.cmi -src/text/txtParser.cmx : src/text/txt.cmx src/common/options.cmx \ - src/common/layer.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/txtCrg.cmi : src/text/txt.cmx src/complete_rg/crg.cmx -src/text/txtCrg.cmo : 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/text/txtCrg.cmi -src/text/txtCrg.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/text/txtCrg.cmi -src/automath/aut.cmo : src/common/entity.cmx -src/automath/aut.cmx : src/common/entity.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/automath/autCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \ - src/automath/aut.cmx -src/automath/autCrg.cmo : src/common/options.cmx src/common/layer.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/automath/autCrg.cmi -src/automath/autCrg.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/automath/autCrg.cmi -src/xml/xmlLibrary.cmi : src/common/layer.cmi src/common/entity.cmx -src/xml/xmlLibrary.cmo : src/common/options.cmx src/common/layer.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ - src/xml/xmlLibrary.cmi -src/xml/xmlLibrary.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ - src/xml/xmlLibrary.cmi -src/xml/xmlCrg.cmi : src/xml/xmlLibrary.cmi src/common/layer.cmi \ - src/complete_rg/crg.cmx -src/xml/xmlCrg.cmo : src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/common/alpha.cmi src/xml/xmlCrg.cmi -src/xml/xmlCrg.cmx : src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/common/alpha.cmx src/xml/xmlCrg.cmi -src/basic_rg/brg.cmo : src/common/layer.cmi src/common/entity.cmx -src/basic_rg/brg.cmx : src/common/layer.cmx src/common/entity.cmx -src/basic_rg/brgCrg.cmi : src/complete_rg/crg.cmx src/basic_rg/brg.cmx -src/basic_rg/brgCrg.cmo : src/common/layer.cmi src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgCrg.cmi -src/basic_rg/brgCrg.cmx : src/common/layer.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgCrg.cmi -src/basic_rg/brgOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ - src/common/layer.cmi src/basic_rg/brg.cmx -src/basic_rg/brgOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \ - src/lib/log.cmi src/common/layer.cmi src/common/hierarchy.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmi \ - src/basic_rg/brg.cmx src/common/alpha.cmi src/basic_rg/brgOutput.cmi -src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ - src/lib/log.cmx src/common/layer.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \ - src/basic_rg/brg.cmx src/common/alpha.cmx src/basic_rg/brgOutput.cmi -src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx -src/basic_rg/brgEnvironment.cmo : src/common/options.cmx \ - src/common/entity.cmx src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgEnvironment.cmx : src/common/options.cmx \ - src/common/entity.cmx src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgSubstitution.cmi : src/basic_rg/brg.cmx -src/basic_rg/brgSubstitution.cmo : src/common/options.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi -src/basic_rg/brgSubstitution.cmx : src/common/options.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgSubstitution.cmi -src/basic_rg/brgReduction.cmi : src/lib/log.cmi src/common/layer.cmi \ - src/common/entity.cmx src/basic_rg/brg.cmx -src/basic_rg/brgReduction.cmo : src/lib/share.cmx src/common/output.cmi \ - src/common/options.cmx src/lib/log.cmi src/common/layer.cmi \ - src/common/hierarchy.cmi src/common/entity.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/common/options.cmx src/lib/log.cmx src/common/layer.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/basic_rg/brgOutput.cmx \ - src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgReduction.cmi -src/basic_rg/brgValidity.cmi : src/common/layer.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx -src/basic_rg/brgValidity.cmo : src/common/options.cmx src/lib/log.cmi \ - src/common/layer.cmi src/common/entity.cmx src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ - src/basic_rg/brgValidity.cmi -src/basic_rg/brgValidity.cmx : src/common/options.cmx src/lib/log.cmx \ - src/common/layer.cmx src/common/entity.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ - src/basic_rg/brgValidity.cmi -src/basic_rg/brgType.cmi : src/common/layer.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx -src/basic_rg/brgType.cmo : src/lib/share.cmx src/common/options.cmx \ - src/lib/log.cmi src/common/layer.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/brgEnvironment.cmi \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi -src/basic_rg/brgType.cmx : src/lib/share.cmx src/common/options.cmx \ - src/lib/log.cmx src/common/layer.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/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi -src/basic_rg/brgUntrusted.cmi : src/common/layer.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx -src/basic_rg/brgUntrusted.cmo : src/lib/log.cmi src/common/entity.cmx \ - src/basic_rg/brgValidity.cmi 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/brgValidity.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/basic_rg/brgGrafite.cmi : -src/basic_rg/brgGrafite.cmo : src/common/options.cmx src/common/layer.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmi src/basic_rg/brgGrafite.cmi -src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgGrafite.cmi -src/basic_rg/brgGallina.cmi : -src/basic_rg/brgGallina.cmo : src/common/options.cmx src/common/layer.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmi src/basic_rg/brgGallina.cmi -src/basic_rg/brgGallina.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgGallina.cmi -src/basic_rg/brgLP.cmi : -src/basic_rg/brgLP.cmo : src/common/options.cmx src/common/layer.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmi src/basic_rg/brgLP.cmi -src/basic_rg/brgLP.cmx : src/common/options.cmx src/common/layer.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgLP.cmi -src/basic_ag/bag.cmo : src/lib/marks.cmi src/lib/log.cmi \ - src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bag.cmx : src/lib/marks.cmx src/lib/log.cmx \ - src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bagCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \ - src/basic_ag/bag.cmx -src/basic_ag/bagCrg.cmo : src/lib/marks.cmi src/common/layer.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi -src/basic_ag/bagCrg.cmx : src/lib/marks.cmx src/common/layer.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi -src/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ - src/common/layer.cmi src/basic_ag/bag.cmx -src/basic_ag/bagOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \ - src/lib/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \ - src/common/entity.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \ - src/basic_ag/bagOutput.cmi -src/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ - src/lib/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/basic_ag/bagCrg.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/common/options.cmx src/lib/log.cmi \ - src/common/entity.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagEnvironment.cmx : src/common/options.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/lib/marks.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/common/layer.cmi src/basic_ag/bag.cmx -src/basic_ag/bagReduction.cmo : src/common/options.cmx src/lib/marks.cmi \ - 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/common/options.cmx src/lib/marks.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/layer.cmi src/basic_ag/bag.cmx -src/basic_ag/bagType.cmo : src/lib/share.cmx src/common/options.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/common/options.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/layer.cmi 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/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ - src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txtCrg.cmi \ - src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \ - src/common/options.cmx src/lib/marks.cmi src/lib/log.cmi \ - src/common/layer.cmi src/common/hierarchy.cmi src/common/entity.cmx \ - src/complete_rg/crgOutput.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/brgLP.cmi \ - src/basic_rg/brgGrafite.cmi src/basic_rg/brgGallina.cmi \ - src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ - src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ - src/basic_ag/bagOutput.cmi src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \ - src/automath/autProcess.cmi src/automath/autParser.cmi \ - src/automath/autOutput.cmi src/automath/autLexer.cmx \ - src/automath/autCrg.cmi src/automath/aut.cmx -src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ - src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \ - src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \ - src/common/options.cmx src/lib/marks.cmx src/lib/log.cmx \ - src/common/layer.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/complete_rg/crgOutput.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/brgLP.cmx \ - src/basic_rg/brgGrafite.cmx src/basic_rg/brgGallina.cmx \ - src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ - src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ - src/basic_ag/bagOutput.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ - src/automath/autProcess.cmx src/automath/autParser.cmx \ - src/automath/autOutput.cmx src/automath/autLexer.cmx \ - src/automath/autCrg.cmx src/automath/aut.cmx diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index f4b0075ba..137084bf9 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -46,6 +46,22 @@ PREAMBLE_MA = ../matita/matita.ma.templ PREAMBLE_V = coq/grundlagen.template PREAMBLE_LP = lp/lp.template +ALL_FEATURES = LEXER PARSER TRACE SUMMARY EXPAND MANAGER OBJECTS PREPROCESS QUOTE STAGE TYPE + +TEST1 = -T 1 -l -u -1 $(O) $(INPUT) + +TEST2 = -X -T 2 -l -1 $(O) $(INPUT) + +all: .depend.opt .depend.byte + @$(CALLMAKE) $(MAIN).opt F="$(ALL_FEATURES)" + @$(CALLMAKE) $(MAIN).byte F="$(ALL_FEATURES)" + +opt: .depend.opt + @$(CALLMAKE) F="$(ALL_FEATURES)" $(MAIN).opt + +byte: .depend.byte + @$(CALLMAKE) F="$(ALL_FEATURES)" $(MAIN).byte + test-si-fast: $(MAIN).opt etc @echo " HELENA -q -u -x -y -1 $(INPUTFAST)" $(H)./$(MAIN).opt -T 1 -q -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt @@ -54,9 +70,13 @@ test-si: $(MAIN).opt etc @echo " HELENA -d -l -u -0 $(INPUT)" $(H)./$(MAIN).opt -T 2 -d -l -u -0 $(O) $(INPUT) > etc/log.txt +test1: $(MAIN).opt etc + @echo " HELENA -l -u -1 $(INPUT)" + ./$(MAIN).opt $(TEST1) > etc/log.txt + test2: $(MAIN).opt etc - @echo " HELENA -T 2 -l $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l -q -1 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -1 $(INPUT)" + ./$(MAIN).opt $(TEST1) $(TEST2) > etc/log.txt test3: $(MAIN).opt etc @echo " HELENA -T 3 -l $(INPUT)" @@ -66,6 +86,42 @@ test6: $(MAIN).opt etc @echo " HELENA -T 6 -l $(INPUT)" $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt +profile-fast: $(MAIN).opt etc + @echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) >> etc/log.txt; done + $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt + +profile: $(MAIN).opt etc + @echo " HELENA -l -u $(INPUT) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for _ in `seq 31`; do ./$(MAIN).opt $(TEST1) >> etc/log.txt; done + $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt + +profile-opt: $(MAIN).opt etc + @echo " HELENA -l $(INPUT) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for _ in `seq 31`; do ./$(MAIN).opt $(TEST1) $(TEST2) >> etc/log.txt; done + $(H)grep "processed" etc/log.txt | sort -k 6 | uniq > etc/profile.txt + +profile-byte: $(MAIN).byte etc + @echo " HELENA -l $(INPUT) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for _ in `seq 31`; do ./$(MAIN).byte $(TEST1) $(TEST2) >> etc/log.txt; done + $(H)grep "processed" etc/log.txt | sort -k 6 | uniq > etc/profile.txt + +profile-coq: $(MAIN).opt etc + @echo " COQTOP $(V) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP) -q $(NULL); done + $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt + +profile-coq-byte: $(MAIN).opt etc + @echo " COQTOP $(V) (31 TIMES)" + $(H)rm -f etc/log.txt + $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP).byte -q $(NULL); done + $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt + xml-si: $(MAIN).opt etc @echo " HELENA -l -o -s 1 -u -y $(INPUT)" $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u -y $(O) $(INPUT) > etc/log.txt @@ -83,52 +139,28 @@ xml-v3: $(MAIN).opt etc $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 -y $(O) $(INPUT) > etc/log.txt export-coq coq/$(V): $(MAIN).opt etc - @echo " HELENA -l -m V8 -u $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -l -m V8 -p $(PREAMBLE_V) -u $(O) $(INPUT) > etc/log.txt + @echo " HELENA -m V8 $(INPUT)" + $(H)./$(MAIN).opt -a n -m V8 -p $(PREAMBLE_V) $(TEST1) > etc/log.txt export-matita matita/$(MA): $(MAIN).opt etc - @echo " HELENA -l -m MA2 -u $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -l -m MA2 -p $(PREAMBLE_MA) -u $(O) $(INPUT) > etc/log.txt + @echo " HELENA -m MA2 $(INPUT)" + $(H)./$(MAIN).opt -a n -m MA2 -p $(PREAMBLE_MA) $(TEST1) > etc/log.txt export-lp1 lp/$(LP1): $(MAIN).opt etc - @echo " HELENA -l -m LP1 -u $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -l -m LP1 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt + @echo " HELENA -m LP1 $(INPUT)" + $(H)./$(MAIN).opt -a n -m LP1 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt export-lp2 lp/$(LP2): $(MAIN).opt etc - @echo " HELENA -l -m LP2 -u $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -l -m LP2 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt + @echo " HELENA -m LP2 $(INPUT)" + $(H)./$(MAIN).opt -a n -m LP2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt export-tj2 lp/$(TJ2): $(MAIN).opt etc @echo " HELENA -l -m TJ2 -u $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -e 253 -l -m TJ2 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -a n -e 253 -m TJ2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt export-tj3 lp/$(TJ3): $(MAIN).opt etc - @echo " HELENA -l -m TJ3 -u $(INPUT)" - $(H)./$(MAIN).opt -T 1 -a n -l -m TJ3 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt - -profile-fast: $(MAIN).opt etc - @echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)" - $(H)rm -f etc/log.txt - $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) >> etc/log.txt; done - $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt - -profile: $(MAIN).opt etc - @echo " HELENA -l -u $(INPUT) (31 TIMES)" - $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -q -u -1 $(O) $(INPUT) >> etc/log.txt; done - $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt - -profile-coq: $(MAIN).opt etc - @echo " COQTOP $(V) (31 TIMES)" - $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP) -q $(NULL); done - $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt - -profile-coq-byte: $(MAIN).opt etc - @echo " COQTOP $(V) (31 TIMES)" - $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP).byte -q $(NULL); done - $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt + @echo " HELENA -m TJ3 $(INPUT)" + $(H)./$(MAIN).opt -a n -m TJ3 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt matita: matita/$(MA) @echo " MATITA $(MA)" diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common index 6845800d5..ae92e7df6 100644 --- a/helm/software/helena/Makefile.common +++ b/helm/software/helena/Makefile.common @@ -24,6 +24,8 @@ OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v TAR = tar -czf etc/$(MAIN:%=%.tgz) +CALLMAKE = $(MAKE) --no-print-directory + define DIR_TEMPLATE MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make)) endef @@ -69,12 +71,6 @@ B_OBJECTS = $(patsubst %.ml,%.cmo,$(SOURCES:%.mli=%.cmi)) CLEAN += $(MAIN).opt -all opt: .depend.opt - @$(MAKE) --no-print-directory $(MAIN).opt - -byte: .depend.byte - @$(MAKE) --no-print-directory $(MAIN).byte - $(MAIN).opt: $(O_OBJECTS) @echo " OCAMLOPT -o $(MAIN).opt" $(H)$(OCAMLOPT) -o $(MAIN).opt $(CMXS) @@ -123,7 +119,7 @@ etc: @echo " OCAMLC $<" $(H)$(OCAMLC) -c $< -O_TAGS += all opt $(MAIN).opt +O_TAGS += opt $(MAIN).opt B_TAGS += byte $(MAIN).byte diff --git a/helm/software/helena/README b/helm/software/helena/README index 88067dee8..646b33526 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -2,20 +2,27 @@ Helena 0.8.3 M ::= +LEXER enable option -L (if unset, -T 0 is implied) +PARSER enable option -P (if unset, -T 0 is implied) +TRACE enable full option -T (if unset, -T > 2 is disabled) +SUMMARY enable option -d (if unset, -d is disabled) EXPAND enable option -g (if unset, -g is disabled) MANAGER enable options -M -m -p (if unset, -m is disabled) -PREPROCESS enable option (if unset, -0 is disabled) +OBJECTS enable options -O -o (if unset, -o is disabled) +PREPROCESS enable option -p (if unset, -p is disabled) +QUOTE enable option -q (if unset, -q is disabled) +TYPE enable option -t (if unset, -t is disabled) -* type "make" or "make opt" to compile the native executable +* type "make opt" to compile the native executable with the desired features listed in the variable F -* type "make clean" to remove the products of compilation +* type "make byte" to compile the bytecode executable + with the desired features listed in the variable F -- type "make export-coq" to build the "grundlagen" for Coq 8 +* type "make" or "make all" to compile both executables + with the desired features listed in the variable F -* type "make profile" to validate the "grundlagen" 31 times - it generates etc/profile.txt with sorted execution times +* type "make clean" to remove the products of compilation -* type "make profile-coq" to run coqc on the "grundlagen" 31 times +* type "make profile" to validate the "grundlagen" 31 times it generates etc/profile.txt with sorted execution times - coqc must be installed on your system diff --git a/helm/software/helena/profile.txt b/helm/software/helena/profile.txt new file mode 100644 index 000000000..65c909fe6 --- /dev/null +++ b/helm/software/helena/profile.txt @@ -0,0 +1,20 @@ +helena.opt : 01.14 to 01.18 (optimized, 2nd run) ages => 904871 beta-steps +helena.byte: 08.73 to 08.77 (optimized, 2nd run) ages + +helena.opt : 01.50 to 01.54 (optimized, 2nd run) no ages => 1423268 beta-steps + +coqtop.opt : 24.26 to 24.43 no ages +coqtop.byte: 94.18 to 95.78 no ages + +coqtop.opt : 27.73 to 28.07 ages + +coqtop.opt : 28.64 to 28.83 reversed ages + +elpi : 00.19 to 00.20 exex, 253 lines +elpi : 00.26 to 00.28 user, 253 lines + +teyjus : 02.03 to 02.18 exec, 253 lines +teyjus : 01.63 to 01.68 link, 253 lines + +elpi : 21.15 to 21.45 exec, full +elpi : 27.52 to 27.82 user, full diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 7a6600898..5a726ca97 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -212,7 +212,9 @@ let xlate_entity err f st lst = function *) let na = E.node_attrs ~apix:lst.line () in let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in - G.set_current_trace lst.line; +IFDEF TRACE THEN + G.set_current_trace lst.line +ELSE () END; f {lst with line = succ lst.line} entity in xlate_term f st lst true lenv w @@ -234,7 +236,9 @@ let xlate_entity err f st lst = function let na = E.node_attrs ~apix:lst.line () in let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in let entity = ra, na, uri_of_qid qid, E.Abbr t in - G.set_current_trace lst.line; +IFDEF TRACE THEN + G.set_current_trace lst.line +ELSE () END; f {lst with line = succ lst.line} entity in xlate_term f st lst false lenv v diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll index 67d8ccd55..5a7155e4a 100644 --- a/helm/software/helena/src/automath/autLexer.mll +++ b/helm/software/helena/src/automath/autLexer.mll @@ -15,9 +15,12 @@ module AP = AutParser let level = 0 - + +IFDEF LEXER THEN let out s = if !G.debug_lexer then L.warn level s else () +END +IFDEF QUOTE THEN (* This turns an Automath identifier into an XML nmtoken *) let quote id = let l = String.length id in @@ -29,6 +32,8 @@ id in aux 0 + +END } let LC = ['#' '%'] @@ -52,41 +57,45 @@ and token = parse | SPC { token lexbuf } | LC { line_comment lexbuf; token lexbuf } | OC { block_comment lexbuf; token lexbuf } - | "_E" { out "E"; AP.E } - | "'_E'" { out "E"; AP.E } - | "---" { out "EB"; AP.EB } - | "'eb'" { out "EB"; AP.EB } - | "EB" { out "EB"; AP.EB } - | "--" { out "EXIT"; AP.EXIT } - | "PN" { out "PN"; AP.PN } - | "'pn'" { out "PN"; AP.PN } - | "PRIM" { out "PN"; AP.PN } - | "'prim'" { out "PN"; AP.PN } - | "???" { out "PN"; AP.PN } - | "PROP" { out "PROP"; AP.PROP } - | "'prop'" { out "PROP"; AP.PROP } - | "TYPE" { out "TYPE"; AP.TYPE } - | "'type'" { out "TYPE"; AP.TYPE } - | ID { out "ID"; + | "_E" { IFDEF LEXER THEN out "E" ELSE () END; AP.E } + | "'_E'" { IFDEF LEXER THEN out "E" ELSE () END; AP.E } + | "---" { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB } + | "'eb'" { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB } + | "EB" { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB } + | "--" { IFDEF LEXER THEN out "EXIT" ELSE () END; AP.EXIT } + | "PN" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN } + | "'pn'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN } + | "PRIM" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN } + | "'prim'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN } + | "???" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN } + | "PROP" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP } + | "'prop'" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP } + | "TYPE" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE } + | "'type'" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE } + | ID { IFDEF LEXER THEN out "ID" ELSE () END; let s = Lexing.lexeme lexbuf in - if !G.unquote then AP.IDENT s else AP.IDENT (quote s) +IFDEF QUOTE THEN + if !G.quote then AP.IDENT (quote s) else AP.IDENT s +ELSE + AP.IDENT s +END } - | ":=" { out "DEF"; AP.DEF } - | "(" { out "OP"; AP.OP } - | ")" { out "CP"; AP.CP } - | "[" { out "OB"; AP.OB } - | "]" { out "CB"; AP.CB } - | "<" { out "OA"; AP.OA } - | ">" { out "CA"; AP.CA } - | "@" { out "AT"; AP.AT } - | "~" { out "TD"; AP.TD } - | "\"" { out "QT"; AP.QT } - | ":" { out "CN"; AP.CN } - | "," { out "CM"; AP.CM } - | ";" { out "SC"; AP.SC } - | "." { out "FS"; AP.FS } - | "+" { out "PLUS"; AP.PLUS } - | "-" { out "MINUS"; AP.MINUS } - | "*" { out "TIMES"; AP.TIMES } - | "=" { out "DEF"; AP.DEF } - | eof { out "EOF"; AP.EOF } + | ":=" { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF } + | "(" { IFDEF LEXER THEN out "OP" ELSE () END; AP.OP } + | ")" { IFDEF LEXER THEN out "CP" ELSE () END; AP.CP } + | "[" { IFDEF LEXER THEN out "OB" ELSE () END; AP.OB } + | "]" { IFDEF LEXER THEN out "CB" ELSE () END; AP.CB } + | "<" { IFDEF LEXER THEN out "OA" ELSE () END; AP.OA } + | ">" { IFDEF LEXER THEN out "CA" ELSE () END; AP.CA } + | "@" { IFDEF LEXER THEN out "AT" ELSE () END; AP.AT } + | "~" { IFDEF LEXER THEN out "TD" ELSE () END; AP.TD } + | "\"" { IFDEF LEXER THEN out "QT" ELSE () END; AP.QT } + | ":" { IFDEF LEXER THEN out "CN" ELSE () END; AP.CN } + | "," { IFDEF LEXER THEN out "CM" ELSE () END; AP.CM } + | ";" { IFDEF LEXER THEN out "SC" ELSE () END; AP.SC } + | "." { IFDEF LEXER THEN out "FS" ELSE () END; AP.FS } + | "+" { IFDEF LEXER THEN out "PLUS" ELSE () END; AP.PLUS } + | "-" { IFDEF LEXER THEN out "MINUS" ELSE () END; AP.MINUS } + | "*" { IFDEF LEXER THEN out "TIMES" ELSE () END; AP.TIMES } + | "=" { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF } + | eof { IFDEF LEXER THEN out "EOF" ELSE () END; AP.EOF } diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml index a1f5ae18c..f9272867c 100644 --- a/helm/software/helena/src/automath/autOutput.ml +++ b/helm/software/helena/src/automath/autOutput.ml @@ -37,6 +37,8 @@ let initial_counters = { sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0; xnodes = 0 } +IFDEF SUMMARY THEN + let rec count_term f c = function | A.Sort _ -> f {c with sorts = succ c.sorts; xnodes = succ c.xnodes} @@ -91,6 +93,8 @@ let print_counters f c = L.warn level (KP.sprintf " + Abbreviation nodes: %7u" c.xnodes); f () +IFDEF PREPROCESS THEN + let print_process_counters f c = let f iao iar iac iag = L.warn level (KP.sprintf "Automath process summary"); @@ -101,3 +105,7 @@ let print_process_counters f c = f () in AA.get_counters f c + +END + +END diff --git a/helm/software/helena/src/automath/autOutput.mli b/helm/software/helena/src/automath/autOutput.mli index 1a5f56104..af72d38f7 100644 --- a/helm/software/helena/src/automath/autOutput.mli +++ b/helm/software/helena/src/automath/autOutput.mli @@ -13,8 +13,16 @@ type counters val initial_counters: counters +IFDEF SUMMARY THEN + val count_command: (counters -> 'a) -> counters -> Aut.command -> 'a val print_counters: (unit -> 'a) -> counters -> 'a +IFDEF PREPROCESS THEN + val print_process_counters: (unit -> 'a) -> AutProcess.status -> 'a + +END + +END diff --git a/helm/software/helena/src/automath/autParser.mly b/helm/software/helena/src/automath/autParser.mly index 31f2c643c..ad98a00cb 100644 --- a/helm/software/helena/src/automath/autParser.mly +++ b/helm/software/helena/src/automath/autParser.mly @@ -27,7 +27,9 @@ module G = Options module A = Aut +IFDEF PARSER THEN let _ = Parsing.set_trace !G.debug_parser +END %} %token NUM %token IDENT diff --git a/helm/software/helena/src/automath/autProcess.ml b/helm/software/helena/src/automath/autProcess.ml index 405952ff5..8ce4c6045 100644 --- a/helm/software/helena/src/automath/autProcess.ml +++ b/helm/software/helena/src/automath/autProcess.ml @@ -25,6 +25,8 @@ type status = { (* internal functions *******************************************************) +IFDEF PREPROCESS THEN + let orc_reset f st = f {st with opening = false; reopening = false; closing = false} @@ -63,7 +65,9 @@ let proc_command f st command = match command with | A.Block _ -> proc_block f st command | A.Decl _ -> proc_global f st command | A.Def _ -> proc_global f st command - + +END + (* interface functions ******************************************************) let initial_status () = { @@ -72,6 +76,10 @@ let initial_status () = { iao = 0; iar = 0; iac = 0; iag = 0 } +let get_counters f st = f st.iao st.iar st.iac st.iag + +IFDEF PREPROCESS THEN + let process_command = proc_command -let get_counters f st = f st.iao st.iar st.iac st.iag +END diff --git a/helm/software/helena/src/automath/autProcess.mli b/helm/software/helena/src/automath/autProcess.mli index 4145ff946..e0c856a0f 100644 --- a/helm/software/helena/src/automath/autProcess.mli +++ b/helm/software/helena/src/automath/autProcess.mli @@ -13,7 +13,11 @@ type status val initial_status: unit -> status +val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a + +IFDEF PREPROCESS THEN + val process_command: (status -> Aut.command -> 'a) -> status -> Aut.command -> 'a -val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a +END diff --git a/helm/software/helena/src/basic_ag/bagEnvironment.ml b/helm/software/helena/src/basic_ag/bagEnvironment.ml index 3f2b5534d..865b6a599 100644 --- a/helm/software/helena/src/basic_ag/bagEnvironment.ml +++ b/helm/software/helena/src/basic_ag/bagEnvironment.ml @@ -16,6 +16,8 @@ module G = Options module E = Entity module Z = Bag +IFDEF TYPE THEN + exception ObjectNotFound of Z.message let hsize = 7000 @@ -39,3 +41,5 @@ END let get_entity f uri = try f (UH.find env uri) with Not_found -> error uri + +END diff --git a/helm/software/helena/src/basic_ag/bagEnvironment.mli b/helm/software/helena/src/basic_ag/bagEnvironment.mli index 4a44c05fe..4152803aa 100644 --- a/helm/software/helena/src/basic_ag/bagEnvironment.mli +++ b/helm/software/helena/src/basic_ag/bagEnvironment.mli @@ -9,8 +9,12 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + exception ObjectNotFound of Bag.message val set_entity: (Bag.entity -> 'a) -> Bag.entity -> 'a val get_entity: (Bag.entity -> 'a) -> Bag.uri -> 'a + +END diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index 41914b062..344c4db06 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -40,6 +40,8 @@ let initial_counters = { tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 } +IFDEF SUMMARY THEN + let rec count_term_binder f c = function | Z.Abst w -> let c = {c with tabsts = succ c.tabsts} in @@ -99,6 +101,8 @@ let print_counters f c = L.warn level (KP.sprintf " Total binder locations: %7u" locations); f () +END + let name err och a = let f n = function | true -> KP.fprintf och "%s" n @@ -155,7 +159,11 @@ let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv } +IFDEF OBJECTS THEN + (* term xml printing ********************************************************) let export_term st = ZD.crg_of_bag (XD.export_term st) + +END diff --git a/helm/software/helena/src/basic_ag/bagOutput.mli b/helm/software/helena/src/basic_ag/bagOutput.mli index 64f6b034f..6ef4385c6 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.mli +++ b/helm/software/helena/src/basic_ag/bagOutput.mli @@ -13,10 +13,18 @@ type counters val initial_counters: counters +IFDEF SUMMARY THEN + val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a +END + val specs: (Layer.status, Bag.lenv, Bag.term) Log.specs +IFDEF OBJECTS THEN + val export_term: Layer.status -> Bag.term -> XmlLibrary.pp + +END diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index a0e4fa739..323de4c9f 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -20,6 +20,8 @@ module ZO = BagOutput module ZE = BagEnvironment module ZS = BagSubstitution +IFDEF TYPE THEN + type machine = { i: int; c: Z.lenv; @@ -124,15 +126,19 @@ let rec ho_whd f c m x = whd aux c m x let ho_whd f st c t = - if !G.ct >= level then log1 st "Now scanning" c t; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now scanning" c t +ELSE () END; ho_whd f c empty_machine t let rec are_convertible f st a c m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) let rec aux m1 r1 m2 r2 = (* L.warn "entering R.are_convertible_aux"; *) +IFDEF TRACE THEN let u, t = term_of_whdr r1, term_of_whdr r2 in - if !G.ct >= level then log2 st "Now really converting" c u c t; + if !G.ct >= level then log2 st "Now really converting" c u c t +ELSE () END; match r1, r2 with | Sort_ k1, Sort_ k2 -> if k1 = k2 then f a else f false @@ -188,6 +194,10 @@ and are_convertible_stacks f st a c m1 m2 = else C.list_fold_left2 f map a m1.s m2.s -let are_convertible f st c u t = - if !G.ct >= level then log2 st "Now converting" c u c t; +let are_convertible f st c u t = +IFDEF TRACE THEN + if !G.ct >= level then log2 st "Now converting" c u c t +ELSE () END; are_convertible f st true c empty_machine u empty_machine t + +END diff --git a/helm/software/helena/src/basic_ag/bagReduction.mli b/helm/software/helena/src/basic_ag/bagReduction.mli index 90aa4053b..13a503673 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.mli +++ b/helm/software/helena/src/basic_ag/bagReduction.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + type ho_whd_result = | Sort of int | Abst of Bag.term @@ -18,3 +20,5 @@ val ho_whd: val are_convertible: (bool -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a + +END diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.ml b/helm/software/helena/src/basic_ag/bagSubstitution.ml index f35cdf4ff..a8109c3ff 100644 --- a/helm/software/helena/src/basic_ag/bagSubstitution.ml +++ b/helm/software/helena/src/basic_ag/bagSubstitution.ml @@ -12,6 +12,8 @@ module S = Share module Z = Bag +IFDEF TYPE THEN + (* Internal functions *******************************************************) let rec lref_map_bind f map b = match b with @@ -46,3 +48,5 @@ and lref_map f map t = match t with let subst f new_l old_l t = let map i = if i = old_l then new_l else i in if new_l = old_l then f t else lref_map f map t + +END diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.mli b/helm/software/helena/src/basic_ag/bagSubstitution.mli index 45325ab44..d6dd6576c 100644 --- a/helm/software/helena/src/basic_ag/bagSubstitution.mli +++ b/helm/software/helena/src/basic_ag/bagSubstitution.mli @@ -9,4 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + val subst: (Bag.term -> 'a) -> Marks.mark -> Marks.mark -> Bag.term -> 'a + +END diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index 1f47b60dd..f92919ec7 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -21,6 +21,8 @@ module ZO = BagOutput module ZE = BagEnvironment module ZR = BagReduction +IFDEF TYPE THEN + (* Internal functions *******************************************************) let level = 4 @@ -45,7 +47,9 @@ let mk_gref u l = let rec b_type_of err f st c x = (* L.warn "Entering T.b_type_of"; *) - if !G.ct >= level then log1 st "Now checking" c x; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now checking" c x +ELSE () END; match x with | Z.Sort h -> let h = H.apply h in f x (Z.Sort h) @@ -93,7 +97,9 @@ let rec b_type_of err f st c x = | Z.Appl (v, t) -> let f xv vv xt tt = function | ZR.Abst w -> - if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w); +IFDEF TRACE THEN + if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w) +ELSE () END; let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt) @@ -118,3 +124,5 @@ let rec b_type_of err f st c x = (* Interface functions ******************************************************) and type_of err f st c x = b_type_of err f st c x + +END diff --git a/helm/software/helena/src/basic_ag/bagType.mli b/helm/software/helena/src/basic_ag/bagType.mli index 3af585c3f..be444c93e 100644 --- a/helm/software/helena/src/basic_ag/bagType.mli +++ b/helm/software/helena/src/basic_ag/bagType.mli @@ -9,7 +9,11 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + val type_of: (Bag.message -> 'a) -> (Bag.term -> Bag.term -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> 'a + +END diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.ml b/helm/software/helena/src/basic_ag/bagUntrusted.ml index 9efbf9182..0b5fa7dba 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.ml +++ b/helm/software/helena/src/basic_ag/bagUntrusted.ml @@ -16,6 +16,8 @@ module Z = Bag module ZE = BagEnvironment module ZT = BagType +IFDEF TYPE THEN + (* Interface functions ******************************************************) (* to share *) @@ -29,3 +31,5 @@ let type_check err f st = function let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abbr xt) in ZT.type_of err f st Z.empty_lenv t | _, _, _, E.Void -> assert false + +END diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.mli b/helm/software/helena/src/basic_ag/bagUntrusted.mli index c9b0b7c4d..41188ff21 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.mli +++ b/helm/software/helena/src/basic_ag/bagUntrusted.mli @@ -9,6 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + val type_check: (Bag.message -> 'a) -> (Bag.term -> Bag.entity -> 'a) -> Layer.status -> Bag.entity -> 'a + +END diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index 0c692045e..f8d8e642b 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -52,6 +52,8 @@ let initial_counters = { uris = []; nodes = 0; xnodes = 0 } +IFDEF SUMMARY THEN + let rec count_term_binder f c e = function | B.Abst (_, _, w) -> let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in @@ -127,6 +129,8 @@ let print_counters f c = L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes); f () +END + (* lenv/term pretty printing ************************************************) let name err och a = @@ -191,7 +195,11 @@ let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv } +IFDEF OBJECTS THEN + (* term xml printing ********************************************************) let export_term st = BD.crg_of_brg (XD.export_term st) + +END diff --git a/helm/software/helena/src/basic_rg/brgOutput.mli b/helm/software/helena/src/basic_rg/brgOutput.mli index 155cc8ee4..59adec3e9 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.mli +++ b/helm/software/helena/src/basic_rg/brgOutput.mli @@ -13,10 +13,18 @@ type counters val initial_counters: counters +IFDEF SUMMARY THEN + val count_entity: (counters -> 'a) -> counters -> Brg.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a +END + val specs: (Layer.status, Brg.lenv, Brg.term) Log.specs +IFDEF OBJECTS THEN + val export_term: Layer.status -> Brg.term -> XmlLibrary.pp + +END diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 8747e6425..e62b90777 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -91,9 +91,11 @@ let get m i = let _, c, a, _, b = B.get m.e i in c, a, b (* to share *) -let rec step st m r = +let rec step st m r = +IFDEF TRACE THEN if !G.ct >= sublevel then - log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r; + log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r +ELSE () END; match r with | B.Sort k -> if assert_tstep m false then @@ -105,7 +107,9 @@ let rec step st m r = m, B.gref a u, Some v | _, _, _, E.Abst w -> if assert_tstep m true then begin - if !G.summary then O.add ~grt:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~grt:1 () +ELSE () END; step st (tstep m) w end else m, r, None @@ -115,11 +119,15 @@ let rec step st m r = | B.LRef (_, i) -> begin match get m i with | c, _, B.Abbr v -> - if !G.summary then O.add ~ldelta:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~ldelta:1 () +ELSE () END; step st {m with e = c} v | c, a, B.Abst (_, _, w) -> if assert_tstep m true then begin - if !G.summary then O.add ~lrt:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~lrt:1 () +ELSE () END; step st {(tstep m) with e = c} w end else m, B.lref a i, None @@ -128,17 +136,23 @@ let rec step st m r = end | B.Cast (u, t) -> if assert_tstep m false then begin - if !G.summary then O.add ~e:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~e:1 () +ELSE () END; step st (tstep m) u end else begin - if !G.summary then O.add ~epsilon:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~epsilon:1 () +ELSE () END; step st m t end | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t | B.Bind (y, B.Abst (false, n, w), t) -> let i = tsteps m in - if !G.summary then O.add ~x:i (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~x:i () +ELSE () END; let n = if i = 0 then n else N.minus st n i in let r = B.Bind (y, B.Abst (true, n, w), t) in step st m r @@ -147,17 +161,23 @@ let rec step st m r = | [] -> m, B.Bind (y, B.Abst (true, n, w), t), None | (c, v) :: s -> - if !G.summary then O.add ~beta:1 ~theta:(List.length s) (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~beta:1 ~theta:(List.length s) () +ELSE () END; let v = B.Cast (w, v) in let e = B.push m.e c E.empty_node y (B.abbr v) in step st {m with e = e; s = s} t end else begin - if !G.summary then O.add ~upsilon:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~upsilon:1 () +ELSE () END; let e = B.push m.e m.e E.empty_node y B.Void in (**) (* this is wrong in general *) step st {m with e = e} t end | B.Bind (y, b, t) -> - if !G.summary then O.add ~theta:(List.length m.s) (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~theta:(List.length m.s) () +ELSE () END; let e = B.push m.e m.e E.empty_node y b in step st {m with e = e} t @@ -176,7 +196,9 @@ let push m y b = {m with e = e; l = l} let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = - if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2; +IFDEF TRACE THEN + if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2 +ELSE () END; match t1, r1, t2, r2 with | B.Sort k1, _, B.Sort k2, _ -> k1 = k2 @@ -188,21 +210,31 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = | B.GRef ({E.n_apix = e1}, u1), Some v1, B.GRef ({E.n_apix = e2}, u2), Some v2 -> if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true - else if e1 < e2 then begin - if !G.summary then O.add ~gdelta:1 (); + else if e1 < e2 then begin +IFDEF SUMMARY THEN + if !G.summary then O.add ~gdelta:1 () +ELSE () END; ac_nfs st (m1, t1, r1) (step st m2 v2) end else if e2 < e1 then begin - if !G.summary then O.add ~gdelta:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~gdelta:1 () +ELSE () END; ac_nfs st (step st m1 v1) (m2, t2, r2) end else begin - if !G.summary then O.add ~gdelta:2 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~gdelta:2 () +ELSE () END; ac st m1 v1 m2 v2 end | _, _, B.GRef _, Some v2 -> - if !G.summary then O.add ~gdelta:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~gdelta:1 () +ELSE () END; ac_nfs st (m1, t1, r1) (step st m2 v2) | B.GRef _, Some v1, _, _ -> - if !G.summary then O.add ~gdelta:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~gdelta:1 () +ELSE () END; ac_nfs st (step st m1 v1) (m2, t2, r2) | B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _, B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _ -> @@ -213,7 +245,9 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = | B.Sort _, _, B.Bind (y, B.Abst (true, n, _), t), _ -> if !G.si then if !G.cc && not (N.assert_zero st n) then false else begin - if !G.summary then O.add ~upsilon:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~upsilon:1 () +ELSE () END; ac st (push m1 y B.Void) t1 (push m2 y B.Void) t end else false | _ -> false @@ -234,7 +268,9 @@ and ac_stacks st m1 m2 = let rec ih_nfs st (m, t, r) = match t, r with | B.GRef _, Some v -> - if !G.summary then O.add ~gdelta:1 (); +IFDEF SUMMARY THEN + if !G.summary then O.add ~gdelta:1 () +ELSE () END; ih st m v | _ -> m, t @@ -251,11 +287,15 @@ let get m i = let _, _, _, _, b = B.get m.e i in b let xwhd st m n t = - if !G.ct >= level then log1 st "Now scanning" m.e t; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now scanning" m.e t +ELSE () END; ih st (reset m n) t let are_convertible st m1 n1 t1 m2 n2 t2 = - if !G.ct >= level then log2 st "Now converting" m1.e t1 m2.e t2; +IFDEF TRACE THEN + if !G.ct >= level then log2 st "Now converting" m1.e t1 m2.e t2 +ELSE () END; let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in r (* let err _ = in diff --git a/helm/software/helena/src/basic_rg/brgSubstitution.ml b/helm/software/helena/src/basic_rg/brgSubstitution.ml index 6fd4575dd..5441f0145 100644 --- a/helm/software/helena/src/basic_rg/brgSubstitution.ml +++ b/helm/software/helena/src/basic_rg/brgSubstitution.ml @@ -12,6 +12,8 @@ module G = Options module B = Brg +IFDEF TYPE THEN + let rec icm a = function | B.Sort _ | B.LRef _ @@ -48,3 +50,5 @@ let lift h d t = *) iter (lift_map h) d t end + +END diff --git a/helm/software/helena/src/basic_rg/brgSubstitution.mli b/helm/software/helena/src/basic_rg/brgSubstitution.mli index a1717666f..068d6b156 100644 --- a/helm/software/helena/src/basic_rg/brgSubstitution.mli +++ b/helm/software/helena/src/basic_rg/brgSubstitution.mli @@ -9,7 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + val lift: int -> int -> Brg.term -> Brg.term (* val lift_bind: (Brg.bind -> 'a) -> int -> int -> Brg.bind -> 'a *) +END diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 7cdeb653a..431e3e473 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -22,6 +22,8 @@ module BE = BrgEnvironment module BS = BrgSubstitution module BR = BrgReduction +IFDEF TYPE THEN + (* Internal functions *******************************************************) let level = 4 @@ -67,7 +69,9 @@ let assert_applicability err f st m x u w v = | _ -> assert false (**) let rec b_type_of err f st m z = - if !G.ct >= level then log1 st "Now checking" m z; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now checking" m z +ELSE () END; match z with | B.Sort k -> let k = H.apply k in f z (B.Sort k) @@ -130,3 +134,5 @@ let rec b_type_of err f st m z = (* Interface functions ******************************************************) and type_of err f st m t = b_type_of err f st m t + +END diff --git a/helm/software/helena/src/basic_rg/brgType.mli b/helm/software/helena/src/basic_rg/brgType.mli index 2a2442097..7e17242a9 100644 --- a/helm/software/helena/src/basic_rg/brgType.mli +++ b/helm/software/helena/src/basic_rg/brgType.mli @@ -9,6 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + val type_of: (BrgReduction.message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> Layer.status -> BrgReduction.rtm -> Brg.term -> 'a + +END diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index d6333552f..a6ab35ea9 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -20,6 +20,8 @@ module BV = BrgValidity (* Interface functions ******************************************************) +IFDEF TYPE THEN + (* to share *) let type_check err f st = function | ra, na, uri, E.Abst t -> @@ -40,6 +42,8 @@ let type_check err f st = function BT.type_of err f st BR.empty_rtm t | _, _, _, E.Void -> assert false +END + let validate err f st e = let uri, t = match e with | _, _, uri, E.Abst t -> uri, t diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.mli b/helm/software/helena/src/basic_rg/brgUntrusted.mli index f3c34ab14..3501e7eab 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.mli +++ b/helm/software/helena/src/basic_rg/brgUntrusted.mli @@ -9,10 +9,14 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF TYPE THEN + val type_check: (BrgReduction.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> Layer.status -> Brg.entity -> 'a +END + val validate: (BrgReduction.message -> 'a) -> (unit -> 'a) -> Layer.status -> Brg.entity -> 'a diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index 5de70fbfa..cb0fc4060 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -46,18 +46,24 @@ let zero = Some 0 let one = Some 1 let assert_convertibility err f st m u t = - if !G.ct >= level then warn "Asserting convertibility for cast"; +IFDEF TRACE THEN + if !G.ct >= level then warn "Asserting convertibility for cast" +ELSE () END; if BR.are_convertible st m zero u m one t then f () else error2 err m u m t let assert_applicability err f st m x v t = let mode, msg = if x then None, "extended" else one, "restricted" in - if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability"); +IFDEF TRACE THEN + if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability") +ELSE () END; match BR.xwhd st m mode t with | mw, B.Bind (_, B.Abst (true, n, w), _) -> if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t else begin - if !G.ct >= level then warn "Asserting convertibility for application"; +IFDEF TRACE THEN + if !G.ct >= level then warn "Asserting convertibility for application" +ELSE () END; if BR.are_convertible st mw zero w m one v then f () else error2 err mw w m v end @@ -66,7 +72,9 @@ let assert_applicability err f st m x v t = | _ -> assert false (**) let rec b_validate err f st m y = - if !G.ct >= level then log1 st "Now checking" m y; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now checking" m y +ELSE () END; match y with | B.Sort _ -> f () | B.LRef (_, i) -> diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index de8b98254..82300931b 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -44,6 +44,8 @@ let string_of_value k = function | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i | Unk -> "-" ^ P.string_of_mark k +IFDEF TRACE THEN + (* Note: remove assigned variables *) let pp_table st = let map k n = @@ -53,6 +55,8 @@ let pp_table st = in KH.iter map st +END + let cell s v = { v = v; s = s; b = false } @@ -85,18 +89,28 @@ let rec generated st h i = let k, n = resolve_key_with_default st default k in if n.s then generated st h i else begin if n <> default then KH.replace st k default; - if !G.ct >= level then pp_table st; default +IFDEF TRACE THEN + if !G.ct >= level then pp_table st +ELSE () END; + default end let assert_finite st n j = - if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j); +IFDEF TRACE THEN + if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j) +ELSE () END; let rec aux (k, n) j = match n.v with | Fin i when i = j -> true | Fin i -> Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**) | Inf -> Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**) - | Unk -> n.v <- Fin j; if !G.ct >= level then pp_table st; true + | Unk -> + n.v <- Fin j; +IFDEF TRACE THEN + if !G.ct >= level then pp_table st +ELSE () END; + true | Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j) in let k, n = resolve_layer st n in @@ -106,12 +120,19 @@ let assert_finite st n j = aux (k, n) j let assert_infinite st n = - if !G.ct >= level then warn "ASSERT INFINITE"; +IFDEF TRACE THEN + if !G.ct >= level then warn "ASSERT INFINITE" +ELSE () END; let rec aux (k, n) = match n.v with | Inf -> true | Fin i -> Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**) - | Unk -> n.v <- Inf; if !G.ct >= level then pp_table st; true + | Unk -> + n.v <- Inf; +IFDEF TRACE THEN + if !G.ct >= level then pp_table st +ELSE () END; + true | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) in aux (resolve_layer st n) @@ -132,19 +153,27 @@ let one = finite 1 let two = finite 2 let rec unknown st = - if !G.ct >= level then warn "UNKNOWN"; +IFDEF TRACE THEN + if !G.ct >= level then warn "UNKNOWN" +ELSE () END; let default = empty () in let k = P.new_mark () in let k, n = resolve_key_with_default st default k in if n.s then match n.v with | Inf | Fin _ -> n - | Unk -> if !G.ct >= level then pp_table st; cell true (Ref (k, 0)) + | Unk -> +IFDEF TRACE THEN + if !G.ct >= level then pp_table st +ELSE () END; + cell true (Ref (k, 0)) | Ref _ -> assert false else unknown st let minus st n j = - if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j); +IFDEF TRACE THEN + if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j) +ELSE () END; let rec aux k n j = match n.v with | Inf -> cell false n.v | Fin i when i > j -> cell false (Fin (i - j)) @@ -163,14 +192,21 @@ let to_string st n = string_of_value k n.v let assert_not_zero st n = - if !G.ct >= level then warn "ASSERT NOT ZERO"; +IFDEF TRACE THEN + if !G.ct >= level then warn "ASSERT NOT ZERO" +ELSE () END; let k, n = resolve_layer st n in match n.b, n.v with - | true, _ -> n.b + | true, _ -> n.b (* | _ , Fin i when i = 0 -> Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**) (* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *) - | _ -> n.b <- true; if !G.ct >= level then pp_table st; n.b + | _ -> + n.b <- true; +IFDEF TRACE THEN + if !G.ct >= level then pp_table st +ELSE () END; + n.b let assert_zero st n = assert_finite st n 0 @@ -185,11 +221,16 @@ let assert_equal st n1 n2 = | Unk -> true | Ref _ -> assert false else false - in begin - if !G.ct >= level then warn "ASSERT EQUAL"; + in +IFDEF TRACE THEN + if !G.ct >= level then warn "ASSERT EQUAL" +ELSE () END; if b && k1 <> P.null_mark && k2 <> P.null_mark then begin - n1.v <- Ref (k2, 0); if !G.ct >= level then pp_table st - end; b end + n1.v <- Ref (k2, 0); +IFDEF TRACE THEN + if !G.ct >= level then pp_table st +ELSE () END + end; b let is_not_zero st n = (* let _, n = resolve_layer st n in *) n.v <> zero diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 415d0b02a..8bc7c9356 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -17,6 +17,8 @@ type uri_generator = string -> string type kernel = V4 | V3 | V0 +IFDEF MANAGER THEN + type manager = Quiet | Coq | Matita @@ -25,22 +27,12 @@ type manager = Quiet | TJ2 (* teyjus *) | TJ3 (* teyjus *) +END + (* interface functions ******************************************************) let version_string = "Helena 0.8.3 M (June 2015)" -let stage = ref 3 (* stage *) - -let trace = ref 0 (* trace level *) - -let ct = ref 0 (* current trace level *) - -let summary = ref false (* log summary information *) - -let export = ref false (* export entities to XML *) - -let xdir = ref "" (* directory for XML output *) - let kernel = ref V3 (* kernel type *) let si = ref false (* use sort inclusion *) @@ -51,14 +43,6 @@ let cc = ref false (* activate conversion constraints *) let indexes = ref false (* show de Bruijn indexes *) -let icm = ref 0 (* complexity measure of relocated terms *) - -let unquote = ref false (* do not quote identifiers when lexing *) - -let debug_parser = ref false (* output parser debug information *) - -let debug_lexer = ref false (* output lexer debug information *) - let alpha = ref "" (* prefix of numeric identifiers *) let first = ref 0 (* begin trace here *) @@ -71,12 +55,28 @@ let infinity = ref false (* use ∞-abstractions in contexts *) let short = ref false (* short global constants *) -IFDEF EXPAND THEN -let expand = ref false (* always expand global definitions *) +let root = ref "" (* initial segment of URI hierarchy *) + +let trace = ref 0 (* trace level *) + +IFDEF LEXER THEN +let debug_lexer = ref false (* output lexer debug information *) END -IFDEF PREPROCESS THEN -let preprocess = ref false (* preprocess source *) +IFDEF PARSER THEN +let debug_parser = ref false (* output parser debug information *) +END + +IFDEF TRACE THEN +let ct = ref 0 (* current trace level *) +END + +IFDEF SUMMARY THEN +let summary = ref false (* log summary information *) +END + +IFDEF EXPAND THEN +let expand = ref false (* always expand global definitions *) END IFDEF MANAGER THEN @@ -85,8 +85,27 @@ let manager = ref Quiet (* manager *) let preamble = ref "" (* preamble file for manager *) END -let set_current_trace n = - ct := if !first <= n && n <= !last then !trace else 0 +IFDEF STAGE THEN +let stage = ref 3 (* stage *) +END + +IFDEF OBJECTS THEN +let export = ref false (* export entities to XML *) +let xdir = ref "" (* directory for XML output *) +END + +IFDEF PREPROCESS THEN +let preprocess = ref false (* preprocess source *) +END + +IFDEF QUOTE THEN +let quote = ref false (* quote identifiers when lexing *) +END + +IFDEF TYPE THEN +let validate = ref true (* validate vs. typecheck *) +let icm = ref 0 (* complexity measure of relocated terms *) +END let kernel_id () = let id = match !kernel with @@ -105,11 +124,22 @@ let get_mk_uri () = let bu = get_baseuri () in fun s -> KF.concat bu (s ^ ".ld") +IFDEF TRACE THEN +let set_current_trace n = + ct := if !first <= n && n <= !last then !trace else 0 +END + let clear () = - stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int; - xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := ""; - indexes := false; icm := 0; unquote := false; short := false; - debug_parser := false; debug_lexer := false; + root := ""; first := 0; last := max_int; + kernel := V3; si := false; extended := false; infinity := false; cover := ""; + indexes := false; short := false; trace := 0; + IFDEF LEXER THEN debug_lexer := false ELSE () END; + IFDEF PARSER THEN debug_parser := false ELSE () END; + IFDEF SUMMARY THEN summary := false ELSE () END; IFDEF EXPAND THEN expand := false ELSE () END; IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END; - IFDEF PREPROCESS THEN preprocess := false ELSE () END + IFDEF STAGE THEN stage := 3 ELSE () END; + IFDEF OBJECTS THEN export := false; xdir := "" ELSE () END; + IFDEF PREPROCESS THEN preprocess := false ELSE () END; + IFDEF QUOTE THEN quote := false ELSE () END; + IFDEF TYPE THEN validate := true; icm := 0 ELSE () END diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 3c813b275..492b6d2c9 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -14,6 +14,8 @@ module KP = Printf module L = Log module G = Options +IFDEF SUMMARY THEN + type reductions = { beta : int; zeta : int; @@ -87,5 +89,9 @@ let print_reductions () = L.warn level (KP.sprintf " Local: %7u" r.lrt); L.warn level (KP.sprintf " Global: %7u" r.grt); L.warn level (KP.sprintf " Cast typing: %7u" r.e); - L.warn level (KP.sprintf " Binder typing: %7u" r.x); + L.warn level (KP.sprintf " Binder typing: %7u" r.x); +IFDEF TYPE THEN L.warn level (KP.sprintf "Relocated nodes (icm): %7u" !G.icm) +ELSE () END + +END diff --git a/helm/software/helena/src/common/output.mli b/helm/software/helena/src/common/output.mli index c2c0c3221..615b1d177 100644 --- a/helm/software/helena/src/common/output.mli +++ b/helm/software/helena/src/common/output.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF SUMMARY THEN + val clear_reductions: unit -> unit val add: @@ -17,3 +19,5 @@ val add: unit -> unit val print_reductions: unit -> unit + +END diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 7463c769a..535ec2beb 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -47,6 +47,8 @@ let initial_counters = { uris = []; nodes = 0; xnodes = 0 } +IFDEF SUMMARY THEN + let rec count_term f c e = function | D.TSort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} @@ -127,6 +129,8 @@ let print_counters f c = L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes); f () +END + (* term/environment pretty printer ******************************************) let pp_b_attrs out a = diff --git a/helm/software/helena/src/complete_rg/crgOutput.mli b/helm/software/helena/src/complete_rg/crgOutput.mli index 86ea0f6c9..9e987e9eb 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.mli +++ b/helm/software/helena/src/complete_rg/crgOutput.mli @@ -13,10 +13,14 @@ type counters val initial_counters: counters +IFDEF SUMMARY THEN + val count_entity: (counters -> 'a) -> counters -> Crg.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a +END + val pp_term: (string -> unit) -> Layer.status -> Crg.term -> unit val pp_lenv: (string -> unit) -> Layer.status -> Crg.lenv -> unit diff --git a/helm/software/helena/src/text/txtLexer.mll b/helm/software/helena/src/text/txtLexer.mll index 9191f11bf..eea312714 100644 --- a/helm/software/helena/src/text/txtLexer.mll +++ b/helm/software/helena/src/text/txtLexer.mll @@ -15,8 +15,10 @@ module TP = TxtParser let level = 0 - + +IFDEF LEXER THEN let out s = if !G.debug_lexer then L.warn level s else () +END } let BS = "\\" @@ -42,35 +44,37 @@ and qstring = parse and token = parse | SPC { token lexbuf } | OC { block_comment lexbuf; token lexbuf } - | ID as id { out ("ID " ^ id); TP.ID id } - | IX as ix { out ("IX " ^ ix); TP.IX (int_of_string ix) } - | QT { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s } - | "\\graph" { out "GRAPH"; TP.GRAPH } - | "\\main" { out "MAIN"; TP.MAIN } - | "\\decl" { out "DECL"; TP.DECL } - | "\\ax" { out "AX"; TP.AX } - | "\\cong" { out "CONG"; TP.CONG } - | "\\def" { out "DEF"; TP.DEF } - | "\\th" { out "TH"; TP.TH } - | "\\generate" { out "GEN"; TP.GEN } - | "\\require" { out "REQ"; TP.REQ } - | "\\open" { out "OPEN"; TP.OPEN } - | "\\close" { out "CLOSE"; TP.CLOSE } - | "\\sorts" { out "SORTS"; TP.SORTS } - | "(" { out "OP"; TP.OP } - | ")" { out "CP"; TP.CP } - | "[" { out "OB"; TP.OB } - | "]" { out "CB"; TP.CB } - | "{" { out "OC"; TP.OC } - | "}" { out "CC"; TP.CC } - | "<" { out "OA"; TP.OA } - | ">" { out "CA"; TP.CA } - | "." { out "FS"; TP.FS } - | ":" { out "CN"; TP.CN } - | "," { out "CM"; TP.CM } - | "=" { out "EQ"; TP.EQ } - | "*" { out "STAR"; TP.STAR } - | "#" { out "HASH"; TP.HASH } - | "~" { out "TE"; TP.TE } - | "^" { out "CT"; TP.CT } - | eof { out "EOF"; TP.EOF } + | ID as id { IFDEF LEXER THEN out ("ID " ^ id) ELSE () END; TP.ID id } + | IX as ix { IFDEF LEXER THEN out ("IX " ^ ix) ELSE () END; TP.IX (int_of_string ix) } + | QT { let s = qstring lexbuf in + IFDEF LEXER THEN out ("STR " ^ s) ELSE () END; TP.STR s + } + | "\\graph" { IFDEF LEXER THEN out "GRAPH" ELSE () END; TP.GRAPH } + | "\\main" { IFDEF LEXER THEN out "MAIN" ELSE () END; TP.MAIN } + | "\\decl" { IFDEF LEXER THEN out "DECL" ELSE () END; TP.DECL } + | "\\ax" { IFDEF LEXER THEN out "AX" ELSE () END; TP.AX } + | "\\cong" { IFDEF LEXER THEN out "CONG" ELSE () END; TP.CONG } + | "\\def" { IFDEF LEXER THEN out "DEF" ELSE () END; TP.DEF } + | "\\th" { IFDEF LEXER THEN out "TH" ELSE () END; TP.TH } + | "\\generate" { IFDEF LEXER THEN out "GEN" ELSE () END; TP.GEN } + | "\\require" { IFDEF LEXER THEN out "REQ" ELSE () END; TP.REQ } + | "\\open" { IFDEF LEXER THEN out "OPEN" ELSE () END; TP.OPEN } + | "\\close" { IFDEF LEXER THEN out "CLOSE" ELSE () END; TP.CLOSE } + | "\\sorts" { IFDEF LEXER THEN out "SORTS" ELSE () END; TP.SORTS } + | "(" { IFDEF LEXER THEN out "OP" ELSE () END; TP.OP } + | ")" { IFDEF LEXER THEN out "CP" ELSE () END; TP.CP } + | "[" { IFDEF LEXER THEN out "OB" ELSE () END; TP.OB } + | "]" { IFDEF LEXER THEN out "CB" ELSE () END; TP.CB } + | "{" { IFDEF LEXER THEN out "OC" ELSE () END; TP.OC } + | "}" { IFDEF LEXER THEN out "CC" ELSE () END; TP.CC } + | "<" { IFDEF LEXER THEN out "OA" ELSE () END; TP.OA } + | ">" { IFDEF LEXER THEN out "CA" ELSE () END; TP.CA } + | "." { IFDEF LEXER THEN out "FS" ELSE () END; TP.FS } + | ":" { IFDEF LEXER THEN out "CN" ELSE () END; TP.CN } + | "," { IFDEF LEXER THEN out "CM" ELSE () END; TP.CM } + | "=" { IFDEF LEXER THEN out "EQ" ELSE () END; TP.EQ } + | "*" { IFDEF LEXER THEN out "STAR" ELSE () END; TP.STAR } + | "#" { IFDEF LEXER THEN out "HASH" ELSE () END; TP.HASH } + | "~" { IFDEF LEXER THEN out "TE" ELSE () END; TP.TE } + | "^" { IFDEF LEXER THEN out "CT" ELSE () END; TP.CT } + | eof { IFDEF LEXER THEN out "EOF" ELSE () END; TP.EOF } diff --git a/helm/software/helena/src/text/txtParser.mly b/helm/software/helena/src/text/txtParser.mly index 32d0df309..32a0decaf 100644 --- a/helm/software/helena/src/text/txtParser.mly +++ b/helm/software/helena/src/text/txtParser.mly @@ -27,8 +27,10 @@ module G = Options module N = Layer module T = Txt - + +IFDEF PARSER THEN let _ = Parsing.set_trace !G.debug_parser +END %} %token IX %token ID STR diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 4641af458..1d1de3572 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -89,17 +89,16 @@ type kernel_entity = BrgEntity of Brg.entity | BagEntity of Bag.entity | CrgEntity of Crg.entity +IFDEF SUMMARY THEN + let print_counters st = function | G.V4 -> DO.print_counters C.start st.dc | G.V3 -> BO.print_counters C.start st.bc | G.V0 -> ZO.print_counters C.start st.zc -let xlate_entity st entity = match !G.kernel, entity with - | G.V3, CrgEntity e -> - let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e - | G.V0, CrgEntity e -> - let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e - | _, entity -> entity +END + +IFDEF TRACE THEN let pp_progress e = let f _ na u = @@ -112,16 +111,28 @@ let pp_progress e = | BrgEntity e -> E.common f e | BagEntity e -> E.common f e +END + +IFDEF SUMMARY THEN + let count_entity st = function | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e} | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e} | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e} +END + +IFDEF OBJECTS THEN + let export_entity st = function | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e +END + +IFDEF TYPE THEN + let type_check st k = let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in let bag_err msg = bag_error st "Type Error" msg; failwith "Interrupted" in @@ -131,13 +142,7 @@ let type_check st k = | BagEntity entity -> ZU.type_check bag_err ok st.kst entity | CrgEntity _ -> st -let validate st k = - let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in - let ok _ = st in - match k with - | BrgEntity entity -> BU.validate brg_err ok st.kst entity - | BagEntity _ -> st - | CrgEntity _ -> st +END IFDEF MANAGER THEN @@ -150,6 +155,21 @@ let manager st output_entity = function END +let xlate_entity st entity = match !G.kernel, entity with + | G.V3, CrgEntity e -> + let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e + | G.V0, CrgEntity e -> + let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e + | _, entity -> entity + +let validate st k = + let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in + let ok _ = st in + match k with + | BrgEntity entity -> BU.validate brg_err ok st.kst entity + | BagEntity _ -> st + | CrgEntity _ -> st + (* extended lexer ***********************************************************) type 'token lexer = { @@ -210,31 +230,57 @@ let entity_of_input lexbuf i = match i, !parbuf with | Text, hd :: tl -> parbuf := tl; hd +IFDEF PREPROCESS THEN + let process_input f st = function | AutEntity e -> let f pst e = f {st with pst = pst} (AutEntity e) in AA.process_command f st.pst e | xe -> f st xe +END + +IFDEF SUMMARY THEN + let count_input st = function | AutEntity e -> {st with ac = AO.count_command C.start st.ac e} | xe -> st +END + (****************************************************************************) -let version = ref true -let root = ref "" let st = ref (initial_status ()) let streaming = ref false (* parsing style (temporary) *) let process_2 st entity = - let st = if !G.summary then count_entity st entity else st in - let st = - if !G.stage >= 3 then - let f = if !version then validate else type_check in f st entity + let st = +IFDEF SUMMARY THEN + if !G.summary then count_entity st entity else st +ELSE + st +END + in + let st = +IFDEF STAGE THEN + if !G.stage >= 3 then +IFDEF TYPE THEN + let f = if !G.validate then validate else type_check in f st entity +ELSE + validate st entity +END else st +ELSE +IFDEF TYPE THEN + let f = if !G.validate then validate else type_check in f st entity +ELSE + validate st entity +END +END in - if !G.export then export_entity st entity; +IFDEF OBJECTS THEN + if !G.export then export_entity st entity +ELSE () END; IFDEF MANAGER THEN match st.mst with | None -> st @@ -243,14 +289,29 @@ ELSE st END -let process_1 st entity = +let process_1 st entity = +IFDEF TRACE THEN if !G.ct >= 3 then pp_progress entity; - let st = if !G.summary then count_entity st entity else st in - if !G.export && !G.stage = 1 then export_entity st entity; +ELSE () END; + let st = +IFDEF SUMMARY THEN + if !G.summary then count_entity st entity else st +ELSE + st +END + in +IFDEF STAGE THEN +IFDEF OBJECTS THEN + if !G.export && !G.stage = 1 then export_entity st entity +ELSE () END; if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st +ELSE + process_2 st (xlate_entity st entity) +END let process_0 st entity = let f st entity = +IFDEF STAGE THEN if !G.stage = 0 then st else match entity with | AutEntity e -> @@ -262,8 +323,26 @@ let process_0 st entity = let d tst e = process_1 {st with tst = tst} (CrgEntity e) in TD.crg_of_txt crr d gen_text st.tst e | NoEntity -> assert false +ELSE + match entity with + | AutEntity e -> + let err ast = {st with ast = ast} in + let g ast e = process_1 {st with ast = ast} (CrgEntity e) in + AD.crg_of_aut err g st.kst st.ast e + | TxtEntity e -> + let crr tst = {st with tst = tst} in + let d tst e = process_1 {st with tst = tst} (CrgEntity e) in + TD.crg_of_txt crr d gen_text st.tst e + | NoEntity -> assert false +END in - let st = if !G.summary then count_input st entity else st in + let st = +IFDEF SUMMARY THEN + if !G.summary then count_input st entity else st +ELSE + st +END + in IFDEF PREPROCESS THEN if !G.preprocess then process_input f st entity else f st entity ELSE @@ -294,7 +373,12 @@ let process_streaming st lexbuf input = IFDEF PREPROCESS THEN let set_preprocess () = - if !G.trace >= 2 then begin G.preprocess := true; G.summary := true end + if !G.trace >= 2 then begin + G.preprocess := true; +IFDEF SUMMARY THEN + G.summary := true +ELSE () END + end END @@ -310,7 +394,28 @@ let set_manager s = match KS.lowercase s with | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) END - + +IFDEF SUMMARY THEN + +let set_summary () = + if !G.trace >= 2 then G.summary := true + +END + +let set_trace i = + if !G.trace = 0 && i > 0 then Y.gmtime G.version_string; + if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit"; + G.trace := i; +IFDEF SUMMARY THEN + if i <= 1 then G.summary := false +ELSE () END; +IFDEF PREPROCESS THEN + if i <= 1 then G.preprocess := false +ELSE () END + +let custom_exit () = + if !G.trace >= 1 then Y.utime_stamp "at exit" + let process st name = let process = if !streaming then process_streaming else process_nostreaming in let input = type_of_input name in @@ -323,9 +428,17 @@ let process st name = let main = let print_version () = let features = [ +(IFDEF LEXER THEN "LEXER" ELSE "" END); +(IFDEF PARSER THEN "PARSER" ELSE "" END); +(IFDEF TRACE THEN "TRACE" ELSE "" END); +(IFDEF SUMMARY THEN "SUMMARY" ELSE "" END); (IFDEF EXPAND THEN "EXPAND" ELSE "" END); (IFDEF MANAGER THEN "MANAGER" ELSE "" END); +(IFDEF OBJECTS THEN "OBJECTS" ELSE "" END); (IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END); +(IFDEF QUOTE THEN "QUOTE" ELSE "" END); +(IFDEF STAGE THEN "STAGE" ELSE "" END); +(IFDEF TYPE THEN "TYPE" ELSE "" END); ] in let map s = s <> "" in let features_string = KT.concat " " (KL.filter map features) in @@ -341,25 +454,12 @@ let main = | "V0" -> G.kernel := G.V0 | s -> L.warn level (KP.sprintf "Unknown kernel version: %s" s) in - let set_trace i = - if !G.trace = 0 && i > 0 then Y.gmtime G.version_string; - if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit"; - G.trace := i; - if i <= 1 then G.summary := false; -IFDEF PREPROCESS THEN - if i <= 1 then G.preprocess := false -ELSE - () -END - in - let set_summary () = - if !G.trace >= 2 then G.summary := true - in let clear_options () = - root := ""; - G.clear (); H.clear (); O.clear_reductions (); + G.clear (); H.clear (); +IFDEF SUMMARY THEN + O.clear_reductions () +ELSE () END; streaming := false; - version := true in let undefined opt () = L.warn level (KP.sprintf "%s was compiled without the support for option %s" G.version_string opt); @@ -367,12 +467,16 @@ END in let arg_undefined opt = Arg.Unit (undefined opt) in let process_file name = - if !G.trace >= 2 then L.warn 1 (KP.sprintf "Processing file: %s" name); - if !G.trace >= 2 then Y.utime_stamp "started"; + if !G.trace >= 2 then begin + L.warn 1 (KP.sprintf "Processing file: %s" name); + Y.utime_stamp "started" + end; let base_name = Filename.chop_extension (Filename.basename name) in - let cover = KF.concat !root base_name in - if !G.stage <= 1 then G.kernel := G.V4; + let cover = KF.concat !G.root base_name in G.cover := cover; +IFDEF STAGE THEN + if !G.stage <= 1 then G.kernel := G.V4; +ELSE () END; IFDEF MANAGER THEN begin match !G.manager with | G.Coq -> st := {!st with mst = Some (BA.open_out base_name)} @@ -383,9 +487,7 @@ IFDEF MANAGER THEN | G.TJ3 -> st := {!st with mst = Some (BP.open_out_tj3 base_name)} | G.Quiet -> () end -ELSE - () -END; +ELSE () END; P.clear_marks (); let sst, input = process (refresh_status !st) name in st := begin match sst.mst with @@ -393,20 +495,23 @@ END; | Some (_, close_out) -> close_out (); {sst with mst = None} end; if !G.trace >= 2 then Y.utime_stamp "processed"; +IFDEF SUMMARY THEN if !G.summary then begin AO.print_counters C.start !st.ac; IFDEF PREPROCESS THEN if !G.preprocess then AO.print_process_counters C.start !st.pst -ELSE - () -END; +ELSE () END; +IFDEF STAGE THEN if !G.stage >= 1 then print_counters !st G.V4; if !G.stage >= 2 then print_counters !st !G.kernel; if !G.stage >= 3 then O.print_reductions () +ELSE + print_counters !st G.V4; + print_counters !st !G.kernel; + O.print_reductions () +END end - in - let exit () = - if !G.trace >= 1 then Y.utime_stamp "at exit" +ELSE () END in let help = "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts | -MO | -p | -ahkmr | -be ]* [ ]*\n\n" ^ @@ -437,7 +542,7 @@ END; let help_n = " [names] Show short constants (default: qualified constants)" in let help_o = " [objects] Export kernel entities (XML)" in let help_p = " [preamble] Set preamble to this file (default: empty)" in - let help_q = " [quote] Disable quotation of identifiers (default: enable)" in + let help_q = " [quote] Quote identifiers (default: disable)" in let help_r = " [root] Set initial segment of URI hierarchy (default: empty)" in let help_s = " [stage] Set translation stage (see above)" in let help_t = " [type] Type check (default: validate)" in @@ -446,18 +551,18 @@ END; let help_y = " [infinity] Use ∞-abstractions in contexts" in let help_0 = " [zero] Preprocess source (Automath)" in let help_1 = " [one] parse files with streaming policy" in - at_exit exit; + at_exit custom_exit; Arg.parse [ - ("-L", Arg.Set G.debug_lexer, help_L); + ("-L", (IFDEF LEXER THEN Arg.Set G.debug_lexer ELSE arg_undefined "-L" END), help_L); ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M); - ("-O", Arg.String ((:=) G.xdir), help_O); - ("-P", Arg.Set G.debug_parser, help_P); + ("-O", (IFDEF OBJECTS THEN Arg.String ((:=) G.xdir) ELSE arg_undefined "-O" END), help_O); + ("-P", (IFDEF PARSER THEN Arg.Set G.debug_parser ELSE arg_undefined "-P" END), help_P); ("-T", Arg.Int set_trace, help_T); ("-V", Arg.Unit print_version, help_V); ("-X", Arg.Unit clear_options, help_X); ("-a", Arg.String ((:=) G.alpha), help_a); ("-b", Arg.Int ((:=) G.first), help_b); - ("-d", Arg.Unit set_summary, help_d); + ("-d", (IFDEF SUMMARY THEN Arg.Unit set_summary ELSE arg_undefined "-d" END), help_d); ("-e", Arg.Int ((:=) G.last), help_e); ("-g", (IFDEF EXPAND THEN Arg.Set G.expand ELSE arg_undefined "-g" END), help_g); ("-h", Arg.String set_hierarchy, help_h); @@ -466,12 +571,12 @@ END; ("-l", Arg.Set G.cc, help_l); ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m); ("-n", Arg.Set G.short, help_n); - ("-o", Arg.Set G.export, help_o); + ("-o", (IFDEF OBJECTS THEN Arg.Set G.export ELSE arg_undefined "-o" END), help_o); ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p); - ("-q", Arg.Set G.unquote, help_q); - ("-r", Arg.String ((:=) root), help_r); - ("-s", Arg.Int ((:=) G.stage), help_s); - ("-t", Arg.Clear version, help_t); + ("-q", (IFDEF QUOTE THEN Arg.Set G.quote ELSE arg_undefined "-q" END), help_q); + ("-r", Arg.String ((:=) G.root), help_r); + ("-s", (IFDEF STAGE THEN Arg.Int ((:=) G.stage) ELSE arg_undefined "-s" END), help_s); + ("-t", (IFDEF TYPE THEN Arg.Clear G.validate ELSE arg_undefined "-t" END), help_t); ("-u", Arg.Set G.si, help_u); ("-x", Arg.Set G.extended, help_x); ("-y", Arg.Set G.infinity, help_y); diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index 673eefa0c..5d112bed2 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -17,6 +17,8 @@ module R = Alpha module XL = XmlLibrary module D = Crg +IFDEF OBJECTS THEN + (* internal functions *******************************************************) let lenv_iter map_bind map_appl map_proj st e lenv out tab = @@ -97,3 +99,5 @@ and exp_proj st e lenv out tab = (* interface functions ******************************************************) let export_term st = exp_term st D.empty_lenv + +END diff --git a/helm/software/helena/src/xml/xmlCrg.mli b/helm/software/helena/src/xml/xmlCrg.mli index 63a9f6800..b4b057f15 100644 --- a/helm/software/helena/src/xml/xmlCrg.mli +++ b/helm/software/helena/src/xml/xmlCrg.mli @@ -9,4 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF OBJECTS THEN + val export_term: Layer.status -> Crg.term -> XmlLibrary.pp + +END diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 901c783a2..4667b3aa5 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -18,6 +18,8 @@ module H = Hierarchy module N = Layer module E = Entity +IFDEF OBJECTS THEN + (* internal functions *******************************************************) let base = "xml" @@ -150,3 +152,5 @@ let export_entity pp_term (ra, na, u, b) = let attrs = [xmlns; "hierarchy", shp; "options", opts] in tag obj_root attrs ~contents out 0; close_out och + +END diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 202ec2c27..552aa3666 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +IFDEF OBJECTS THEN + type och = string -> unit type attr = string * string @@ -56,3 +58,5 @@ val apix: Entity.node_attrs -> attr val meta: Entity.root_attrs -> attr val info: Entity.root_attrs -> attr list + +END