From: Ferruccio Guidi Date: Mon, 1 Nov 2010 15:18:57 +0000 (+0000) Subject: - some bugfix X-Git-Tag: make_still_working~2744 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d145ea48ed0bdb9642ced01283231f3f13d476b8;p=helm.git - some bugfix - some - old intermediate language (meta) has been removed --- 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/automath/autCrg.ml b/helm/software/lambda-delta/src/automath/autCrg.ml new file mode 100644 index 000000000..388b0c2b9 --- /dev/null +++ b/helm/software/lambda-delta/src/automath/autCrg.ml @@ -0,0 +1,250 @@ +(* + ||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 A = Aut +module D = Crg + +(* qualified identifier: uri, name, qualifiers *) +type qid = D.uri * D.id * D.id list + +type context = E.attrs * D.term list + +type context_node = qid option (* context node: None = root *) + +type status = { + path: D.id list; (* current section path *) + node: context_node; (* current context node *) + nodes: context_node list; (* context node list *) + line: int; (* line number *) + mk_uri:G.uri_generator (* uri generator *) +} + +type resolver = Local of int + | Global of context + +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 empty_cnt = [], [], [] + +let add_abst (a, ws, ns) id w n = + E.Name (id, true) :: a, w :: ws, N.succ n :: ns + +let mk_lref f n i j k = f n (D.TLRef ([E.Apix k], i, j)) + +let id_of_name (id, _, _) = id + +let mk_qid f st id path = + let str = String.concat "/" path in + let str = Filename.concat str id in + let str = st.mk_uri str in + f (U.uri_of_string str, id, path) + +let uri_of_qid (uri, _, _) = uri + +let complete_qid f st (id, is_local, qs) = + let f path = C.list_rev_append (mk_qid f st id) 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 = function + | _ :: tl -> C.list_rev (mk_qid f st id) 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_gref err f st qid = + try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt + with Not_found -> err qid + +let resolve_gref_relaxed f st qid = +(* this is not tail recursive *) + let rec err qid = relax_qid (resolve_gref err f st) st qid in + resolve_gref err f st qid + +let get_cnt err f st = function + | None -> f empty_cnt + | Some qid as node -> + try let cnt = K.find hcnt (uri_of_qid qid) in f cnt + with Not_found -> err node + +let get_cnt_relaxed f st = +(* this is not tail recursive *) + let rec err node = relax_opt_qid (get_cnt err f st) st node in + get_cnt err f st st.node + +(****************************************************************************) + +let push_abst f (lenv, ns) a n w = + let bw = D.Abst (N.infinite, [w]) in + let f lenv = f (lenv, N.succ n :: ns) in + D.push_bind f lenv a bw + +let resolve_lref err f id (lenv, ns) = + let f i j k = f (List.nth ns k) i j k in + D.resolve_lref err f id lenv + +let lenv_of_cnt (a, ws, ns) = + D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns + +(* this is not tail recursive in the GRef branch *) +let rec xlate_term f st lenv = function + | A.Sort s -> + let f h = f (N.finite 0) (D.TSort ([], h)) in + if s then f 0 else f 1 + | A.Appl (v, t) -> + let f vv n tt = f n (D.TAppl ([], [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 f nw ww = + let a = [E.Name (name, true)] in + let f nt tt = + let b = D.Abst (nt, [ww]) in + f nt (D.TBind (a, b, tt)) + in + let f lenv = xlate_term f st lenv t in + push_abst f lenv a nw ww + in + xlate_term f st lenv w + | A.GRef (name, args) -> + let map1 f = function + | E.Name (id, _) -> f (A.GRef ((id, true, []), [])) + | _ -> C.err () + in + let map2 f t = + let f _ tt = f tt in xlate_term f st lenv t + in + let g n qid (a, _, _) = + let gref = D.TGRef ([], uri_of_qid qid) in + match args, a with + | [], [] -> f n gref + | _ -> + let f args = f n (D.TAppl ([], args, gref)) in + let f args = C.list_rev_map f map2 args in + let f a = C.list_rev_map_append f map1 a ~tail:args in + C.list_sub_strict f a args + in + let g qid = resolve_gref_relaxed g st qid in + let err () = complete_qid g st name in + resolve_lref err (mk_lref f) (id_of_name name) lenv + +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 cnt = + let lenv = lenv_of_cnt cnt in + let f nw ww = + K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw); + err {st with node = Some qid} + in + xlate_term f st lenv w + in + get_cnt_relaxed f st + in + complete_qid f st (name, true, []) + | A.Decl (name, w) -> + let f cnt = + let a, ws, _ = cnt in + let lenv = lenv_of_cnt cnt in + let f qid = + let f nw ww = + K.add henv (uri_of_qid qid) (N.succ nw, cnt); + let t = match ws with + | [] -> ww + | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww) + in +(* + print_newline (); CrgOutput.pp_term print_string t; +*) + let b = E.Abst (N.infinite, t) in + let entity = [E.Mark st.line], uri_of_qid qid, b in + f {st with line = succ st.line} entity + in + xlate_term f st lenv w + in + complete_qid f st (name, true, []) + in + get_cnt_relaxed f st + | A.Def (name, w, trans, v) -> + let f cnt = + let a, ws, _ = cnt in + let lenv = lenv_of_cnt cnt in + let f qid = + let f nw ww = + let f nv vv = + assert (nv = N.succ nw); (**) + K.add henv (uri_of_qid qid) (nv, cnt); + let t = match ws with + | [] -> D.TCast ([], ww, vv) + | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv)) + in +(* + print_newline (); CrgOutput.pp_term print_string t; +*) + let b = E.Abbr t in + let a = E.Mark st.line :: if trans then [] else [E.Priv] in + let entity = a, uri_of_qid qid, b in + f {st with line = succ st.line} entity + in + xlate_term f st lenv v + in + xlate_term f st lenv w + in + complete_qid f st (name, true, []) + in + get_cnt_relaxed f st + +(* Interface functions ******************************************************) + +let initial_status () = + K.clear henv; K.clear hcnt; { + path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri () +} + +let refresh_status st = {st with + mk_uri = G.get_mk_uri () +} + +let crg_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/src/automath/autCrg.mli b/helm/software/lambda-delta/src/automath/autCrg.mli new file mode 100644 index 000000000..c7d93d3ce --- /dev/null +++ b/helm/software/lambda-delta/src/automath/autCrg.mli @@ -0,0 +1,19 @@ +(* + ||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 crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> + status -> Aut.command -> 'a 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/basic_ag/bagCrg.mli b/helm/software/lambda-delta/src/basic_ag/bagCrg.mli new file mode 100644 index 000000000..aae9eb280 --- /dev/null +++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.mli @@ -0,0 +1,15 @@ +(* + ||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 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/complete_rg/crgAut.ml b/helm/software/lambda-delta/src/complete_rg/crgAut.ml deleted file mode 100644 index 388b0c2b9..000000000 --- a/helm/software/lambda-delta/src/complete_rg/crgAut.ml +++ /dev/null @@ -1,250 +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 A = Aut -module D = Crg - -(* qualified identifier: uri, name, qualifiers *) -type qid = D.uri * D.id * D.id list - -type context = E.attrs * D.term list - -type context_node = qid option (* context node: None = root *) - -type status = { - path: D.id list; (* current section path *) - node: context_node; (* current context node *) - nodes: context_node list; (* context node list *) - line: int; (* line number *) - mk_uri:G.uri_generator (* uri generator *) -} - -type resolver = Local of int - | Global of context - -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 empty_cnt = [], [], [] - -let add_abst (a, ws, ns) id w n = - E.Name (id, true) :: a, w :: ws, N.succ n :: ns - -let mk_lref f n i j k = f n (D.TLRef ([E.Apix k], i, j)) - -let id_of_name (id, _, _) = id - -let mk_qid f st id path = - let str = String.concat "/" path in - let str = Filename.concat str id in - let str = st.mk_uri str in - f (U.uri_of_string str, id, path) - -let uri_of_qid (uri, _, _) = uri - -let complete_qid f st (id, is_local, qs) = - let f path = C.list_rev_append (mk_qid f st id) 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 = function - | _ :: tl -> C.list_rev (mk_qid f st id) 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_gref err f st qid = - try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt - with Not_found -> err qid - -let resolve_gref_relaxed f st qid = -(* this is not tail recursive *) - let rec err qid = relax_qid (resolve_gref err f st) st qid in - resolve_gref err f st qid - -let get_cnt err f st = function - | None -> f empty_cnt - | Some qid as node -> - try let cnt = K.find hcnt (uri_of_qid qid) in f cnt - with Not_found -> err node - -let get_cnt_relaxed f st = -(* this is not tail recursive *) - let rec err node = relax_opt_qid (get_cnt err f st) st node in - get_cnt err f st st.node - -(****************************************************************************) - -let push_abst f (lenv, ns) a n w = - let bw = D.Abst (N.infinite, [w]) in - let f lenv = f (lenv, N.succ n :: ns) in - D.push_bind f lenv a bw - -let resolve_lref err f id (lenv, ns) = - let f i j k = f (List.nth ns k) i j k in - D.resolve_lref err f id lenv - -let lenv_of_cnt (a, ws, ns) = - D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns - -(* this is not tail recursive in the GRef branch *) -let rec xlate_term f st lenv = function - | A.Sort s -> - let f h = f (N.finite 0) (D.TSort ([], h)) in - if s then f 0 else f 1 - | A.Appl (v, t) -> - let f vv n tt = f n (D.TAppl ([], [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 f nw ww = - let a = [E.Name (name, true)] in - let f nt tt = - let b = D.Abst (nt, [ww]) in - f nt (D.TBind (a, b, tt)) - in - let f lenv = xlate_term f st lenv t in - push_abst f lenv a nw ww - in - xlate_term f st lenv w - | A.GRef (name, args) -> - let map1 f = function - | E.Name (id, _) -> f (A.GRef ((id, true, []), [])) - | _ -> C.err () - in - let map2 f t = - let f _ tt = f tt in xlate_term f st lenv t - in - let g n qid (a, _, _) = - let gref = D.TGRef ([], uri_of_qid qid) in - match args, a with - | [], [] -> f n gref - | _ -> - let f args = f n (D.TAppl ([], args, gref)) in - let f args = C.list_rev_map f map2 args in - let f a = C.list_rev_map_append f map1 a ~tail:args in - C.list_sub_strict f a args - in - let g qid = resolve_gref_relaxed g st qid in - let err () = complete_qid g st name in - resolve_lref err (mk_lref f) (id_of_name name) lenv - -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 cnt = - let lenv = lenv_of_cnt cnt in - let f nw ww = - K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw); - err {st with node = Some qid} - in - xlate_term f st lenv w - in - get_cnt_relaxed f st - in - complete_qid f st (name, true, []) - | A.Decl (name, w) -> - let f cnt = - let a, ws, _ = cnt in - let lenv = lenv_of_cnt cnt in - let f qid = - let f nw ww = - K.add henv (uri_of_qid qid) (N.succ nw, cnt); - let t = match ws with - | [] -> ww - | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww) - in -(* - print_newline (); CrgOutput.pp_term print_string t; -*) - let b = E.Abst (N.infinite, t) in - let entity = [E.Mark st.line], uri_of_qid qid, b in - f {st with line = succ st.line} entity - in - xlate_term f st lenv w - in - complete_qid f st (name, true, []) - in - get_cnt_relaxed f st - | A.Def (name, w, trans, v) -> - let f cnt = - let a, ws, _ = cnt in - let lenv = lenv_of_cnt cnt in - let f qid = - let f nw ww = - let f nv vv = - assert (nv = N.succ nw); (**) - K.add henv (uri_of_qid qid) (nv, cnt); - let t = match ws with - | [] -> D.TCast ([], ww, vv) - | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv)) - in -(* - print_newline (); CrgOutput.pp_term print_string t; -*) - let b = E.Abbr t in - let a = E.Mark st.line :: if trans then [] else [E.Priv] in - let entity = a, uri_of_qid qid, b in - f {st with line = succ st.line} entity - in - xlate_term f st lenv v - in - xlate_term f st lenv w - in - complete_qid f st (name, true, []) - in - get_cnt_relaxed f st - -(* Interface functions ******************************************************) - -let initial_status () = - K.clear henv; K.clear hcnt; { - path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri () -} - -let refresh_status st = {st with - mk_uri = G.get_mk_uri () -} - -let crg_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/src/complete_rg/crgAut.mli b/helm/software/lambda-delta/src/complete_rg/crgAut.mli deleted file mode 100644 index c7d93d3ce..000000000 --- a/helm/software/lambda-delta/src/complete_rg/crgAut.mli +++ /dev/null @@ -1,19 +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 crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> - status -> Aut.command -> 'a diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml deleted file mode 100644 index 980b74a08..000000000 --- a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml +++ /dev/null @@ -1,161 +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 H = Hierarchy -module C = Cps -module G = Options -module E = Entity -module T = Txt -module TT = TxtTxt -module D = Crg - -type status = { - path : T.id list; (* current section path *) - line : int; (* line number *) - sort : int; (* first default sort index *) - mk_uri: G.uri_generator (* uri generator *) -} - -let henv_size = 7000 (* hash tables initial size *) - -let henv = Hashtbl.create henv_size (* optimized global environment *) - -(* Internal functions *******************************************************) - -let name_of_id ?(r=true) id = E.Name (id, r) - -let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) - -let mk_gref f uri = f (D.TGRef ([], uri)) - -let uri_of_id st id path = - let str = String.concat "/" path in - let str = Filename.concat str id in - let str = st.mk_uri str in - U.uri_of_string str - -let resolve_gref err f st id = - try f (Hashtbl.find henv id) - with Not_found -> err () - -let rec xlate_term f st lenv = function - | T.Inst _ - | T.Impl _ -> assert false - | T.Sort h -> - f (D.TSort ([], h)) - | T.NSrt id -> - let f h = f (D.TSort ([], h)) in - H.sort_of_string C.err f id - | T.LRef (i, j) -> - D.get_index C.err (mk_lref f i j) i j lenv - | T.NRef id -> - let err () = resolve_gref C.err (mk_gref f) st id in - D.resolve_lref err (mk_lref f) id lenv - | T.Cast (u, t) -> - let f uu tt = f (D.TCast ([], uu, tt)) in - let f uu = xlate_term (f uu) st lenv t in - xlate_term f st lenv u - | T.Appl (vs, t) -> - let map f = xlate_term f st lenv in - let f vvs tt = f (D.TAppl ([], vvs, tt)) in - let f vvs = xlate_term (f vvs) st lenv t in - C.list_map f map vs - | T.Bind (n, b, t) -> - let abst_map (lenv, a, wws) (id, r, w) = - let attr = name_of_id ~r id in - let ww = xlate_term C.start st lenv w in - D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws - in - let abbr_map (lenv, a, wws) (id, w) = - let attr = name_of_id id in - let ww = xlate_term C.start st lenv w in - D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws - in - let void_map (lenv, a, n) id = - let attr = name_of_id id in - D.push2 C.err C.start lenv ~attr (), attr :: a, succ n - in - let lenv, aa, bb = match b with - | T.Abst xws -> - let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in - let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in - lenv, aa, D.Abst (n, wws) - | T.Abbr xvs -> - let lenv = D.push_bind C.start lenv [] (D.Abbr []) in - let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in - lenv, aa, D.Abbr vvs - | T.Void ids -> - let lenv = D.push_bind C.start lenv [] (D.Void 0) in - let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in - lenv, aa, D.Void n - in - let f tt = f (D.TBind (aa, bb, tt)) in - xlate_term f st lenv t - -let xlate_term f st lenv t = - TT.contract (xlate_term f st lenv) t - -let mk_contents n tt = function - | T.Decl -> [], E.Abst (n, tt) - | T.Ax -> [], E.Abst (n, tt) - | T.Cong -> [], E.Abst (n, tt) - | T.Def -> [], E.Abbr tt - | T.Th -> [], E.Abbr tt - -let xlate_entity err f gen st = function - | T.Require _ -> - err st - | T.Section (Some name) -> - err {st with path = name :: st.path} - | T.Section None -> - begin match st.path with - | _ :: ptl -> - err {st with path = ptl} - | _ -> assert false - end - | T.Sorts sorts -> - let map st (xix, s) = - let ix = match xix with - | None -> st.sort - | Some ix -> ix - in - {st with sort = H.set_sorts ix [s]} - in - err (List.fold_left map st sorts) - | T.Graph id -> - assert (H.set_graph id); err st - | T.Entity (kind, n, id, meta, t) -> - let uri = uri_of_id st id st.path in - Hashtbl.add henv id uri; - let tt = xlate_term C.start st D.empty_lenv t in -(* - print_newline (); CrgOutput.pp_term print_string tt; -*) - let a, b = mk_contents n tt kind in - let a = if meta <> "" then E.Meta meta :: a else a in - let entity = E.Mark st.line :: a, uri, b in - f {st with line = succ st.line} entity - | T.Generate _ -> - err st - -(* Interface functions ******************************************************) - -let initial_status () = - Hashtbl.clear henv; { - path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri () -} - -let refresh_status st = {st with - mk_uri = G.get_mk_uri () -} - -let crg_of_txt = xlate_entity diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.mli b/helm/software/lambda-delta/src/complete_rg/crgTxt.mli deleted file mode 100644 index 150268a55..000000000 --- a/helm/software/lambda-delta/src/complete_rg/crgTxt.mli +++ /dev/null @@ -1,19 +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 crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) -> - (Txt.command -> unit) -> status -> Txt.command -> 'a 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/text/txtCrg.ml b/helm/software/lambda-delta/src/text/txtCrg.ml new file mode 100644 index 000000000..980b74a08 --- /dev/null +++ b/helm/software/lambda-delta/src/text/txtCrg.ml @@ -0,0 +1,161 @@ +(* + ||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 H = Hierarchy +module C = Cps +module G = Options +module E = Entity +module T = Txt +module TT = TxtTxt +module D = Crg + +type status = { + path : T.id list; (* current section path *) + line : int; (* line number *) + sort : int; (* first default sort index *) + mk_uri: G.uri_generator (* uri generator *) +} + +let henv_size = 7000 (* hash tables initial size *) + +let henv = Hashtbl.create henv_size (* optimized global environment *) + +(* Internal functions *******************************************************) + +let name_of_id ?(r=true) id = E.Name (id, r) + +let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) + +let mk_gref f uri = f (D.TGRef ([], uri)) + +let uri_of_id st id path = + let str = String.concat "/" path in + let str = Filename.concat str id in + let str = st.mk_uri str in + U.uri_of_string str + +let resolve_gref err f st id = + try f (Hashtbl.find henv id) + with Not_found -> err () + +let rec xlate_term f st lenv = function + | T.Inst _ + | T.Impl _ -> assert false + | T.Sort h -> + f (D.TSort ([], h)) + | T.NSrt id -> + let f h = f (D.TSort ([], h)) in + H.sort_of_string C.err f id + | T.LRef (i, j) -> + D.get_index C.err (mk_lref f i j) i j lenv + | T.NRef id -> + let err () = resolve_gref C.err (mk_gref f) st id in + D.resolve_lref err (mk_lref f) id lenv + | T.Cast (u, t) -> + let f uu tt = f (D.TCast ([], uu, tt)) in + let f uu = xlate_term (f uu) st lenv t in + xlate_term f st lenv u + | T.Appl (vs, t) -> + let map f = xlate_term f st lenv in + let f vvs tt = f (D.TAppl ([], vvs, tt)) in + let f vvs = xlate_term (f vvs) st lenv t in + C.list_map f map vs + | T.Bind (n, b, t) -> + let abst_map (lenv, a, wws) (id, r, w) = + let attr = name_of_id ~r id in + let ww = xlate_term C.start st lenv w in + D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws + in + let abbr_map (lenv, a, wws) (id, w) = + let attr = name_of_id id in + let ww = xlate_term C.start st lenv w in + D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws + in + let void_map (lenv, a, n) id = + let attr = name_of_id id in + D.push2 C.err C.start lenv ~attr (), attr :: a, succ n + in + let lenv, aa, bb = match b with + | T.Abst xws -> + let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in + let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in + lenv, aa, D.Abst (n, wws) + | T.Abbr xvs -> + let lenv = D.push_bind C.start lenv [] (D.Abbr []) in + let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in + lenv, aa, D.Abbr vvs + | T.Void ids -> + let lenv = D.push_bind C.start lenv [] (D.Void 0) in + let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in + lenv, aa, D.Void n + in + let f tt = f (D.TBind (aa, bb, tt)) in + xlate_term f st lenv t + +let xlate_term f st lenv t = + TT.contract (xlate_term f st lenv) t + +let mk_contents n tt = function + | T.Decl -> [], E.Abst (n, tt) + | T.Ax -> [], E.Abst (n, tt) + | T.Cong -> [], E.Abst (n, tt) + | T.Def -> [], E.Abbr tt + | T.Th -> [], E.Abbr tt + +let xlate_entity err f gen st = function + | T.Require _ -> + err st + | T.Section (Some name) -> + err {st with path = name :: st.path} + | T.Section None -> + begin match st.path with + | _ :: ptl -> + err {st with path = ptl} + | _ -> assert false + end + | T.Sorts sorts -> + let map st (xix, s) = + let ix = match xix with + | None -> st.sort + | Some ix -> ix + in + {st with sort = H.set_sorts ix [s]} + in + err (List.fold_left map st sorts) + | T.Graph id -> + assert (H.set_graph id); err st + | T.Entity (kind, n, id, meta, t) -> + let uri = uri_of_id st id st.path in + Hashtbl.add henv id uri; + let tt = xlate_term C.start st D.empty_lenv t in +(* + print_newline (); CrgOutput.pp_term print_string tt; +*) + let a, b = mk_contents n tt kind in + let a = if meta <> "" then E.Meta meta :: a else a in + let entity = E.Mark st.line :: a, uri, b in + f {st with line = succ st.line} entity + | T.Generate _ -> + err st + +(* Interface functions ******************************************************) + +let initial_status () = + Hashtbl.clear henv; { + path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri () +} + +let refresh_status st = {st with + mk_uri = G.get_mk_uri () +} + +let crg_of_txt = xlate_entity diff --git a/helm/software/lambda-delta/src/text/txtCrg.mli b/helm/software/lambda-delta/src/text/txtCrg.mli new file mode 100644 index 000000000..150268a55 --- /dev/null +++ b/helm/software/lambda-delta/src/text/txtCrg.mli @@ -0,0 +1,19 @@ +(* + ||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 crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) -> + (Txt.command -> unit) -> status -> Txt.command -> 'a 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/metaBag.mli b/helm/software/lambda-delta/src/toplevel/metaBag.mli deleted file mode 100644 index 62ce68f4e..000000000 --- a/helm/software/lambda-delta/src/toplevel/metaBag.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 bag_of_meta: (Bag.term -> 'a) -> Meta.entry -> 'a 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;