From: Ferruccio Guidi Date: Sun, 14 Dec 2014 19:17:51 +0000 (+0000) Subject: - we are moving from old (patched) management of sort inclusion X-Git-Tag: make_still_working~783 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbc1c6ccb596693c46f4d75d7875b94c79f1d575;p=helm.git - we are moving from old (patched) management of sort inclusion to new (proper) one via \lambda\delta 3 - some refactoring - omega.out: committed for reference - Makefiles: some bugs fixed --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 0580e6bfc..b6d1f4d83 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -15,13 +15,13 @@ 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/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/layer.cmi : +src/common/layer.cmo : src/common/options.cmx src/common/marks.cmi \ + src/lib/log.cmi src/common/layer.cmi +src/common/layer.cmx : src/common/options.cmx src/common/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 @@ -30,26 +30,24 @@ src/common/output.cmx : src/common/options.cmx src/lib/log.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/complete_rg/crg.cmo : src/common/layer.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/layer.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.cmi : src/common/layer.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/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/common/marks.cmx src/lib/log.cmx \ - src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.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/level.cmi -src/text/txt.cmx : src/common/level.cmx +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/level.cmi src/text/txtParser.cmi + src/common/layer.cmi src/text/txtParser.cmi src/text/txtParser.cmx : src/text/txt.cmx src/common/options.cmx \ - src/common/level.cmx src/text/txtParser.cmi + 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 \ @@ -88,22 +86,22 @@ 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/status.cmx src/complete_rg/crg.cmx \ +src/automath/autCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \ src/automath/aut.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/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/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/level.cmx \ +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/level.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 \ @@ -111,23 +109,23 @@ src/xml/xmlCrg.cmo : src/xml/xmlLibrary.cmi src/common/hierarchy.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/level.cmi src/common/entity.cmx -src/basic_rg/brg.cmx : src/common/level.cmx src/common/entity.cmx +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/level.cmi src/common/entity.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/level.cmx src/common/entity.cmx \ +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/level.cmi src/basic_rg/brg.cmx + 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/level.cmi src/common/hierarchy.cmi \ + 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/basic_rg/brgOutput.cmi 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/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/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi : src/basic_rg/brg.cmx @@ -140,43 +138,41 @@ 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/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/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/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/status.cmx src/common/options.cmx \ - src/lib/log.cmi src/common/entity.cmx src/basic_rg/brgReduction.cmi \ +src/basic_rg/brgValidity.cmo : 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/lib/log.cmx src/common/entity.cmx src/basic_rg/brgReduction.cmx \ +src/basic_rg/brgValidity.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/brgType.cmi : src/common/layer.cmi \ 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/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/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 \ @@ -186,27 +182,27 @@ 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/layer.cmi src/basic_rg/brg.cmx +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/level.cmx \ +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_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/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/layer.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/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/common/marks.cmx src/common/level.cmx \ +src/basic_ag/bagCrg.cmx : src/common/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/level.cmi src/basic_ag/bag.cmx + src/common/layer.cmi src/basic_ag/bag.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 \ @@ -225,29 +221,29 @@ 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/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/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/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/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/bagReduction.cmi : src/common/layer.cmi src/basic_ag/bag.cmx +src/basic_ag/bagReduction.cmo : 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/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/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 @@ -256,8 +252,8 @@ src/basic_ag/bagUntrusted.cmx : src/lib/log.cmx src/common/entity.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/status.cmx \ - src/common/output.cmi src/common/options.cmx src/lib/log.cmi \ + src/text/txt.cmx src/lib/time.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/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ @@ -270,8 +266,8 @@ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ 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/status.cmx \ - src/common/output.cmx src/common/options.cmx src/lib/log.cmx \ + src/text/txt.cmx src/lib/time.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/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 5d359ba39..09dffb04d 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -42,7 +42,7 @@ test-si-matita matita/$(MA): $(MAIN).opt etc profile: $(MAIN).opt etc @echo " HELENA -o -q $(INPUTFAST) (30 TIMES)" - $(H)rm etc/log.txt + $(H)rm -f etc/log.txt $(H)for T in `seq 30`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common index 34c521bb6..babfcf50f 100644 --- a/helm/software/helena/Makefile.common +++ b/helm/software/helena/Makefile.common @@ -91,6 +91,6 @@ etc: @echo " OCAMLOPT $<" $(H)$(OCAMLOPT) -c $< -TAGS += $(MAIN).opt +TAGS += all opt $(MAIN).opt $(foreach TAG, $(TAGS), $(eval $(call INCLUDE_TEMPLATE, $(TAG)))) diff --git a/helm/software/helena/examples/automath/omega.aut b/helm/software/helena/examples/automath/omega.aut new file mode 100644 index 000000000..9e6c30e6f --- /dev/null +++ b/helm/software/helena/examples/automath/omega.aut @@ -0,0 +1,8 @@ +# This book is not valid in AUT-QE because [y:'type'] is not allowed +# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed +# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1 + ++l +@ Delta := [x:[y:'type']'type']x : [x:[y:'type']'type']'type' +@ Omega := Delta : 'type' +-l diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 1c2759d15..c38e8532c 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -13,9 +13,8 @@ module U = NUri module UH = U.UriHash module C = Cps module G = Options -module N = Level +module N = Layer module E = Entity -module S = Status module A = Aut module D = Crg @@ -130,7 +129,7 @@ let rec xlate_term f st lst y lenv = function let l = if !G.cc then match y, at.E.n_degr with | true, _ -> N.one | _ , 0 -> N.one - | _ , 1 -> N.unknown st.S.lenv + | _ , 1 -> N.unknown st | _ , 2 -> N.two | _ -> assert false else N.infinite diff --git a/helm/software/helena/src/automath/autCrg.mli b/helm/software/helena/src/automath/autCrg.mli index 9d58247ea..d4e7cef66 100644 --- a/helm/software/helena/src/automath/autCrg.mli +++ b/helm/software/helena/src/automath/autCrg.mli @@ -16,4 +16,4 @@ val initial_status: unit -> status val refresh_status: status -> status val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> - Status.status -> status -> Aut.command -> 'a + Layer.status -> status -> Aut.command -> 'a diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index de74dcb2b..8d35483ea 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -11,7 +11,7 @@ module C = Cps module J = Marks -module N = Level +module N = Layer module E = Entity module D = Crg module Z = Bag diff --git a/helm/software/helena/src/basic_ag/bagCrg.mli b/helm/software/helena/src/basic_ag/bagCrg.mli index b1ffee4af..a46705f78 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.mli +++ b/helm/software/helena/src/basic_ag/bagCrg.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val bag_of_crg: Level.status -> (Bag.term -> 'a) -> Crg.term -> 'a +val bag_of_crg: Layer.status -> (Bag.term -> 'a) -> Crg.term -> 'a val crg_of_bag: (Crg.term -> 'a) -> Bag.term -> 'a diff --git a/helm/software/helena/src/basic_ag/bagOutput.mli b/helm/software/helena/src/basic_ag/bagOutput.mli index 71c388380..64f6b034f 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.mli +++ b/helm/software/helena/src/basic_ag/bagOutput.mli @@ -17,6 +17,6 @@ val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val specs: (Level.status, Bag.lenv, Bag.term) Log.specs +val specs: (Layer.status, Bag.lenv, Bag.term) Log.specs -val export_term: Level.status -> Bag.term -> XmlLibrary.pp +val export_term: Layer.status -> Bag.term -> XmlLibrary.pp diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index 513c14e59..c9cc85e9b 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -15,7 +15,6 @@ module L = Log module G = Options module J = Marks module E = Entity -module S = Status module Z = Bag module ZO = BagOutput module ZE = BagEnvironment @@ -125,7 +124,7 @@ let rec ho_whd f c m x = whd aux c m x let ho_whd f st c t = - if !G.trace >= level then log1 st.S.lenv "Now scanning" c t; + if !G.trace >= level then log1 st "Now scanning" c t; ho_whd f c empty_machine t let rec are_convertible f st a c m1 t1 m2 t2 = @@ -133,7 +132,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 = let rec aux m1 r1 m2 r2 = (* L.warn "entering R.are_convertible_aux"; *) let u, t = term_of_whdr r1, term_of_whdr r2 in - if !G.trace >= level then log2 st.S.lenv "Now really converting" c u c t; + if !G.trace >= level then log2 st "Now really converting" c u c t; match r1, r2 with | Sort_ h1, Sort_ h2 -> if h1 = h2 then f a else f false @@ -166,7 +165,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 = let f r = if r then push "!" h c m1 a1 l w1 else f false in are_convertible f st a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) - | Sort_ _, Bind_ (a2, l2, w2, t2) when st.S.si -> + | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si -> let m1, m2 = inc m1, inc m2 in let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in push "nsi" f c m2 a2 l2 w2 @@ -190,5 +189,5 @@ and are_convertible_stacks f st a c m1 m2 = C.list_fold_left2 f map a m1.s m2.s let are_convertible f st c u t = - if !G.trace >= level then log2 st.S.lenv "Now converting" c u c t; + if !G.trace >= level then log2 st "Now converting" c u c t; are_convertible f st true c empty_machine u empty_machine t diff --git a/helm/software/helena/src/basic_ag/bagReduction.mli b/helm/software/helena/src/basic_ag/bagReduction.mli index 9a3c849fb..90aa4053b 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.mli +++ b/helm/software/helena/src/basic_ag/bagReduction.mli @@ -14,7 +14,7 @@ type ho_whd_result = | Abst of Bag.term val ho_whd: - (ho_whd_result -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> 'a + (ho_whd_result -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> 'a val are_convertible: - (bool -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a + (bool -> 'a) -> Layer.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.ml b/helm/software/helena/src/basic_ag/bagSubstitution.ml index f8c347892..5585b5d6a 100644 --- a/helm/software/helena/src/basic_ag/bagSubstitution.ml +++ b/helm/software/helena/src/basic_ag/bagSubstitution.ml @@ -9,35 +9,35 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module W = Share +module S = Share module Z = Bag (* Internal functions *******************************************************) let rec lref_map_bind f map b = match b with | Z.Abbr v -> - let f v' = f (W.sh1 v v' b Z.abbr) in + let f v' = f (S.sh1 v v' b Z.abbr) in lref_map f map v | Z.Abst w -> - let f w' = f (W.sh1 w w' b Z.abst) in + let f w' = f (S.sh1 w w' b Z.abst) in lref_map f map w | Z.Void -> f b and lref_map f map t = match t with | Z.LRef i -> - let ii = map i in f (W.sh1 i ii t Z.lref) + let ii = map i in f (S.sh1 i ii t Z.lref) | Z.GRef _ -> f t | Z.Sort _ -> f t | Z.Cast (w, u) -> - let f w' u' = f (W.sh2 w w' u u' t Z.cast) in + let f w' u' = f (S.sh2 w w' u u' t Z.cast) in let f w' = lref_map (f w') map u in lref_map f map w | Z.Appl (w, u) -> - let f w' u' = f (W.sh2 w w' u u' t Z.appl) in + let f w' u' = f (S.sh2 w w' u u' t Z.appl) in let f w' = lref_map (f w') map u in lref_map f map w | Z.Bind (a, l, b, u) -> - let f b' u' = f (W.sh2 b b' u u' t (Z.bind a l)) in + let f b' u' = f (S.sh2 b b' u u' t (Z.bind a l)) in let f b' = lref_map (f b') map u in lref_map_bind f map b diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index 33953d6ad..e76399c5f 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -11,12 +11,11 @@ module U = NUri module C = Cps -module W = Share +module S = Share module L = Log module G = Options module H = Hierarchy module E = Entity -module S = Status module Z = Bag module ZO = BagOutput module ZE = BagEnvironment @@ -46,7 +45,7 @@ let mk_gref u l = let rec b_type_of err f st c x = (* L.warn "Entering T.b_type_of"; *) - if !G.trace >= level then log1 st.S.lenv "Now checking" c x; + if !G.trace >= level then log1 st "Now checking" c x; match x with | Z.Sort h -> let h = H.apply h in f x (Z.Sort h) @@ -69,7 +68,7 @@ let rec b_type_of err f st c x = ZE.get_entity f uri | Z.Bind (a, l, Z.Abbr v, t) -> let f xv xt tt = - f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt) + f (S.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt) in let f xv cc = b_type_of err (f xv) st cc t in let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in @@ -80,24 +79,24 @@ let rec b_type_of err f st c x = type_of err f st c v | Z.Bind (a, l, Z.Abst u, t) -> let f xu xt tt = - f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt) + f (S.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt) in let f xu cc = b_type_of err (f xu) st cc t in let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in type_of err f st c u | Z.Bind (a, l, Z.Void, t) -> let f xt tt = - f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt) + f (S.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt) in let f cc = b_type_of err f st cc t in Z.push "type void" f c a l Z.Void | Z.Appl (v, t) -> let f xv vv xt tt = function | ZR.Abst w -> - if !G.trace > level then L.log st.S.lenv ZO.specs (succ level) (L.t_items1 "Just scanned" c w); + if !G.trace > level then L.log st ZO.specs (succ level) (L.t_items1 "Just scanned" c w); let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt) + if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt) else error3 err c xv vv w in ZR.are_convertible f st c w vv @@ -110,7 +109,7 @@ let rec b_type_of err f st c x = | Z.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu + if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu in let f xu xt tt = ZR.are_convertible (f xu xt tt) st c xu tt in let f xu _ = b_type_of err (f xu) st c t in diff --git a/helm/software/helena/src/basic_ag/bagType.mli b/helm/software/helena/src/basic_ag/bagType.mli index 8f343a624..3af585c3f 100644 --- a/helm/software/helena/src/basic_ag/bagType.mli +++ b/helm/software/helena/src/basic_ag/bagType.mli @@ -12,4 +12,4 @@ val type_of: (Bag.message -> 'a) -> (Bag.term -> Bag.term -> 'a) -> - Status.status -> Bag.lenv -> Bag.term -> 'a + Layer.status -> Bag.lenv -> Bag.term -> 'a diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.mli b/helm/software/helena/src/basic_ag/bagUntrusted.mli index d9ea41897..c9b0b7c4d 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.mli +++ b/helm/software/helena/src/basic_ag/bagUntrusted.mli @@ -11,4 +11,4 @@ val type_check: (Bag.message -> 'a) -> (Bag.term -> Bag.entity -> 'a) -> - Status.status -> Bag.entity -> 'a + Layer.status -> Bag.entity -> 'a diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index cdfa93c6e..9cf2f47d2 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -12,14 +12,14 @@ (* kernel version: basic, relative, global *) (* note : ufficial basic \lambda\delta *) -module N = Level +module N = Layer module E = Entity type uri = E.uri type attrs = E.node_attrs type bind = Void (* *) - | Abst of N.level * term (* level, type *) + | Abst of N.layer * term (* layer, type *) | Abbr of term (* body *) and term = Sort of attrs * int (* attrs, hierarchy index *) diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index cc1223c0a..0fcde12aa 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -10,7 +10,7 @@ V_______________________________________________________________ *) module C = Cps -module N = Level +module N = Layer module E = Entity module D = Crg module B = Brg diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index 53956d932..cb4935f1e 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -15,7 +15,7 @@ module P = Printf module U = NUri module C = Cps module G = Options -module N = Level +module N = Layer module E = Entity module R = Alpha module B = Brg diff --git a/helm/software/helena/src/basic_rg/brgGrafite.mli b/helm/software/helena/src/basic_rg/brgGrafite.mli index 27b927773..5b5fca4c5 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.mli +++ b/helm/software/helena/src/basic_rg/brgGrafite.mli @@ -11,6 +11,6 @@ val open_out: string -> out_channel -val output_entity: Level.status -> out_channel -> Brg.entity -> bool +val output_entity: Layer.status -> out_channel -> Brg.entity -> bool val close_out: out_channel -> unit diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index 5f2866d24..a49177855 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -16,7 +16,7 @@ module C = Cps module L = Log module G = Options module H = Hierarchy -module N = Level +module N = Layer module E = Entity module XD = XmlCrg module B = Brg diff --git a/helm/software/helena/src/basic_rg/brgOutput.mli b/helm/software/helena/src/basic_rg/brgOutput.mli index 2a603669d..155cc8ee4 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.mli +++ b/helm/software/helena/src/basic_rg/brgOutput.mli @@ -17,6 +17,6 @@ val count_entity: (counters -> 'a) -> counters -> Brg.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val specs: (Level.status, Brg.lenv, Brg.term) Log.specs +val specs: (Layer.status, Brg.lenv, Brg.term) Log.specs -val export_term: Level.status -> Brg.term -> XmlLibrary.pp +val export_term: Layer.status -> Brg.term -> XmlLibrary.pp diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 7f7dd4e78..002f12ce1 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -10,14 +10,13 @@ V_______________________________________________________________ *) module U = NUri -module W = Share +module S = Share module L = Log module G = Options module H = Hierarchy -module N = Level +module N = Layer module E = Entity module O = Output -module S = Status module B = Brg module BO = BrgOutput module BE = BrgEnvironment @@ -75,7 +74,7 @@ let are_alpha_convertible err f t1 t2 = | B.Void, B.Void -> f () | _ -> err () in - if W.eq t1 t2 then f () else aux f (t1, t2) + if S.eq t1 t2 then f () else aux f (t1, t2) let assert_tstep m vo = match m.n with | Some n -> n > m.d @@ -93,7 +92,7 @@ let get m i = (* to share *) let rec step st m x = if !G.trace >= sublevel then - log1 st.S.lenv (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x; + log1 st (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x; match x with | B.Sort (a, h) -> if assert_tstep m false then @@ -149,10 +148,10 @@ let rec step st m x = | [] -> let i = tsteps m in if i = 0 then m, x, None else - let n = N.minus st.S.lenv n i in + let n = N.minus st n i in m, B.Bind (a, B.Abst (n, w), t), None | (c, v) :: s -> - if !G.cc && not (N.assert_not_zero st.S.lenv n) then assert false; + if !G.cc && not (N.assert_not_zero st n) then assert false; if !G.summary then O.add ~beta:1 ~theta:(List.length s) (); let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in let e = B.push m.e c a (B.abbr v) in @@ -179,7 +178,7 @@ let push m a b = {m with e = e; l = l} 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; + if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2; match t1, r1, t2, r2 with | B.Sort (_, h1), _, B.Sort (_, h2), _ -> h1 = h2 @@ -209,13 +208,13 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = 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), _ -> - 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 + if !G.cc && not (N.assert_equal st n1 n2) then false else + if ac st (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, _), t), _ -> - if st.S.si then - if !G.cc && not (N.assert_zero st.S.lenv n) then false else begin + 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 (); ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end else false @@ -230,7 +229,7 @@ and ac_stacks st m1 m2 = if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in - ac {st with S.si = false} m1 v1 m2 v2 + ac st m1 v1 m2 v2 in list_and map (m1.s, m2.s) @@ -245,16 +244,16 @@ let get m i = let _, _, _, b = B.get m.e i in b let xwhd st m n t = - if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t; + if !G.trace >= level then log1 st "Now scanning" m.e t; 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; + if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2; 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 () *) + if S.eq mu mw then are_alpha_convertible err f u w else err () *) (* error reporting **********************************************************) diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli index 85df40283..1a2f35007 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.mli +++ b/helm/software/helena/src/basic_rg/brgReduction.mli @@ -19,10 +19,10 @@ val get: rtm -> int -> Brg.bind val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm -val xwhd: Status.status -> rtm -> int option -> Brg.term -> rtm * Brg.term +val xwhd: Layer.status -> rtm -> int option -> Brg.term -> rtm * Brg.term (* arguments: expected type, inferred type *) val are_convertible: - Status.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool + Layer.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool -val specs: (Level.status, rtm, Brg.term) Log.specs +val specs: (Layer.status, rtm, Brg.term) Log.specs diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 85a20cbc0..2dfb2552d 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -11,13 +11,12 @@ module U = NUri module C = Cps -module W = Share +module S = Share module L = Log module G = Options module H = Hierarchy -module N = Level +module N = Layer module E = Entity -module S = Status module B = Brg module BE = BrgEnvironment module BS = BrgSubstitution @@ -66,7 +65,7 @@ let assert_applicability err f st m u w v = | _ -> assert false (**) let rec b_type_of err f st m x = - if !G.trace >= level then log1 st.S.lenv "Now checking" m x; + if !G.trace >= level then log1 st "Now checking" m x; match x with | B.Sort (a, h) -> let h = H.apply h in f x (B.Sort (a, h)) @@ -90,7 +89,7 @@ let rec b_type_of err f st m x = end | B.Bind (a, B.Abbr v, t) -> let f xv xt tt = - f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) + f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in let f xv m = b_type_of err (f xv) st m t in let f xv = f xv (BR.push m a (B.abbr xv)) in @@ -101,27 +100,27 @@ let rec b_type_of err f st m x = type_of err f st m v | B.Bind (a, B.Abst (n, u), t) -> let f xu xt tt = - f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st.S.lenv n 1) a xu tt) + f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st n 1) a xu tt) in let f xu m = b_type_of err (f xu) st m t in let f xu _ = f xu (BR.push m a (B.abst n xu)) in type_of err f st m u | B.Bind (a, B.Void, t) -> let f xt tt = - f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) + f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) in b_type_of err f st (BR.push m a B.Void) t | B.Appl (a, v, t) -> let f xv vv xt tt = - let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in + let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in assert_applicability err f st m tt vv xv in let f xv vv = b_type_of err (f xv vv) st m t in type_of err f st m v | B.Cast (a, u, t) -> let f xu xt tt = - let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in + let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in assert_convertibility err f st m xu tt xt in let f xu _ = b_type_of err (f xu) st m t in diff --git a/helm/software/helena/src/basic_rg/brgType.mli b/helm/software/helena/src/basic_rg/brgType.mli index f68259a6e..2a2442097 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.rtm -> Brg.term -> 'a + Layer.status -> BrgReduction.rtm -> Brg.term -> 'a diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.mli b/helm/software/helena/src/basic_rg/brgUntrusted.mli index a93abd5b6..f3c34ab14 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.mli +++ b/helm/software/helena/src/basic_rg/brgUntrusted.mli @@ -11,8 +11,8 @@ val type_check: (BrgReduction.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> - Status.status -> Brg.entity -> 'a + Layer.status -> Brg.entity -> 'a val validate: (BrgReduction.message -> 'a) -> (unit -> 'a) -> - Status.status -> Brg.entity -> 'a + Layer.status -> Brg.entity -> 'a diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index ea3ce2f42..458962b1f 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -12,7 +12,6 @@ module L = Log module G = Options module E = Entity -module S = Status module B = Brg module BE = BrgEnvironment module BR = BrgReduction @@ -62,7 +61,7 @@ let assert_applicability err f st m v t = | _ -> assert false (**) let rec b_validate err f st m x = - if !G.trace >= level then log1 st.S.lenv "Now checking" m x; + if !G.trace >= level then log1 st "Now checking" m x; match x with | B.Sort _ -> f () | B.LRef (_, i) -> diff --git a/helm/software/helena/src/basic_rg/brgValidity.mli b/helm/software/helena/src/basic_rg/brgValidity.mli index 1b552b83c..fca8589ab 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.rtm -> Brg.term -> 'a + Layer.status -> BrgReduction.rtm -> Brg.term -> 'a diff --git a/helm/software/helena/src/common/Make b/helm/software/helena/src/common/Make index 5ccf50d11..c019e1d23 100644 --- a/helm/software/helena/src/common/Make +++ b/helm/software/helena/src/common/Make @@ -1 +1 @@ -options marks hierarchy level entity output alpha status +options marks hierarchy layer entity output alpha diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml index d4bfef5d3..c53db162b 100644 --- a/helm/software/helena/src/common/entity.ml +++ b/helm/software/helena/src/common/entity.ml @@ -10,7 +10,7 @@ V_______________________________________________________________ *) module U = NUri -module N = Level +module N = Layer type uri = U.uri diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml new file mode 100644 index 000000000..61254620f --- /dev/null +++ b/helm/software/helena/src/common/layer.ml @@ -0,0 +1,187 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module H = Hashtbl + +module L = Log +module G = Options +module J = Marks + +type value = Inf (* infinite layer *) + | Fin of int (* finite layer *) + | Ref of J.mark * int (* referred layer, step *) + | Unk (* no layer set *) + +type layer = { + mutable v: value; (* value *) + s: bool; (* static layer? *) + mutable b: bool; (* beta allowed? *) +} + +type status = (J.mark, layer) H.t (* environment for layer variables *) + +(* Internal functions *******************************************************) + +let level = 6 + +let env_size = 1300 + +let zero = Fin 0 + +let warn s = L.warn level s + +let string_of_value k = function + | Inf -> "" + | Fin i -> string_of_int i + | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i + | Unk -> "-" ^ J.string_of_mark k + +let pp_table st = + let map k n = + warn (Printf.sprintf "%s: v %s (s:%b b:%b)" + (J.string_of_mark k) (string_of_value k n.v) n.s n.b + ) + in + H.iter map st + +let cell s v = { + v = v; s = s; b = false +} + +let empty () = cell true Unk + +let dynamic k i = cell false (Ref (k, i)) + +let find_with_default st default k = + try H.find st k with Not_found -> H.add st k default; default + +let find st k = + try H.find st k with Not_found -> assert false + +let rec resolve_key_with_default st default k = match find_with_default st default k with + | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k + | cell -> k, cell + +let rec resolve_key st k = match find st k with + | {v = Ref (k, i)} when i = 0 -> resolve_key st k + | cell -> k, cell + +let resolve_layer st = function + | {v = Ref (k, i)} when i = 0 -> resolve_key st k + | cell -> J.null_mark, cell + +let rec generated st h i = + let default = dynamic h i in + let k = J.new_mark () in + match resolve_key_with_default st default k with + | k, n when n = default -> if !G.trace >= level then pp_table st; n + | _, n when n.s = true -> generated st h i + | _ -> assert false + +let assert_finite st n j = + if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j); + 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" (J.string_of_mark k) i j; true (**) + | Inf -> + Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**) + | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true + | Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j) + in + let k, n = resolve_layer st n in +(* if j = 0 && n.b then begin + Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**) + end else *) + aux (k, n) j + +let assert_infinite st n = + if !G.trace >= level then warn "ASSERT INFINITE"; + let rec aux (k, n) = match n.v with + | Inf -> true + | Fin i -> + Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**) + | Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true + | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) + in + aux (resolve_layer st n) + +(* Interface functions ******************************************************) + +let initial_status () = + H.create env_size + +let refresh_status st = st + +let infinite = cell true Inf + +let finite i = cell true (Fin i) + +let one = finite 1 + +let two = finite 2 + +let rec unknown st = + if !G.trace >= level then warn "UNKNOWN"; + let default = empty () in + let k = J.new_mark () in + match resolve_key_with_default st default k with + | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0)) + | _, n when n.s = true -> n + | _ -> unknown st + +let minus st n j = + if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j); + 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)) + | Fin _ -> cell false zero + | Unk -> + if k = J.null_mark then assert false else generated st k j + | Ref (k, i) -> + let k, n = resolve_key st k in + aux k n (i+j) + in + let k, n = resolve_layer st n in + aux k n j + +let to_string st n = + let k, n = resolve_layer st n in + string_of_value k n.v + +let assert_not_zero st n = + if !G.trace >= level then warn "ASSERT NOT ZERO"; + let k, n = resolve_layer st n in + match n.b, n.v with + | true, _ -> n.b +(* | _ , Fin i when i = 0 -> + Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**) +(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *) + | _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b + +let assert_zero st n = assert_finite st n 0 + +let assert_equal st n1 n2 = + let k1, n1 = resolve_layer st n1 in + let k2, n2 = resolve_layer st n2 in + if n1 = n2 then true else + let b = + if not n1.b || assert_not_zero st n2 then match n1.v with + | Inf -> assert_infinite st n2 + | Fin i -> assert_finite st n2 i + | Unk -> true + | Ref _ -> assert false + else false + in begin + if !G.trace >= level then warn "ASSERT EQUAL"; + if b && k1 <> J.null_mark && k2 <> J.null_mark then begin + n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st + end; b end diff --git a/helm/software/helena/src/common/layer.mli b/helm/software/helena/src/common/layer.mli new file mode 100644 index 000000000..9d8b34e72 --- /dev/null +++ b/helm/software/helena/src/common/layer.mli @@ -0,0 +1,38 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +type status + +type layer + +val initial_status: unit -> status + +val refresh_status: status -> status + +val infinite: layer + +val finite: int -> layer + +val one: layer + +val two: layer + +val unknown: status -> layer + +val minus: status -> layer -> int -> layer + +val to_string: status -> layer -> string + +val assert_not_zero: status -> layer -> bool + +val assert_zero: status -> layer -> bool + +val assert_equal: status -> layer -> layer -> bool diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml deleted file mode 100644 index 5f5251f6c..000000000 --- a/helm/software/helena/src/common/level.ml +++ /dev/null @@ -1,185 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module H = Hashtbl - -module L = Log -module G = Options -module J = Marks - -type value = Inf (* infinite level *) - | Fin of int (* finite level *) - | Ref of J.mark * int (* referred level, step *) - | Unk (* no level set *) - -type level = { - mutable v: value; (* value *) - s: bool; (* static level? *) - mutable b: bool; (* beta allowed? *) -} - -type status = (J.mark, level) H.t (* environment for level variables *) - -(* Internal functions *******************************************************) - -let level = 6 - -let env_size = 1300 - -let zero = Fin 0 - -let warn s = L.warn level s - -let string_of_value k = function - | Inf -> "" - | Fin i -> string_of_int i - | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i - | Unk -> "-" ^ J.string_of_mark k - -let pp_table st = - let map k n = - warn (Printf.sprintf "%s: v %s (s:%b b:%b)" - (J.string_of_mark k) (string_of_value k n.v) n.s n.b - ) - in - H.iter map st - -let cell s v = { - v = v; s = s; b = false -} - -let empty () = cell true Unk - -let dynamic k i = cell false (Ref (k, i)) - -let find_with_default st default k = - try H.find st k with Not_found -> H.add st k default; default - -let find st k = - try H.find st k with Not_found -> assert false - -let rec resolve_key_with_default st default k = match find_with_default st default k with - | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k - | cell -> k, cell - -let rec resolve_key st k = match find st k with - | {v = Ref (k, i)} when i = 0 -> resolve_key st k - | cell -> k, cell - -let resolve_level st = function - | {v = Ref (k, i)} when i = 0 -> resolve_key st k - | cell -> J.null_mark, cell - -let rec generated st h i = - let default = dynamic h i in - let k = J.new_mark () in - match resolve_key_with_default st default k with - | k, n when n = default -> if !G.trace >= level then pp_table st; n - | _, n when n.s = true -> generated st h i - | _ -> assert false - -let assert_finite st n j = - if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j); - 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" (J.string_of_mark k) i j; true (**) - | Inf -> - Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**) - | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true - | Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j) - in - let k, n = resolve_level st n in -(* if j = 0 && n.b then begin - Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**) - end else *) - aux (k, n) j - -let assert_infinite st n = - if !G.trace >= level then warn "ASSERT INFINITE"; - let rec aux (k, n) = match n.v with - | Inf -> true - | Fin i -> - Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**) - | Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true - | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) - in - aux (resolve_level st n) - -(* Interface functions ******************************************************) - -let initial_status () = - H.create env_size - -let infinite = cell true Inf - -let finite i = cell true (Fin i) - -let one = finite 1 - -let two = finite 2 - -let rec unknown st = - if !G.trace >= level then warn "UNKNOWN"; - let default = empty () in - let k = J.new_mark () in - match resolve_key_with_default st default k with - | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0)) - | _, n when n.s = true -> n - | _ -> unknown st - -let minus st n j = - if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j); - 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)) - | Fin _ -> cell false zero - | Unk -> - if k = J.null_mark then assert false else generated st k j - | Ref (k, i) -> - let k, n = resolve_key st k in - aux k n (i+j) - in - let k, n = resolve_level st n in - aux k n j - -let to_string st n = - let k, n = resolve_level st n in - string_of_value k n.v - -let assert_not_zero st n = - if !G.trace >= level then warn "ASSERT NOT ZERO"; - let k, n = resolve_level st n in - match n.b, n.v with - | true, _ -> n.b -(* | _ , Fin i when i = 0 -> - Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**) -(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *) - | _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b - -let assert_zero st n = assert_finite st n 0 - -let assert_equal st n1 n2 = - let k1, n1 = resolve_level st n1 in - let k2, n2 = resolve_level st n2 in - if n1 = n2 then true else - let b = - if not n1.b || assert_not_zero st n2 then match n1.v with - | Inf -> assert_infinite st n2 - | Fin i -> assert_finite st n2 i - | Unk -> true - | Ref _ -> assert false - else false - in begin - if !G.trace >= level then warn "ASSERT EQUAL"; - if b && k1 <> J.null_mark && k2 <> J.null_mark then begin - n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st - end; b end diff --git a/helm/software/helena/src/common/level.mli b/helm/software/helena/src/common/level.mli deleted file mode 100644 index fe12b3671..000000000 --- a/helm/software/helena/src/common/level.mli +++ /dev/null @@ -1,36 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -type status - -type level - -val initial_status: unit -> status - -val infinite: level - -val finite: int -> level - -val one: level - -val two: level - -val unknown: status -> level - -val minus: status -> level -> int -> level - -val to_string: status -> level -> string - -val assert_not_zero: status -> level -> bool - -val assert_zero: status -> level -> bool - -val assert_equal: status -> level -> level -> bool diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml deleted file mode 100644 index 401faf9af..000000000 --- a/helm/software/helena/src/common/status.ml +++ /dev/null @@ -1,28 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module G = Options -module N = Level - -type status = { - si: bool; (* sort inclusion *) - lenv: N.status; (* level environment *) -} - -(* helpers ******************************************************************) - -let initial_status () = { - si = !G.si; lenv = N.initial_status (); -} - -let refresh_status st = {st with - si = !G.si (*; lenv = N.initial_status (); *) -} diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 87fbaf3e2..673b3a0ba 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -13,14 +13,14 @@ (* note : fragment of complete \lambda\delta serving as abstract layer *) module C = Cps -module N = Level +module N = Layer module E = Entity type uri = E.uri type id = E.id type attrs = E.node_attrs -type bind = Abst of N.level * term (* level, type *) +type bind = Abst of N.layer * term (* layer, type *) | Abbr of term (* body *) | Void (* *) diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index dfef1f250..6ccf47af0 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -15,7 +15,7 @@ module U = NUri module C = Cps module L = Log module J = Marks -module N = Level +module N = Layer module E = Entity module D = Crg diff --git a/helm/software/helena/src/complete_rg/crgOutput.mli b/helm/software/helena/src/complete_rg/crgOutput.mli index b0a4c718c..a3f636381 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.mli +++ b/helm/software/helena/src/complete_rg/crgOutput.mli @@ -17,4 +17,4 @@ val count_entity: (counters -> 'a) -> counters -> Crg.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val pp_term: (string -> unit) -> Level.status -> Crg.term -> unit +val pp_term: (string -> unit) -> Layer.status -> Crg.term -> unit diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 07709401c..834a9a19f 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -1,21 +1,20 @@ -(* free = F I K M P Q U V *) +(* free = F I K M P Q U V W *) module U = NUri module UH = NUri.UriHash module C = Cps -module W = Share (**) +module S = Share module L = Log module Y = Time (**) module G = Options module J = Marks (**) module H = Hierarchy -module N = Level +module N = Layer module E = Entity module O = Output module R = Alpha -module S = Status module D = Crg module DO = CrgOutput diff --git a/helm/software/helena/src/text/txt.ml b/helm/software/helena/src/text/txt.ml index bdd96bf6b..0633d39a9 100644 --- a/helm/software/helena/src/text/txt.ml +++ b/helm/software/helena/src/text/txt.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module N = Level +module N = Layer type ix = int (* index *) @@ -45,11 +45,11 @@ and term = (* arguments, function *) | Appl of term list * term (* level, binder, scope *) - | Bind of N.level * bind * term + | Bind of N.layer * bind * term (* function, arguments *) | Inst of term * term list (* level, strong?, label, source, target *) - | Impl of N.level * bool * id * term * term + | Impl of N.layer * bool * id * term * term type command = (* required files: names *) @@ -61,6 +61,6 @@ type command = (* section: Some id = open, None = close last *) | Section of id option (* entity: main?, class, name, info, contents *) - | Entity of bool * kind * N.level * id * info * term + | Entity of bool * kind * N.layer * id * info * term (* predefined generated entity: arguments *) | Generate of term list diff --git a/helm/software/helena/src/text/txtParser.mly b/helm/software/helena/src/text/txtParser.mly index 2c9abe079..d9336b189 100644 --- a/helm/software/helena/src/text/txtParser.mly +++ b/helm/software/helena/src/text/txtParser.mly @@ -25,7 +25,7 @@ %{ module G = Options - module N = Level + module N = Layer module T = Txt let _ = Parsing.set_trace !G.debug_parser diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 535450c1f..bded35b3b 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -18,9 +18,9 @@ module L = Log module Y = Time module G = Options module H = Hierarchy +module N = Layer module E = Entity module O = Output -module S = Status module DO = CrgOutput module TD = TxtCrg module AA = AutProcess @@ -39,7 +39,7 @@ module ZT = BagType module ZU = BagUntrusted type status = { - kst: S.status; + kst: N.status; tst: TD.status; pst: AA.status; ast: AD.status; @@ -53,13 +53,13 @@ type status = { let level = 0 let bag_error st s msg = - L.error st.kst.S.lenv ZO.specs (L.Warn s :: msg) + L.error st.kst ZO.specs (L.Warn s :: msg) let brg_error st s msg = - L.error st.kst.S.lenv BR.specs (L.Warn s :: msg) + L.error st.kst BR.specs (L.Warn s :: msg) let initial_status () = { - kst = S.initial_status (); + kst = N.initial_status (); tst = TD.initial_status (); pst = AA.initial_status (); ast = AD.initial_status (); @@ -71,7 +71,7 @@ let initial_status () = { } let refresh_status st = {st with - kst = S.refresh_status st.kst; + kst = N.refresh_status st.kst; tst = TD.refresh_status st.tst; ast = AD.refresh_status st.ast; } @@ -91,7 +91,7 @@ let xlate_entity st entity = match !G.kernel, entity with | G.Brg, CrgEntity e -> let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e | G.Bag, CrgEntity e -> - let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst.S.lenv) e + let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e | _, entity -> entity let pp_progress e = @@ -110,9 +110,9 @@ let count_entity st = function | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e} let export_entity st = function - | CrgEntity e -> XL.export_entity (XD.export_term st.kst.S.lenv) e - | BrgEntity e -> XL.export_entity (BO.export_term st.kst.S.lenv) e - | BagEntity e -> XL.export_entity (ZO.export_term st.kst.S.lenv) e + | 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 let type_check st k = let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in @@ -132,7 +132,7 @@ let validate st k = begin match st.och with | None -> st | Some och -> - if BG.output_entity st.kst.S.lenv och entity then st + if BG.output_entity st.kst och entity then st else begin L.warn level "Matita exportation stopped"; {st with och = None} end end | BagEntity _ -> st diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index 311a0b4a1..535682143 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -81,7 +81,7 @@ and exp_appl st e a v out tab = and exp_bind st e a b out tab = match b with | D.Abst (n, w) -> - let attrs = [XL.level st n; XL.name a; XL.kind a] in + let attrs = [XL.layer st n; XL.name a; XL.kind a] in XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab | D.Abbr v -> let attrs = [XL.name a] in diff --git a/helm/software/helena/src/xml/xmlCrg.mli b/helm/software/helena/src/xml/xmlCrg.mli index f1f5e131d..63a9f6800 100644 --- a/helm/software/helena/src/xml/xmlCrg.mli +++ b/helm/software/helena/src/xml/xmlCrg.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val export_term: Level.status -> Crg.term -> XmlLibrary.pp +val export_term: Layer.status -> Crg.term -> XmlLibrary.pp diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 4caa7c1c2..77fb9351a 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -15,7 +15,7 @@ module U = NUri module C = Cps module G = Options module H = Hierarchy -module N = Level +module N = Layer module E = Entity (* internal functions *******************************************************) @@ -99,8 +99,8 @@ let name a = let apix a = "position", string_of_int a.E.n_apix -let level st n = - "level", N.to_string st n +let layer st n = + "layer", N.to_string st n let kind a = "position", string_of_int a.E.n_sort diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 1ac861aee..ed7901f57 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -41,7 +41,7 @@ val position: int -> attr val uri: Entity.uri -> attr -val level: Level.status -> Level.level -> attr +val layer: Layer.status -> Layer.layer -> attr val name: Entity.node_attrs -> attr