From 30eb28f8c35d7667b3a0052c30d2750a492fa464 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 14 Dec 2014 15:29:51 +0000 Subject: [PATCH] - we removed a flag from the kernel status - some renaming --- helm/software/helena/.depend.opt | 257 +++++++++--------- .../helena/src/basic_rg/brgReduction.ml | 42 +-- .../helena/src/basic_rg/brgReduction.mli | 16 +- helm/software/helena/src/basic_rg/brgType.mli | 2 +- .../helena/src/basic_rg/brgUntrusted.ml | 6 +- .../helena/src/basic_rg/brgValidity.mli | 2 +- helm/software/helena/src/common/output.ml | 16 +- helm/software/helena/src/common/output.mli | 2 +- helm/software/helena/src/common/status.ml | 4 +- 9 files changed, 176 insertions(+), 171 deletions(-) diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 016521236..0580e6bfc 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -1,257 +1,260 @@ -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/common/options.cmo: src/lib/cps.cmx -src/common/options.cmx: src/lib/cps.cmx -src/common/marks.cmi: -src/common/marks.cmo: src/common/marks.cmi -src/common/marks.cmx: src/common/marks.cmi -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/level.cmi: -src/common/level.cmo: src/common/options.cmx src/common/marks.cmi \ +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/common/options.cmo : src/lib/cps.cmx +src/common/options.cmx : src/lib/cps.cmx +src/common/marks.cmi : +src/common/marks.cmo : src/common/marks.cmi +src/common/marks.cmx : src/common/marks.cmi +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/level.cmi : +src/common/level.cmo : src/common/options.cmx src/common/marks.cmi \ src/lib/log.cmi src/common/level.cmi -src/common/level.cmx: src/common/options.cmx src/common/marks.cmx \ +src/common/level.cmx : src/common/options.cmx src/common/marks.cmx \ src/lib/log.cmx src/common/level.cmi -src/common/entity.cmo: src/common/level.cmi -src/common/entity.cmx: src/common/level.cmx -src/common/output.cmi: -src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \ +src/common/entity.cmo : src/common/level.cmi +src/common/entity.cmx : src/common/level.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.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/common/status.cmo: src/common/options.cmx src/common/level.cmi -src/common/status.cmx: src/common/options.cmx src/common/level.cmx -src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx \ +src/common/alpha.cmi : src/common/entity.cmx +src/common/alpha.cmo : src/common/entity.cmx src/common/alpha.cmi +src/common/alpha.cmx : src/common/entity.cmx src/common/alpha.cmi +src/common/status.cmo : src/common/options.cmx src/common/level.cmi +src/common/status.cmx : src/common/options.cmx src/common/level.cmx +src/complete_rg/crg.cmo : src/common/level.cmi src/common/entity.cmx \ src/lib/cps.cmx -src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \ +src/complete_rg/crg.cmx : src/common/level.cmx src/common/entity.cmx \ src/lib/cps.cmx -src/complete_rg/crgOutput.cmi: src/common/level.cmi src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo: src/common/marks.cmi src/lib/log.cmi \ +src/complete_rg/crgOutput.cmi : src/common/level.cmi src/complete_rg/crg.cmx +src/complete_rg/crgOutput.cmo : src/common/marks.cmi src/lib/log.cmi \ src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ src/lib/cps.cmx src/complete_rg/crgOutput.cmi -src/complete_rg/crgOutput.cmx: src/common/marks.cmx src/lib/log.cmx \ +src/complete_rg/crgOutput.cmx : src/common/marks.cmx src/lib/log.cmx \ src/common/level.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/level.cmi -src/text/txt.cmx: src/common/level.cmx -src/text/txtParser.cmi: src/text/txt.cmx -src/text/txtParser.cmo: src/text/txt.cmx src/common/options.cmx \ +src/text/txt.cmo : src/common/level.cmi +src/text/txt.cmx : src/common/level.cmx +src/text/txtParser.cmi : src/text/txt.cmx +src/text/txtParser.cmo : src/text/txt.cmx src/common/options.cmx \ src/common/level.cmi src/text/txtParser.cmi -src/text/txtParser.cmx: src/text/txt.cmx src/common/options.cmx \ +src/text/txtParser.cmx : src/text/txt.cmx src/common/options.cmx \ src/common/level.cmx src/text/txtParser.cmi -src/text/txtLexer.cmo: src/text/txtParser.cmi src/common/options.cmx \ +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/text/txtLexer.cmx : src/text/txtParser.cmx src/common/options.cmx \ src/lib/log.cmx -src/text/txtTxt.cmi: src/text/txt.cmx -src/text/txtTxt.cmo: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi -src/text/txtTxt.cmx: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi -src/text/txtCrg.cmi: src/text/txt.cmx src/complete_rg/crg.cmx -src/text/txtCrg.cmo: src/text/txtTxt.cmi src/text/txt.cmx \ +src/text/txtTxt.cmi : src/text/txt.cmx +src/text/txtTxt.cmo : src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi +src/text/txtTxt.cmx : src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi +src/text/txtCrg.cmi : src/text/txt.cmx src/complete_rg/crg.cmx +src/text/txtCrg.cmo : src/text/txtTxt.cmi src/text/txt.cmx \ src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \ src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi -src/text/txtCrg.cmx: src/text/txtTxt.cmx src/text/txt.cmx \ +src/text/txtCrg.cmx : src/text/txtTxt.cmx src/text/txt.cmx \ src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \ src/complete_rg/crg.cmx src/lib/cps.cmx src/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/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/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/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.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/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/autLexer.cmx : src/common/options.cmx src/lib/log.cmx \ src/automath/autParser.cmx -src/automath/autCrg.cmi: src/common/status.cmx src/complete_rg/crg.cmx \ +src/automath/autCrg.cmi : src/common/status.cmx src/complete_rg/crg.cmx \ src/automath/aut.cmx -src/automath/autCrg.cmo: src/common/status.cmx src/common/options.cmx \ +src/automath/autCrg.cmo : src/common/status.cmx src/common/options.cmx \ src/common/level.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/status.cmx src/common/options.cmx \ +src/automath/autCrg.cmx : src/common/status.cmx src/common/options.cmx \ src/common/level.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/level.cmi src/common/entity.cmx -src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \ +src/xml/xmlLibrary.cmi : src/common/level.cmi src/common/entity.cmx +src/xml/xmlLibrary.cmo : src/common/options.cmx src/common/level.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/level.cmx \ +src/xml/xmlLibrary.cmx : src/common/options.cmx src/common/level.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/level.cmi \ +src/xml/xmlCrg.cmi : src/xml/xmlLibrary.cmi src/common/level.cmi \ src/complete_rg/crg.cmx -src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \ +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/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/level.cmi src/common/entity.cmx -src/basic_rg/brg.cmx: src/common/level.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/level.cmi src/common/entity.cmx \ +src/basic_rg/brg.cmo : src/common/level.cmi src/common/entity.cmx +src/basic_rg/brg.cmx : src/common/level.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/level.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/level.cmx src/common/entity.cmx \ +src/basic_rg/brgCrg.cmx : src/common/level.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/basic_rg/brgOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ src/common/level.cmi src/basic_rg/brg.cmx -src/basic_rg/brgOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \ +src/basic_rg/brgOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \ src/lib/log.cmi src/common/level.cmi src/common/hierarchy.cmi \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi -src/basic_rg/brgOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \ +src/basic_rg/brgOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ src/lib/log.cmx src/common/level.cmx src/common/hierarchy.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brgCrg.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi -src/basic_rg/brgEnvironment.cmi: src/basic_rg/brg.cmx -src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx \ +src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx +src/basic_rg/brgEnvironment.cmo : src/common/entity.cmx \ src/basic_rg/brgEnvironment.cmi -src/basic_rg/brgEnvironment.cmx: src/common/entity.cmx \ +src/basic_rg/brgEnvironment.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/common/status.cmx src/lib/log.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/common/status.cmx src/lib/log.cmi \ src/common/level.cmi src/common/entity.cmx src/basic_rg/brg.cmx -src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \ +src/basic_rg/brgReduction.cmo : src/common/status.cmx src/lib/share.cmx \ src/common/output.cmi src/common/options.cmx src/lib/log.cmi \ src/common/level.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/common/status.cmx src/lib/share.cmx \ +src/basic_rg/brgReduction.cmx : src/common/status.cmx src/lib/share.cmx \ src/common/output.cmx src/common/options.cmx src/lib/log.cmx \ src/common/level.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/status.cmx \ +src/basic_rg/brgValidity.cmi : src/common/status.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx -src/basic_rg/brgValidity.cmo: src/common/status.cmx src/common/options.cmx \ +src/basic_rg/brgValidity.cmo : src/common/status.cmx src/common/options.cmx \ src/lib/log.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/status.cmx src/common/options.cmx \ +src/basic_rg/brgValidity.cmx : src/common/status.cmx src/common/options.cmx \ src/lib/log.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/status.cmx src/basic_rg/brgReduction.cmi \ - src/basic_rg/brg.cmx -src/basic_rg/brgType.cmo: src/common/status.cmx src/lib/share.cmx \ +src/basic_rg/brgType.cmi : src/common/status.cmx \ + src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx +src/basic_rg/brgType.cmo : src/common/status.cmx src/lib/share.cmx \ src/common/options.cmx src/lib/log.cmi src/common/level.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/common/status.cmx src/lib/share.cmx \ +src/basic_rg/brgType.cmx : src/common/status.cmx src/lib/share.cmx \ src/common/options.cmx src/lib/log.cmx src/common/level.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/status.cmx \ +src/basic_rg/brgUntrusted.cmi : src/common/status.cmx \ 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/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/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/common/level.cmi src/basic_rg/brg.cmx -src/basic_rg/brgGrafite.cmo: src/common/options.cmx src/common/level.cmi \ +src/basic_rg/brgGrafite.cmi : src/common/level.cmi src/basic_rg/brg.cmx +src/basic_rg/brgGrafite.cmo : src/common/options.cmx src/common/level.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/level.cmx \ +src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/level.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_ag/bag.cmo: src/common/marks.cmi src/lib/log.cmi \ +src/basic_ag/bag.cmo : src/common/marks.cmi src/lib/log.cmi \ src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bag.cmx: src/common/marks.cmx src/lib/log.cmx \ +src/basic_ag/bag.cmx : src/common/marks.cmx src/lib/log.cmx \ src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bagCrg.cmi: src/common/level.cmi src/complete_rg/crg.cmx \ +src/basic_ag/bagCrg.cmi : src/common/level.cmi src/complete_rg/crg.cmx \ src/basic_ag/bag.cmx -src/basic_ag/bagCrg.cmo: src/common/marks.cmi src/common/level.cmi \ +src/basic_ag/bagCrg.cmo : src/common/marks.cmi src/common/level.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/common/marks.cmx src/common/level.cmx \ +src/basic_ag/bagCrg.cmx : src/common/marks.cmx src/common/level.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/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ src/common/level.cmi src/basic_ag/bag.cmx -src/basic_ag/bagOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \ +src/basic_ag/bagOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \ src/common/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/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ src/common/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/lib/log.cmi src/common/entity.cmx \ +src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmx +src/basic_ag/bagEnvironment.cmo : src/lib/log.cmi src/common/entity.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \ +src/basic_ag/bagEnvironment.cmx : src/lib/log.cmx src/common/entity.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagSubstitution.cmi: src/common/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/common/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.cmx : src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi -src/basic_ag/bagReduction.cmi: src/common/status.cmx src/basic_ag/bag.cmx -src/basic_ag/bagReduction.cmo: src/common/status.cmx src/common/options.cmx \ +src/basic_ag/bagReduction.cmi : src/common/status.cmx src/basic_ag/bag.cmx +src/basic_ag/bagReduction.cmo : src/common/status.cmx src/common/options.cmx \ src/common/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/status.cmx src/common/options.cmx \ +src/basic_ag/bagReduction.cmx : src/common/status.cmx src/common/options.cmx \ src/common/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/status.cmx src/basic_ag/bag.cmx -src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \ +src/basic_ag/bagType.cmi : src/common/status.cmx src/basic_ag/bag.cmx +src/basic_ag/bagType.cmo : src/common/status.cmx 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/common/status.cmx src/lib/share.cmx \ +src/basic_ag/bagType.cmx : src/common/status.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/status.cmx src/basic_ag/bag.cmx -src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ +src/basic_ag/bagUntrusted.cmi : src/common/status.cmx src/basic_ag/bag.cmx +src/basic_ag/bagUntrusted.cmo : src/lib/log.cmi src/common/entity.cmx \ src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \ src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi -src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ +src/basic_ag/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/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/status.cmx \ src/common/output.cmi src/common/options.cmx src/lib/log.cmi \ @@ -265,7 +268,7 @@ src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ 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/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/status.cmx \ src/common/output.cmx src/common/options.cmx src/lib/log.cmx \ diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 1fd77cd51..7f7dd4e78 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -22,7 +22,7 @@ module B = Brg module BO = BrgOutput module BE = BrgEnvironment -type kam = { +type rtm = { e: B.lenv; (* environment *) s: (B.lenv * B.term) list; (* stack *) l: int; (* level *) @@ -30,7 +30,7 @@ type kam = { n: int option; (* expected type iterations *) } -type message = (kam, B.term) L.message +type message = (rtm, B.term) L.message (* Internal functions *******************************************************) @@ -102,7 +102,7 @@ let rec step st m x = | B.GRef (_, uri) -> begin match BE.get_entity uri with | _, _, _, E.Abbr v -> - if st.S.delta then begin + if m.n = None || !G.expand then begin if !G.summary then O.add ~gdelta:1 (); step st m v end else @@ -141,7 +141,11 @@ let rec step st m x = | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t | B.Bind (a, B.Abst (n, w), t) -> - begin match m.s with +(* if not !G.cc && st.S.si && N.to_string st.S.lenv n = "0" then begin + if !G.summary then O.add ~upsilon:1 (); + let e = B.push m.e m.e a B.Void in + step st {m with e = e} t + end else *) begin match m.s with | [] -> let i = tsteps m in if i = 0 then m, x, None else @@ -169,7 +173,7 @@ let assert_iterations m1 m2 = match m1.n, m2.n with let push m a b = let a, l = match b with | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l - | b -> a, m.l + | _ -> a, m.l in let e = B.push m.e m.e a b in {m with e = e; l = l} @@ -177,15 +181,15 @@ let push m a b = let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = if !G.trace >= level then log2 st.S.lenv "Now converting nfs" m1.e t1 m2.e t2; match t1, r1, t2, r2 with - | B.Sort (_, h1), _, B.Sort (_, h2), _ -> + | B.Sort (_, h1), _, B.Sort (_, h2), _ -> h1 = h2 | B.LRef ({E.n_apix = e1}, _), _, - B.LRef ({E.n_apix = e2}, _), _ -> + B.LRef ({E.n_apix = e2}, _), _ -> if e1 = e2 then ac_stacks st m1 m2 else false - | B.GRef (_, u1), None, B.GRef (_, u2), None -> + | B.GRef (_, u1), None, B.GRef (_, u2), None -> if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false | B.GRef ({E.n_apix = e1}, u1), Some v1, - B.GRef ({E.n_apix = e2}, u2), Some v2 -> + B.GRef ({E.n_apix = e2}, u2), Some v2 -> if e1 < e2 then begin if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) @@ -197,25 +201,25 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = if !G.summary then O.add ~gdelta:2 (); ac st m1 v1 m2 v2 end - | _, _, B.GRef _, Some v2 -> + | _, _, B.GRef _, Some v2 -> if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) - | B.GRef _, Some v1, _, _ -> + | B.GRef _, Some v1, _, _ -> if !G.summary then O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, t2, r2) | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, - B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ -> + B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ -> if !G.cc && not (N.assert_equal st.S.lenv n1 n2) then false else if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false - | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ -> + | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ -> if st.S.si then if !G.cc && not (N.assert_zero st.S.lenv n) then false else begin - if !G.summary then O.add ~si:1 (); - ac st (push m1 a b) t1 (push m2 a b) t end + if !G.summary then O.add ~upsilon:1 (); + ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end else false - | _ -> false + | _ -> false and ac st m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) @@ -232,7 +236,7 @@ and ac_stacks st m1 m2 = (* Interface functions ******************************************************) -let empty_kam = { +let empty_rtm = { e = B.empty; s = []; l = 0; d = 0; n = None } @@ -242,12 +246,12 @@ let get m i = let xwhd st m n t = if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t; - let m, t, _ = step {st with S.delta = true} (reset m n) t in + let m, t, _ = step st (reset m n) t in m, t let are_convertible st m1 n1 t1 m2 n2 t2 = if !G.trace >= level then log2 st.S.lenv "Now converting" m1.e t1 m2.e t2; - let r = ac {st with S.delta = !G.expand} (reset m1 n1) t1 (reset m2 n2) t2 in + let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in r (* let err _ = in if W.eq mu mw then are_alpha_convertible err f u w else err () *) diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli index 42798aeee..85df40283 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.mli +++ b/helm/software/helena/src/basic_rg/brgReduction.mli @@ -9,20 +9,20 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type kam +type rtm -type message = (kam, Brg.term) Log.message +type message = (rtm, Brg.term) Log.message -val empty_kam: kam +val empty_rtm: rtm -val get: kam -> int -> Brg.bind +val get: rtm -> int -> Brg.bind -val push: kam -> Entity.node_attrs -> Brg.bind -> kam +val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm -val xwhd: Status.status -> kam -> int option -> Brg.term -> kam * Brg.term +val xwhd: Status.status -> rtm -> int option -> Brg.term -> rtm * Brg.term (* arguments: expected type, inferred type *) val are_convertible: - Status.status -> kam -> int option -> Brg.term -> kam -> int option -> Brg.term -> bool + Status.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool -val specs: (Level.status, kam, Brg.term) Log.specs +val specs: (Level.status, rtm, Brg.term) Log.specs diff --git a/helm/software/helena/src/basic_rg/brgType.mli b/helm/software/helena/src/basic_rg/brgType.mli index dd8e9a8f6..f68259a6e 100644 --- a/helm/software/helena/src/basic_rg/brgType.mli +++ b/helm/software/helena/src/basic_rg/brgType.mli @@ -11,4 +11,4 @@ val type_of: (BrgReduction.message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> - Status.status -> BrgReduction.kam -> Brg.term -> 'a + Status.status -> BrgReduction.rtm -> Brg.term -> 'a diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 87a3f60cf..8425774d2 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -27,7 +27,7 @@ let type_check err f st = function let f xt tt = let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e in - BT.type_of err f st BR.empty_kam t + BT.type_of err f st BR.empty_rtm t | ra, na, uri, E.Abbr t -> let err msg = err (L.Uri uri :: msg) in let f xt tt = @@ -37,7 +37,7 @@ let type_check err f st = function in let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e in - BT.type_of err f st BR.empty_kam t + BT.type_of err f st BR.empty_rtm t | _, _, _, E.Void -> assert false let validate err f st e = @@ -48,4 +48,4 @@ let validate err f st e = in let err msg = err (L.Uri uri :: msg) in let f () = let _ = BE.set_entity e in f () in - BV.validate err f st BR.empty_kam t + BV.validate err f st BR.empty_rtm t diff --git a/helm/software/helena/src/basic_rg/brgValidity.mli b/helm/software/helena/src/basic_rg/brgValidity.mli index 8ee88457d..1b552b83c 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.mli +++ b/helm/software/helena/src/basic_rg/brgValidity.mli @@ -11,4 +11,4 @@ val validate: (BrgReduction.message -> 'a) -> (unit -> 'a) -> - Status.status -> BrgReduction.kam -> Brg.term -> 'a + Status.status -> BrgReduction.rtm -> Brg.term -> 'a diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 51d6ddfc1..5fba63786 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -21,7 +21,7 @@ type reductions = { epsilon: int; ldelta : int; gdelta : int; - si : int; + upsilon: int; lrt : int; grt : int; e : int; @@ -30,8 +30,8 @@ type reductions = { let level = 2 let initial_reductions = { - beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; - si = 0; lrt = 0; grt = 0; e = 0; + beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0; + lrt = 0; grt = 0; e = 0; } let reductions = ref initial_reductions @@ -40,7 +40,7 @@ let clear_reductions () = reductions := initial_reductions let add ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) - ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) () + ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) () = reductions := { beta = !reductions.beta + beta; zeta = !reductions.zeta + zeta; @@ -48,7 +48,7 @@ let add epsilon = !reductions.epsilon + epsilon; ldelta = !reductions.ldelta + ldelta; gdelta = !reductions.gdelta + gdelta; - si = !reductions.si + si; + upsilon = !reductions.upsilon + upsilon; lrt = !reductions.lrt + lrt; grt = !reductions.grt + grt; e = !reductions.e + e; @@ -56,8 +56,8 @@ let add let print_reductions () = let r = !reductions in - let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta in - let prs = r.si + r.lrt + r.grt + r.e in + let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta + r.upsilon in + let prs = r.lrt + r.grt + r.e in let delta = r.ldelta + r.gdelta in let rt = r.lrt + r.grt in L.warn level (P.sprintf "Reductions summary"); @@ -69,10 +69,10 @@ let print_reductions () = L.warn level (P.sprintf " Theta: %7u" r.theta); L.warn level (P.sprintf " Zeta for abbreviation: %7u" r.zeta); L.warn level (P.sprintf " Zeta for cast: %7u" r.epsilon); + L.warn level (P.sprintf " Sort inclusion: %7u" r.upsilon); L.warn level (P.sprintf " Pseudo reductions: %7u" prs); L.warn level (P.sprintf " Reference typing: %7u" rt); L.warn level (P.sprintf " Local: %7u" r.lrt); L.warn level (P.sprintf " Global: %7u" r.grt); L.warn level (P.sprintf " Cast typing: %7u" r.e); - L.warn level (P.sprintf " Sort inclusion: %7u" r.si); L.warn level (P.sprintf "Relocated nodes (icm): %7u" !G.icm) diff --git a/helm/software/helena/src/common/output.mli b/helm/software/helena/src/common/output.mli index ba2d294da..3b6ecdab9 100644 --- a/helm/software/helena/src/common/output.mli +++ b/helm/software/helena/src/common/output.mli @@ -13,7 +13,7 @@ val clear_reductions: unit -> unit val add: ?beta:int -> ?theta:int -> ?epsilon:int -> ?ldelta:int -> ?gdelta:int -> - ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> ?e:int -> + ?zeta:int -> ?upsilon:int -> ?lrt:int -> ?grt:int -> ?e:int -> unit -> unit val print_reductions: unit -> unit diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml index 89bf28e86..401faf9af 100644 --- a/helm/software/helena/src/common/status.ml +++ b/helm/software/helena/src/common/status.ml @@ -13,7 +13,6 @@ module G = Options module N = Level type status = { - delta: bool; (* global delta-expansion *) si: bool; (* sort inclusion *) lenv: N.status; (* level environment *) } @@ -21,10 +20,9 @@ type status = { (* helpers ******************************************************************) let initial_status () = { - delta = false; si = !G.si; lenv = N.initial_status (); } let refresh_status st = {st with - si = !G.si; lenv = N.initial_status (); + si = !G.si (*; lenv = N.initial_status (); *) } -- 2.39.2