From 88977b2d546e547e23b046792fe2ad8f6ff192a4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 9 Jan 2018 19:53:51 +0100 Subject: [PATCH] update in helena MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit - new system of attributes for terms - exportation to λΥP λProlog engine - now based on ocamlbuild --- .gitignore | 3 + helm/software/helena/Make | 2 - helm/software/helena/Makefile | 144 +++++------ helm/software/helena/Makefile.common | 157 ++++-------- helm/software/helena/README | 2 +- helm/software/helena/src/Make | 1 - helm/software/helena/src/automath/Make | 1 - helm/software/helena/src/automath/autCrg.ml | 104 ++++---- helm/software/helena/src/basic_ag/Make | 2 - helm/software/helena/src/basic_ag/bagCrg.ml | 2 +- .../software/helena/src/basic_ag/bagOutput.ml | 6 +- .../helena/src/basic_ag/bagReduction.ml | 22 +- helm/software/helena/src/basic_ag/bagType.ml | 8 +- .../helena/src/basic_ag/bagUntrusted.ml | 10 +- helm/software/helena/src/basic_rg/Make | 3 - helm/software/helena/src/basic_rg/brg.ml | 18 +- .../src/basic_rg/{brgGallina.ml => brgCoq.ml} | 22 +- .../basic_rg/{brgGallina.mli => brgCoq.mli} | 0 helm/software/helena/src/basic_rg/brgCrg.ml | 8 +- .../src/basic_rg/{brgLP.ml => brgHelena.ml} | 44 ++-- .../src/basic_rg/{brgLP.mli => brgHelena.mli} | 0 helm/software/helena/src/basic_rg/brgLYP.ml | 226 ++++++++++++++++++ helm/software/helena/src/basic_rg/brgLYP.mli | 16 ++ .../basic_rg/{brgGrafite.ml => brgMatita.ml} | 24 +- .../{brgGrafite.mli => brgMatita.mli} | 0 .../software/helena/src/basic_rg/brgOutput.ml | 6 +- .../helena/src/basic_rg/brgReduction.ml | 6 +- .../helena/src/basic_rg/brgSubstitution.ml | 2 +- helm/software/helena/src/basic_rg/brgType.ml | 18 +- .../helena/src/basic_rg/brgUntrusted.ml | 16 +- .../helena/src/basic_rg/brgValidity.ml | 8 +- helm/software/helena/src/common/Make | 1 - helm/software/helena/src/common/entity.ml | 45 +++- helm/software/helena/src/common/options.ml | 24 +- helm/software/helena/src/complete_rg/Make | 1 - helm/software/helena/src/complete_rg/crg.ml | 57 ++--- .../helena/src/complete_rg/crgOutput.ml | 6 +- helm/software/helena/src/lib/Make | 1 - helm/software/helena/src/modules.ml | 8 +- helm/software/helena/src/text/Make | 1 - helm/software/helena/src/text/txtCrg.ml | 18 +- helm/software/helena/src/toplevel/Make | 1 - .../helena/src/toplevel/{top.ml => helena.ml} | 41 +++- helm/software/helena/src/xml/Make | 1 - helm/software/helena/src/xml/xmlCrg.ml | 32 +-- helm/software/helena/src/xml/xmlLibrary.ml | 18 +- helm/software/helena/src/xml/xmlLibrary.mli | 8 +- 47 files changed, 686 insertions(+), 458 deletions(-) delete mode 100644 helm/software/helena/src/Make delete mode 100644 helm/software/helena/src/automath/Make delete mode 100644 helm/software/helena/src/basic_ag/Make delete mode 100644 helm/software/helena/src/basic_rg/Make rename helm/software/helena/src/basic_rg/{brgGallina.ml => brgCoq.ml} (90%) rename helm/software/helena/src/basic_rg/{brgGallina.mli => brgCoq.mli} (100%) rename helm/software/helena/src/basic_rg/{brgLP.ml => brgHelena.ml} (93%) rename helm/software/helena/src/basic_rg/{brgLP.mli => brgHelena.mli} (100%) create mode 100644 helm/software/helena/src/basic_rg/brgLYP.ml create mode 100644 helm/software/helena/src/basic_rg/brgLYP.mli rename helm/software/helena/src/basic_rg/{brgGrafite.ml => brgMatita.ml} (87%) rename helm/software/helena/src/basic_rg/{brgGrafite.mli => brgMatita.mli} (100%) delete mode 100644 helm/software/helena/src/common/Make delete mode 100644 helm/software/helena/src/complete_rg/Make delete mode 100644 helm/software/helena/src/lib/Make delete mode 100644 helm/software/helena/src/text/Make delete mode 100644 helm/software/helena/src/toplevel/Make rename helm/software/helena/src/toplevel/{top.ml => helena.ml} (94%) delete mode 100644 helm/software/helena/src/xml/Make diff --git a/.gitignore b/.gitignore index a433c4179..6671ac4fd 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,7 @@ _build *.native +*.byte matita/Makefile.defs matita/autom4te.cache @@ -34,6 +35,8 @@ matita/matita/matitaclean.opt matita/matita/help/C/version.txt +helm/software/helena/matita + matita/matita/contribs/lambdadelta/token matita/matita/contribs/lambdadelta/2A1 matita/matita/contribs/lambdadelta/apps_2/notation diff --git a/helm/software/helena/Make b/helm/software/helena/Make index 058236bd8..aa92833bc 100644 --- a/helm/software/helena/Make +++ b/helm/software/helena/Make @@ -1,4 +1,3 @@ -.depend.opt Make* README examples/automath/*.aut @@ -7,5 +6,4 @@ scripts/coq/*.v scripts/coq/*.template scripts/lp/*.template src/*.ml -src/Make* src/*/* diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 6194e6c4c..38dab9e6b 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -1,21 +1,33 @@ -MAIN = helena - SRC = src +DIRECTORIES = $(shell find $(SRC) -type d) + +ALL_FEATURES = LEXER PARSER TRACE SUMMARY EXPAND MANAGER OBJECTS PREPROCESS QUOTE STAGE TYPE + +FF = $(F:ALL=$(ALL_FEATURES)) + +EXEC = helena + REQUIRES = unix str helm-ng_kernel OCAMLOPTIONS = -rectypes +CAMLPOPTIONS = $(FF:%=-D%) + +BUILDOPTIONS = -Is "$(DIRECTORIES)" + KEEP = README CLEAN = etc/log.txt etc/profile.txt -TAGS = test-si-fast test-si test2-opt test2-byte test3 test6 \ - profile-fast profile profile-coq profile-coq-byte \ - xml-si xml-si-v3 xml xml-v3 \ - export-coq export-matita \ - export-lp1 export-lp2 export-tj2 export-tj3 \ - matita matitac +TARGETS = test-si-fast test-si test2-opt test2-byte test3 test6 \ + profile-fast profile profile-coq profile-coq-byte \ + xml-si xml-si-v3 xml xml-v3 \ + export-coq export-matita \ + export-lp1 export-lp2 export-tj2 export-tj3 export-lyp \ + matita matitac + +include Makefile.common TIME = `which time` -p -a -o etc/log.txt @@ -41,130 +53,128 @@ LP1 = grundlagen_21.elpi LP2 = grundlagen_22.elpi TJ2 = grundlagen_22.mod TJ3 = grundlagen_23.mod +CC0 = grundlagen_20.elpi +LYP = grundlagen_2b_lyp.elpi PREAMBLE_MA = ../matita/matita.ma.templ PREAMBLE_V = $(OUTPUT)/coq/grundlagen.template PREAMBLE_LP = $(OUTPUT)/lp/lp.template -ALL_FEATURES = LEXER PARSER TRACE SUMMARY EXPAND MANAGER OBJECTS PREPROCESS QUOTE STAGE TYPE - TEST1 = -T 1 -l -u -1 $(O) $(INPUT) TEST2 = -X -T 2 -l -1 $(O) $(INPUT) -all: .depend.opt .depend.byte - @$(CALLMAKE) $(MAIN).opt F="$(ALL_FEATURES)" - @$(CALLMAKE) $(MAIN).byte F="$(ALL_FEATURES)" - -opt: .depend.opt - @$(CALLMAKE) F="$(ALL_FEATURES)" $(MAIN).opt - -byte: .depend.byte - @$(CALLMAKE) F="$(ALL_FEATURES)" $(MAIN).byte - -test-si-fast: $(MAIN).opt etc +test-si-fast: $(EXEC).native etc @echo " HELENA -u -x -y -1 $(INPUTFAST)" - $(H)./$(MAIN).opt -T 1 -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt + $(H)./$(EXEC).native -T 1 -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt -test-si: $(MAIN).opt etc +test-si: $(EXEC).native etc @echo " HELENA -d -l -u -0 $(INPUT)" - $(H)./$(MAIN).opt -T 2 -d -l -u -0 $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -T 2 -d -l -u -0 $(O) $(INPUT) > etc/log.txt -test1: $(MAIN).opt etc +test1: $(EXEC).native etc @echo " HELENA -l -u -1 $(INPUT)" - $(H)./$(MAIN).opt $(TEST1) > etc/log.txt + $(H)./$(EXEC).native $(TEST1) > etc/log.txt -test2-opt: $(MAIN).opt etc +test2-opt: $(EXEC).native etc @echo " HELENA -l -1 $(INPUT)" - $(H)./$(MAIN).opt $(TEST1) $(TEST2) > etc/log.txt + $(H)./$(EXEC).native $(TEST1) $(TEST2) > etc/log.txt -test2-byte: $(MAIN).byte etc +test2-byte: $(EXEC).byte etc @echo " HELENA -l -1 $(INPUT)" - $(H)./$(MAIN).byte $(TEST1) $(TEST2) > etc/log.txt + $(H)./$(EXEC).byte $(TEST1) $(TEST2) > etc/log.txt -test3: $(MAIN).opt etc +test3: $(EXEC).native etc @echo " HELENA -T 3 -l $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 3 -l $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -l -u $(O) $(INPUT) -X -T 3 -l $(O) $(INPUT) > etc/log.txt -test6: $(MAIN).opt etc +test6: $(EXEC).native etc @echo " HELENA -T 6 -l $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt -profile-fast: $(MAIN).opt etc +profile-fast: $(EXEC).native etc @echo " HELENA -u -x -y -1 $(INPUTFAST) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -u -x -y -1 $(O) $(INPUTFAST) >> etc/log.txt; done + $(H)for T in `seq 31`; do ./$(EXEC).native -T 1 -u -x -y -1 $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt -profile: $(MAIN).opt etc +profile: $(EXEC).native etc @echo " HELENA -l -u -1 $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do ./$(MAIN).opt $(TEST1) >> etc/log.txt; done + $(H)for _ in `seq 31`; do ./$(EXEC).native $(TEST1) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt -profile-opt: $(MAIN).opt etc +profile-opt: $(EXEC).native etc @echo " HELENA -l -1 $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do ./$(MAIN).opt $(TEST1) $(TEST2) >> etc/log.txt; done + $(H)for _ in `seq 31`; do ./$(EXEC).native $(TEST1) $(TEST2) >> etc/log.txt; done $(H)grep "processed" etc/log.txt | sort -k 6 | uniq > etc/profile.txt -profile-byte: $(MAIN).byte etc +profile-byte: $(EXEC).byte etc @echo " HELENA -l -1 $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do ./$(MAIN).byte $(TEST1) $(TEST2) >> etc/log.txt; done + $(H)for _ in `seq 31`; do ./$(EXEC).byte $(TEST1) $(TEST2) >> etc/log.txt; done $(H)grep "processed" etc/log.txt | sort -k 6 | uniq > etc/profile.txt -profile-coq: $(MAIN).opt etc +profile-coq: etc @echo " COQTOP $(V) (31 TIMES)" $(H)rm -f etc/log.txt $(H)for _ in `seq 31`; do echo Load \"$(OUTPUT)/coq/$(V)\". | $(TIME) $(COQTOP) -q $(NULL); done $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt -profile-coq-byte: $(MAIN).opt etc +profile-coq-byte: etc @echo " COQTOP $(V) (31 TIMES)" $(H)rm -f etc/log.txt $(H)for _ in `seq 31`; do echo Load \"$(OUTPUT)/coq/$(V)\". | $(TIME) $(COQTOP).byte -q $(NULL); done $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt -xml-si: $(MAIN).opt etc +xml-si: $(EXEC).native etc @echo " HELENA -l -o -q -s 1 -u -y $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -q -s 1 -u -y $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -O $(XMLDIR) -T 1 -l -o -q -s 1 -u -y $(O) $(INPUT) > etc/log.txt -xml-si-v3: $(MAIN).opt etc +xml-si-v3: $(EXEC).native etc @echo " HELENA -l -o -q -s 2 -u -y $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -q -s 2 -u -y $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -O $(XMLDIR) -T 1 -l -o -q -s 2 -u -y $(O) $(INPUT) > etc/log.txt -xml: $(MAIN).opt etc +xml: $(EXEC).native etc @echo " HELENA -l -o -q -s 1 -y $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -q -s 1 -y $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -q -s 1 -y $(O) $(INPUT) > etc/log.txt -xml-v3: $(MAIN).opt etc +xml-v3: $(EXEC).native etc @echo " HELENA -l -o -q -s 2 -y $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -q -s 2 -y $(O) $(INPUT) > etc/log.txt + $(H)./$(EXEC).native -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -q -s 2 -y $(O) $(INPUT) > etc/log.txt -export-coq $(OUTPUT)/coq/$(V): $(MAIN).opt etc +export-coq $(OUTPUT)/coq/$(V): $(EXEC).native etc @echo " HELENA -m V8 -q $(INPUT)" - $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(TEST1) > etc/log.txt -export-matita $(OUTPUT)/matita/$(MA): $(MAIN).opt etc +export-matita $(OUTPUT)/matita/$(MA): $(EXEC).native etc @echo " HELENA -m MA2 -q $(INPUT)" - $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(TEST1) > etc/log.txt -export-lp1 $(OUTPUT)/lp/$(LP1): $(MAIN).opt etc +export-lp1 $(OUTPUT)/lp/$(LP1): $(EXEC).native etc @echo " HELENA -m LP1 -q $(INPUT)" - $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -export-lp2 $(OUTPUT)/lp/$(LP2): $(MAIN).opt etc +export-lp2 $(OUTPUT)/lp/$(LP2): $(EXEC).native etc @echo " HELENA -m LP2 -q $(INPUT)" - $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -export-tj2 $(OUTPUT)/lp/$(TJ2): $(MAIN).opt etc +export-tj2 $(OUTPUT)/lp/$(TJ2): $(EXEC).native etc @echo " HELENA -m TJ2 -q $(INPUT)" - $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -export-tj3 $(OUTPUT)/lp/$(TJ3): $(MAIN).opt etc +export-tj3 $(OUTPUT)/lp/$(TJ3): $(EXEC).native etc @echo " HELENA -m TJ3 -q $(INPUT)" - $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + +export-cc0 $(OUTPUT)/cc/$(CC0): $(EXEC).native etc + @echo " HELENA -m CC0 -q $(INPUT)" + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m CC0 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + +export-lyp $(OUTPUT)/lp/$(LYP): $(EXEC).native etc + @echo " HELENA -m lyp -q $(INPUT)" + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m lyp -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt matita: $(OUTPUT)/matita/$(MA) @echo " MATITA $(MA)" @@ -174,10 +184,8 @@ matitac: $(OUTPUT)/matita/$(MA) @echo " MATITAC $(MA)" $(H)cd matita && $(MATITAC) $(MA) -#profile-matita: $(MAIN).opt etc +#profile-matita: $(EXEC).native etc # @echo " HELENA -u $(INPUT) (1 TIMES)" # $(H)rm -f etc/log.txt -# $(H)for T in `seq 1`; do ./$(MAIN).opt -T 1 -M $(OUTPUT) -a n -l -m $(PREAMBLE) -o -u $(INPUT) >> etc/log.txt; done +# $(H)for T in `seq 1`; do ./$(EXEC).native -T 1 -M $(OUTPUT) -a n -l -m $(PREAMBLE) -o -u $(INPUT) >> etc/log.txt; done # $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt - -include Makefile.common diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common index 1db6ea340..dee058728 100644 --- a/helm/software/helena/Makefile.common +++ b/helm/software/helena/Makefile.common @@ -1,125 +1,58 @@ H=@ -OCAMLPATH ?= /home/fguidi/svn/matita_patched/components/METAS -OCAMLFIND = OCAMLPATH=$(OCAMLPATH) ocamlfind - -RELISE = $(MAIN:%=%_$(shell cat MakeVersion)) - -DOWNDIR = ../../www/lambdadelta/download - -DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make)) - -INCLUDES = $(DIRECTORIES:%=-I %) - -CAMLP = -pp "camlp5o pa_macro.cmo $(CAMLPOPTIONS)" - -CAMLPOPTIONS = $(F:%=-D%) - -OCAMLDEP = $(OCAMLFIND) ocamldep $(CAMLP) $(INCLUDES) -OCAMLOPT = $(OCAMLFIND) ocamlopt $(CAMLP) $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES) -OCAMLC = $(OCAMLFIND) ocamlc $(CAMLP) $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES) -OCAMLLEX = ocamllex.opt -OCAMLYACC = ocamlyacc -v -TAR = tar -czf etc/$(MAIN:%=%.tgz) - CALLMAKE = $(MAKE) --no-print-directory -define DIR_TEMPLATE - MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make)) -endef - -define MOD_TEMPLATE - SOURCES += $$(if $$(wildcard $(1).ml[yi]),$(1).mli $(1).ml,$(1).ml) - CMXS += $(1).cmx - CMOS += $(1).cmo - CLEAN += $(1).cmi $(1).cmx $(1).o $(1).cmo - CLEAN += $$(if $$(wildcard $(1).ml[ly]),$(1).ml,) - CLEAN += $$(if $$(wildcard $(1).mly),$(1).mli $(1).output,) - KEEP += $$(if $$(wildcard $(1).mly),$(1).mly,\ - $$(if $$(wildcard $(1).mll),$(1).mll,\ - $$(if $$(wildcard $(1).mli),$(1).mli $(1).ml,$(1).ml)\ - )\ - ) -endef - -define INCLUDE_O_TEMPLATE - ifeq ($(MAKECMDGOALS), $(1)) -%.cmi: %.mli - @echo " OCAMLOPT $$<" - $$(H)$(OCAMLOPT) -c $$< - -include .depend.opt - endif -endef - -define INCLUDE_B_TEMPLATE - ifeq ($(MAKECMDGOALS), $(1)) -%.cmi: %.mli - @echo " OCAMLC $$<" - $$(H)$(OCAMLC) -c $$< - -include .depend.byte - endif -endef +OCAMLPATH ?= `readlink -f -n ./matita/components/METAS` +OCAMLFIND = OCAMLPATH=$(OCAMLPATH) ocamlfind -$(foreach DIR, $(DIRECTORIES), $(eval $(call DIR_TEMPLATE, $(DIR)))) -$(foreach MOD, $(MODULES), $(eval $(call MOD_TEMPLATE, $(MOD)))) -O_OBJECTS = $(patsubst %.ml,%.cmx,$(SOURCES:%.mli=%.cmi)) -B_OBJECTS = $(patsubst %.ml,%.cmo,$(SOURCES:%.mli=%.cmi)) +CAMLP = -pp \"camlp5o pa_macro.cmo $(CAMLPOPTIONS)\" -CLEAN += $(MAIN).opt +OCAMLDEP = $(OCAMLFIND) ocamldep $(CAMLP) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(CAMLP) $(OCAMLOPTIONS) -linkpkg -package \"$(REQUIRES)\" +OCAMLC = $(OCAMLFIND) ocamlc $(CAMLP) $(OCAMLOPTIONS) -linkpkg -package \"$(REQUIRES)\" +OCAMLYACC = ocamlyacc -v +OCAMLLEX = ocamllex.opt -$(MAIN).opt: $(O_OBJECTS) - @echo " OCAMLOPT -o $(MAIN).opt" - $(H)$(OCAMLOPT) -o $(MAIN).opt $(CMXS) +BUILDCMDS = -ocamldep "$(OCAMLDEP)" \ + -ocamlc "$(OCAMLC)" \ + -ocamlopt "$(OCAMLOPT)" \ + -ocamlyacc "$(OCAMLYACC)" \ + -ocamllex "$(OCAMLLEX)" -$(MAIN).byte: $(B_OBJECTS) - @echo " OCAMLC -o $(MAIN).byte" - $(H)$(OCAMLC) -o $(MAIN).byte $(CMOS) +all: opt byte -.depend.opt: $(SOURCES) - @echo " OCAMLDEP -native" - $(H)$(OCAMLDEP) -native $^ > .depend.opt +opt: + @echo " OCAMLBUILD $(EXEC).native" + $(H)ocamlbuild $(BUILDCMDS) $(BUILDOPTIONS) $(EXEC).native -.depend.byte: $(SOURCES) - @echo " OCAMLDEP -byte" - $(H)$(OCAMLDEP) $^ > .depend.byte +byte: + @echo " OCAMLBUILD $(EXEC).byte" + $(H)ocamlbuild $(BUILDCMDS) $(BUILDOPTIONS) $(EXEC).byte clean: - @echo " CLEAN . $(SRC)" + @echo " OCAMLBUILD -clean" +# $(H)ocamlbuild -clean + $(H)$(RM) -r _build $(EXEC).native $(EXEC).byte $(H)find -name "*~" | xargs $(RM) $(CLEAN) -relise: clean - @echo " RELISE $(RELISE)" - $(H)mkdir -p $(RELISE) - $(H)$(foreach FILE, $(shell cat Make), cp --parents $(FILE) $(RELISE);) - $(H)tar -czf etc/$(RELISE).tar.gz $(RELISE) - $(H)scp etc/$(RELISE).tar.gz $(DOWNDIR) - -tgz: clean - @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)" - $(H)find -name "Make*" | xargs $(TAR) $(KEEP) - -etc: - @echo " MKDIR etc" - $(H)mkdir etc - -%.ml %.mli: %.mly - @echo " OCAMLYACC $<" - $(H)$(OCAMLYACC) $< -%.ml: %.mll - @echo " OCAMLLEX $<" - $(H)$(OCAMLLEX) $< -%.cmx: %.ml - @echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) -c $< -%.cmo: %.ml - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< - -O_TAGS += opt $(MAIN).opt - -B_TAGS += byte $(MAIN).byte - -$(foreach TAG, $(O_TAGS), $(eval $(call INCLUDE_O_TEMPLATE, $(TAG)))) - -$(foreach TAG, $(B_TAGS), $(eval $(call INCLUDE_B_TEMPLATE, $(TAG)))) +.PHONY: all opt byte clean $(TARGETS) + +#RELISE = $(EXEC:%=%_$(shell cat MakeVersion)) +# +#DOWNDIR = ../../www/lambdadelta/download +# +#TAR = tar -czf etc/$(EXEC:%=%.tgz) +# +#relise: clean +# @echo " RELISE $(RELISE)" +# $(H)mkdir -p $(RELISE) +# $(H)$(foreach FILE, $(shell cat Make), cp --parents $(FILE) $(RELISE);) +# $(H)tar -czf etc/$(RELISE).tar.gz $(RELISE) +# $(H)scp etc/$(RELISE).tar.gz $(DOWNDIR) +# +#tgz: clean +# @echo " TAR -czf $(EXEC:%=%.tgz) . $(DIRECTORIES)" +# $(H)find -name "Make*" | xargs $(TAR) $(KEEP) +# +#etc: +# @echo " MKDIR etc" +# $(H)mkdir -p etc diff --git a/helm/software/helena/README b/helm/software/helena/README index 37f553a25..3a7b77d67 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -43,7 +43,7 @@ TYPE enable option -t (if unset, -t is disabled) xml-si xml-si-v3 xml xml-v3 * Set at least F="MANAGER QUOTE" for targets: - export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 + export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 export-cc0 export-lyp * Type "make profile.opt" or "make profile.byte" to validate the "grundlagen" 31 times (two runs each time) diff --git a/helm/software/helena/src/Make b/helm/software/helena/src/Make deleted file mode 100644 index 9e637c2c0..000000000 --- a/helm/software/helena/src/Make +++ /dev/null @@ -1 +0,0 @@ -lib common complete_rg text automath xml basic_rg basic_ag toplevel diff --git a/helm/software/helena/src/automath/Make b/helm/software/helena/src/automath/Make deleted file mode 100644 index 094f99eb4..000000000 --- a/helm/software/helena/src/automath/Make +++ /dev/null @@ -1 +0,0 @@ -aut autProcess autOutput autParser autLexer autCrg diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 5ed896306..d1a72518b 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -24,7 +24,7 @@ type qid = D.uri * D.id * D.id list type context_node = qid option (* context node: None = root *) type status = { - path: D.id list; (* current section path *) + path: D.id list; (* current section path *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) @@ -44,28 +44,29 @@ let empty_cnt = D.empty_lenv let alpha id = if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id -let attrs_for_abst id aw = +let attrs_for_appl yv yt = + E.appl_attrs ~side:yv ~main:yt !G.restricted + +let attrs_for_abst id yw = let id = if !G.alpha <> "" then alpha id else id in - let main = E.succ aw.E.b_main in - E.bind_attrs ~name:(id, true) ~side:aw.E.b_main ~main () + E.bind_attrs ~name:(id, true) ~side:yw ~main:(E.succ yw) () -let attrs_for_decl aw = - let main = E.succ aw.E.b_main in - E.bind_attrs ~side:aw.E.b_main ~main () +let attrs_for_env y = + E.env_attrs ~side:y () -let add_abst cnt id aw w = - let y = attrs_for_abst id aw in +let add_abst cnt id yw w = + let a = attrs_for_abst id yw in let l = if !G.infinity then N.infinity else N.two in - D.EBind (cnt, E.empty_node, y, D.Abst (false, l, w)) + D.EBind (cnt, E.empty_node, a, D.Abst (false, l, w)) -let mk_lref f _ y i = f y (D.TLRef (E.empty_node, i)) +let mk_lref f _ a i = f a.E.b_main (D.TLRef (E.empty_node, i)) let id_of_name (id, _, _) = if !G.alpha <> "" then alpha id else id let mk_qid f lst id path = let str = String.concat "/" path in - let str = Filename.concat str id in + let str = Filename.concat str id in let str = lst.mk_uri str in f (U.uri_of_string str, id, path) @@ -96,7 +97,7 @@ let resolve_gref err f lst qid = with Not_found -> err qid let resolve_gref_relaxed f lst qid = -(* this is not tail recursive *) +(* this is not tail recursive *) let rec err qid = relax_qid (resolve_gref err f lst) lst qid in resolve_gref err f lst qid @@ -107,23 +108,23 @@ let get_cnt err f lst = function with Not_found -> err node let get_cnt_relaxed f lst = -(* this is not tail recursive *) +(* this is not tail recursive *) let rec err node = relax_opt_qid (get_cnt err f lst) lst node in get_cnt err f lst lst.node -let push_abst f y w lenv = +let push_abst f a w lenv = let bw = D.Abst (false, N.infinity, w) in - D.push_bind f E.empty_node y bw lenv + D.push_bind f E.empty_node a bw lenv (* let rec set_name_y f = function | D.ESort -> f D.ESort | D.EBind (e, a, y, b) -> set_name_y (D.push_bind f a {y with E.b_name = Some ("Y", true)} b) e - | D.EAppl (e, x, v) -> set_name_y (D.push_appl f x v) e + | D.EAppl (e, a, v) -> set_name_y (D.push_appl f a v) e | D.EProj (e, d) -> let f d = set_name_y (D.push_proj f d) e in set_name_y f d *) let add_proj yt e t = match e with | D.ESort -> t - | D.EBind (D.ESort, _, y, b) -> D.TBind (E.compose y yt, b, t) + | D.EBind (D.ESort, _, a, b) -> D.TBind (E.compose a yt, b, t) | e -> D.TProj (D.set_attrs C.start yt e, t) @@ -131,21 +132,19 @@ let add_proj yt e t = match e with let rec xlate_term f st lst z lenv = function | A.Sort s -> let k = if s then 0 else 1 in - let y = E.bind_attrs ~main:(k, 0) () in - f y (D.TSort k) + f (k, 0) (D.TSort k) | A.Appl (v, t) -> - let f vv yt tt = - f yt (D.TAppl (!G.extended, vv, tt)) + let f yv vv yt tt = + f yt (D.TAppl (attrs_for_appl yv yt, vv, tt)) in - let f _ vv = xlate_term (f vv) st lst z lenv t in + let f yv vv = xlate_term (f yv vv) st lst z lenv t in xlate_term f st lst false lenv v | A.Abst (name, w, t) -> let f yw ww = - let yw = attrs_for_abst name yw in + let a = attrs_for_abst name yw in let f yt tt = - let yt = E.compose yw yt in - let l = - if !G.cc then match z, snd yt.E.b_main with + let l = + if !G.cc then match z, snd yt with | true, _ -> N.one | _ , 0 -> N.one | _ , 1 -> N.unknown st @@ -155,26 +154,26 @@ let rec xlate_term f st lst z lenv = function in let b = D.Abst (false, l, ww) in (* let yt = {yt with E.b_name = Some ("P", true)} in *) - f yt (D.TBind (yt, b, tt)) + f yt (D.TBind (E.compose a yt, b, tt)) in let f lenv = xlate_term f st lst z lenv t in - push_abst f yw ww lenv + push_abst f a ww lenv in xlate_term f st lst true lenv w | A.GRef (name, args) -> let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in - let map2 f arg args = - let f _ v = f (D.EAppl (args, !G.extended, v)) in + let map2 y f arg args = + let f yv v = f (D.EAppl (args, attrs_for_appl yv y, v)) in xlate_term f st lst false lenv arg in let g qid y cnt = let gref = D.TGRef (E.empty_node, uri_of_qid qid) in if cnt = D.ESort then f y gref else - let f = function - | D.EAppl (D.ESort, x, v) -> f y (D.TAppl (x, v, gref)) + let f = function + | D.EAppl (D.ESort, a, v) -> f y (D.TAppl (a, v, gref)) | args -> f y (D.TProj (args, gref)) in - let f args = C.list_fold_right f map2 args D.ESort in + let f args = C.list_fold_right f (map2 y) args D.ESort in D.sub_list_strict (D.fold_names f map1 args) cnt args in let g qid = resolve_gref_relaxed g lst qid in @@ -186,7 +185,7 @@ let xlate_entity err f st lst = function err {lst with path = name :: lst.path; nodes = lst.node :: lst.nodes} | A.Section None -> begin match lst.path, lst.nodes with - | _ :: ptl, nhd :: ntl -> + | _ :: ptl, nhd :: ntl -> err {lst with path = ptl; node = nhd; nodes = ntl} | _ -> assert false end @@ -194,12 +193,12 @@ let xlate_entity err f st lst = function err {lst with node = None} | A.Context (Some name) -> let f name = err {lst with node = Some name} in - complete_qid f lst name + complete_qid f lst name | A.Block (name, w) -> - let f qid = + let f qid = let f cnt = - let f aw ww = - UH.add hcnt (uri_of_qid qid) (add_abst cnt name aw ww); + let f yw ww = + UH.add hcnt (uri_of_qid qid) (add_abst cnt name yw ww); err {lst with node = Some qid} in xlate_term f st lst true cnt w @@ -209,13 +208,14 @@ let xlate_entity err f st lst = function complete_qid f lst (name, true, []) | A.Decl (name, w) -> let f lenv = - let f qid = + let f qid = let f yw ww = - let y = attrs_for_decl yw in - UH.add henv (uri_of_qid qid) (y, lenv); + let yv = E.succ yw in + let a = attrs_for_env yv in + UH.add henv (uri_of_qid qid) (yv, lenv); let t = add_proj yw lenv ww in let na = E.node_attrs ~apix:lst.line () in - let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in + let entity = E.empty_root, na, uri_of_qid qid, E.abst a t in IFDEF TRACE THEN G.set_current_trace lst.line ELSE () END; @@ -225,22 +225,24 @@ ELSE () END; in complete_qid f lst (name, true, []) in - let f = if !G.infinity then f else D.set_layer f N.one in + let f = if !G.infinity then f else D.set_layer f N.one in get_cnt_relaxed f lst | A.Def (name, w, trans, v) -> let f lenv = - let f qid = + let f qid = let f yw ww = let f yv vv = + let a = attrs_for_env yv in UH.add henv (uri_of_qid qid) (yv, lenv); - let t = add_proj yv lenv (D.TCast (ww, vv)) in -(* - let lenv0 = D.set_layer C.start N.one lenv in - let t = D.TCast (add_proj yw lenv0 ww, add_proj yv lenv vv) in -*) + let t = if !G.cast then + let f e = D.TCast (add_proj yw e ww, add_proj yv lenv vv) in + if !G.infinity then f lenv else D.set_layer f N.one lenv + else + add_proj yv lenv (D.TCast (ww, vv)) + in let na = E.node_attrs ~apix:lst.line () in let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in - let entity = ra, na, uri_of_qid qid, E.Abbr t in + let entity = ra, na, uri_of_qid qid, E.abbr a t in IFDEF TRACE THEN G.set_current_trace lst.line ELSE () END; diff --git a/helm/software/helena/src/basic_ag/Make b/helm/software/helena/src/basic_ag/Make deleted file mode 100644 index 74961c692..000000000 --- a/helm/software/helena/src/basic_ag/Make +++ /dev/null @@ -1,2 +0,0 @@ -bag bagCrg bagOutput -bagEnvironment bagSubstitution bagReduction bagType bagUntrusted diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index e9ad2417e..31ce2afa5 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -67,7 +67,7 @@ let rec xlate_bk_term f c = function let f tt = xlate_bk_term (f tt) c u in xlate_bk_term f c t | Z.Appl (u, t) -> - let f tt uu = f (D.TAppl (true, uu, tt)) in + let f tt uu = f (D.TAppl (E.appl_attrs false, uu, tt)) in let f tt = xlate_bk_term (f tt) c u in xlate_bk_term f c t | Z.Bind (y, l, b, t) -> diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index 344c4db06..689423167 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -71,13 +71,13 @@ and count_term f c = function count_term f c t let count_entity f c = function - | _, _, _, E.Abst w -> + | _, _, _, E.Abst (_, w) -> let c = {c with eabsts = succ c.eabsts} in count_term f c w - | _, _, _, E.Abbr v -> + | _, _, _, E.Abbr (_, v) -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index 323de4c9f..e26a7ec1e 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -114,14 +114,14 @@ let rec whd f c m x = let rec ho_whd f c m x = (* L.warn "entering R.ho_whd"; *) let aux m = function - | Sort_ h -> f (Sort h) - | Bind_ (_, _, w, _) -> + | Sort_ h -> f (Sort h) + | Bind_ (_, _, w, _) -> let f w = f (Abst w) in unwind_to_term f m w - | LRef_ (_, Some w) -> ho_whd f c m w - | GRef_ (_, _, _, E.Abst w) -> ho_whd f c m w - | GRef_ (_, _, _, E.Abbr v) -> ho_whd f c m v - | LRef_ (_, None) -> assert false - | GRef_ (_, _, _, E.Void) -> assert false + | LRef_ (_, Some w) -> ho_whd f c m w + | GRef_ (_, _, _, E.Abst (_, w)) -> ho_whd f c m w + | GRef_ (_, _, _, E.Abbr (_, v)) -> ho_whd f c m v + | LRef_ (_, None) -> assert false + | GRef_ (_, _, _, E.Void) -> assert false in whd aux c m x @@ -147,8 +147,8 @@ ELSE () END; | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), GRef_ (_, {E.n_apix = a2}, _, E.Abst _) -> if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false - | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), - GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) -> + | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)), + GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) -> if a1 = a2 then let f a = if a then f a else are_convertible f st true c m1 v1 m2 v2 @@ -157,9 +157,9 @@ ELSE () END; else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 - | _, GRef_ (_, _, _, E.Abbr v2) -> + | _, GRef_ (_, _, _, E.Abbr (_, v2)) -> whd (aux m1 r1) c m2 v2 - | GRef_ (_, _, _, E.Abbr v1), _ -> + | GRef_ (_, _, _, E.Abbr (_, v1)), _ -> whd (aux_rev m2 r2) c m1 v1 | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) -> let l = P.new_mark () in diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index f92919ec7..c7ecb1512 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -64,10 +64,10 @@ ELSE () END; Z.get err0 f c i | Z.GRef uri -> let f = function - | _, _, _, E.Abst w -> f x w - | _, _, _, E.Abbr (Z.Cast (w, v)) -> f x w - | _, _, _, E.Abbr _ -> assert false - | _, _, _, E.Void -> assert false + | _, _, _, E.Abst (_, w) -> f x w + | _, _, _, E.Abbr (_, Z.Cast (w, v)) -> f x w + | _, _, _, E.Abbr _ -> assert false + | _, _, _, E.Void -> assert false in ZE.get_entity f uri | Z.Bind (y, l, Z.Abbr v, t) -> diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.ml b/helm/software/helena/src/basic_ag/bagUntrusted.ml index 0b5fa7dba..dc1a310f9 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.ml +++ b/helm/software/helena/src/basic_ag/bagUntrusted.ml @@ -22,14 +22,14 @@ IFDEF TYPE THEN (* to share *) let type_check err f st = function - | ra, na, uri, E.Abst t -> + | ra, na, uri, E.Abst (a, t) -> let err msg = err (L.Uri uri :: msg) in - let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abst xt) in + let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.abst a xt) in ZT.type_of err f st Z.empty_lenv t - | ra, na, uri, E.Abbr t -> + | ra, na, uri, E.Abbr (a, t) -> let err msg = err (L.Uri uri :: msg) in - let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abbr xt) in + let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.abbr a xt) in ZT.type_of err f st Z.empty_lenv t - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false END diff --git a/helm/software/helena/src/basic_rg/Make b/helm/software/helena/src/basic_rg/Make deleted file mode 100644 index df1b318e5..000000000 --- a/helm/software/helena/src/basic_rg/Make +++ /dev/null @@ -1,3 +0,0 @@ -brg brgCrg brgOutput -brgEnvironment brgSubstitution brgReduction brgValidity brgType brgUntrusted -brgGrafite brgGallina brgLP diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index e6ac94e5b..fcf503c6f 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -17,6 +17,7 @@ module E = Entity type uri = E.uri type n_attrs = E.node_attrs +type a_attrs = E.appl_attrs type b_attrs = E.bind_attrs (* x-reduced abstractions are output by RTM only *) @@ -28,7 +29,7 @@ and term = Sort of int (* hierarchy index *) | LRef of n_attrs * int (* attrs, position index *) | GRef of n_attrs * uri (* attrs, reference *) | Cast of term * term (* type, term *) - | Appl of bool * term * term (* extended?, argument, function *) + | Appl of a_attrs * term * term (* attrs, argument, function *) | Bind of b_attrs * bind * term (* attrs, binder, scope *) type entity = term E.entity (* attrs, uri, binder *) @@ -51,7 +52,7 @@ let gref a u = GRef (a, u) let cast u t = Cast (u, t) -let appl x u t = Appl (x, u, t) +let appl a u t = Appl (a, u, t) let bind y b t = Bind (y, b, t) @@ -72,12 +73,17 @@ let rec get e i = match e with | Cons (e, c, a, y, b) when i = 0 -> e, c, a, y, b | Cons (e, _, _, _, _) -> get e (pred i) +let rec mem err f e y0 = match e with + | Null -> err () + | Cons (e, _, _, y, _) -> + if y.E.b_name = y0.E.b_name then f () else mem err f e y0 + (* used in BrgOutput.pp_lenv *) let rec fold_right f map e x = match e with | Null -> f x | Cons (e, c, a, y, b) -> fold_right (map f c a y b) map e x -let rec mem err f e y0 = match e with - | Null -> err () - | Cons (e, _, _, y, _) -> - if y.E.b_name = y0.E.b_name then f () else mem err f e y0 +(* used in BrgCC.output_entity_cc0 *) +let rec fold_left map x e = match e with + | Null -> x + | Cons (e, c, a, y, b) -> fold_left map (map x c a y b) e diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgCoq.ml similarity index 90% rename from helm/software/helena/src/basic_rg/brgGallina.ml rename to helm/software/helena/src/basic_rg/brgCoq.ml index 7346e5835..3a3dea1e6 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ b/helm/software/helena/src/basic_rg/brgCoq.ml @@ -93,24 +93,24 @@ let rec out_term st p e och = function let pt = match t with B.Appl _ -> false | _ -> true in let op, cp = if p then "(", ")" else "", "" in KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp - | B.Bind (y, B.Abst (r, n, w), t) -> + | B.Bind (a, B.Abst (r, n, w), t) -> let p = true in let op, cp = if p then "(", ")" else "", "" in - let y = R.alpha B.mem e y in - let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abst r n w) in let ob, cb = match N.to_string st n with | "1" -> "forall", "," | "2" -> "fun", " =>" | _ -> ok := false; "?", "?" in KP.fprintf och "%s%s (%a:%a)%s %a%s" - op ob out_name y (out_term st false e) w cb (out_term st false ee) t cp - | B.Bind (y, B.Abbr v, t) -> + op ob out_name a (out_term st false e) w cb (out_term st false ee) t cp + | B.Bind (a, B.Abbr v, t) -> let op, cp = if p then "(", ")" else "", "" in - let y = R.alpha B.mem e y in - let ee = B.push e B.empty E.empty_node y (B.abbr v) in + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abbr v) in KP.fprintf och "%slet %a := %a in %a%s" - op out_name y (out_term st false e) v (out_term st false ee) t cp + op out_name a (out_term st false e) v (out_term st false ee) t cp | B.Bind (a, B.Void, t) -> C.err () let close_out och () = close_out och @@ -124,12 +124,12 @@ let output_entity och st (_, na, u, b) = KP.fprintf och "exact %a.\n%!" (out_term st true B.empty) v; KP.fprintf och "Time Defined.\n\n%!"; *) - | E.Abbr v -> + | E.Abbr (_, v) -> KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v; (* KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok - | E.Abst w -> + | E.Abst (_, w) -> KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok - | E.Void -> C.err () + | E.Void -> C.err () (* Interface functions ******************************************************) diff --git a/helm/software/helena/src/basic_rg/brgGallina.mli b/helm/software/helena/src/basic_rg/brgCoq.mli similarity index 100% rename from helm/software/helena/src/basic_rg/brgGallina.mli rename to helm/software/helena/src/basic_rg/brgCoq.mli diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index a7064d074..984f84916 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -25,8 +25,8 @@ let rec xlate_term f = function let f tt uu = f (B.Cast (uu, tt)) in let f tt = xlate_term (f tt) u in xlate_term f t - | D.TAppl (x, v, t) -> - let f tt vv = f (B.Appl (x, vv, tt)) in + | D.TAppl (a, v, t) -> + let f tt vv = f (B.Appl (a, vv, tt)) in let f tt = xlate_term (f tt) v in xlate_term f t | D.TProj (e, t) -> @@ -54,8 +54,8 @@ let rec xlate_bk_term f = function let f tt uu = f (D.TCast (uu, tt)) in let f tt = xlate_bk_term (f tt) u in xlate_bk_term f t - | B.Appl (x, u, t) -> - let f tt uu = f (D.TAppl (x, uu, tt)) in + | B.Appl (a, u, t) -> + let f tt uu = f (D.TAppl (a, uu, tt)) in let f tt = xlate_bk_term (f tt) u in xlate_bk_term f t | B.Bind (y, b, t) -> diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgHelena.ml similarity index 93% rename from helm/software/helena/src/basic_rg/brgLP.ml rename to helm/software/helena/src/basic_rg/brgHelena.ml index 8a8f9d4f2..07aa99601 100644 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ b/helm/software/helena/src/basic_rg/brgHelena.ml @@ -97,12 +97,12 @@ let rec out_term st e och = function KP.fprintf och "%a" out_uri s | B.Cast (u, t) -> KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t - | B.Appl (x, v, t) -> - let c = if x then "appx" else "appr" in + | B.Appl (a, v, t) -> + let c = if a.E.a_rest then "appr" else "appx" in KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t - | B.Bind (y, B.Abst (r, n, w), t) -> - let y = R.alpha B.mem e y in - let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + | B.Bind (a, B.Abst (r, n, w), t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abst r n w) in let c = if r then "prod" else "abst" in let l = match N.to_string st n with | "1" -> "l+1" @@ -110,12 +110,12 @@ let rec out_term st e och = function | _ -> ok := false; "?" in KP.fprintf och "(%s %s %a %a\\ %a)" - c l (out_term st e) w out_name y (out_term st ee) t - | B.Bind (y, B.Abbr v, t) -> - let y = R.alpha B.mem e y in - let ee = B.push e B.empty E.empty_node y (B.abbr v) in + c l (out_term st e) w out_name a (out_term st ee) t + | B.Bind (a, B.Abbr v, t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abbr v) in KP.fprintf och "(abbr %a %a\\ %a)" - (out_term st e) v out_name y (out_term st ee) t + (out_term st e) v out_name a (out_term st ee) t | B.Bind (_, B.Void, _) -> C.err () (* elpi variant 1 ***********************************************************) @@ -123,13 +123,13 @@ let rec out_term st e och = function let output_entity_lp1 och st (_, na, u, b) = if na.E.n_apix <= !G.last then begin match b with - | E.Abbr v -> + | E.Abbr (_, v) -> KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) v out_uri u; uris := (true, u) :: !uris; !ok - | E.Abst w -> + | E.Abst (_, w) -> KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) w out_uri u; uris := (false, u) :: !uris; !ok - | E.Void -> C.err () + | E.Void -> C.err () end else !ok let close_out_lp1 och () = @@ -144,15 +144,15 @@ let close_out_lp1 och () = let output_entity_lp2 och st (_, na, u, b) = if na.E.n_apix <= !G.last then begin match b with - | E.Abbr v -> + | E.Abbr (_, v) -> KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" out_uri u na.E.n_apix (out_term st B.empty) v; uris := (true, u) :: !uris; !ok - | E.Abst w -> + | E.Abst (_, w) -> KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" out_uri u na.E.n_apix (out_term st B.empty) w; uris := (false, u) :: !uris; !ok - | E.Void -> C.err () + | E.Void -> C.err () end else !ok let close_out_lp2 och () = @@ -207,15 +207,15 @@ let output_entity_tj2 och st (_, na, u, b) = end; out_comment !sub_och (KP.sprintf "constant %u" na.E.n_apix); match b with - | E.Abbr v -> + | E.Abbr (_, v) -> KP.fprintf !sub_och "line+%02u %a %u\n %a\n.\n\n" !chunk out_uri u (top_age - na.E.n_apix) (out_term st B.empty) v; uris := (true, u) :: !uris; !ok - | E.Abst w -> + | E.Abst (_, w) -> KP.fprintf !sub_och "line+%02u %a %u\n %a\n.\n\n" !chunk out_uri u (top_age - na.E.n_apix) (out_term st B.empty) w; uris := (false, u) :: !uris; !ok - | E.Void -> C.err () + | E.Void -> C.err () end else !ok let close_out_tj2 och () = @@ -266,21 +266,21 @@ let output_entity_tj3 och st (_, na, u, b) = out_comment och (KP.sprintf "constant %u" na.E.n_apix); let age = top_age - na.E.n_apix in match b with - | E.Abbr v -> + | E.Abbr (_, v) -> KP.fprintf och "g+line %a %u\n %a\n.\n\n" out_uri u age (out_term st B.empty) v; KP.fprintf och "tv+ %a.\n\n" out_uri u; KP.fprintf och "r+exp %a M C E M V :- g+line %a C V.\n\n" out_uri u out_uri u; uris := (true, u) :: !uris; !ok - | E.Abst w -> + | E.Abst (_, w) -> KP.fprintf och "g+line %a %u\n %a\n.\n\n" out_uri u age (out_term st B.empty) w; KP.fprintf och "tv+ %a.\n\n" out_uri u; KP.fprintf och "r+exp %a M1 C E M2 W :- m+pred M1 M2, g+line %a C W.\n\n" out_uri u out_uri u; uris := (false, u) :: !uris; !ok - | E.Void -> C.err () + | E.Void -> C.err () end else !ok let close_out_tj3 och () = diff --git a/helm/software/helena/src/basic_rg/brgLP.mli b/helm/software/helena/src/basic_rg/brgHelena.mli similarity index 100% rename from helm/software/helena/src/basic_rg/brgLP.mli rename to helm/software/helena/src/basic_rg/brgHelena.mli diff --git a/helm/software/helena/src/basic_rg/brgLYP.ml b/helm/software/helena/src/basic_rg/brgLYP.ml new file mode 100644 index 000000000..0c4a2abbd --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgLYP.ml @@ -0,0 +1,226 @@ +(* + ||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 KF = Filename +module KP = Printf + +module U = NUri +module C = Cps +module G = Options +module N = Layer +module E = Entity +module R = Alpha +module B = Brg + +IFDEF MANAGER THEN + +(* Internal functions *******************************************************) + +let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) + +let affiliation = "This file is part of the LYP engine" + +let description = "This file contains the Grundlagen for lyp_global: validate by invoking clause (grundlagen)" + +let ok = ref true + +let trusted = ref false (* "trusted" indicator out? *) + +let untrusted = ref false (* "untrusted" indicator out? *) + +let uris = ref [] + +let chunk = ref 0 + +let sub_och = ref stdout + +let top_age = 7000 + +let size = 250 + +let base = "lp" + +let ext_lp = ".elpi" +let ext_tj = ".mod" +let ext_tj_sig = ".sig" + +let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"] + +let alpha n = + if List.mem n reserved then !G.alpha ^ n else n + +let appl_fragment (_, ds) (_, dm) = match ds, dm with + | 2, 2 -> "ss" + | 2, 1 -> "sb" + | 1, 2 -> "bs" + | 1, 1 -> "bb" + | _ -> ok := false; "??" + +let abst_fragment (_, ds) (_, dm) = match ds, dm with + | 1, 2 -> "ss" + | 1, 1 -> "sb" + | 0, 2 -> "bs" + | 0, 1 -> "bb" + | _ -> ok := false; "??" + +let prod_fragment (_, ds) (_, dm) = match ds, dm with + | 1, 1 -> "ss" + | 1, 0 -> "sb" + | 0, 1 -> "bs" + | 0, 0 -> "bb" + | _ -> ok := false; "??" + +let entity_level (_, ds) = match ds with + | 1 -> "1" + | 2 -> "2" + | _ -> ok := false; "?" + +let out_preamble och = + let ich = open_in !G.preamble in + let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in + try aux () with End_of_file -> close_in ich + +let out_top_comment och msg = + KP.fprintf och "%% %s\n\n" msg + +let out_comment och msg = + KP.fprintf och "%% %s\n" msg + +let out_clause och msg = + KP.fprintf och "%s\n\n" msg + +let out_uri och u = + let str = U.string_of_uri u in + let rec aux i = + let c = str.[i] in + if c = '.' then () else begin + output_char och (if c = '/' then '_' else c); + aux (succ i) + end + in + let rec strip i n = + if n <= 0 then succ i else + strip (String.index_from str (succ i) '/') (pred n) + in + aux (strip 0 3) + +let out_name och a = + let f n = function + | true -> KP.fprintf och "%s" (alpha n) + | false -> KP.fprintf och "_" + in + let err () = f "" false in + E.name err f a + +let rec out_term st e och = function + | B.Sort k -> + KP.fprintf och "sort" + | B.LRef (_, i) -> + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" out_name y + | B.GRef (_, s) -> + KP.fprintf och "%a" out_uri s + | B.Cast (u, t) -> + C.err () + | B.Appl (a, v, t) -> + let f = appl_fragment a.E.a_side a.E.a_main in + KP.fprintf och "(appl f_%s %a %a)" f (out_term st e) v (out_term st e) t + | B.Bind (a, B.Abst (r, n, w), t) -> (* r *) + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abst r n w) in + let lf = match N.to_string st n with + | "1" -> "prod", prod_fragment a.E.b_side a.E.b_main + | "2" -> "abst", abst_fragment a.E.b_side a.E.b_main + | _ -> ok := false; "????", "??" + in + let l, f = match lf with + | "abst", "bs" -> "rest", "bs" + | "prod", "bs" -> "rest", "ho" + | "abst", "bb" -> "rest", "ho" + | "prod", "bb" -> "rest", "bb" + | lf -> lf + in + KP.fprintf och "(%s f_%s %a %a\\ %a)" + l f (out_term st e) w out_name a (out_term st ee) t + | B.Bind (_, B.Abbr _, _) -> C.err () + | B.Bind (_, B.Void, _) -> C.err () + +(* LYP variant 2 ***********************************************************) + +let output_entity_lyp2 och st (_, na, u, b) = + begin match !trusted, !untrusted with + | false, _ when na.E.n_apix < !G.first -> + out_top_comment och "Trusted part"; + trusted := true + | _ , false when !G.first <= na.E.n_apix && na.E.n_apix <= !G.last -> + out_top_comment och "Untrusted part"; + untrusted := true + | _ -> () + end; + if na.E.n_apix < !G.first then match b with + | E.Abbr (a, B.Cast (w, v)) -> + KP.fprintf och "type %a @id.\n" out_uri u; + KP.fprintf och "dec_l %a d_%s\n %a\n.\n" + out_uri u (entity_level a.E.e_side) (out_term st B.empty) w; + KP.fprintf och "def_l %a\n %a\n.\n\n" + out_uri u (out_term st B.empty) v; + !ok + | E.Abst (a, w) -> + KP.fprintf och "type %a @id.\n" out_uri u; + KP.fprintf och "dec_l %a d_%s\n %a\n.\n\n" + out_uri u (entity_level a.E.e_side) (out_term st B.empty) w; + !ok + | _ -> C.err () + else if na.E.n_apix <= !G.last then match b with + | E.Abbr (a, B.Cast (w, v)) -> + KP.fprintf och "type %a @id.\n" out_uri u; + KP.fprintf och "type c_%u ann.\n" na.E.n_apix; + KP.fprintf och "cast_g %a c_%u d_%s\n %a\n %a\n.\n\n" + out_uri u na.E.n_apix (entity_level a.E.e_side) + (out_term st B.empty) w (out_term st B.empty) v; + uris := (true, u) :: !uris; !ok + | E.Abst (a, w) -> + KP.fprintf och "type %a @id.\n" out_uri u; + KP.fprintf och "type c_%u ann.\n" na.E.n_apix; + KP.fprintf och "type_g %a c_%u d_%s\n %a\n.\n\n" + out_uri u na.E.n_apix (entity_level a.E.e_side) + (out_term st B.empty) w; + uris := (false, u) :: !uris; !ok + | _ -> C.err () + else !ok + +let close_out_lyp2 och () = + let aux_name (b, s) = + let gde = if b then "g_def" else "g_dec" in + KP.fprintf och "(%s %a\n" gde out_uri s + in + let aux_sep _ = KP.fprintf och "%s" ")" in + out_clause och "type grundlagen prop."; + out_clause och "grundlagen :- valid_g"; + List.iter aux_name (List.rev !uris); + KP.fprintf och "%s" "g_top"; + List.iter aux_sep !uris; + out_clause och "\n\n."; + close_out och + +(* Interface functions ******************************************************) + +let open_out_lyp2 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "b_lyp" ^ ext_lp) in + out_preamble och; + out_comment och version; + out_comment och affiliation; + out_top_comment och description; + output_entity_lyp2 och, close_out_lyp2 och + +END diff --git a/helm/software/helena/src/basic_rg/brgLYP.mli b/helm/software/helena/src/basic_rg/brgLYP.mli new file mode 100644 index 000000000..629f29326 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgLYP.mli @@ -0,0 +1,16 @@ +(* + ||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_______________________________________________________________ *) + +IFDEF MANAGER THEN + +val open_out_lyp2: string -> Brg.manager + +END diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgMatita.ml similarity index 87% rename from helm/software/helena/src/basic_rg/brgGrafite.ml rename to helm/software/helena/src/basic_rg/brgMatita.ml index 27ed9a1c4..adf79da58 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgMatita.ml @@ -88,24 +88,24 @@ let rec out_term st p e och = function let pt = match t with B.Appl _ -> false | _ -> true in let op, cp = if p then "(", ")" else "", "" in KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp - | B.Bind (y, B.Abst (r, n, w), t) -> + | B.Bind (a, B.Abst (r, n, w), t) -> let op, cp = if p then "(", ")" else "", "" in - let y = R.alpha B.mem e y in - let ee = B.push e B.empty E.empty_node y (B.abst r n w) in - let binder = match N.to_string st n, fst y.E.b_main with + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abst r n w) in + let binder = match N.to_string st n, fst a.E.b_main with | "1", 0 -> "Π" | "1", 1 -> "∀" | "2", _ -> "λ" | _ -> ok := false; "?" in KP.fprintf och "%s%s%a:%a.%a%s" - op binder out_name y (out_term st false e) w (out_term st false ee) t cp - | B.Bind (y, B.Abbr v, t) -> + op binder out_name a (out_term st false e) w (out_term st false ee) t cp + | B.Bind (a, B.Abbr v, t) -> let op, cp = if p then "(", ")" else "", "" in - let y = R.alpha B.mem e y in - let ee = B.push e B.empty E.empty_node y (B.abbr v) in + let a = R.alpha B.mem e a in + let ee = B.push e B.empty E.empty_node a (B.abbr v) in KP.fprintf och "%slet %a ≝ %a in %a%s" - op out_name y (out_term st false e) v (out_term st false ee) t cp + op out_name a (out_term st false e) v (out_term st false ee) t cp | B.Bind (a, B.Void, t) -> C.err () let close_out och () = close_out och @@ -113,11 +113,11 @@ let close_out och () = close_out och let output_entity och st (_, na, u, b) = out_comment och (KP.sprintf "constant %u" na.E.n_apix); match b with - | E.Abbr v -> + | E.Abbr (_, v) -> KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri u (out_term st false B.empty) v; !ok - | E.Abst w -> + | E.Abst (_, w) -> KP.fprintf och "axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok - | E.Void -> C.err () + | E.Void -> C.err () (* Interface functions ******************************************************) diff --git a/helm/software/helena/src/basic_rg/brgGrafite.mli b/helm/software/helena/src/basic_rg/brgMatita.mli similarity index 100% rename from helm/software/helena/src/basic_rg/brgGrafite.mli rename to helm/software/helena/src/basic_rg/brgMatita.mli diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index f8d8e642b..7bb9ce436 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -96,15 +96,15 @@ and count_term f c e = function count_term_binder f c e b let count_entity f c = function - | _, _, u, E.Abst w -> + | _, _, u, E.Abst (_, w) -> let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris } in count_term f c B.empty w - | _, _, _, E.Abbr v -> + | _, _, _, E.Abbr (_, v) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty v - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 4a9570d50..ffe223ab5 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -105,9 +105,9 @@ ELSE () END; else m, r, None | B.GRef (_, u) -> begin match BE.get_entity u with - | _, a, _, E.Abbr v -> + | _, a, _, E.Abbr (_, v) -> m, B.gref a u, Some v - | _, _, _, E.Abst w -> + | _, _, _, E.Abst (_, w) -> if assert_tstep m true then begin IFDEF SUMMARY THEN if !G.summary then O.add ~grt:1 () @@ -115,7 +115,7 @@ ELSE () END; step st (tstep m) w end else m, r, None - | _, _, _, E.Void -> + | _, _, _, E.Void -> assert false end | B.LRef (_, i) -> diff --git a/helm/software/helena/src/basic_rg/brgSubstitution.ml b/helm/software/helena/src/basic_rg/brgSubstitution.ml index 5441f0145..727524ca7 100644 --- a/helm/software/helena/src/basic_rg/brgSubstitution.ml +++ b/helm/software/helena/src/basic_rg/brgSubstitution.ml @@ -34,7 +34,7 @@ let iter map d = | B.GRef _ as t -> t | B.LRef (a, i) as t -> if i < d then t else map d a i | B.Cast (w, v) -> B.Cast (iter_term d w, iter_term d v) - | B.Appl (x, w, u) -> B.Appl (x, iter_term d w, iter_term d u) + | B.Appl (a, w, u) -> B.Appl (a, iter_term d w, iter_term d u) | B.Bind (y, b, u) -> B.Bind (y, iter_bind d b, iter_term (succ d) u) in iter_term d diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 431e3e473..28a275548 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -57,8 +57,8 @@ let assert_convertibility err f st m u w v = if BR.are_convertible st m zero u m zero w then f () else error3 err m v w u -let assert_applicability err f st m x u w v = - let mode = if x then None else zero in +let assert_applicability err f st m a u w v = + let mode = if a.E.a_rest then zero else None in match BR.xwhd st m mode u with | _, B.Sort _ -> error1 err "not a function type" m u @@ -87,10 +87,10 @@ ELSE () END; end | B.GRef (_, u) -> begin match BE.get_entity u with - | _, _, _, E.Abst w -> f z w - | _, _, _, E.Abbr (B.Cast (w, _)) -> f z w - | _, _, _, E.Abbr _ -> assert false - | _, _, _, E.Void -> + | _, _, _, E.Abst (_, w) -> f z w + | _, _, _, E.Abbr (_, B.Cast (w, _)) -> f z w + | _, _, _, E.Abbr _ -> assert false + | _, _, _, E.Void -> error1 err "reference to unknown entry" m z end | B.Bind (y, B.Abbr v, t) -> @@ -116,10 +116,10 @@ ELSE () END; f (S.sh1 t rt z (B.bind_void y)) (B.bind_void y tt) in b_type_of err f st (BR.push m y B.Void) t - | B.Appl (x, v, t) -> + | B.Appl (a, v, t) -> let f rv vv rt tt = - let f _ = f (S.sh2 v rv t rt z (B.appl x)) (B.appl x rv tt) in - assert_applicability err f st m x tt vv rv + let f _ = f (S.sh2 v rv t rt z (B.appl a)) (B.appl a rv tt) in + assert_applicability err f st m a tt vv rv in let f rv vv = b_type_of err (f rv vv) st m t in type_of err f st m v diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 0806a3d32..b1cd52523 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -26,23 +26,23 @@ IFDEF TYPE THEN (* to share *) let type_check err f st = function - | ra, na, uri, E.Abst t -> + | ra, na, uri, E.Abst (a, t) -> let err msg = err (L.Uri uri :: msg) in let f xt tt = - let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e + let e = BE.set_entity (ra, na, uri, E.abst a xt) in f tt e in BT.type_of err f st BR.empty_rtm t - | ra, na, uri, E.Abbr t -> + | ra, na, uri, E.Abbr (a, t) -> let err msg = err (L.Uri uri :: msg) in let f xt tt = let xt = match xt with | B.Cast _ -> xt | _ -> B.Cast (tt, xt) in - let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e + let e = BE.set_entity (ra, na, uri, E.abbr a xt) in f tt e in BT.type_of err f st BR.empty_rtm t - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false END @@ -51,9 +51,9 @@ IFDEF PROFV THEN Y.utime_lap "" ELSE () END; let uri, t = match e with - | _, _, uri, E.Abst t -> uri, t - | _, _, uri, E.Abbr t -> uri, t - | _, _, _, E.Void -> assert false + | _, _, uri, E.Abst (_, t) -> uri, t + | _, _, uri, E.Abbr (_, t) -> uri, t + | _, _, _, E.Void -> assert false in let err msg = err (L.Uri uri :: msg) in let f () = diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index cb0fc4060..a1401c125 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -52,8 +52,8 @@ ELSE () END; if BR.are_convertible st m zero u m one t then f () else error2 err m u m t -let assert_applicability err f st m x v t = - let mode, msg = if x then None, "extended" else one, "restricted" in +let assert_applicability err f st m a v t = + let mode, msg = if a.E.a_rest then one, "restricted" else None, "extended" in IFDEF TRACE THEN if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability") ELSE () END; @@ -98,8 +98,8 @@ ELSE () END; | B.Abbr v -> validate err f st m v | B.Void -> f () end - | B.Appl (x, v, t) -> - let f () = assert_applicability err f st m x v t in + | B.Appl (a, v, t) -> + let f () = assert_applicability err f st m a v t in let f () = b_validate err f st m t in validate err f st m v | B.Cast (u, t) -> diff --git a/helm/software/helena/src/common/Make b/helm/software/helena/src/common/Make deleted file mode 100644 index 4abdda084..000000000 --- a/helm/software/helena/src/common/Make +++ /dev/null @@ -1 +0,0 @@ -options hierarchy layer entity output alpha diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml index ab99e24cd..039ed63a4 100644 --- a/helm/software/helena/src/common/entity.ml +++ b/helm/software/helena/src/common/entity.ml @@ -29,6 +29,12 @@ type node_attrs = { n_apix: int; (* additional position index *) } +type appl_attrs = { + a_rest: bool; (* restricted application? *) + a_main: arity; (* main arity *) + a_side: arity; (* side arity *) +} + type bind_attrs = { b_name: name option; (* name *) b_main: arity; (* main arity *) @@ -40,9 +46,14 @@ type root_attrs = { r_info: (string * string) option; (* metaliguistic annotation: language (defaults to "en-US"), text *) } -type 'term bind = Abst of 'term (* declaration: domain *) - | Abbr of 'term (* definition: body *) - | Void (* exclusion *) +type env_attrs = { + e_side: arity; (* arity *) +} + + +type 'term bind = Abst of env_attrs * 'term (* declaration: attrs, domain *) + | Abbr of env_attrs * 'term (* definition: attrs, body *) + | Void (* exclusion *) type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, binder *) @@ -52,6 +63,10 @@ let node_attrs ?(apix=0) () = { n_apix = apix; } +let appl_attrs ?(main=(0,0)) ?(side=(0,0)) rest = { + a_rest = rest; a_main = main; a_side = side; +} + let bind_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = { b_name = name; b_main = main; b_side = side; } @@ -60,19 +75,27 @@ let root_attrs ?(meta=[]) ?info () = { r_meta = meta; r_info = info; } +let env_attrs ?(side=(0,0)) () = { + e_side = side; +} + let empty_node = node_attrs () let empty_bind = bind_attrs () let empty_root = root_attrs () +let empty_env = env_attrs () + +let abst a t = Abst (a, t) + +let abbr a t = Abbr (a, t) + let common f (ra, na, u, _) = f ra na u let succ (sort, degr) = sort, succ degr -let compose av at = {av with b_main = at.b_main} - -let shift av = {av with b_side = av.b_main} +let compose av yt = {av with b_main = yt} let rec name err f a = match a.b_name with | Some (n, r) -> f n r @@ -83,9 +106,9 @@ let rec info err f a = match a.r_info with | None -> err () let xlate f xlate_term = function - | ra, na, uri, Abst t -> - let f t = f (ra, na, uri, Abst t) in xlate_term f t - | ra, na, uri, Abbr t -> - let f t = f (ra, na, uri, Abbr t) in xlate_term f t - | _, _, _, Void -> + | ra, na, uri, Abst (a, t) -> + let f t = f (ra, na, uri, abst a t) in xlate_term f t + | ra, na, uri, Abbr (a, t) -> + let f t = f (ra, na, uri, abbr a t) in xlate_term f t + | _, _, _, Void -> assert false diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index f268ba344..71e55ecec 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -22,18 +22,20 @@ IFDEF MANAGER THEN type manager = Quiet | Coq | Matita - | LP1 (* newelpi *) - | LP2 (* newelpi *) - | TJ2 (* teyjus *) - | TJ3 (* teyjus *) + | LP1 (* elpi helena *) + | LP2 (* elpi helena *) + | TJ2 (* teyjus helena *) + | TJ3 (* teyjus helena *) + | CC0 (* elpi cic *) + | LYP (* elpi lyp *) END (* interface functions ******************************************************) let version_string b = - if b then "Helena 0.8.3 M (December 2015)" - else "Helena 0.8.3 M - December 2015" + if b then "Helena 0.8.3 M (December 2017)" + else "Helena 0.8.3 M - December 2017" let kernel = ref V3 (* kernel type *) @@ -51,12 +53,14 @@ let first = ref 0 (* begin trace here *) let last = ref max_int (* end trace here *) -let extended = ref false (* extended applications *) +let restricted = ref true (* restricted applications *) let infinity = ref false (* use ∞-abstractions in contexts *) let short = ref false (* short global constants *) +let cast = ref false (* anticipate cast *) + let root = ref "" (* initial segment of URI hierarchy *) let trace = ref 0 (* trace level *) @@ -116,8 +120,8 @@ let kernel_id () = | V0 -> "Environment_V0" in let si = if !si then "_si" else "" in - let ext = if !extended then "_x" else "" in - id ^ si ^ ext + let rest = if !restricted then "" else "_x" in + id ^ si ^ rest let get_baseuri () = String.concat "/" ["ld:"; kernel_id (); !cover; "" ] @@ -133,7 +137,7 @@ END let clear () = root := ""; first := 0; last := max_int; - kernel := V3; si := false; extended := false; infinity := false; cover := ""; + kernel := V3; si := false; restricted := true; infinity := false; cast := false; cover := ""; indexes := false; short := false; trace := 0; IFDEF LEXER THEN debug_lexer := false ELSE () END; IFDEF PARSER THEN debug_parser := false ELSE () END; diff --git a/helm/software/helena/src/complete_rg/Make b/helm/software/helena/src/complete_rg/Make deleted file mode 100644 index a7b947730..000000000 --- a/helm/software/helena/src/complete_rg/Make +++ /dev/null @@ -1 +0,0 @@ -crg crgOutput diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 36a1c8d59..5eb81e3e1 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -19,6 +19,7 @@ module E = Entity type uri = E.uri type id = E.id type n_attrs = E.node_attrs +type a_attrs = E.appl_attrs type b_attrs = E.bind_attrs @@ -30,13 +31,13 @@ and term = TSort of int (* hierarchy index *) | TLRef of n_attrs * int (* attrs, position indexe *) | TGRef of n_attrs * uri (* attrs, reference *) | TCast of term * term (* domain, element *) - | TAppl of bool * term * term (* extended?, argument, function *) + | TAppl of a_attrs * term * term (* attrs, argument, function *) | TBind of b_attrs * bind * term (* attrs, binder, scope *) | TProj of lenv * term (* closure, member *) and lenv = ESort (* top *) | EBind of lenv * n_attrs * b_attrs * bind (* environment, attrs, binder *) - | EAppl of lenv * bool * term (* environment, extended?, argument *) + | EAppl of lenv * a_attrs * term (* environment, attrs, argument *) | EProj of lenv * lenv (* environment, closure *) type entity = term E.entity @@ -47,36 +48,36 @@ let empty_lenv = ESort let push_bind f a y b lenv = f (EBind (lenv, a, y, b)) -let push_appl f x t lenv = f (EAppl (lenv, x, t)) +let push_appl f a t lenv = f (EAppl (lenv, a, t)) let push_proj f e lenv = f (EProj (lenv, e)) let add_bind f y b t = f (TBind (y, b, t)) -let add_appl f x v t = f (TAppl (x, v, t)) +let add_appl f a v t = f (TAppl (a, v, t)) let add_proj f e t = f (TProj (e, t)) let rec shift f c t = match c with | ESort -> f t - | EBind (e, _, y, b) -> add_bind (shift f e) y b t - | EAppl (e, x, v) -> add_appl (shift f e) x v t + | EBind (e, _, a, b) -> add_bind (shift f e) a b t + | EAppl (e, a, v) -> add_appl (shift f e) a v t | EProj (e, d) -> add_proj (shift f e) d t let rec append f c = function | ESort -> f c - | EBind (e, a, y, b) -> append (push_bind f a y b) c e - | EAppl (e, x, t) -> append (push_appl f x t) c e + | EBind (e, y, a, b) -> append (push_bind f y a b) c e + | EAppl (e, a, t) -> append (push_appl f a t) c e | EProj (e, d) -> append (push_proj f d) c e let resolve_lref err f id lenv = let rec aux i = function | ESort -> err () | EAppl (tl, _, _) -> aux i tl - | EBind (tl, a, y, _) -> - let f id0 _ = if id0 = id then f a y i else aux (succ i) tl in + | EBind (tl, y, a, _) -> + let f id0 _ = if id0 = id then f y a i else aux (succ i) tl in let err () = aux (succ i) tl in - E.name err f y + E.name err f a | EProj (tl, d) -> append (aux i) tl d in aux 0 lenv @@ -84,9 +85,9 @@ let resolve_lref err f id lenv = let rec get_name err f i = function | ESort -> err i | EAppl (tl, _, _) -> get_name err f i tl - | EBind (_, _, y, _) when i = 0 -> + | EBind (_, _, a, _) when i = 0 -> let err () = err i in - E.name err f y + E.name err f a | EBind (tl, _, _, _) -> get_name err f (pred i) tl | EProj (tl, e) -> let err i = get_name err f i tl in @@ -94,7 +95,7 @@ let rec get_name err f i = function let rec get e i = match e with | ESort -> ESort, E.empty_node, E.empty_bind, Void - | EBind (e, a, y, b) when i = 0 -> e, a, y, b + | EBind (e, y, a, b) when i = 0 -> e, y, a, b | EBind (e, _, _, _) -> get e (pred i) | EAppl (e, _, _) -> get e i | EProj (e, d) -> get (append C.start e d) i @@ -109,32 +110,32 @@ let rec fold_names f map x = function | EBind (e, _, {E.b_name = Some n}, Abst _) -> fold_names f map (map x n) e | _ -> assert false -let rec mem err f e y0 = match e with +let rec mem err f e a0 = match e with | ESort -> err () - | EBind (e, _, y, _) -> - if y.E.b_name = y0.E.b_name then f () else mem err f e y0 - | EAppl (e, _, _) -> mem err f e y0 + | EBind (e, _, a, _) -> + if a.E.b_name = a0.E.b_name then f () else mem err f e a0 + | EAppl (e, _, _) -> mem err f e a0 | EProj (e, d) -> - let err () = mem err f e y0 in mem err f d y0 + let err () = mem err f e a0 in mem err f d a0 let set_layer f n0 e = let rec aux f = function | ESort -> f ESort - | EBind (e, a, y, Abst (r, n, w)) -> aux (push_bind f a y (Abst (r, n0, w))) e - | EBind (e, a, y, b) -> aux (push_bind f a y b) e - | EAppl (e, x, v) -> aux (push_appl f x v) e + | EBind (e, y, a, Abst (r, n, w)) -> aux (push_bind f y a (Abst (r, n0, w))) e + | EBind (e, y, a, b) -> aux (push_bind f y a b) e + | EAppl (e, a, v) -> aux (push_appl f a v) e | EProj (e, d) -> let f d = aux (push_proj f d) e in aux f d in aux f e -let set_attrs f y0 e = +let set_attrs f a0 e = let rec aux f = function | ESort -> f ESort - | EBind (e, a, y, b) -> - let y = E.compose y y0 in - aux (push_bind f a y b) e - | EAppl (e, x, v) -> - aux (push_appl f x v) e + | EBind (e, y, a, b) -> + let a = E.compose a a0 in + aux (push_bind f y a b) e + | EAppl (e, a, v) -> + aux (push_appl f a v) e | EProj (e, d) -> let f d = aux (push_proj f d) e in aux f d diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 535ec2beb..f068181a7 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -94,15 +94,15 @@ and count_binder f c e y b = match b with D.push_bind (f c) E.empty_node y b e let count_entity f c = function - | _, _, u, E.Abst w -> + | _, _, u, E.Abst (_, w) -> let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris } in count_term f c D.ESort w - | _, _, _, E.Abbr v -> + | _, _, _, E.Abbr (_, v) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c D.ESort v - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = diff --git a/helm/software/helena/src/lib/Make b/helm/software/helena/src/lib/Make deleted file mode 100644 index c72a054c3..000000000 --- a/helm/software/helena/src/lib/Make +++ /dev/null @@ -1 +0,0 @@ -cps share log time marks diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 72895c06f..dd8cd7358 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -50,9 +50,11 @@ module BR = BrgReduction module BT = BrgType module BV = BrgValidity module BU = BrgUntrusted -module BG = BrgGrafite (**) -module BA = BrgGallina (**) -module BP = BrgLP +module BM = BrgMatita +module BQ = BrgCoq +module BH = BrgHelena +module BC = BrgCC +module BY = BrgLYP module Z = Bag module ZD = BrgCrg diff --git a/helm/software/helena/src/text/Make b/helm/software/helena/src/text/Make deleted file mode 100644 index 2cdbfd792..000000000 --- a/helm/software/helena/src/text/Make +++ /dev/null @@ -1 +0,0 @@ -txt txtParser txtLexer txtCrg diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index 174857d43..4580d2d86 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -25,7 +25,7 @@ type status = { path : T.id list; (* current section path *) line : int; (* line number *) sort : int; (* first default sort index *) - ext : bool; (* extended applications *) + rest : bool; (* restricted applications *) mk_uri: G.uri_generator (* uri generator *) } @@ -81,7 +81,7 @@ let rec xlate_term f st lenv = function let f _ uu = xlate_term (f uu) st lenv t in xlate_term f st lenv u | T.Appl (v, t) -> - let f vv y tt = f y (D.TAppl (st.ext, vv, tt)) in + let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in let f _ vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | T.Proj (bs, t) -> @@ -90,7 +90,7 @@ let rec xlate_term f st lenv = function C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs | T.Inst (t, vs) -> let map f v e = - let f _ vv = D.push_appl f st.ext vv e in + let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in xlate_term f st lenv v in let f e y tt = f y (D.TProj (e, tt)) in @@ -120,11 +120,11 @@ and xlate_bind st f (lenv, e) b = let mk_contents main kind tt = let ms, b = match kind with - | T.Decl -> [] , E.Abst tt - | T.Ax -> [E.InProp] , E.Abst tt - | T.Cong -> [E.InProp; E.Progress], E.Abst tt - | T.Def -> [] , E.Abbr tt - | T.Th -> [E.InProp] , E.Abbr tt + | T.Decl -> [] , E.abst E.empty_env tt + | T.Ax -> [E.InProp] , E.abst E.empty_env tt + | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt + | T.Def -> [] , E.abbr E.empty_env tt + | T.Th -> [E.InProp] , E.abbr E.empty_env tt in if main then E.Main :: ms, b else ms, b @@ -171,7 +171,7 @@ let xlate_entity err f gen st = function let initial_status () = KH.clear henv; { - path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri () + path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri () } let refresh_status st = {st with diff --git a/helm/software/helena/src/toplevel/Make b/helm/software/helena/src/toplevel/Make deleted file mode 100644 index bf1a1fdef..000000000 --- a/helm/software/helena/src/toplevel/Make +++ /dev/null @@ -1 +0,0 @@ -top diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/helena.ml similarity index 94% rename from helm/software/helena/src/toplevel/top.ml rename to helm/software/helena/src/toplevel/helena.ml index b7c6fc135..1070dd915 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/helena.ml @@ -37,9 +37,11 @@ module BD = BrgCrg module BO = BrgOutput module BR = BrgReduction module BU = BrgUntrusted -module BG = BrgGrafite -module BA = BrgGallina -module BP = BrgLP +module BM = BrgMatita +module BQ = BrgCoq +module BH = BrgHelena +(* module BC = BrgCC *) +module BY = BrgLYP module ZD = BagCrg module ZO = BagOutput module ZT = BagType @@ -391,6 +393,10 @@ let set_manager s = match KS.lowercase s with | "lp2" -> G.manager := G.LP2 | "tj2" -> G.manager := G.TJ2 | "tj3" -> G.manager := G.TJ3 +(* + | "cc0" -> G.manager := G.CC0 +*) + | "lyp" -> G.manager := G.LYP | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) END @@ -466,7 +472,7 @@ ELSE () END; L.warn level (KP.sprintf "%s was compiled without the support for option %s" (G.version_string true) opt); exit 0 in - let arg_undefined opt = Arg.Unit (undefined opt) in + let arg_undefined opt = Arg.Unit (undefined opt) in let process_file name = if !G.trace >= 2 then begin L.warn 1 (KP.sprintf "Processing file: %s" name); @@ -480,12 +486,16 @@ IFDEF STAGE THEN ELSE () END; IFDEF MANAGER THEN begin match !G.manager with - | G.Coq -> st := {!st with mst = Some (BA.open_out base_name)} - | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)} - | G.LP1 -> st := {!st with mst = Some (BP.open_out_lp1 base_name)} - | G.LP2 -> st := {!st with mst = Some (BP.open_out_lp2 base_name)} - | G.TJ2 -> st := {!st with mst = Some (BP.open_out_tj2 base_name)} - | G.TJ3 -> st := {!st with mst = Some (BP.open_out_tj3 base_name)} + | G.Coq -> st := {!st with mst = Some (BQ.open_out base_name)} + | G.Matita -> st := {!st with mst = Some (BM.open_out base_name)} + | G.LP1 -> st := {!st with mst = Some (BH.open_out_lp1 base_name)} + | G.LP2 -> st := {!st with mst = Some (BH.open_out_lp2 base_name)} + | G.TJ2 -> st := {!st with mst = Some (BH.open_out_tj2 base_name)} + | G.TJ3 -> st := {!st with mst = Some (BH.open_out_tj3 base_name)} +(* + | G.CC0 -> st := {!st with mst = Some (BC.open_out_cc0 base_name)} +*) + | G.LYP -> st := {!st with mst = Some (BY.open_out_lyp2 base_name)} | G.Quiet -> () end ELSE () END; @@ -520,7 +530,7 @@ ELSE () END " 4 typing information, 5 conversion information, 6 reduction information,\n" ^ " 7 level disambiguation\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^ - "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" (lambda-Prolog)\n" + "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"lyp\" (lambda-Prolog)\n" in let help_L = " [lexer] Show lexer debug information" in let help_M = " [manager] Set location of output directory (manager) to (default: current directory)" in @@ -532,6 +542,7 @@ ELSE () END let help_a = " [alpha] Set prefix of numeric identifiers (default: empty)" in let help_b = " [begin] Begin trace at this global constant (default: first)" in + let help_c = " [cast] Anticipate cast in global definitions (Automath) (default: posticipate)" in let help_d = " [data] Show summary information (requires trace >= 2)" in let help_e = " [end] End trace at this global constant (default: last)" in let help_g = " [global] Disable age-driven expansion of global definitions (default: enable)" in @@ -563,6 +574,7 @@ ELSE () END ("-X", Arg.Unit clear_options, help_X); ("-a", Arg.String ((:=) G.alpha), help_a); ("-b", Arg.Int ((:=) G.first), help_b); + ("-c", Arg.Set G.cast, help_c); ("-d", (IFDEF SUMMARY THEN Arg.Unit set_summary ELSE arg_undefined "-d" END), help_d); ("-e", Arg.Int ((:=) G.last), help_e); ("-g", (IFDEF EXPAND THEN Arg.Set G.expand ELSE arg_undefined "-g" END), help_g); @@ -579,8 +591,11 @@ ELSE () END ("-s", (IFDEF STAGE THEN Arg.Int ((:=) G.stage) ELSE arg_undefined "-s" END), help_s); ("-t", (IFDEF TYPE THEN Arg.Clear G.validate ELSE arg_undefined "-t" END), help_t); ("-u", Arg.Set G.si, help_u); - ("-x", Arg.Set G.extended, help_x); + ("-x", Arg.Clear G.restricted, help_x); ("-y", Arg.Set G.infinity, help_y); ("-0", (IFDEF PREPROCESS THEN Arg.Unit set_preprocess ELSE arg_undefined "-0" END), help_0); ("-1", Arg.Set streaming, help_1); - ] process_file help + ] process_file help; +IFDEF LEXER AND MANAGER AND OBJECTS AND PARSER AND SUMMARY AND EXPAND AND QUOTE AND STAGE AND TYPE AND PREPROCESS THEN + if false then ignore (arg_undefined "") (* invocation of arg_undefined to make the compiler happy *) +ELSE () END diff --git a/helm/software/helena/src/xml/Make b/helm/software/helena/src/xml/Make deleted file mode 100644 index 3a626cece..000000000 --- a/helm/software/helena/src/xml/Make +++ /dev/null @@ -1 +0,0 @@ -xmlLibrary xmlCrg diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index 5d112bed2..34c78dd9e 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -29,9 +29,9 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab = (* NOTE: the inner binders are alpha-converted first *) let y = R.alpha D.mem e y in map_bind st e a y b out tab; D.EBind (e, a, y, b) - | D.EAppl (e, x, v) -> + | D.EAppl (e, a, v) -> let e = aux e in - map_appl st e x v out tab; D.EAppl (e, x, v) + map_appl st e a v out tab; D.EAppl (e, a, v) | D.EProj (e, d) -> let e = aux e in map_proj st e d out tab; D.EProj (e, d) @@ -63,33 +63,33 @@ let rec exp_term st e t out tab = match t with let attrs = [] in XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab; exp_term st e t out tab - | D.TAppl (x, v, t) -> - let attrs = [] in - XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab; + | D.TAppl (a, v, t) -> + let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in + XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab; exp_term st e t out tab | D.TProj (lenv, t) -> let attrs = [] in XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab; exp_term st (D.push_proj C.start lenv e) t out tab - | D.TBind (y, b, t) -> + | D.TBind (a, b, t) -> (* NOTE: the inner binders are alpha-converted first *) - let y = R.alpha D.mem e y in - exp_bind st e E.empty_node y b out tab; - exp_term st (D.push_bind C.start E.empty_node y b e) t out tab + let a = R.alpha D.mem e a in + exp_bind st e E.empty_node a b out tab; + exp_term st (D.push_bind C.start E.empty_node a b e) t out tab -and exp_appl st e x v out tab = - let attrs = [] in - XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab; +and exp_appl st e a v out tab = + let attrs = XL.restricted a.E.a_rest :: XL.side a.E.a_side @ XL.main a.E.a_main in + XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab; -and exp_bind st e a y b out tab = match b with +and exp_bind st e y a b out tab = match b with | D.Abst (_, n, w) -> - let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in + let attrs = XL.layer st n :: XL.name a :: XL.side a.E.b_side @ XL.main a.E.b_main in XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab | D.Abbr v -> - let attrs = [XL.name y] in + let attrs = [XL.name a] in XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab | D.Void -> - let attrs = [XL.name y] in + let attrs = [XL.name a] in XL.tag XL.void attrs out tab and exp_proj st e lenv out tab = diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 4667b3aa5..59dbc4d66 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -10,6 +10,7 @@ V_______________________________________________________________ *) module KF = Filename +module KP = Printf module U = NUri module C = Cps @@ -77,7 +78,7 @@ let gref = "GRef" let cast = "Cast" -let appl x = if x then "Appx" else "Appr" +let appl = "Appl" let proj = "Proj" @@ -101,17 +102,18 @@ let name a = let f n r = "name", if r then n else "-" ^ n in E.name err f a +let restricted r = + "restricted", KP.sprintf "%b" r + let layer st n = "layer", N.to_string st n -let main a = - let sort, degr = a.E.b_main in +let main (sort, degr) = ["main-position", string_of_int sort; "main-degree", string_of_int degr; ] -let side a = - let sort, degr = a.E.b_side in +let side (sort, degr) = ["side-position", string_of_int sort; "side-degree", string_of_int degr; ] @@ -141,10 +143,10 @@ let export_entity pp_term (ra, na, u, b) = let out = output_string och in xml out "1.0" "UTF-8"; doctype out obj_root system; let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in - let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in + let attrs a = uri u :: name ba :: apix na :: meta ra :: info ra @ side a.E.e_side in let contents = match b with - | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) - | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) + | E.Abst (a, w) -> tag "GDec" (attrs a) ~contents:(pp_term w) + | E.Abbr (a, v) -> tag "GDef" (attrs a) ~contents:(pp_term v) | E.Void -> assert false in let opts = if !G.si then "si" else "" in diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 552aa3666..d6ce856bb 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -29,7 +29,7 @@ val gref: string val cast: string -val appl: bool -> string +val appl: string val proj: string @@ -45,13 +45,15 @@ val depth: int -> attr val uri: Entity.uri -> attr +val restricted: bool -> attr + val layer: Layer.status -> Layer.layer -> attr val name: Entity.bind_attrs -> attr -val main: Entity.bind_attrs -> attr list +val main: Entity.arity -> attr list -val side: Entity.bind_attrs -> attr list +val side: Entity.arity -> attr list val apix: Entity.node_attrs -> attr -- 2.39.2