_build
*.native
+*.byte
matita/Makefile.defs
matita/autom4te.cache
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
-.depend.opt
Make*
README
examples/automath/*.aut
scripts/coq/*.template
scripts/lp/*.template
src/*.ml
-src/Make*
src/*/*
-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
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)"
@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
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
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)
+++ /dev/null
-lib common complete_rg text automath xml basic_rg basic_ag toplevel
+++ /dev/null
-aut autProcess autOutput autParser autLexer autCrg
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 *)
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)
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
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)
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
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
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
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
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;
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;
+++ /dev/null
-bag bagCrg bagOutput
-bagEnvironment bagSubstitution bagReduction bagType bagUntrusted
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) ->
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 =
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
| 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
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
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) ->
(* 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
+++ /dev/null
-brg brgCrg brgOutput
-brgEnvironment brgSubstitution brgReduction brgValidity brgType brgUntrusted
-brgGrafite brgGallina brgLP
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 *)
| 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 *)
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)
| 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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
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) ->
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) ->
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
+++ /dev/null
-(*
- ||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
+++ /dev/null
-(*
- ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
--- /dev/null
+(*
+ ||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
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 =
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 ()
step st (tstep m) w
end else
m, r, None
- | _, _, _, E.Void ->
+ | _, _, _, E.Void ->
assert false
end
| B.LRef (_, i) ->
| 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
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
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) ->
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
(* 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
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 () =
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;
| 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) ->
+++ /dev/null
-options hierarchy layer entity output alpha
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 *)
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 *)
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;
}
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
| 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
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 *)
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 *)
| 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; "" ]
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;
+++ /dev/null
-crg crgOutput
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
| 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
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
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
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
| 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
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 =
+++ /dev/null
-cps share log time marks
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
+++ /dev/null
-txt txtParser txtLexer txtCrg
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 *)
}
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) ->
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
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
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
--- /dev/null
+(*
+ ||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 <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\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 = "<dir> [manager] Set location of output directory (manager) to <dir> (default: current directory)" in
+ let help_O = "<dir> [output] Set location of output directory (XML) to <dir> (default: current directory)" in
+ let help_P = " [parser] Show parser debug information" in
+ let help_T = "<number> [trace] Set trace level (see above)" in
+ let help_V = " [version] Show version information" in
+ let help_X = " Clear options" in
+
+ let help_a = "<string> [alpha] Set prefix of numeric identifiers (default: empty)" in
+ let help_b = "<age> [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 = "<age> [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 = "<string> [hierarchy] Set type hierarchy (default: \"Z1\")" in
+ let help_i = " [indexes] Show local references by index" in
+ let help_k = "<string> [kernel] Set kernel version (default: \"V3\")" in
+ let help_l = " [layer] Disambiguate binders layer (Automath)" in
+ let help_m = "<string> [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 = "<file> [preamble] Set preamble to this file (default: empty)" in
+ let help_q = " [quote] Quote identifiers (default: disable)" in
+ let help_r = "<string> [root] Set initial segment of URI hierarchy (default: empty)" in
+ let help_s = "<number> [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
+++ /dev/null
-(*
- ||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 <number> | -MO <dir> | -p <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\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 = "<dir> [manager] Set location of output directory (manager) to <dir> (default: current directory)" in
- let help_O = "<dir> [output] Set location of output directory (XML) to <dir> (default: current directory)" in
- let help_P = " [parser] Show parser debug information" in
- let help_T = "<number> [trace] Set trace level (see above)" in
- let help_V = " [version] Show version information" in
- let help_X = " Clear options" in
-
- let help_a = "<string> [alpha] Set prefix of numeric identifiers (default: empty)" in
- let help_b = "<age> [begin] Begin trace at this global constant (default: first)" in
- let help_d = " [data] Show summary information (requires trace >= 2)" in
- let help_e = "<age> [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 = "<string> [hierarchy] Set type hierarchy (default: \"Z1\")" in
- let help_i = " [indexes] Show local references by index" in
- let help_k = "<string> [kernel] Set kernel version (default: \"V3\")" in
- let help_l = " [layer] Disambiguate binders layer (Automath)" in
- let help_m = "<string> [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 = "<file> [preamble] Set preamble to this file (default: empty)" in
- let help_q = " [quote] Quote identifiers (default: disable)" in
- let help_r = "<string> [root] Set initial segment of URI hierarchy (default: empty)" in
- let help_s = "<number> [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
+++ /dev/null
-xmlLibrary xmlCrg
(* 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)
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 =
V_______________________________________________________________ *)
module KF = Filename
+module KP = Printf
module U = NUri
module C = Cps
let cast = "Cast"
-let appl x = if x then "Appx" else "Appr"
+let appl = "Appl"
let proj = "Proj"
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;
]
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
val cast: string
-val appl: bool -> string
+val appl: string
val proj: string
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
projects / helm.git / commitdiff