From d145ea48ed0bdb9642ced01283231f3f13d476b8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 1 Nov 2010 15:18:57 +0000 Subject: [PATCH] - some bugfix - some - old intermediate language (meta) has been removed --- helm/software/lambda-delta/.depend.opt | 200 +++++++--------- helm/software/lambda-delta/Makefile | 40 +--- helm/software/lambda-delta/src/Make | 2 +- helm/software/lambda-delta/src/automath/Make | 2 +- .../crgAut.ml => automath/autCrg.ml} | 0 .../crgAut.mli => automath/autCrg.mli} | 0 .../lambda-delta/src/basic_ag/bagCrg.ml | 102 ++++++++ .../metaBag.mli => basic_ag/bagCrg.mli} | 5 +- .../lambda-delta/src/basic_rg/brgReduction.ml | 7 +- .../lambda-delta/src/complete_rg/Make | 2 +- helm/software/lambda-delta/src/modules.ml | 33 ++- helm/software/lambda-delta/src/text/Make | 2 +- .../{complete_rg/crgTxt.ml => text/txtCrg.ml} | 0 .../crgTxt.mli => text/txtCrg.mli} | 0 helm/software/lambda-delta/src/toplevel/Make | 2 +- .../lambda-delta/src/toplevel/meta.ml | 27 --- .../lambda-delta/src/toplevel/metaAut.ml | 219 ------------------ .../lambda-delta/src/toplevel/metaAut.mli | 20 -- .../lambda-delta/src/toplevel/metaBag.ml | 67 ------ .../lambda-delta/src/toplevel/metaBrg.ml | 67 ------ .../lambda-delta/src/toplevel/metaBrg.mli | 12 - .../lambda-delta/src/toplevel/metaOutput.ml | 108 --------- .../lambda-delta/src/toplevel/metaOutput.mli | 18 -- .../software/lambda-delta/src/toplevel/top.ml | 84 +++---- 24 files changed, 253 insertions(+), 766 deletions(-) rename helm/software/lambda-delta/src/{complete_rg/crgAut.ml => automath/autCrg.ml} (100%) rename helm/software/lambda-delta/src/{complete_rg/crgAut.mli => automath/autCrg.mli} (100%) create mode 100644 helm/software/lambda-delta/src/basic_ag/bagCrg.ml rename helm/software/lambda-delta/src/{toplevel/metaBag.mli => basic_ag/bagCrg.mli} (86%) rename helm/software/lambda-delta/src/{complete_rg/crgTxt.ml => text/txtCrg.ml} (100%) rename helm/software/lambda-delta/src/{complete_rg/crgTxt.mli => text/txtCrg.mli} (100%) delete mode 100644 helm/software/lambda-delta/src/toplevel/meta.ml delete mode 100644 helm/software/lambda-delta/src/toplevel/metaAut.ml delete mode 100644 helm/software/lambda-delta/src/toplevel/metaAut.mli delete mode 100644 helm/software/lambda-delta/src/toplevel/metaBag.ml delete mode 100644 helm/software/lambda-delta/src/toplevel/metaBrg.ml delete mode 100644 helm/software/lambda-delta/src/toplevel/metaBrg.mli delete mode 100644 helm/software/lambda-delta/src/toplevel/metaOutput.ml delete mode 100644 helm/software/lambda-delta/src/toplevel/metaOutput.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index f5f9bcdcf..97e811578 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -34,6 +34,15 @@ src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \ src/lib/cps.cmx src/common/ccs.cmi src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx +src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx +src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx +src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx +src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \ + src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \ + src/common/hierarchy.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 @@ -48,6 +57,13 @@ src/text/txtLexer.cmx: src/text/txtParser.cmx src/common/options.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/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 @@ -69,75 +85,13 @@ src/automath/autLexer.cmo: src/common/options.cmx src/lib/log.cmi \ src/automath/autParser.cmi src/automath/autLexer.cmx: src/common/options.cmx src/lib/log.cmx \ src/automath/autParser.cmx -src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx -src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagOutput.cmi -src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagOutput.cmi -src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx -src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx -src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagSubstitution.cmi -src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagSubstitution.cmi -src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx -src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \ - src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \ - src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi -src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \ - src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi -src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx -src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \ - src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \ - src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \ - src/basic_ag/bagType.cmi -src/basic_ag/bagType.cmx: src/common/status.cmx src/lib/share.cmx \ - src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \ - src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagType.cmi -src/basic_ag/bagUntrusted.cmi: src/common/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/bagType.cmx src/basic_ag/bagEnvironment.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi -src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx -src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx -src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/complete_rg/crgOutput.cmi -src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/complete_rg/crgOutput.cmi -src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx -src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \ - src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi -src/complete_rg/crgTxt.cmx: src/text/txtTxt.cmx src/text/txt.cmx \ - src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi -src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx -src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/level.cmi \ +src/automath/autCrg.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx +src/automath/autCrg.cmo: 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/complete_rg/crgAut.cmi -src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/level.cmx \ + src/automath/aut.cmx src/automath/autCrg.cmi +src/automath/autCrg.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/complete_rg/crgAut.cmi + src/automath/aut.cmx src/automath/autCrg.cmi src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx \ src/common/ccs.cmi src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \ @@ -216,59 +170,75 @@ src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ src/basic_rg/brgType.cmx src/basic_rg/brgReduction.cmx \ src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgUntrusted.cmi -src/toplevel/meta.cmo: src/common/entity.cmx -src/toplevel/meta.cmx: src/common/entity.cmx -src/toplevel/metaOutput.cmi: src/toplevel/meta.cmx -src/toplevel/metaOutput.cmo: src/toplevel/meta.cmx src/lib/log.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi -src/toplevel/metaOutput.cmx: src/toplevel/meta.cmx src/lib/log.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi -src/toplevel/metaAut.cmi: src/toplevel/meta.cmx src/automath/aut.cmx -src/toplevel/metaAut.cmo: src/common/options.cmx src/toplevel/meta.cmx \ - src/common/level.cmi src/common/entity.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/toplevel/metaAut.cmi -src/toplevel/metaAut.cmx: src/common/options.cmx src/toplevel/meta.cmx \ - src/common/level.cmx src/common/entity.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/toplevel/metaAut.cmi -src/toplevel/metaBag.cmi: src/toplevel/meta.cmx src/basic_ag/bag.cmx -src/toplevel/metaBag.cmo: src/toplevel/meta.cmx src/lib/cps.cmx \ - src/basic_ag/bag.cmx src/toplevel/metaBag.cmi -src/toplevel/metaBag.cmx: src/toplevel/meta.cmx src/lib/cps.cmx \ - src/basic_ag/bag.cmx src/toplevel/metaBag.cmi -src/toplevel/metaBrg.cmi: src/toplevel/meta.cmx src/basic_rg/brg.cmx -src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/level.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/toplevel/metaBrg.cmi -src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/level.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/toplevel/metaBrg.cmi +src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx +src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx +src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx +src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \ + src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagOutput.cmi +src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \ + src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagOutput.cmi +src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx +src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi +src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi +src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx +src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagSubstitution.cmi +src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagSubstitution.cmi +src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx +src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \ + src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \ + src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \ + src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi +src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \ + src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi +src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx +src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \ + src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \ + src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \ + src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \ + src/basic_ag/bagType.cmi +src/basic_ag/bagType.cmx: src/common/status.cmx src/lib/share.cmx \ + src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \ + src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagType.cmi +src/basic_ag/bagUntrusted.cmi: src/common/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/bagType.cmx src/basic_ag/bagEnvironment.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ - src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \ - src/lib/time.cmx src/common/status.cmx src/common/output.cmi \ - src/common/options.cmx src/toplevel/metaOutput.cmi \ - src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \ - src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \ - src/complete_rg/crgOutput.cmi src/complete_rg/crgAut.cmi \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brgOutput.cmi \ - src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ + 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/common/hierarchy.cmi src/common/entity.cmx \ + src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ + src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \ src/automath/autProcess.cmi src/automath/autParser.cmi \ - src/automath/autOutput.cmi src/automath/autLexer.cmx src/automath/aut.cmx + src/automath/autOutput.cmi src/automath/autLexer.cmx \ + src/automath/autCrg.cmi src/automath/aut.cmx src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ - src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txt.cmx \ - src/lib/time.cmx src/common/status.cmx src/common/output.cmx \ - src/common/options.cmx src/toplevel/metaOutput.cmx \ - src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \ - src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \ - src/complete_rg/crgOutput.cmx src/complete_rg/crgAut.cmx \ - src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmx \ - src/basic_rg/brgReduction.cmx src/basic_rg/brgOutput.cmx \ - src/basic_rg/brgCrg.cmx src/basic_rg/brg.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/common/hierarchy.cmx src/common/entity.cmx \ + src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ + src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \ src/automath/autProcess.cmx src/automath/autParser.cmx \ - src/automath/autOutput.cmx src/automath/autLexer.cmx src/automath/aut.cmx + src/automath/autOutput.cmx src/automath/autLexer.cmx \ + src/automath/autCrg.cmx src/automath/aut.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 03f1f1704..9d55e6292 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -10,7 +10,7 @@ KEEP = README CLEAN = etc/log.txt etc/profile.txt -TAGS = test-si test-si-fast hal xml-si-crg xml-si profile +TAGS = test-si test-si-fast xml-si-crg xml-si profile XMLLINTLOCAL = --nonet --path xml --dtdvalid ld.dtd @@ -30,26 +30,26 @@ include Makefile.common INPUT = examples/grundlagen/grundlagen.aut test-si: $(MAIN).opt etc - @echo " HELENA -p -u -c $(INPUT)" - $(H)./$(MAIN).opt -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -p -o -c $(INPUT)" + $(H)./$(MAIN).opt -p -o -c -S 3 $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt etc - @echo " HELENA -u -q $(INPUT)" - $(H)./$(MAIN).opt -u -q -S 1 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -o -q $(INPUT)" + $(H)./$(MAIN).opt -o -q -S 1 $(O) $(INPUT) > etc/log.txt profile: $(MAIN).opt etc - @echo " HELENA -u -q $(INPUT) (30 TIMES)" + @echo " HELENA -o -q $(INPUT) (30 TIMES)" $(H)rm etc/log.txt - $(H)for T in `seq 30`; do ./$(MAIN).opt -u -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done + $(H)for T in `seq 30`; do ./$(MAIN).opt -o -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt xml-si: $(MAIN).opt etc - @echo " HELENA -u -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt + @echo " HELENA -o -x -s 2 $(INPUT)" + $(H)./$(MAIN).opt -o -x -s 2 -S 1 $(INPUT) > etc/log.txt xml-si-crg: $(MAIN).opt etc - @echo " HELENA -u -x -s 1 $(INPUT)" - $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt + @echo " HELENA -o -x -s 1 $(INPUT)" + $(H)./$(MAIN).opt -o -x -s 1 -S 1 $(INPUT) > etc/log.txt etc: @echo " MKDIR etc" @@ -89,21 +89,3 @@ install-dtd: xml/ld.dtd install-xml: etc/make-html.sh @echo " INSTALL xml" $(H)scp -r xml/index.txt xml/ld.dtd xml/brg-si/ xml/crg-si/ $(XMLDIR) - -# old targets ########################################################## - -test: $(MAIN).opt etc - @echo " HELENA -o -p $(INPUT)" - $(H)./$(MAIN).opt -o -p -S 3 $(O) $(INPUT) > etc/log.txt - -test-si-old: $(MAIN).opt etc - @echo " HELENA -o -p -u -c $(INPUT)" - $(H)./$(MAIN).opt -o -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt - -test-si-fast-old: $(MAIN).opt etc - @echo " HELENA -o -u -q $(INPUT)" - $(H)./$(MAIN).opt -o -u -q -S 1 $(O) $(INPUT) > etc/log.txt - -xml-si-old: $(MAIN).opt etc - @echo " HELENA -o -u -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt diff --git a/helm/software/lambda-delta/src/Make b/helm/software/lambda-delta/src/Make index abc5de2e1..9e637c2c0 100644 --- a/helm/software/lambda-delta/src/Make +++ b/helm/software/lambda-delta/src/Make @@ -1 +1 @@ -lib common text automath basic_ag complete_rg xml basic_rg toplevel +lib common complete_rg text automath xml basic_rg basic_ag toplevel diff --git a/helm/software/lambda-delta/src/automath/Make b/helm/software/lambda-delta/src/automath/Make index 29d237864..094f99eb4 100644 --- a/helm/software/lambda-delta/src/automath/Make +++ b/helm/software/lambda-delta/src/automath/Make @@ -1 +1 @@ -aut autProcess autOutput autParser autLexer +aut autProcess autOutput autParser autLexer autCrg diff --git a/helm/software/lambda-delta/src/complete_rg/crgAut.ml b/helm/software/lambda-delta/src/automath/autCrg.ml similarity index 100% rename from helm/software/lambda-delta/src/complete_rg/crgAut.ml rename to helm/software/lambda-delta/src/automath/autCrg.ml diff --git a/helm/software/lambda-delta/src/complete_rg/crgAut.mli b/helm/software/lambda-delta/src/automath/autCrg.mli similarity index 100% rename from helm/software/lambda-delta/src/complete_rg/crgAut.mli rename to helm/software/lambda-delta/src/automath/autCrg.mli diff --git a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml new file mode 100644 index 000000000..d4366b60b --- /dev/null +++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml @@ -0,0 +1,102 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module C = Cps +module E = Entity +module J = Marks +module N = Level +module D = Crg +module Z = Bag + +(* internal functions: crg to bag term **************************************) + +let rec lenv_fold_left map1 map2 x = function + | D.ESort -> x + | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl + | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl + +let rec xlate_term f = function + | D.TSort (a, l) -> f (Z.Sort (a, l)) + | D.TGRef (a, n) -> f (Z.GRef (a, n)) + | D.TLRef (a, _, _) -> let f i = f (Z.LRef (a, i)) in E.apix C.err f a + | D.TCast (a, u, t) -> + let f uu tt = f (Z.Cast (a, uu, tt)) in + let f uu = xlate_term (f uu) t in + xlate_term f u + | D.TAppl (a, vs, t) -> + let map f v tt = let f vv = f (Z.Appl (a, vv, tt)) in xlate_term f v in + let f tt = C.list_fold_right f map vs tt in + xlate_term f t + | D.TProj (a, e, t) -> + let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in + xlate_term f t + | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) -> + xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t))) + | D.TBind (a, b, t) -> + let f tt = f (xlate_bind tt a b) in xlate_term f t + +and xlate_bind x a b = + let f a ns = a, ns in + let a, ns = E.get_names f a in + match b with + | D.Abst (m, ws) -> + let map x n w = + let f ww = Z.Bind (n :: J.new_mark () :: a, Z.Abst (m, ww), x) in + xlate_term f w + in + List.fold_left2 map x ns ws + | D.Abbr vs -> + let map x n v = + let f vv = Z.Bind (n :: a, Z.Abbr vv, x) in + xlate_term f v + in + List.fold_left2 map x ns vs + | D.Void _ -> + let map x n = Z.Bind (n :: a, Z.Void, x) in + List.fold_left map x ns + +and xlate_proj x _ e = + lenv_fold_left xlate_bind xlate_proj x e + +(* internal functions: bag to crg term **************************************) + +let rec xlate_bk_term f = function + | Z.Sort (a, l) -> f (D.TSort (a, l)) + | Z.GRef (a, n) -> f (D.TGRef (a, n)) + | Z.LRef (a, i) -> f (D.TLRef (a, i, 0)) + | Z.Cast (a, u, t) -> + let f uu tt = f (D.TCast (a, uu, tt)) in + let f uu = xlate_bk_term (f uu) t in + xlate_bk_term f u + | Z.Appl (a, u, t) -> + let f uu tt = f (D.TAppl (a, [uu], tt)) in + let f uu = xlate_bk_term (f uu) t in + xlate_bk_term f u + | Z.Bind (a, b, t) -> + let f bb tt = f (D.TBind (a, bb, tt)) in + let f bb = xlate_bk_term (f bb) t in + xlate_bk_bind f b + +and xlate_bk_bind f = function + | Z.Abst (n, t) -> + let f tt = f (D.Abst (n, [tt])) in + xlate_bk_term f t + | Z.Abbr t -> + let f tt = f (D.Abbr [tt]) in + xlate_bk_term f t + | Z.Void -> f (D.Void 1) + +(* interface functions ******************************************************) + +let bag_of_crg f t = + f (xlate_term C.start t) + +let crg_of_bag = xlate_bk_term diff --git a/helm/software/lambda-delta/src/toplevel/metaBag.mli b/helm/software/lambda-delta/src/basic_ag/bagCrg.mli similarity index 86% rename from helm/software/lambda-delta/src/toplevel/metaBag.mli rename to helm/software/lambda-delta/src/basic_ag/bagCrg.mli index 62ce68f4e..aae9eb280 100644 --- a/helm/software/lambda-delta/src/toplevel/metaBag.mli +++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.mli @@ -9,4 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val bag_of_meta: (Bag.term -> 'a) -> Meta.entry -> 'a +val bag_of_crg: (Bag.term -> 'a) -> Crg.term -> 'a +(* +val crg_of_bag: (Crg.term -> 'a) -> Bag.term -> 'a +*) diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index 79ffcb32f..5f73a4fc0 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -159,12 +159,13 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) = O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, r2, t) | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), - _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) -> - if n1 = n2 && ac {st with S.si = false} m1 w1 m2 w2 then + _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) + when n1 = n2 || st.S.si -> + if ac {st with S.si = false} m1 w1 m2 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) - when N.is_zero n && st.S.si -> + when N.is_zero n || st.S.si -> O.add ~si:1 (); ac st (push m1 a b) u (push m2 a b) t | _ -> false diff --git a/helm/software/lambda-delta/src/complete_rg/Make b/helm/software/lambda-delta/src/complete_rg/Make index ccb5b1559..a7b947730 100644 --- a/helm/software/lambda-delta/src/complete_rg/Make +++ b/helm/software/lambda-delta/src/complete_rg/Make @@ -1 +1 @@ -crg crgOutput crgTxt crgAut +crg crgOutput diff --git a/helm/software/lambda-delta/src/modules.ml b/helm/software/lambda-delta/src/modules.ml index 619a6cce6..9fbb2cdf7 100644 --- a/helm/software/lambda-delta/src/modules.ml +++ b/helm/software/lambda-delta/src/modules.ml @@ -1,4 +1,4 @@ -(* free = F I P U V *) +(* free = F I M P U V *) module U = NUri module K = NUri.UriHash @@ -18,29 +18,21 @@ module R = alpha module Q = ccs module S = status +module D = crg +module DO = crgOutput + module T = txt module TP = txtParser module TL = txtLexer module TT = txtTxt +module TD = txtCrg module A = aut module AA = autProcess module AO = autOutput module AP = autParser module AL = autLexer - -module Z = bag -module ZO = bagOutput -module ZE = bagEnvironment -module ZS = bagSubstitution -module ZR = bagReduction -module ZT = bagType -module ZU = bagUntrusted - -module D = crg -module DO = crgOutput -module TD = crgTxt -module AD = crgAut +module AD = autCrg module XL = xmlLibrary module XD = xmlCrg @@ -54,11 +46,14 @@ module BR = brgReduction module BT = brgType module BU = brgUntrusted -module M = meta -module MO = metaOutput -module MA = metaAut -module MZ = metaBag -module MB = metaBrg +module Z = bag +module ZD = brgCrg +module ZO = bagOutput +module ZE = bagEnvironment +module ZS = bagSubstitution +module ZR = bagReduction +module ZT = bagType +module ZU = bagUntrusted (* top *) diff --git a/helm/software/lambda-delta/src/text/Make b/helm/software/lambda-delta/src/text/Make index f1c0ffe26..3690bbaeb 100644 --- a/helm/software/lambda-delta/src/text/Make +++ b/helm/software/lambda-delta/src/text/Make @@ -1 +1 @@ -txt txtParser txtLexer txtTxt +txt txtParser txtLexer txtTxt txtCrg diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml b/helm/software/lambda-delta/src/text/txtCrg.ml similarity index 100% rename from helm/software/lambda-delta/src/complete_rg/crgTxt.ml rename to helm/software/lambda-delta/src/text/txtCrg.ml diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.mli b/helm/software/lambda-delta/src/text/txtCrg.mli similarity index 100% rename from helm/software/lambda-delta/src/complete_rg/crgTxt.mli rename to helm/software/lambda-delta/src/text/txtCrg.mli diff --git a/helm/software/lambda-delta/src/toplevel/Make b/helm/software/lambda-delta/src/toplevel/Make index c32bec6c7..bf1a1fdef 100644 --- a/helm/software/lambda-delta/src/toplevel/Make +++ b/helm/software/lambda-delta/src/toplevel/Make @@ -1 +1 @@ -meta metaOutput metaAut metaBag metaBrg top +top diff --git a/helm/software/lambda-delta/src/toplevel/meta.ml b/helm/software/lambda-delta/src/toplevel/meta.ml deleted file mode 100644 index 1a710278e..000000000 --- a/helm/software/lambda-delta/src/toplevel/meta.ml +++ /dev/null @@ -1,27 +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 E = Entity - -type uri = E.uri -type id = E.id - -type term = Sort of bool (* sorts: true = TYPE, false = PROP *) - | LRef of int * int (* local reference: local environment length, de bruijn index *) - | GRef of int * uri * term list (* global reference: local environment length, name, arguments *) - | Appl of term * term (* application: argument, function *) - | Abst of id * term * term (* abstraction: name, domain, scope *) - -type pars = (id * term) list (* parameter declarations: name, type *) - -type entry = pars * term * term option (* parameters, domain, body *) - -type entity = entry E.entity diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.ml b/helm/software/lambda-delta/src/toplevel/metaAut.ml deleted file mode 100644 index be6345007..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaAut.ml +++ /dev/null @@ -1,219 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module U = NUri -module K = U.UriHash -module C = Cps -module G = Options -module E = Entity -module N = Level -module M = Meta -module A = Aut - -(* qualified identifier: uri, name, qualifiers *) -type qid = M.uri * M.id * M.id list - -type context_node = qid option (* context node: None = root *) - -type status = { - path: M.id list; (* current section path *) - node: context_node; (* current context node *) - nodes: context_node list; (* context node list *) - line: int; (* line number *) - cover: string (* initial segment of URI hierarchy *) -} - -type resolver = Local of int - | Global of M.pars - -let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) - -let henv = K.create henv_size (* optimized global environment *) - -let hcnt = K.create hcnt_size (* optimized context *) - -(* Internal functions *******************************************************) - -let id_of_name (id, _, _) = id - -let mk_qid st id path = - let uripath = if st.cover = "" then path else st.cover :: path in - let str = String.concat "/" uripath in - let str = Filename.concat str id in - U.uri_of_string ("ld:/" ^ str ^ ".ld"), id, path - -let uri_of_qid (uri, _, _) = uri - -let complete_qid f st (id, is_local, qs) = - let f qs = f (mk_qid st id qs) in - let f path = C.list_rev_append f path ~tail:qs in - let rec skip f = function - | phd :: ptl, qshd :: _ when phd = qshd -> f ptl - | _ :: ptl, _ :: _ -> skip f (ptl, qs) - | _ -> f [] - in - if is_local then f st.path else skip f (st.path, qs) - -let relax_qid f st (_, id, path) = - let f path = f (mk_qid st id path) in - let f = function - | _ :: tl -> C.list_rev f tl - | [] -> assert false - in - C.list_rev f path - -let relax_opt_qid f st = function - | None -> f None - | Some qid -> let f qid = f (Some qid) in relax_qid f st qid - -let resolve_lref f st l lenv id = - let rec aux f i = function - | [] -> f None - | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i))) - | _ :: tl -> aux f (succ i) tl - in - aux f 0 lenv - -let resolve_lref_strict f st l lenv id = - let f = function - | Some t -> f t - | None -> assert false - in - resolve_lref f st l lenv id - -let resolve_gref f st qid = - try let args = K.find henv (uri_of_qid qid) in f qid (Some args) - with Not_found -> f qid None - -let resolve_gref_relaxed f st qid = -(* this is not tail recursive *) - let rec g qid = function - | None -> relax_qid (resolve_gref g st) st qid - | Some args -> f qid args - in - resolve_gref g st qid - -let get_pars f st = function - | None -> f [] None - | Some qid as node -> - try let pars = K.find hcnt (uri_of_qid qid) in f pars None - with Not_found -> f [] (Some node) - -let get_pars_relaxed f st = -(* this is not tail recursive *) - let rec g pars = function - | None -> f pars - | Some node -> relax_opt_qid (get_pars g st) st node - in - get_pars g st st.node - -(* this is not tail recursive on the GRef branch *) -let rec xlate_term f st lenv = function - | A.Sort sort -> - f (M.Sort sort) - | A.Appl (v, t) -> - let f vv tt = f (M.Appl (vv, tt)) in - let f vv = xlate_term (f vv) st lenv t in - xlate_term f st lenv v - | A.Abst (name, w, t) -> - let add name w lenv = (name, w) :: lenv in - let f ww tt = f (M.Abst (name, ww, tt)) in - let f ww = xlate_term (f ww) st (add name ww lenv) t in - xlate_term f st lenv w - | A.GRef (name, args) -> - let l = List.length lenv in - let g qid defs = - let map1 f = xlate_term f st lenv in - let map2 f (id, _) = resolve_lref_strict f st l lenv id in - let f tail = - let f args = f (M.GRef (l, uri_of_qid qid, args)) in - let f defs = C.list_rev_map_append f map2 defs ~tail in - C.list_sub_strict f defs args - in - C.list_map f map1 args - in - let g qid = resolve_gref_relaxed g st qid in - let f = function - | Some t -> f t - | None -> complete_qid g st name - in - resolve_lref f st l lenv (id_of_name name) - -let xlate_entity err f st = function - | A.Section (Some (_, name)) -> - err {st with path = name :: st.path; nodes = st.node :: st.nodes} - | A.Section None -> - begin match st.path, st.nodes with - | _ :: ptl, nhd :: ntl -> - err {st with path = ptl; node = nhd; nodes = ntl} - | _ -> assert false - end - | A.Context None -> - err {st with node = None} - | A.Context (Some name) -> - let f name = err {st with node = Some name} in - complete_qid f st name - | A.Block (name, w) -> - let f qid = - let f pars = - let f ww = - K.add hcnt (uri_of_qid qid) ((name, ww) :: pars); - err {st with node = Some qid} - in - xlate_term f st pars w - in - get_pars_relaxed f st - in - complete_qid f st (name, true, []) - | A.Decl (name, w) -> - let f pars = - let f qid = - let f ww = - K.add henv (uri_of_qid qid) pars; - let a = [E.Mark st.line] in - let entry = pars, ww, None in - let entity = a, uri_of_qid qid, E.Abst (N.infinite, entry) in - f {st with line = succ st.line} entity - in - xlate_term f st pars w - in - complete_qid f st (name, true, []) - in - get_pars_relaxed f st - | A.Def (name, w, trans, v) -> - let f pars = - let f qid = - let f ww vv = - K.add henv (uri_of_qid qid) pars; - let a = E.Mark st.line :: if trans then [] else [E.Priv] in - let entry = pars, ww, Some vv in - let entity = a, uri_of_qid qid, E.Abbr entry in - f {st with line = succ st.line} entity - in - let f ww = xlate_term (f ww) st pars v in - xlate_term f st pars w - in - complete_qid f st (name, true, []) - in - get_pars_relaxed f st - -(* Interface functions ******************************************************) - -let initial_status () = - K.clear henv; K.clear hcnt; { - path = []; node = None; nodes = []; line = 1; cover = !G.cover -} - -let refresh_status st = {st with - cover = !G.cover -} - -let meta_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.mli b/helm/software/lambda-delta/src/toplevel/metaAut.mli deleted file mode 100644 index a1210c527..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaAut.mli +++ /dev/null @@ -1,20 +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 - -val initial_status: unit -> status - -val refresh_status: status -> status - -val meta_of_aut: - (status -> 'a) -> (status -> Meta.entity -> 'a) -> - status -> Aut.command -> 'a diff --git a/helm/software/lambda-delta/src/toplevel/metaBag.ml b/helm/software/lambda-delta/src/toplevel/metaBag.ml deleted file mode 100644 index 97148c737..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaBag.ml +++ /dev/null @@ -1,67 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module C = Cps -module Z = Bag -module M = Meta - -(* Internal functions *******************************************************) - -let rec xlate_term c f = function - | M.Sort s -> - let f h = f (Z.Sort h) in - if s then f 0 else f 1 - | M.LRef (_, i) -> - let l, _, _ = List.nth c i in - f (Z.LRef l) - | M.GRef (_, uri, vs) -> - let map f t v = f (Z.appl v t) in - let f vs = C.list_fold_left f map (Z.GRef uri) vs in - C.list_map f (xlate_term c) vs - | M.Appl (v, t) -> - let f v t = f (Z.Appl (v, t)) in - let f v = xlate_term c (f v) t in - xlate_term c f v - | M.Abst (id, w, t) -> - let f w = - let l = Z.new_location () in - let f t = f (Z.Bind (l, id, Z.Abst w, t)) in - let f c = xlate_term c f t in - Z.push "meta" f c l id (Z.Abst w) - in - xlate_term c f w - -let xlate_pars f pars = - let map f (id, w) c = - let l = Z.new_location () in - let f w = Z.push "meta" f c l id (Z.Abst w) in - xlate_term c f w - in - C.list_fold_right f map pars Z.empty_lenv - -let unwind_to_xlate_term f c t = - let map f t (l, id, b) = f (Z.bind l id b t) in - let f t = C.list_fold_left f map t c in - xlate_term c f t - -let xlate_entry f = function - | pars, u, None -> - let f c = unwind_to_xlate_term f c u in - xlate_pars f pars - | pars, u, Some t -> - let f u t = f (Z.Cast (u, t)) in - let f c u = unwind_to_xlate_term (f u) c t in - let f c = unwind_to_xlate_term (f c) c u in - xlate_pars f pars - -(* Interface functions ******************************************************) - -let bag_of_meta = xlate_entry diff --git a/helm/software/lambda-delta/src/toplevel/metaBrg.ml b/helm/software/lambda-delta/src/toplevel/metaBrg.ml deleted file mode 100644 index f1497697c..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaBrg.ml +++ /dev/null @@ -1,67 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module C = Cps -module E = Entity -module N = Level -module B = Brg -module M = Meta - -(* Internal functions *******************************************************) - -let rec xlate_term c f = function - | M.Sort s -> - let f h = f (B.Sort ([], h)) in - if s then f 0 else f 1 - | M.LRef (_, i) -> - f (B.LRef ([], i)) - | M.GRef (_, uri, vs) -> - let map f t v = f (B.appl [] v t) in - let f vs = C.list_fold_left f map (B.GRef ([], uri)) vs in - C.list_map f (xlate_term c) vs - | M.Appl (v, t) -> - let f v t = f (B.Appl ([], v, t)) in - let f v = xlate_term c (f v) t in - xlate_term c f v - | M.Abst (id, w, t) -> - let f w = - let a = [E.Name (id, true)] in - let f t = f (B.Bind (a, B.Abst (N.infinite, w), t)) in - xlate_term (B.push c B.empty a (B.Abst (N.infinite, w))) f t - in - xlate_term c f w - -let xlate_pars f pars = - let map f (id, w) c = - let a = [E.Name (id, true)] in - let f w = f (B.push c B.empty a (B.Abst (N.infinite, w))) in - xlate_term c f w - in - C.list_fold_right f map pars B.empty - -let unwind_to_xlate_term f c t = - let map t a b = B.bind a b t in - let f t = f (B.fold_left map t c) in - xlate_term c f t - -let xlate_entry f = function - | pars, u, None -> - let f c = unwind_to_xlate_term f c u in - xlate_pars f pars - | pars, u, Some t -> - let f u t = f (B.Cast ([], u, t)) in - let f c u = unwind_to_xlate_term (f u) c t in - let f c = unwind_to_xlate_term (f c) c u in - xlate_pars f pars - -(* Interface functions ******************************************************) - -let brg_of_meta = xlate_entry diff --git a/helm/software/lambda-delta/src/toplevel/metaBrg.mli b/helm/software/lambda-delta/src/toplevel/metaBrg.mli deleted file mode 100644 index 4ce275fb8..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaBrg.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -val brg_of_meta: (Brg.term -> 'a) -> Meta.entry -> 'a diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.ml b/helm/software/lambda-delta/src/toplevel/metaOutput.ml deleted file mode 100644 index 73ff70e59..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.ml +++ /dev/null @@ -1,108 +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 P = Printf -module F = Format -module U = NUri -module C = Cps -module L = Log -module E = Entity -module M = Meta - -type counters = { - eabsts: int; - eabbrs: int; - pabsts: int; - tsorts: int; - tlrefs: int; - tgrefs: int; - pappls: int; - tappls: int; - tabsts: int; - uris : U.uri list; - nodes : int; - xnodes: int -} - -let initial_counters = { - eabsts = 0; eabbrs = 0; pabsts = 0; pappls = 0; - tsorts = 0; tlrefs = 0; tgrefs = 0; tappls = 0; tabsts = 0; - uris = []; nodes = 0; xnodes = 0 -} - -let rec count_term f c = function - | M.Sort _ -> - f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} - | M.LRef _ -> - f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} - | M.GRef (_, u, ts) -> - let c = {c with tgrefs = succ c.tgrefs} in - let c = {c with pappls = c.pappls + List.length ts} in - let c = {c with nodes = c.nodes + List.length ts} in - let c = - if Cps.list_mem ~eq:U.eq u c.uris - then {c with nodes = succ c.nodes} - else {c with xnodes = succ c.xnodes} - in - Cps.list_fold_left f count_term c ts - | M.Appl (v, t) -> - let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in - let f c = count_term f c t in - count_term f c v - | M.Abst (_, w, t) -> - let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in - let f c = count_term f c t in - count_term f c w - -let count_par f c (_, w) = count_term f c w - -let count_xterm f c = function - | None -> f c - | Some v -> count_term f c v - -let count_entity f c = function - | _, u, E.Abst (_, (pars, w, xv)) -> - let c = {c with eabsts = succ c.eabsts} in - let c = {c with pabsts = c.pabsts + List.length pars} in - let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in - let f c = count_xterm f c xv in - let f c = count_term f c w in - Cps.list_fold_left f count_par c pars - | _, _, E.Abbr (pars, w, xv) -> - let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in - let c = {c with pabsts = c.pabsts + List.length pars} in - let c = {c with nodes = c.nodes + List.length pars} in - let f c = count_xterm f c xv in - let f c = count_term f c w in - Cps.list_fold_left f count_par c pars - | _, _, E.Void -> assert false - -let print_counters f c = - let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in - let pars = c.pabsts + c.pappls in - let entries = c.eabsts + c.eabbrs in - let nodes = c.nodes + c.xnodes in - L.warn (P.sprintf " Intermediate representation summary (meta)"); - L.warn (P.sprintf " Total entries: %7u" entries); - L.warn (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn (P.sprintf " Total parameter items: %7u" pars); - L.warn (P.sprintf " Application items: %7u" c.pappls); - L.warn (P.sprintf " Abstraction items: %7u" c.pabsts); - L.warn (P.sprintf " Total term items: %7u" terms); - L.warn (P.sprintf " Sort items: %7u" c.tsorts); - L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn (P.sprintf " Application items: %7u" c.tappls); - L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes); - L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes); - f () diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.mli b/helm/software/lambda-delta/src/toplevel/metaOutput.mli deleted file mode 100644 index 26b873cf9..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.mli +++ /dev/null @@ -1,18 +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 counters - -val initial_counters: counters - -val count_entity: (counters -> 'a) -> counters -> Meta.entity -> 'a - -val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 579f5e658..b47d00725 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -20,11 +20,11 @@ module H = Hierarchy module O = Output module E = Entity module S = Status -module TD = CrgTxt +module DO = CrgOutput +module TD = TxtCrg module AA = AutProcess module AO = AutOutput -module AD = CrgAut -module DO = CrgOutput +module AD = AutCrg module XL = XmlLibrary module XD = XmlCrg module BD = BrgCrg @@ -35,11 +35,6 @@ module ZO = BagOutput module ZT = BagType module ZU = BagUntrusted -module MA = MetaAut -module MO = MetaOutput -module MB = MetaBrg -module MZ = MetaBag - type status = { kst: S.status; tst: TD.status; @@ -49,8 +44,6 @@ type status = { dc : DO.counters; bc : BO.counters; zc : ZO.counters; - mst: MA.status; - mc : MO.counters; } let flush_all () = L.flush 0; L.flush_err () @@ -70,23 +63,19 @@ let initial_status () = { dc = DO.initial_counters; bc = BO.initial_counters; zc = ZO.initial_counters; - mst = MA.initial_status (); - mc = MO.initial_counters; } let refresh_status st = {st with kst = S.refresh_status st.kst; tst = TD.refresh_status st.tst; ast = AD.refresh_status st.ast; - mst = MA.refresh_status st.mst; } (* kernel related ***********************************************************) -type kernel_entity = BrgEntity of Brg.entity - | BagEntity of Bag.entity - | CrgEntity of Crg.entity - | MetaEntity of Meta.entity +type kernel_entity = BrgEntity of Brg.entity + | BagEntity of Bag.entity + | CrgEntity of Crg.entity let print_counters st = function | G.Crg -> DO.print_counters C.start st.dc @@ -94,13 +83,9 @@ let print_counters st = function | G.Bag -> ZO.print_counters C.start st.zc let xlate_entity entity = match !G.kernel, entity with - | G.Brg, CrgEntity e -> + | G.Brg, CrgEntity e -> let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e - | G.Brg, MetaEntity e -> - let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e - | G.Bag, MetaEntity e -> - let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e - | _, entity -> entity + | _, entity -> entity let pp_progress e = let f a u = @@ -110,22 +95,19 @@ let pp_progress e = E.mark err f a in match e with - | CrgEntity e -> E.common f e - | BrgEntity e -> E.common f e - | BagEntity e -> E.common f e - | MetaEntity e -> E.common f e + | CrgEntity e -> E.common f e + | BrgEntity e -> E.common f e + | BagEntity e -> E.common f e let count_entity st = function - | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e} - | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e} - | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e} - | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} + | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e} + | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e} + | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e} let export_entity = function - | CrgEntity e -> XL.export_entity XD.export_term e - | BrgEntity e -> XL.export_entity BO.export_term e - | MetaEntity _ - | BagEntity _ -> () + | CrgEntity e -> XL.export_entity XD.export_term e + | BrgEntity e -> XL.export_entity BO.export_term e + | BagEntity _ -> () let type_check st k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in @@ -133,8 +115,7 @@ let type_check st k = match k with | BrgEntity entity -> BU.type_check brg_err ok st.kst entity | BagEntity entity -> ZU.type_check ok st.kst entity - | CrgEntity _ - | MetaEntity _ -> st + | CrgEntity _ -> st (* extended lexer ***********************************************************) @@ -213,7 +194,6 @@ let progress = ref false let preprocess = ref false let root = ref "" let export = ref false -let old = ref false let st = ref (initial_status ()) let streaming = ref false (* parsing style (temporary) *) @@ -231,20 +211,16 @@ let process_1 st entity = let process_0 st entity = let f st entity = if !stage = 0 then st else - match entity, !old with - | AutEntity e, true -> - let frr mst = {st with mst = mst} in - let h mst e = process_1 {st with mst = mst} (MetaEntity e) in - MA.meta_of_aut frr h st.mst e - | AutEntity e, false -> + match entity with + | AutEntity e -> let err ast = {st with ast = ast} in let g ast e = process_1 {st with ast = ast} (CrgEntity e) in AD.crg_of_aut err g st.ast e - | TxtEntity e, _ -> + | TxtEntity e -> let crr tst = {st with tst = tst} in let d tst e = process_1 {st with tst = tst} (CrgEntity e) in TD.crg_of_txt crr d gen_text st.tst e - | NoEntity, _ -> assert false + | NoEntity -> assert false in let st = if !L.level > 2 then count_input st entity else st in if !preprocess then process_input f st entity else f st entity @@ -282,7 +258,7 @@ let process st name = let main = try - let version_string = "Helena 0.8.1 M - October 2010" in + let version_string = "Helena 0.8.1 M - November 2010" in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else @@ -298,7 +274,7 @@ try let set_xdir s = G.xdir := s in let set_root s = root := s in let clear_options () = - progress := false; old := false; export := false; preprocess := false; + progress := false; export := false; preprocess := false; stage := 3; root := ""; st := initial_status (); L.clear (); G.clear (); H.clear (); O.clear_reductions (); @@ -319,9 +295,7 @@ try if !L.level > 2 then begin AO.print_counters C.start !st.ac; if !preprocess then AO.print_process_counters C.start !st.pst; - if !stage > 0 then - if !old then MO.print_counters C.start !st.mc - else print_counters !st G.Crg; + if !stage > 0 then print_counters !st G.Crg; if !stage > 1 then print_counters !st !G.kernel; if !stage > 2 then O.print_reductions () end @@ -331,7 +305,7 @@ try flush_all () in let help = - "Usage: helena [ -LPVXcgijopqux1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXcgijopqx1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" @@ -349,12 +323,11 @@ try let help_i = " show local references by index" in let help_j = " show URI of processed kernel objects" in let help_k = " set kernel version (default: \"brg\")" in - let help_o = " use old abstract language instead of crg" in + let help_o = " activate sort inclusion" in let help_p = " preprocess source" in let help_q = " disable quotation of identifiers" in let help_r = " set initial segment of URI hierarchy (default: empty)" in let help_s = " set translation stage (see above)" in - let help_u = " activate sort inclusion" in let help_x = " export kernel entities (XML)" in let help_1 = " parse files with streaming policy" in @@ -373,12 +346,11 @@ try ("-i", Arg.Set G.indexes, help_i); ("-j", Arg.Set progress, help_j); ("-k", Arg.String set_kernel, help_k); - ("-o", Arg.Set old, help_o); + ("-o", Arg.Set G.si, help_o); ("-p", Arg.Set preprocess, help_p); ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String set_root, help_r); ("-s", Arg.Int set_stage, help_s); - ("-u", Arg.Set G.si, help_u); ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help; -- 2.39.2