+++ /dev/null
-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
+++ /dev/null
-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
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
@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)"
@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
$(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)"
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
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)
@echo " OCAMLC $<"
$(H)$(OCAMLC) -c $<
-O_TAGS += all opt $(MAIN).opt
+O_TAGS += opt $(MAIN).opt
B_TAGS += byte $(MAIN).byte
<compile-time feature> ::=
+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
--- /dev/null
+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
*)
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
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
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
id
in
aux 0
+
+END
}
let LC = ['#' '%']
| 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 }
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}
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");
f ()
in
AA.get_counters f c
+
+END
+
+END
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
module G = Options
module A = Aut
+IFDEF PARSER THEN
let _ = Parsing.set_trace !G.debug_parser
+END
%}
%token <int> NUM
%token <string> IDENT
(* internal functions *******************************************************)
+IFDEF PREPROCESS THEN
+
let orc_reset f st =
f {st with opening = false; reopening = false; closing = false}
| 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 () = {
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
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
module E = Entity
module Z = Bag
+IFDEF TYPE THEN
+
exception ObjectNotFound of Z.message
let hsize = 7000
let get_entity f uri =
try f (UH.find env uri) with Not_found -> error uri
+
+END
\ / 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
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
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
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
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
module ZE = BagEnvironment
module ZS = BagSubstitution
+IFDEF TYPE THEN
+
type machine = {
i: int;
c: Z.lenv;
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
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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+IFDEF TYPE THEN
+
type ho_whd_result =
| Sort of int
| Abst of Bag.term
val are_convertible:
(bool -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a
+
+END
module S = Share
module Z = Bag
+IFDEF TYPE THEN
+
(* Internal functions *******************************************************)
let rec lref_map_bind f map b = match b 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
\ / 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
module ZE = BagEnvironment
module ZR = BagReduction
+IFDEF TYPE THEN
+
(* Internal functions *******************************************************)
let level = 4
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)
| 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)
(* Interface functions ******************************************************)
and type_of err f st c x = b_type_of err f st c x
+
+END
\ / 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
module ZE = BagEnvironment
module ZT = BagType
+IFDEF TYPE THEN
+
(* Interface functions ******************************************************)
(* to share *)
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
\ / 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
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
L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes);
f ()
+END
+
(* lenv/term pretty printing ************************************************)
let name err och a =
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
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
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
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
| 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
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
| [] ->
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
{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
| 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), _ ->
| 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
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
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
module G = Options
module B = Brg
+IFDEF TYPE THEN
+
let rec icm a = function
| B.Sort _
| B.LRef _
*)
iter (lift_map h) d t
end
+
+END
\ / 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
module BS = BrgSubstitution
module BR = BrgReduction
+IFDEF TYPE THEN
+
(* Internal functions *******************************************************)
let level = 4
| _ -> 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)
(* Interface functions ******************************************************)
and type_of err f st m t = b_type_of err f st m t
+
+END
\ / 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
(* Interface functions ******************************************************)
+IFDEF TYPE THEN
+
(* to share *)
let type_check err f st = function
| ra, na, uri, E.Abst t ->
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
\ / 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
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
| _ -> 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) ->
| 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 =
in
KH.iter map st
+END
+
let cell s v = {
v = v; s = s; b = false
}
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
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)
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))
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
| 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
type kernel = V4 | V3 | V0
+IFDEF MANAGER THEN
+
type manager = Quiet
| Coq
| Matita
| 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 *)
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 *)
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
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
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
module L = Log
module G = Options
+IFDEF SUMMARY THEN
+
type reductions = {
beta : int;
zeta : int;
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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+IFDEF SUMMARY THEN
+
val clear_reductions: unit -> unit
val add:
unit -> unit
val print_reductions: unit -> unit
+
+END
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}
L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes);
f ()
+END
+
(* term/environment pretty printer ******************************************)
let pp_b_attrs out a =
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
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 = "\\"
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 }
module G = Options
module N = Layer
module T = Txt
-
+
+IFDEF PARSER THEN
let _ = Parsing.set_trace !G.debug_parser
+END
%}
%token <int> IX
%token <string> ID STR
| 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 =
| 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
| 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
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 = {
| 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
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 ->
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
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
| 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
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
| "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);
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)}
| 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
| 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 <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
let help_n = " [names] Show short constants (default: qualified constants)" in
let help_o = " [objects] Export kernel entities (XML)" in
let help_p = "<file> [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 = "<string> [root] Set initial segment of URI hierarchy (default: empty)" in
let help_s = "<number> [stage] Set translation stage (see above)" in
let help_t = " [type] Type check (default: validate)" in
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);
("-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);
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 =
(* interface functions ******************************************************)
let export_term st = exp_term st D.empty_lenv
+
+END
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+IFDEF OBJECTS THEN
+
val export_term: Layer.status -> Crg.term -> XmlLibrary.pp
+
+END
module N = Layer
module E = Entity
+IFDEF OBJECTS THEN
+
(* internal functions *******************************************************)
let base = "xml"
let attrs = [xmlns; "hierarchy", shp; "options", opts] in
tag obj_root attrs ~contents out 0;
close_out och
+
+END
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+IFDEF OBJECTS THEN
+
type och = string -> unit
type attr = string * string
val meta: Entity.root_attrs -> attr
val info: Entity.root_attrs -> attr list
+
+END
projects / helm.git / commitdiff