From: Ferruccio Guidi Date: Tue, 9 Jan 2018 18:53:51 +0000 (+0100) Subject: update in helena X-Git-Tag: make_still_working~374 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=88977b2d546e547e23b046792fe2ad8f6ff192a4 update in helena - new system of attributes for terms - exportation to λΥP λProlog engine - now based on ocamlbuild --- 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/brgCoq.ml b/helm/software/helena/src/basic_rg/brgCoq.ml new file mode 100644 index 000000000..3a3dea1e6 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgCoq.ml @@ -0,0 +1,144 @@ +(* + ||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 ok = ref true + +let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) + +let base = "coq" + +let ext = ".v" + +let width = 70 + +let reserved = ["if"] + +let alpha n = + if List.mem n reserved then !G.alpha ^ n else n + +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 = + let padding = width - String.length msg in + let padding = if padding >= 0 then padding else 0 in + KP.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*') + +let out_comment och msg = + KP.fprintf och "(* %s *)\n" msg + +let out_include och src = + KP.fprintf och "include \"%s.ma\".\n\n" src + +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 p e och = function + | B.Sort k -> + let sort = if k = 0 then "Type" else if k = 1 then "Prop" else assert false in + KP.fprintf och "%s" 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) -> + KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u + | B.Appl (_, v, t) -> + 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 (a, B.Abst (r, n, w), t) -> + let p = true in + let op, cp = if p then "(", ")" else "", "" 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 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 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 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 + +let output_entity och st (_, na, u, b) = + out_comment och (KP.sprintf "constant %u" na.E.n_apix); + match b with +(* + | E.Abbr (B.Cast (w, v)) -> + KP.fprintf och "Definition %a : %a.\n%!" out_uri u (out_term st false B.empty) w; + KP.fprintf och "exact %a.\n%!" (out_term st true B.empty) v; + KP.fprintf och "Time Defined.\n\n%!"; +*) + | 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) -> + KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok + | E.Void -> C.err () + +(* Interface functions ******************************************************) + +let open_out fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ ext) in + out_preamble och; + out_top_comment och version; + output_entity och, close_out och + +END diff --git a/helm/software/helena/src/basic_rg/brgCoq.mli b/helm/software/helena/src/basic_rg/brgCoq.mli new file mode 100644 index 000000000..1b68ccedb --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgCoq.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: string -> Brg.manager + +END 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/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml deleted file mode 100644 index 7346e5835..000000000 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ /dev/null @@ -1,144 +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 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 ok = ref true - -let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) - -let base = "coq" - -let ext = ".v" - -let width = 70 - -let reserved = ["if"] - -let alpha n = - if List.mem n reserved then !G.alpha ^ n else n - -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 = - let padding = width - String.length msg in - let padding = if padding >= 0 then padding else 0 in - KP.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*') - -let out_comment och msg = - KP.fprintf och "(* %s *)\n" msg - -let out_include och src = - KP.fprintf och "include \"%s.ma\".\n\n" src - -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 p e och = function - | B.Sort k -> - let sort = if k = 0 then "Type" else if k = 1 then "Prop" else assert false in - KP.fprintf och "%s" 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) -> - KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u - | B.Appl (_, v, t) -> - 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) -> - 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 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) -> - 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 - 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 - | B.Bind (a, B.Void, t) -> C.err () - -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 (B.Cast (w, v)) -> - KP.fprintf och "Definition %a : %a.\n%!" out_uri u (out_term st false B.empty) w; - KP.fprintf och "exact %a.\n%!" (out_term st true B.empty) v; - KP.fprintf och "Time Defined.\n\n%!"; -*) - | 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 -> - KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok - | E.Void -> C.err () - -(* Interface functions ******************************************************) - -let open_out fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname in - let och = open_out (path ^ ext) in - out_preamble och; - out_top_comment och version; - output_entity och, close_out och - -END diff --git a/helm/software/helena/src/basic_rg/brgGallina.mli b/helm/software/helena/src/basic_rg/brgGallina.mli deleted file mode 100644 index 1b68ccedb..000000000 --- a/helm/software/helena/src/basic_rg/brgGallina.mli +++ /dev/null @@ -1,16 +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_______________________________________________________________ *) - -IFDEF MANAGER THEN - -val open_out: string -> Brg.manager - -END diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml deleted file mode 100644 index 27ed9a1c4..000000000 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ /dev/null @@ -1,133 +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 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 ok = ref true - -let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) - -let base = "matita" - -let ext = ".ma" - -let width = 70 - -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 = - let padding = width - String.length msg in - let padding = if padding >= 0 then padding else 0 in - KP.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*') - -let out_comment och msg = - KP.fprintf och "(* %s *)\n" msg - -let out_include och src = - KP.fprintf och "include \"%s.ma\".\n\n" src - -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" n - | false -> KP.fprintf och "_" - in - let err () = f "" false in - E.name err f a - -let rec out_term st p e och = function - | B.Sort k -> - let sort = if k = 0 then "Type[0]" else if k = 1 then "Prop" else assert false in - KP.fprintf och "%s" 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) -> - KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u - | B.Appl (_, v, t) -> - 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) -> - 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 - | "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) -> - 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 - 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 - | B.Bind (a, B.Void, t) -> C.err () - -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 -> - KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri u (out_term st false B.empty) v; !ok - | 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 () - -(* Interface functions ******************************************************) - -let open_out fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname in - let och = open_out (path ^ ext) in - out_preamble och; - out_top_comment och version; - out_include och "basics/pts"; - output_entity och, close_out och - -END diff --git a/helm/software/helena/src/basic_rg/brgGrafite.mli b/helm/software/helena/src/basic_rg/brgGrafite.mli deleted file mode 100644 index 1b68ccedb..000000000 --- a/helm/software/helena/src/basic_rg/brgGrafite.mli +++ /dev/null @@ -1,16 +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_______________________________________________________________ *) - -IFDEF MANAGER THEN - -val open_out: string -> Brg.manager - -END diff --git a/helm/software/helena/src/basic_rg/brgHelena.ml b/helm/software/helena/src/basic_rg/brgHelena.ml new file mode 100644 index 000000000..07aa99601 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgHelena.ml @@ -0,0 +1,353 @@ +(* + ||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 ok = ref true + +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 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 -> + let sort = if k = 0 then "k+set" else if k = 1 then "k+prop" else assert false in + KP.fprintf och "(sort %s)" 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) -> + KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t + | 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 (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" + | "2" -> "l+2" + | _ -> ok := false; "?" + in + KP.fprintf och "(%s %s %a %a\\ %a)" + 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 a (out_term st ee) t + | B.Bind (_, B.Void, _) -> C.err () + +(* elpi variant 1 ***********************************************************) + +let output_entity_lp1 och st (_, na, u, b) = + if na.E.n_apix <= !G.last then begin + match b with + | 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) -> + 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 () + end else !ok + +let close_out_lp1 och () = + let aux_sep _ = KP.fprintf och "%s" ")" in + KP.fprintf och "%s" "gtop"; + List.iter aux_sep !uris; + out_clause och "\n\n."; + close_out och + +(* elpi variant 2 ***********************************************************) + +let output_entity_lp2 och st (_, na, u, b) = + if na.E.n_apix <= !G.last then begin + match b with + | 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) -> + 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 () + end else !ok + +let close_out_lp2 och () = + let aux_name (b, s) = + let gde = if b then "gdef+2" else "gdec+2" in + KP.fprintf och "(%s %a\n" gde out_uri s + in + let aux_sep _ = KP.fprintf och "%s" ")" in + if !G.first > 0 then begin + let s = KP.sprintf "tv+c C T :- $lt C c+%u, !." !G.first in + out_clause och s; + out_clause och "tv+c C T :- tv+ T." + end; + out_clause och "main :- grundlagen."; + out_clause och "grundlagen :- gv+"; + List.iter aux_name (List.rev !uris); + KP.fprintf och "%s" "gtop"; + List.iter aux_sep !uris; + out_clause och "\n\n."; + close_out och + +(* teyjus variant 2 *************************************************) + +let append_out name = + open_out_gen [Open_append; Open_creat; Open_text] 0o666 name + +let sub_close () = if !sub_och <> stdout then close_out !sub_och + +let mk_name chunk = + let dir = KF.concat !G.manager_dir base in + let name = KP.sprintf "grundlagen%02u" chunk in + dir, name + +let output_entity_tj2 och st (_, na, u, b) = + if na.E.n_apix <= !G.last then begin + if pred na.E.n_apix mod size = 0 then begin + sub_close (); + incr chunk; + let dir, name = mk_name !chunk in + let soch = open_out (KF.concat dir name ^ ext_tj_sig) in + out_preamble soch; + out_top_comment soch version; + out_clause soch (KP.sprintf "sig %s." name); + out_clause soch "accum_sig grundlagen."; + out_clause soch (KP.sprintf "type line+%02u t -> int -> t -> o." !chunk); + close_out soch; + let soch = open_out (KF.concat dir name ^ ext_tj) in + out_preamble soch; + out_top_comment soch version; + out_clause soch (KP.sprintf "module %s." name); + sub_och := soch + end; + out_comment !sub_och (KP.sprintf "constant %u" na.E.n_apix); + match b with + | 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) -> + 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 () + end else !ok + +let close_out_tj2 och () = + let out_name och (b, u) = + let gde = if b then "gdef+2" else "gdec+2" in + KP.fprintf och "(%s %a\n" gde out_uri u + in + let rec out_pars och p = + if p > 0 then begin KP.fprintf och "%s" ")"; out_pars och (pred p) end + in + let rec out_list chunk pars first items uris = match first, items, uris with + | true, _, _ -> + let dir, name = mk_name chunk in + let soch = append_out (KF.concat dir name ^ ext_tj) in + out_clause soch (KP.sprintf "g+line R C T :- line+%02u R C T, !." chunk); + KP.fprintf soch "g+list %u\n" chunk; + sub_och := soch; + out_list (succ chunk) pars false items uris + | false, _, [] -> + KP.fprintf !sub_och "gtop%a.\n\n" out_pars pars; + sub_close () + | false, 0, _ -> + KP.fprintf !sub_och "(genv %u)%a.\n\n" chunk out_pars pars; + sub_close (); + out_list chunk 0 true size uris + | false, _, hd :: tl -> + out_name !sub_och hd; out_list chunk (succ pars) false (pred items) tl + in + let rec out_accumulate c = + if !chunk < c then KP.fprintf och "\n" else begin + let _, name = mk_name c in + KP.fprintf och "accumulate %s.\n" name; + out_accumulate (succ c) + end + in + sub_close (); + out_list 1 0 true size (List.rev !uris); + KP.fprintf och "accumulate helena.\n"; + out_accumulate 1; + out_clause och "main :- grundlagen."; + out_clause och "grundlagen :- gv+ (genv 1)."; + close_out och + +(* teyjus variant 3 *************************************************) + +let output_entity_tj3 och st (_, na, u, b) = + if na.E.n_apix <= !G.last then begin + 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) -> + 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) -> + 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 () + end else !ok + +let close_out_tj3 och () = + let out_name (_, u) = + KP.fprintf och "gv+3 %a,\n" out_uri u + in + let rec out_list och chunk first items uris = match first, items, uris with + | true, _, _ -> + KP.fprintf och "chunk %u :-\n" chunk; + out_list och (succ chunk) false items uris + | false, _, [] -> KP.fprintf och "!.\n\n"; chunk + | false, 0, _ -> + KP.fprintf och "!.\n\n"; + out_list och chunk true size uris + | false, _, hd :: tl -> + out_name hd; out_list och chunk false (pred items) tl + in + let rec out_chunks och chunks c = + if chunks < c then out_clause och "!." else begin + KP.fprintf och "chunk %u,\n" c; out_chunks och chunks (succ c) + end + in + let chunks = out_list och 1 true size (List.rev !uris) in + out_clause och "main :- grundlagen."; + KP.fprintf och "grundlagen :-\n"; + out_chunks och (pred chunks) 1; + close_out och + +(* Interface functions ******************************************************) + +let open_out_lp1 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "1" ^ ext_lp) in + out_preamble och; + out_top_comment och version; + out_clause och "accumulate helena."; + out_clause och "main :- grundlagen."; + out_clause och "grundlagen :- gv+"; + output_entity_lp1 och, close_out_lp1 och + +let open_out_lp2 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "2" ^ ext_lp) in + out_preamble och; + out_top_comment och version; + out_clause och "accumulate helena."; + output_entity_lp2 och, close_out_lp2 och + +let open_out_tj2 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname ^ "2" in + let och = open_out (path ^ ext_tj) in + out_preamble och; + out_top_comment och version; + out_clause och "module grundlagen."; + output_entity_tj2 och, close_out_tj2 och + +let open_out_tj3 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "3" ^ ext_tj) in + out_preamble och; + out_top_comment och version; + out_clause och "module grundlagen."; + out_clause och "accumulate helena."; + output_entity_tj3 och, close_out_tj3 och + +END diff --git a/helm/software/helena/src/basic_rg/brgHelena.mli b/helm/software/helena/src/basic_rg/brgHelena.mli new file mode 100644 index 000000000..c56c6c079 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgHelena.mli @@ -0,0 +1,22 @@ +(* + ||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_lp1: string -> Brg.manager + +val open_out_lp2: string -> Brg.manager + +val open_out_tj2: string -> Brg.manager + +val open_out_tj3: string -> Brg.manager + +END diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml deleted file mode 100644 index 8a8f9d4f2..000000000 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ /dev/null @@ -1,353 +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 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 ok = ref true - -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 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 -> - let sort = if k = 0 then "k+set" else if k = 1 then "k+prop" else assert false in - KP.fprintf och "(sort %s)" 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) -> - 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 - 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 - let c = if r then "prod" else "abst" in - let l = match N.to_string st n with - | "1" -> "l+1" - | "2" -> "l+2" - | _ -> 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 - KP.fprintf och "(abbr %a %a\\ %a)" - (out_term st e) v out_name y (out_term st ee) t - | B.Bind (_, B.Void, _) -> C.err () - -(* elpi variant 1 ***********************************************************) - -let output_entity_lp1 och st (_, na, u, b) = - if na.E.n_apix <= !G.last then begin - match b with - | 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 -> - 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 () - end else !ok - -let close_out_lp1 och () = - let aux_sep _ = KP.fprintf och "%s" ")" in - KP.fprintf och "%s" "gtop"; - List.iter aux_sep !uris; - out_clause och "\n\n."; - close_out och - -(* elpi variant 2 ***********************************************************) - -let output_entity_lp2 och st (_, na, u, b) = - if na.E.n_apix <= !G.last then begin - match b with - | 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 -> - 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 () - end else !ok - -let close_out_lp2 och () = - let aux_name (b, s) = - let gde = if b then "gdef+2" else "gdec+2" in - KP.fprintf och "(%s %a\n" gde out_uri s - in - let aux_sep _ = KP.fprintf och "%s" ")" in - if !G.first > 0 then begin - let s = KP.sprintf "tv+c C T :- $lt C c+%u, !." !G.first in - out_clause och s; - out_clause och "tv+c C T :- tv+ T." - end; - out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+"; - List.iter aux_name (List.rev !uris); - KP.fprintf och "%s" "gtop"; - List.iter aux_sep !uris; - out_clause och "\n\n."; - close_out och - -(* teyjus variant 2 *************************************************) - -let append_out name = - open_out_gen [Open_append; Open_creat; Open_text] 0o666 name - -let sub_close () = if !sub_och <> stdout then close_out !sub_och - -let mk_name chunk = - let dir = KF.concat !G.manager_dir base in - let name = KP.sprintf "grundlagen%02u" chunk in - dir, name - -let output_entity_tj2 och st (_, na, u, b) = - if na.E.n_apix <= !G.last then begin - if pred na.E.n_apix mod size = 0 then begin - sub_close (); - incr chunk; - let dir, name = mk_name !chunk in - let soch = open_out (KF.concat dir name ^ ext_tj_sig) in - out_preamble soch; - out_top_comment soch version; - out_clause soch (KP.sprintf "sig %s." name); - out_clause soch "accum_sig grundlagen."; - out_clause soch (KP.sprintf "type line+%02u t -> int -> t -> o." !chunk); - close_out soch; - let soch = open_out (KF.concat dir name ^ ext_tj) in - out_preamble soch; - out_top_comment soch version; - out_clause soch (KP.sprintf "module %s." name); - sub_och := soch - end; - out_comment !sub_och (KP.sprintf "constant %u" na.E.n_apix); - match b with - | 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 -> - 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 () - end else !ok - -let close_out_tj2 och () = - let out_name och (b, u) = - let gde = if b then "gdef+2" else "gdec+2" in - KP.fprintf och "(%s %a\n" gde out_uri u - in - let rec out_pars och p = - if p > 0 then begin KP.fprintf och "%s" ")"; out_pars och (pred p) end - in - let rec out_list chunk pars first items uris = match first, items, uris with - | true, _, _ -> - let dir, name = mk_name chunk in - let soch = append_out (KF.concat dir name ^ ext_tj) in - out_clause soch (KP.sprintf "g+line R C T :- line+%02u R C T, !." chunk); - KP.fprintf soch "g+list %u\n" chunk; - sub_och := soch; - out_list (succ chunk) pars false items uris - | false, _, [] -> - KP.fprintf !sub_och "gtop%a.\n\n" out_pars pars; - sub_close () - | false, 0, _ -> - KP.fprintf !sub_och "(genv %u)%a.\n\n" chunk out_pars pars; - sub_close (); - out_list chunk 0 true size uris - | false, _, hd :: tl -> - out_name !sub_och hd; out_list chunk (succ pars) false (pred items) tl - in - let rec out_accumulate c = - if !chunk < c then KP.fprintf och "\n" else begin - let _, name = mk_name c in - KP.fprintf och "accumulate %s.\n" name; - out_accumulate (succ c) - end - in - sub_close (); - out_list 1 0 true size (List.rev !uris); - KP.fprintf och "accumulate helena.\n"; - out_accumulate 1; - out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+ (genv 1)."; - close_out och - -(* teyjus variant 3 *************************************************) - -let output_entity_tj3 och st (_, na, u, b) = - if na.E.n_apix <= !G.last then begin - 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 -> - 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 -> - 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 () - end else !ok - -let close_out_tj3 och () = - let out_name (_, u) = - KP.fprintf och "gv+3 %a,\n" out_uri u - in - let rec out_list och chunk first items uris = match first, items, uris with - | true, _, _ -> - KP.fprintf och "chunk %u :-\n" chunk; - out_list och (succ chunk) false items uris - | false, _, [] -> KP.fprintf och "!.\n\n"; chunk - | false, 0, _ -> - KP.fprintf och "!.\n\n"; - out_list och chunk true size uris - | false, _, hd :: tl -> - out_name hd; out_list och chunk false (pred items) tl - in - let rec out_chunks och chunks c = - if chunks < c then out_clause och "!." else begin - KP.fprintf och "chunk %u,\n" c; out_chunks och chunks (succ c) - end - in - let chunks = out_list och 1 true size (List.rev !uris) in - out_clause och "main :- grundlagen."; - KP.fprintf och "grundlagen :-\n"; - out_chunks och (pred chunks) 1; - close_out och - -(* Interface functions ******************************************************) - -let open_out_lp1 fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname in - let och = open_out (path ^ "1" ^ ext_lp) in - out_preamble och; - out_top_comment och version; - out_clause och "accumulate helena."; - out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+"; - output_entity_lp1 och, close_out_lp1 och - -let open_out_lp2 fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname in - let och = open_out (path ^ "2" ^ ext_lp) in - out_preamble och; - out_top_comment och version; - out_clause och "accumulate helena."; - output_entity_lp2 och, close_out_lp2 och - -let open_out_tj2 fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname ^ "2" in - let och = open_out (path ^ ext_tj) in - out_preamble och; - out_top_comment och version; - out_clause och "module grundlagen."; - output_entity_tj2 och, close_out_tj2 och - -let open_out_tj3 fname = - let dir = KF.concat !G.manager_dir base in - let path = KF.concat dir fname in - let och = open_out (path ^ "3" ^ ext_tj) in - out_preamble och; - out_top_comment och version; - out_clause och "module grundlagen."; - out_clause och "accumulate helena."; - output_entity_tj3 och, close_out_tj3 och - -END diff --git a/helm/software/helena/src/basic_rg/brgLP.mli b/helm/software/helena/src/basic_rg/brgLP.mli deleted file mode 100644 index c56c6c079..000000000 --- a/helm/software/helena/src/basic_rg/brgLP.mli +++ /dev/null @@ -1,22 +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_______________________________________________________________ *) - -IFDEF MANAGER THEN - -val open_out_lp1: string -> Brg.manager - -val open_out_lp2: string -> Brg.manager - -val open_out_tj2: string -> Brg.manager - -val open_out_tj3: string -> Brg.manager - -END 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/brgMatita.ml b/helm/software/helena/src/basic_rg/brgMatita.ml new file mode 100644 index 000000000..adf79da58 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgMatita.ml @@ -0,0 +1,133 @@ +(* + ||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 ok = ref true + +let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) + +let base = "matita" + +let ext = ".ma" + +let width = 70 + +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 = + let padding = width - String.length msg in + let padding = if padding >= 0 then padding else 0 in + KP.fprintf och "(* %s %s*)\n\n" msg (String.make padding '*') + +let out_comment och msg = + KP.fprintf och "(* %s *)\n" msg + +let out_include och src = + KP.fprintf och "include \"%s.ma\".\n\n" src + +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" n + | false -> KP.fprintf och "_" + in + let err () = f "" false in + E.name err f a + +let rec out_term st p e och = function + | B.Sort k -> + let sort = if k = 0 then "Type[0]" else if k = 1 then "Prop" else assert false in + KP.fprintf och "%s" 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) -> + KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u + | B.Appl (_, v, t) -> + 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 (a, B.Abst (r, n, w), t) -> + let op, cp = if p then "(", ")" else "", "" 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 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 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 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 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 + +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) -> + KP.fprintf och "definition %a ≝ %a.\n\n%!" out_uri u (out_term st false B.empty) v; !ok + | 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 () + +(* Interface functions ******************************************************) + +let open_out fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ ext) in + out_preamble och; + out_top_comment och version; + out_include och "basics/pts"; + output_entity och, close_out och + +END diff --git a/helm/software/helena/src/basic_rg/brgMatita.mli b/helm/software/helena/src/basic_rg/brgMatita.mli new file mode 100644 index 000000000..1b68ccedb --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgMatita.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: string -> Brg.manager + +END 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/helena.ml b/helm/software/helena/src/toplevel/helena.ml new file mode 100644 index 000000000..1070dd915 --- /dev/null +++ b/helm/software/helena/src/toplevel/helena.ml @@ -0,0 +1,601 @@ +(* + ||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 KL = List +module KP = Printf +module KS = String +module KT = String + +module U = NUri +module C = Cps +module L = Log +module Y = Time +module P = Marks +module G = Options +module H = Hierarchy +module N = Layer +module E = Entity +module O = Output +module DO = CrgOutput +module TD = TxtCrg +module AA = AutProcess +module AO = AutOutput +module AD = AutCrg +module XL = XmlLibrary +module XD = XmlCrg +module B = Brg +module BD = BrgCrg +module BO = BrgOutput +module BR = BrgReduction +module BU = BrgUntrusted +module BM = BrgMatita +module BQ = BrgCoq +module BH = BrgHelena +(* module BC = BrgCC *) +module BY = BrgLYP +module ZD = BagCrg +module ZO = BagOutput +module ZT = BagType +module ZU = BagUntrusted + +type status = { + kst: N.status; + tst: TD.status; + pst: AA.status; + ast: AD.status; + ac : AO.counters; + dc : DO.counters; + bc : BO.counters; + zc : ZO.counters; + mst: B.manager option; +} + +let level = 0 + +let bag_error st s msg = + L.error st.kst ZO.specs (L.Warn s :: msg) + +let brg_error st s msg = + L.error st.kst BR.specs (L.Warn s :: msg) + +let initial_status () = { + kst = N.initial_status (); + tst = TD.initial_status (); + pst = AA.initial_status (); + ast = AD.initial_status (); + ac = AO.initial_counters; + dc = DO.initial_counters; + bc = BO.initial_counters; + zc = ZO.initial_counters; + mst = None; +} + +let refresh_status st = {st with + kst = N.refresh_status st.kst; + tst = TD.refresh_status st.tst; + ast = AD.refresh_status st.ast; +} + +(* kernel related ***********************************************************) + +type kernel_entity = BrgEntity of Brg.entity + | BagEntity of Bag.entity + | CrgEntity of Crg.entity + +IFDEF SUMMARY THEN + +let print_counters st = function + | G.V4 -> DO.print_counters C.start st.dc + | G.V3 -> BO.print_counters C.start st.bc + | G.V0 -> ZO.print_counters C.start st.zc + +END + +IFDEF TRACE THEN + +let pp_progress e = + let f _ na u = + let s = U.string_of_uri u in + L.warn 2 (KP.sprintf "[%u] <%s>" na.E.n_apix s); + in + Y.utime_stamp "intermediate"; + match e with + | CrgEntity e -> E.common f e + | BrgEntity e -> E.common f e + | BagEntity e -> E.common f e + +END + +IFDEF SUMMARY THEN + +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} + +END + +IFDEF OBJECTS THEN + +let export_entity st = function + | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e + | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e + | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e + +END + +IFDEF TYPE THEN + +let type_check st k = + let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in + let bag_err msg = bag_error st "Type Error" msg; failwith "Interrupted" in + let ok _ _ = st in + match k with + | BrgEntity entity -> BU.type_check brg_err ok st.kst entity + | BagEntity entity -> ZU.type_check bag_err ok st.kst entity + | CrgEntity _ -> st + +END + +IFDEF MANAGER THEN + +let manager st output_entity = function + | BrgEntity entity -> + if output_entity st.kst entity then st else + begin L.warn level "manager exportation stopped"; {st with mst = None} end + | BagEntity _ -> st + | CrgEntity _ -> st + +END + +let xlate_entity st entity = match !G.kernel, entity with + | G.V3, CrgEntity e -> + let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e + | G.V0, CrgEntity e -> + let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e + | _, entity -> entity + +let validate st k = + let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in + let ok _ = st in + match k with + | BrgEntity entity -> BU.validate brg_err ok st.kst entity + | BagEntity _ -> st + | CrgEntity _ -> st + +(* extended lexer ***********************************************************) + +type 'token lexer = { + parse : Lexing.lexbuf -> 'token; + mutable tokbuf: 'token option; + mutable unget : bool +} + +let initial_lexer parse = { + parse = parse; tokbuf = None; unget = false +} + +let token xl lexbuf = match xl.tokbuf with + | Some token when xl.unget -> + xl.unget <- false; token + | _ -> + let token = xl.parse lexbuf in + xl.tokbuf <- Some token; token + +(* input related ************************************************************) + +type input = Text | Automath + +type input_entity = TxtEntity of Txt.command + | AutEntity of Aut.command + | NoEntity + +let type_of_input name = + if KF.check_suffix name ".hln" then Text + else if KF.check_suffix name ".aut" then + let _ = H.set_sorts 0 ["Set"; "Prop"] in + assert (H.set_graph "Z2"); + Automath + else begin + L.warn level (KP.sprintf "Unknown file type: %s" name); exit 2 + end + +let txt_xl = initial_lexer TxtLexer.token + +let aut_xl = initial_lexer AutLexer.token + +let parbuf = ref [] (* parser buffer *) + +let gen_text command = + parbuf := TxtEntity command :: !parbuf + +let entity_of_input lexbuf i = match i, !parbuf with + | Automath, _ -> + begin match AutParser.entry (token aut_xl) lexbuf with + | Some e -> aut_xl.unget <- true; AutEntity e + | None -> NoEntity + end + | Text, [] -> + begin match TxtParser.entry (token txt_xl) lexbuf with + | Some e -> txt_xl.unget <- true; TxtEntity e + | None -> NoEntity + end + | Text, hd :: tl -> + parbuf := tl; hd + +IFDEF PREPROCESS THEN + +let process_input f st = function + | AutEntity e -> + let f pst e = f {st with pst = pst} (AutEntity e) in + AA.process_command f st.pst e + | xe -> f st xe + +END + +IFDEF SUMMARY THEN + +let count_input st = function + | AutEntity e -> {st with ac = AO.count_command C.start st.ac e} + | xe -> st + +END + +(****************************************************************************) + +let st = ref (initial_status ()) +let streaming = ref false (* parsing style (temporary) *) + +let process_2 st entity = + let st = +IFDEF SUMMARY THEN + if !G.summary then count_entity st entity else st +ELSE + st +END + in + let st = +IFDEF STAGE THEN + if !G.stage >= 3 then +IFDEF TYPE THEN + let f = if !G.validate then validate else type_check in f st entity +ELSE + validate st entity +END + else st +ELSE +IFDEF TYPE THEN + let f = if !G.validate then validate else type_check in f st entity +ELSE + validate st entity +END +END + in +IFDEF OBJECTS THEN + if !G.export then export_entity st entity +ELSE () END; +IFDEF MANAGER THEN + match st.mst with + | None -> st + | Some (export_entity, _) -> manager st export_entity entity +ELSE + st +END + +let process_1 st entity = +IFDEF TRACE THEN + if !G.ct >= 3 then pp_progress entity; +ELSE () END; + let st = +IFDEF SUMMARY THEN + if !G.summary then count_entity st entity else st +ELSE + st +END + in +IFDEF STAGE THEN +IFDEF OBJECTS THEN + if !G.export && !G.stage = 1 then export_entity st entity +ELSE () END; + if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st +ELSE + process_2 st (xlate_entity st entity) +END + +let process_0 st entity = + let f st entity = +IFDEF STAGE THEN + if !G.stage = 0 then st else + 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.kst st.ast 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 +ELSE + 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.kst st.ast 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 +END + in + let st = +IFDEF SUMMARY THEN + if !G.summary then count_input st entity else st +ELSE + st +END + in +IFDEF PREPROCESS THEN + if !G.preprocess then process_input f st entity else f st entity +ELSE + f st entity +END + +let process_nostreaming st lexbuf input = + let id x = x in + let rec aux1 book = match entity_of_input lexbuf input with + | NoEntity -> List.rev book + | e -> aux1 (id e :: book) + in + let rec aux2 st = function + | [] -> st + | entity :: tl -> aux2 (process_0 st entity) tl + in + aux2 st (aux1 []) + +let process_streaming st lexbuf input = + let rec aux st = match entity_of_input lexbuf input with + | NoEntity -> st + | e -> aux (process_0 st e) + in + aux st + +(****************************************************************************) + +IFDEF PREPROCESS THEN + +let set_preprocess () = + if !G.trace >= 2 then begin + G.preprocess := true; +IFDEF SUMMARY THEN + G.summary := true +ELSE () END + end + +END + +IFDEF MANAGER THEN + +let set_manager s = match KS.lowercase s with + | "v8" -> G.manager := G.Coq + | "ma2" -> G.manager := G.Matita + | "lp1" -> G.manager := G.LP1 + | "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 + +IFDEF SUMMARY THEN + +let set_summary () = + if !G.trace >= 2 then G.summary := true + +END + +let set_trace i = + if !G.trace = 0 && i > 0 then Y.gmtime (G.version_string false); + if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit"; + G.trace := i; +IFDEF SUMMARY THEN + if i <= 1 then G.summary := false +ELSE () END; +IFDEF PREPROCESS THEN + if i <= 1 then G.preprocess := false +ELSE () END + +let custom_exit () = + if !G.trace >= 1 then Y.utime_stamp "at exit" + +let process st name = + let process = if !streaming then process_streaming else process_nostreaming in + let input = type_of_input name in + let ich = open_in name in + let lexbuf = Lexing.from_channel ich in + let st = process st lexbuf input in + close_in ich; + st, input + +let main = + let print_version () = + let features = [ +(IFDEF LEXER THEN "LEXER" ELSE "" END); +(IFDEF PARSER THEN "PARSER" ELSE "" END); +(IFDEF TRACE THEN "TRACE" ELSE "" END); +(IFDEF SUMMARY THEN "SUMMARY" ELSE "" END); +(IFDEF EXPAND THEN "EXPAND" ELSE "" END); +(IFDEF MANAGER THEN "MANAGER" ELSE "" END); +(IFDEF OBJECTS THEN "OBJECTS" ELSE "" END); +(IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END); +(IFDEF QUOTE THEN "QUOTE" ELSE "" END); +(IFDEF STAGE THEN "STAGE" ELSE "" END); +(IFDEF TYPE THEN "TYPE" ELSE "" END); +(IFDEF PROFV THEN "PROFV" ELSE "" END); + ] in + let map s = s <> "" in + let features_string = KT.concat " " (KL.filter map features) in + L.warn level (KP.sprintf "%s [%s]" (G.version_string true) features_string); + exit 0 + in + let set_hierarchy s = + if H.set_graph s then () else + L.warn level (KP.sprintf "Unknown type hierarchy: %s" s) + in + let set_kernel = function + | "V3" -> G.kernel := G.V3 + | "V0" -> G.kernel := G.V0 + | s -> L.warn level (KP.sprintf "Unknown kernel version: %s" s) + in + let clear_options () = + G.clear (); H.clear (); +IFDEF SUMMARY THEN + O.clear_reductions () +ELSE () END; + streaming := false; + in + let undefined opt () = + 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 process_file name = + if !G.trace >= 2 then begin + L.warn 1 (KP.sprintf "Processing file: %s" name); + Y.utime_stamp "started" + end; + let base_name = Filename.chop_extension (Filename.basename name) in + let cover = KF.concat !G.root base_name in + G.cover := cover; +IFDEF STAGE THEN + if !G.stage <= 1 then G.kernel := G.V4; +ELSE () END; +IFDEF MANAGER THEN + begin match !G.manager with + | 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; + P.clear_marks (); + let sst, input = process (refresh_status !st) name in + st := begin match sst.mst with + | None -> sst + | Some (_, close_out) -> close_out (); {sst with mst = None} + end; + if !G.trace >= 2 then Y.utime_stamp "processed"; +IFDEF SUMMARY THEN + if !G.summary then begin + AO.print_counters C.start !st.ac; +IFDEF PREPROCESS THEN + if !G.preprocess then AO.print_process_counters C.start !st.pst +ELSE () END; +IFDEF STAGE THEN + if !G.stage >= 1 then print_counters !st G.V4; + if !G.stage >= 2 then print_counters !st !G.kernel; + if !G.stage >= 3 then O.print_reductions () +ELSE + print_counters !st G.V4; + print_counters !st !G.kernel; + O.print_reductions () +END + end +ELSE () END + in + let help = + "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts | -MO | -p | -ahkmr | -be ]* [ ]*\n\n" ^ + "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^ + " 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\" \"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 + let help_O = " [output] Set location of output directory (XML) to (default: current directory)" in + let help_P = " [parser] Show parser debug information" in + let help_T = " [trace] Set trace level (see above)" in + let help_V = " [version] Show version information" in + let help_X = " Clear options" in + + 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 + let help_h = " [hierarchy] Set type hierarchy (default: \"Z1\")" in + let help_i = " [indexes] Show local references by index" in + let help_k = " [kernel] Set kernel version (default: \"V3\")" in + let help_l = " [layer] Disambiguate binders layer (Automath)" in + let help_m = " [manager] Export kernel entities for this manager (see above, default: no manager)" in + let help_n = " [names] Show short constants (default: qualified constants)" in + let help_o = " [objects] Export kernel entities (XML)" in + let help_p = " [preamble] Set preamble to this file (default: empty)" in + let help_q = " [quote] Quote identifiers (default: disable)" in + let help_r = " [root] Set initial segment of URI hierarchy (default: empty)" in + let help_s = " [stage] Set translation stage (see above)" in + let help_t = " [type] Type check (default: validate)" in + let help_u = " [upsilon] Activate type comparison by sort inclusion (default: deactivate)" in + let help_x = " [extended] Use extended applications (Automath)" in + let help_y = " [infinity] Use ∞-abstractions in contexts" in + let help_0 = " [zero] Preprocess source (Automath)" in + let help_1 = " [one] parse files with streaming policy" in + at_exit custom_exit; + Arg.parse [ + ("-L", (IFDEF LEXER THEN Arg.Set G.debug_lexer ELSE arg_undefined "-L" END), help_L); + ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M); + ("-O", (IFDEF OBJECTS THEN Arg.String ((:=) G.xdir) ELSE arg_undefined "-O" END), help_O); + ("-P", (IFDEF PARSER THEN Arg.Set G.debug_parser ELSE arg_undefined "-P" END), help_P); + ("-T", Arg.Int set_trace, help_T); + ("-V", Arg.Unit print_version, help_V); + ("-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); + ("-h", Arg.String set_hierarchy, help_h); + ("-i", Arg.Set G.indexes, help_i); + ("-k", Arg.String set_kernel, help_k); + ("-l", Arg.Set G.cc, help_l); + ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m); + ("-n", Arg.Set G.short, help_n); + ("-o", (IFDEF OBJECTS THEN Arg.Set G.export ELSE arg_undefined "-o" END), help_o); + ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p); + ("-q", (IFDEF QUOTE THEN Arg.Set G.quote ELSE arg_undefined "-q" END), help_q); + ("-r", Arg.String ((:=) G.root), help_r); + ("-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.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; +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/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml deleted file mode 100644 index b7c6fc135..000000000 --- a/helm/software/helena/src/toplevel/top.ml +++ /dev/null @@ -1,586 +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 KF = Filename -module KL = List -module KP = Printf -module KS = String -module KT = String - -module U = NUri -module C = Cps -module L = Log -module Y = Time -module P = Marks -module G = Options -module H = Hierarchy -module N = Layer -module E = Entity -module O = Output -module DO = CrgOutput -module TD = TxtCrg -module AA = AutProcess -module AO = AutOutput -module AD = AutCrg -module XL = XmlLibrary -module XD = XmlCrg -module B = Brg -module BD = BrgCrg -module BO = BrgOutput -module BR = BrgReduction -module BU = BrgUntrusted -module BG = BrgGrafite -module BA = BrgGallina -module BP = BrgLP -module ZD = BagCrg -module ZO = BagOutput -module ZT = BagType -module ZU = BagUntrusted - -type status = { - kst: N.status; - tst: TD.status; - pst: AA.status; - ast: AD.status; - ac : AO.counters; - dc : DO.counters; - bc : BO.counters; - zc : ZO.counters; - mst: B.manager option; -} - -let level = 0 - -let bag_error st s msg = - L.error st.kst ZO.specs (L.Warn s :: msg) - -let brg_error st s msg = - L.error st.kst BR.specs (L.Warn s :: msg) - -let initial_status () = { - kst = N.initial_status (); - tst = TD.initial_status (); - pst = AA.initial_status (); - ast = AD.initial_status (); - ac = AO.initial_counters; - dc = DO.initial_counters; - bc = BO.initial_counters; - zc = ZO.initial_counters; - mst = None; -} - -let refresh_status st = {st with - kst = N.refresh_status st.kst; - tst = TD.refresh_status st.tst; - ast = AD.refresh_status st.ast; -} - -(* kernel related ***********************************************************) - -type kernel_entity = BrgEntity of Brg.entity - | BagEntity of Bag.entity - | CrgEntity of Crg.entity - -IFDEF SUMMARY THEN - -let print_counters st = function - | G.V4 -> DO.print_counters C.start st.dc - | G.V3 -> BO.print_counters C.start st.bc - | G.V0 -> ZO.print_counters C.start st.zc - -END - -IFDEF TRACE THEN - -let pp_progress e = - let f _ na u = - let s = U.string_of_uri u in - L.warn 2 (KP.sprintf "[%u] <%s>" na.E.n_apix s); - in - Y.utime_stamp "intermediate"; - match e with - | CrgEntity e -> E.common f e - | BrgEntity e -> E.common f e - | BagEntity e -> E.common f e - -END - -IFDEF SUMMARY THEN - -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} - -END - -IFDEF OBJECTS THEN - -let export_entity st = function - | CrgEntity e -> XL.export_entity (XD.export_term st.kst) e - | BrgEntity e -> XL.export_entity (BO.export_term st.kst) e - | BagEntity e -> XL.export_entity (ZO.export_term st.kst) e - -END - -IFDEF TYPE THEN - -let type_check st k = - let brg_err msg = brg_error st "Type Error" msg; failwith "Interrupted" in - let bag_err msg = bag_error st "Type Error" msg; failwith "Interrupted" in - let ok _ _ = st in - match k with - | BrgEntity entity -> BU.type_check brg_err ok st.kst entity - | BagEntity entity -> ZU.type_check bag_err ok st.kst entity - | CrgEntity _ -> st - -END - -IFDEF MANAGER THEN - -let manager st output_entity = function - | BrgEntity entity -> - if output_entity st.kst entity then st else - begin L.warn level "manager exportation stopped"; {st with mst = None} end - | BagEntity _ -> st - | CrgEntity _ -> st - -END - -let xlate_entity st entity = match !G.kernel, entity with - | G.V3, CrgEntity e -> - let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e - | G.V0, CrgEntity e -> - let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e - | _, entity -> entity - -let validate st k = - let brg_err msg = brg_error st "Validation Error" msg; failwith "Interrupted" in - let ok _ = st in - match k with - | BrgEntity entity -> BU.validate brg_err ok st.kst entity - | BagEntity _ -> st - | CrgEntity _ -> st - -(* extended lexer ***********************************************************) - -type 'token lexer = { - parse : Lexing.lexbuf -> 'token; - mutable tokbuf: 'token option; - mutable unget : bool -} - -let initial_lexer parse = { - parse = parse; tokbuf = None; unget = false -} - -let token xl lexbuf = match xl.tokbuf with - | Some token when xl.unget -> - xl.unget <- false; token - | _ -> - let token = xl.parse lexbuf in - xl.tokbuf <- Some token; token - -(* input related ************************************************************) - -type input = Text | Automath - -type input_entity = TxtEntity of Txt.command - | AutEntity of Aut.command - | NoEntity - -let type_of_input name = - if KF.check_suffix name ".hln" then Text - else if KF.check_suffix name ".aut" then - let _ = H.set_sorts 0 ["Set"; "Prop"] in - assert (H.set_graph "Z2"); - Automath - else begin - L.warn level (KP.sprintf "Unknown file type: %s" name); exit 2 - end - -let txt_xl = initial_lexer TxtLexer.token - -let aut_xl = initial_lexer AutLexer.token - -let parbuf = ref [] (* parser buffer *) - -let gen_text command = - parbuf := TxtEntity command :: !parbuf - -let entity_of_input lexbuf i = match i, !parbuf with - | Automath, _ -> - begin match AutParser.entry (token aut_xl) lexbuf with - | Some e -> aut_xl.unget <- true; AutEntity e - | None -> NoEntity - end - | Text, [] -> - begin match TxtParser.entry (token txt_xl) lexbuf with - | Some e -> txt_xl.unget <- true; TxtEntity e - | None -> NoEntity - end - | Text, hd :: tl -> - parbuf := tl; hd - -IFDEF PREPROCESS THEN - -let process_input f st = function - | AutEntity e -> - let f pst e = f {st with pst = pst} (AutEntity e) in - AA.process_command f st.pst e - | xe -> f st xe - -END - -IFDEF SUMMARY THEN - -let count_input st = function - | AutEntity e -> {st with ac = AO.count_command C.start st.ac e} - | xe -> st - -END - -(****************************************************************************) - -let st = ref (initial_status ()) -let streaming = ref false (* parsing style (temporary) *) - -let process_2 st entity = - let st = -IFDEF SUMMARY THEN - if !G.summary then count_entity st entity else st -ELSE - st -END - in - let st = -IFDEF STAGE THEN - if !G.stage >= 3 then -IFDEF TYPE THEN - let f = if !G.validate then validate else type_check in f st entity -ELSE - validate st entity -END - else st -ELSE -IFDEF TYPE THEN - let f = if !G.validate then validate else type_check in f st entity -ELSE - validate st entity -END -END - in -IFDEF OBJECTS THEN - if !G.export then export_entity st entity -ELSE () END; -IFDEF MANAGER THEN - match st.mst with - | None -> st - | Some (export_entity, _) -> manager st export_entity entity -ELSE - st -END - -let process_1 st entity = -IFDEF TRACE THEN - if !G.ct >= 3 then pp_progress entity; -ELSE () END; - let st = -IFDEF SUMMARY THEN - if !G.summary then count_entity st entity else st -ELSE - st -END - in -IFDEF STAGE THEN -IFDEF OBJECTS THEN - if !G.export && !G.stage = 1 then export_entity st entity -ELSE () END; - if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st -ELSE - process_2 st (xlate_entity st entity) -END - -let process_0 st entity = - let f st entity = -IFDEF STAGE THEN - if !G.stage = 0 then st else - 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.kst st.ast 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 -ELSE - 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.kst st.ast 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 -END - in - let st = -IFDEF SUMMARY THEN - if !G.summary then count_input st entity else st -ELSE - st -END - in -IFDEF PREPROCESS THEN - if !G.preprocess then process_input f st entity else f st entity -ELSE - f st entity -END - -let process_nostreaming st lexbuf input = - let id x = x in - let rec aux1 book = match entity_of_input lexbuf input with - | NoEntity -> List.rev book - | e -> aux1 (id e :: book) - in - let rec aux2 st = function - | [] -> st - | entity :: tl -> aux2 (process_0 st entity) tl - in - aux2 st (aux1 []) - -let process_streaming st lexbuf input = - let rec aux st = match entity_of_input lexbuf input with - | NoEntity -> st - | e -> aux (process_0 st e) - in - aux st - -(****************************************************************************) - -IFDEF PREPROCESS THEN - -let set_preprocess () = - if !G.trace >= 2 then begin - G.preprocess := true; -IFDEF SUMMARY THEN - G.summary := true -ELSE () END - end - -END - -IFDEF MANAGER THEN - -let set_manager s = match KS.lowercase s with - | "v8" -> G.manager := G.Coq - | "ma2" -> G.manager := G.Matita - | "lp1" -> G.manager := G.LP1 - | "lp2" -> G.manager := G.LP2 - | "tj2" -> G.manager := G.TJ2 - | "tj3" -> G.manager := G.TJ3 - | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) - -END - -IFDEF SUMMARY THEN - -let set_summary () = - if !G.trace >= 2 then G.summary := true - -END - -let set_trace i = - if !G.trace = 0 && i > 0 then Y.gmtime (G.version_string false); - if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit"; - G.trace := i; -IFDEF SUMMARY THEN - if i <= 1 then G.summary := false -ELSE () END; -IFDEF PREPROCESS THEN - if i <= 1 then G.preprocess := false -ELSE () END - -let custom_exit () = - if !G.trace >= 1 then Y.utime_stamp "at exit" - -let process st name = - let process = if !streaming then process_streaming else process_nostreaming in - let input = type_of_input name in - let ich = open_in name in - let lexbuf = Lexing.from_channel ich in - let st = process st lexbuf input in - close_in ich; - st, input - -let main = - let print_version () = - let features = [ -(IFDEF LEXER THEN "LEXER" ELSE "" END); -(IFDEF PARSER THEN "PARSER" ELSE "" END); -(IFDEF TRACE THEN "TRACE" ELSE "" END); -(IFDEF SUMMARY THEN "SUMMARY" ELSE "" END); -(IFDEF EXPAND THEN "EXPAND" ELSE "" END); -(IFDEF MANAGER THEN "MANAGER" ELSE "" END); -(IFDEF OBJECTS THEN "OBJECTS" ELSE "" END); -(IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END); -(IFDEF QUOTE THEN "QUOTE" ELSE "" END); -(IFDEF STAGE THEN "STAGE" ELSE "" END); -(IFDEF TYPE THEN "TYPE" ELSE "" END); -(IFDEF PROFV THEN "PROFV" ELSE "" END); - ] in - let map s = s <> "" in - let features_string = KT.concat " " (KL.filter map features) in - L.warn level (KP.sprintf "%s [%s]" (G.version_string true) features_string); - exit 0 - in - let set_hierarchy s = - if H.set_graph s then () else - L.warn level (KP.sprintf "Unknown type hierarchy: %s" s) - in - let set_kernel = function - | "V3" -> G.kernel := G.V3 - | "V0" -> G.kernel := G.V0 - | s -> L.warn level (KP.sprintf "Unknown kernel version: %s" s) - in - let clear_options () = - G.clear (); H.clear (); -IFDEF SUMMARY THEN - O.clear_reductions () -ELSE () END; - streaming := false; - in - let undefined opt () = - 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 process_file name = - if !G.trace >= 2 then begin - L.warn 1 (KP.sprintf "Processing file: %s" name); - Y.utime_stamp "started" - end; - let base_name = Filename.chop_extension (Filename.basename name) in - let cover = KF.concat !G.root base_name in - G.cover := cover; -IFDEF STAGE THEN - if !G.stage <= 1 then G.kernel := G.V4; -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.Quiet -> () - end -ELSE () END; - P.clear_marks (); - let sst, input = process (refresh_status !st) name in - st := begin match sst.mst with - | None -> sst - | Some (_, close_out) -> close_out (); {sst with mst = None} - end; - if !G.trace >= 2 then Y.utime_stamp "processed"; -IFDEF SUMMARY THEN - if !G.summary then begin - AO.print_counters C.start !st.ac; -IFDEF PREPROCESS THEN - if !G.preprocess then AO.print_process_counters C.start !st.pst -ELSE () END; -IFDEF STAGE THEN - if !G.stage >= 1 then print_counters !st G.V4; - if !G.stage >= 2 then print_counters !st !G.kernel; - if !G.stage >= 3 then O.print_reductions () -ELSE - print_counters !st G.V4; - print_counters !st !G.kernel; - O.print_reductions () -END - end -ELSE () END - in - let help = - "Usage: helena [ -LPVXdgilnoqtuxy01 | -Ts | -MO | -p | -ahkmr | -be ]* [ ]*\n\n" ^ - "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^ - " 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" - 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 - let help_O = " [output] Set location of output directory (XML) to (default: current directory)" in - let help_P = " [parser] Show parser debug information" in - let help_T = " [trace] Set trace level (see above)" in - let help_V = " [version] Show version information" in - let help_X = " Clear options" in - - 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_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 - let help_h = " [hierarchy] Set type hierarchy (default: \"Z1\")" in - let help_i = " [indexes] Show local references by index" in - let help_k = " [kernel] Set kernel version (default: \"V3\")" in - let help_l = " [layer] Disambiguate binders layer (Automath)" in - let help_m = " [manager] Export kernel entities for this manager (see above, default: no manager)" in - let help_n = " [names] Show short constants (default: qualified constants)" in - let help_o = " [objects] Export kernel entities (XML)" in - let help_p = " [preamble] Set preamble to this file (default: empty)" in - let help_q = " [quote] Quote identifiers (default: disable)" in - let help_r = " [root] Set initial segment of URI hierarchy (default: empty)" in - let help_s = " [stage] Set translation stage (see above)" in - let help_t = " [type] Type check (default: validate)" in - let help_u = " [upsilon] Activate type comparison by sort inclusion (default: deactivate)" in - let help_x = " [extended] Use extended applications (Automath)" in - let help_y = " [infinity] Use ∞-abstractions in contexts" in - let help_0 = " [zero] Preprocess source (Automath)" in - let help_1 = " [one] parse files with streaming policy" in - at_exit custom_exit; - Arg.parse [ - ("-L", (IFDEF LEXER THEN Arg.Set G.debug_lexer ELSE arg_undefined "-L" END), help_L); - ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M); - ("-O", (IFDEF OBJECTS THEN Arg.String ((:=) G.xdir) ELSE arg_undefined "-O" END), help_O); - ("-P", (IFDEF PARSER THEN Arg.Set G.debug_parser ELSE arg_undefined "-P" END), help_P); - ("-T", Arg.Int set_trace, help_T); - ("-V", Arg.Unit print_version, help_V); - ("-X", Arg.Unit clear_options, help_X); - ("-a", Arg.String ((:=) G.alpha), help_a); - ("-b", Arg.Int ((:=) G.first), help_b); - ("-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); - ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Set G.indexes, help_i); - ("-k", Arg.String set_kernel, help_k); - ("-l", Arg.Set G.cc, help_l); - ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m); - ("-n", Arg.Set G.short, help_n); - ("-o", (IFDEF OBJECTS THEN Arg.Set G.export ELSE arg_undefined "-o" END), help_o); - ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p); - ("-q", (IFDEF QUOTE THEN Arg.Set G.quote ELSE arg_undefined "-q" END), help_q); - ("-r", Arg.String ((:=) G.root), help_r); - ("-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); - ("-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 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