src/lib/cps.cmx src/common/ccs.cmi
src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi
src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx
+src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx
+src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx
+src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
+src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/complete_rg/crgOutput.cmi
src/text/txt.cmo: src/common/level.cmi
src/text/txt.cmx: src/common/level.cmx
src/text/txtParser.cmi: src/text/txt.cmx
src/text/txtTxt.cmi: src/text/txt.cmx
src/text/txtTxt.cmo: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
src/text/txtTxt.cmx: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
+src/text/txtCrg.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
+src/text/txtCrg.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
+ src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi
+src/text/txtCrg.cmx: src/text/txtTxt.cmx src/text/txt.cmx \
+ src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/text/txtCrg.cmi
src/automath/aut.cmo: src/common/entity.cmx
src/automath/aut.cmx: src/common/entity.cmx
src/automath/autProcess.cmi: src/automath/aut.cmx
src/automath/autParser.cmi
src/automath/autLexer.cmx: src/common/options.cmx src/lib/log.cmx \
src/automath/autParser.cmx
-src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx
-src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx
-src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx
-src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \
- src/basic_ag/bagOutput.cmi
-src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \
- src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \
- src/basic_ag/bagOutput.cmi
-src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx
-src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \
- src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
-src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \
- src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
-src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx
-src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \
- src/basic_ag/bagSubstitution.cmi
-src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \
- src/basic_ag/bagSubstitution.cmi
-src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx
-src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \
- src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \
- src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
-src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \
- src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \
- src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
-src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx
-src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \
- src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \
- src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
- src/basic_ag/bagType.cmi
-src/basic_ag/bagType.cmx: src/common/status.cmx src/lib/share.cmx \
- src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \
- src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
- src/basic_ag/bagType.cmi
-src/basic_ag/bagUntrusted.cmi: src/common/status.cmx src/basic_ag/bag.cmx
-src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
- src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \
- src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
-src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
- src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \
- src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
-src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx
-src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx
-src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
-src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
- src/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \
- src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
- src/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
-src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
- src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
-src/complete_rg/crgTxt.cmx: src/text/txtTxt.cmx src/text/txt.cmx \
- src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
-src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx
-src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/level.cmi \
+src/automath/autCrg.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx
+src/automath/autCrg.cmo: src/common/options.cmx src/common/level.cmi \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/automath/aut.cmx src/complete_rg/crgAut.cmi
-src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/level.cmx \
+ src/automath/aut.cmx src/automath/autCrg.cmi
+src/automath/autCrg.cmx: src/common/options.cmx src/common/level.cmx \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/automath/aut.cmx src/complete_rg/crgAut.cmi
+ src/automath/aut.cmx src/automath/autCrg.cmi
src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx \
src/common/ccs.cmi
src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \
src/basic_rg/brgType.cmx src/basic_rg/brgReduction.cmx \
src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
src/basic_rg/brgUntrusted.cmi
-src/toplevel/meta.cmo: src/common/entity.cmx
-src/toplevel/meta.cmx: src/common/entity.cmx
-src/toplevel/metaOutput.cmi: src/toplevel/meta.cmx
-src/toplevel/metaOutput.cmo: src/toplevel/meta.cmx src/lib/log.cmi \
- src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi
-src/toplevel/metaOutput.cmx: src/toplevel/meta.cmx src/lib/log.cmx \
- src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi
-src/toplevel/metaAut.cmi: src/toplevel/meta.cmx src/automath/aut.cmx
-src/toplevel/metaAut.cmo: src/common/options.cmx src/toplevel/meta.cmx \
- src/common/level.cmi src/common/entity.cmx src/lib/cps.cmx \
- src/automath/aut.cmx src/toplevel/metaAut.cmi
-src/toplevel/metaAut.cmx: src/common/options.cmx src/toplevel/meta.cmx \
- src/common/level.cmx src/common/entity.cmx src/lib/cps.cmx \
- src/automath/aut.cmx src/toplevel/metaAut.cmi
-src/toplevel/metaBag.cmi: src/toplevel/meta.cmx src/basic_ag/bag.cmx
-src/toplevel/metaBag.cmo: src/toplevel/meta.cmx src/lib/cps.cmx \
- src/basic_ag/bag.cmx src/toplevel/metaBag.cmi
-src/toplevel/metaBag.cmx: src/toplevel/meta.cmx src/lib/cps.cmx \
- src/basic_ag/bag.cmx src/toplevel/metaBag.cmi
-src/toplevel/metaBrg.cmi: src/toplevel/meta.cmx src/basic_rg/brg.cmx
-src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/level.cmi \
- src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
- src/toplevel/metaBrg.cmi
-src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/level.cmx \
- src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
- src/toplevel/metaBrg.cmi
+src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx
+src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx
+src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx
+src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagOutput.cmi
+src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagOutput.cmi
+src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx
+src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \
+ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
+src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \
+ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
+src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx
+src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagSubstitution.cmi
+src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagSubstitution.cmi
+src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx
+src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \
+ src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \
+ src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \
+ src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
+src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \
+ src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \
+ src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \
+ src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
+src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx
+src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \
+ src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
+ src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \
+ src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
+ src/basic_ag/bagType.cmi
+src/basic_ag/bagType.cmx: src/common/status.cmx src/lib/share.cmx \
+ src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+ src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \
+ src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagType.cmi
+src/basic_ag/bagUntrusted.cmi: src/common/status.cmx src/basic_ag/bag.cmx
+src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
+ src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \
+ src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
+src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
+ src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \
+ src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
- src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \
- src/lib/time.cmx src/common/status.cmx src/common/output.cmi \
- src/common/options.cmx src/toplevel/metaOutput.cmi \
- src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \
- src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \
- src/complete_rg/crgOutput.cmi src/complete_rg/crgAut.cmi \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmi \
- src/basic_rg/brgReduction.cmi src/basic_rg/brgOutput.cmi \
- src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
+ src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txtCrg.cmi \
+ src/text/txt.cmx src/lib/time.cmx src/common/status.cmx \
+ src/common/output.cmi src/common/options.cmx src/lib/log.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx \
+ src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
+ src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \
src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \
src/automath/autProcess.cmi src/automath/autParser.cmi \
- src/automath/autOutput.cmi src/automath/autLexer.cmx src/automath/aut.cmx
+ src/automath/autOutput.cmi src/automath/autLexer.cmx \
+ src/automath/autCrg.cmi src/automath/aut.cmx
src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \
- src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txt.cmx \
- src/lib/time.cmx src/common/status.cmx src/common/output.cmx \
- src/common/options.cmx src/toplevel/metaOutput.cmx \
- src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \
- src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \
- src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \
- src/complete_rg/crgOutput.cmx src/complete_rg/crgAut.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmx \
- src/basic_rg/brgReduction.cmx src/basic_rg/brgOutput.cmx \
- src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
+ src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \
+ src/text/txt.cmx src/lib/time.cmx src/common/status.cmx \
+ src/common/output.cmx src/common/options.cmx src/lib/log.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx \
+ src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
+ src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \
src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \
src/automath/autProcess.cmx src/automath/autParser.cmx \
- src/automath/autOutput.cmx src/automath/autLexer.cmx src/automath/aut.cmx
+ src/automath/autOutput.cmx src/automath/autLexer.cmx \
+ src/automath/autCrg.cmx src/automath/aut.cmx
CLEAN = etc/log.txt etc/profile.txt
-TAGS = test-si test-si-fast hal xml-si-crg xml-si profile
+TAGS = test-si test-si-fast xml-si-crg xml-si profile
XMLLINTLOCAL = --nonet --path xml --dtdvalid ld.dtd
INPUT = examples/grundlagen/grundlagen.aut
test-si: $(MAIN).opt etc
- @echo " HELENA -p -u -c $(INPUT)"
- $(H)./$(MAIN).opt -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -p -o -c $(INPUT)"
+ $(H)./$(MAIN).opt -p -o -c -S 3 $(O) $(INPUT) > etc/log.txt
test-si-fast: $(MAIN).opt etc
- @echo " HELENA -u -q $(INPUT)"
- $(H)./$(MAIN).opt -u -q -S 1 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -o -q $(INPUT)"
+ $(H)./$(MAIN).opt -o -q -S 1 $(O) $(INPUT) > etc/log.txt
profile: $(MAIN).opt etc
- @echo " HELENA -u -q $(INPUT) (30 TIMES)"
+ @echo " HELENA -o -q $(INPUT) (30 TIMES)"
$(H)rm etc/log.txt
- $(H)for T in `seq 30`; do ./$(MAIN).opt -u -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done
+ $(H)for T in `seq 30`; do ./$(MAIN).opt -o -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done
$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
xml-si: $(MAIN).opt etc
- @echo " HELENA -u -x -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
+ @echo " HELENA -o -x -s 2 $(INPUT)"
+ $(H)./$(MAIN).opt -o -x -s 2 -S 1 $(INPUT) > etc/log.txt
xml-si-crg: $(MAIN).opt etc
- @echo " HELENA -u -x -s 1 $(INPUT)"
- $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt
+ @echo " HELENA -o -x -s 1 $(INPUT)"
+ $(H)./$(MAIN).opt -o -x -s 1 -S 1 $(INPUT) > etc/log.txt
etc:
@echo " MKDIR etc"
install-xml: etc/make-html.sh
@echo " INSTALL xml"
$(H)scp -r xml/index.txt xml/ld.dtd xml/brg-si/ xml/crg-si/ $(XMLDIR)
-
-# old targets ##########################################################
-
-test: $(MAIN).opt etc
- @echo " HELENA -o -p $(INPUT)"
- $(H)./$(MAIN).opt -o -p -S 3 $(O) $(INPUT) > etc/log.txt
-
-test-si-old: $(MAIN).opt etc
- @echo " HELENA -o -p -u -c $(INPUT)"
- $(H)./$(MAIN).opt -o -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt
-
-test-si-fast-old: $(MAIN).opt etc
- @echo " HELENA -o -u -q $(INPUT)"
- $(H)./$(MAIN).opt -o -u -q -S 1 $(O) $(INPUT) > etc/log.txt
-
-xml-si-old: $(MAIN).opt etc
- @echo " HELENA -o -u -x -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
-lib common text automath basic_ag complete_rg xml basic_rg toplevel
+lib common complete_rg text automath xml basic_rg basic_ag toplevel
-aut autProcess autOutput autParser autLexer
+aut autProcess autOutput autParser autLexer autCrg
--- /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 U = NUri
+module K = U.UriHash
+module C = Cps
+module G = Options
+module E = Entity
+module N = Level
+module A = Aut
+module D = Crg
+
+(* qualified identifier: uri, name, qualifiers *)
+type qid = D.uri * D.id * D.id list
+
+type context = E.attrs * D.term list
+
+type context_node = qid option (* context node: None = root *)
+
+type status = {
+ path: D.id list; (* current section path *)
+ node: context_node; (* current context node *)
+ nodes: context_node list; (* context node list *)
+ line: int; (* line number *)
+ mk_uri:G.uri_generator (* uri generator *)
+}
+
+type resolver = Local of int
+ | Global of context
+
+let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
+
+let henv = K.create henv_size (* optimized global environment *)
+
+let hcnt = K.create hcnt_size (* optimized context *)
+
+(* Internal functions *******************************************************)
+
+let empty_cnt = [], [], []
+
+let add_abst (a, ws, ns) id w n =
+ E.Name (id, true) :: a, w :: ws, N.succ n :: ns
+
+let mk_lref f n i j k = f n (D.TLRef ([E.Apix k], i, j))
+
+let id_of_name (id, _, _) = id
+
+let mk_qid f st id path =
+ let str = String.concat "/" path in
+ let str = Filename.concat str id in
+ let str = st.mk_uri str in
+ f (U.uri_of_string str, id, path)
+
+let uri_of_qid (uri, _, _) = uri
+
+let complete_qid f st (id, is_local, qs) =
+ let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
+ let rec skip f = function
+ | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
+ | _ :: ptl, _ :: _ -> skip f (ptl, qs)
+ | _ -> f []
+ in
+ if is_local then f st.path else skip f (st.path, qs)
+
+let relax_qid f st (_, id, path) =
+ let f = function
+ | _ :: tl -> C.list_rev (mk_qid f st id) tl
+ | [] -> assert false
+ in
+ C.list_rev f path
+
+let relax_opt_qid f st = function
+ | None -> f None
+ | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
+
+let resolve_gref err f st qid =
+ try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt
+ with Not_found -> err qid
+
+let resolve_gref_relaxed f st qid =
+(* this is not tail recursive *)
+ let rec err qid = relax_qid (resolve_gref err f st) st qid in
+ resolve_gref err f st qid
+
+let get_cnt err f st = function
+ | None -> f empty_cnt
+ | Some qid as node ->
+ try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
+ with Not_found -> err node
+
+let get_cnt_relaxed f st =
+(* this is not tail recursive *)
+ let rec err node = relax_opt_qid (get_cnt err f st) st node in
+ get_cnt err f st st.node
+
+(****************************************************************************)
+
+let push_abst f (lenv, ns) a n w =
+ let bw = D.Abst (N.infinite, [w]) in
+ let f lenv = f (lenv, N.succ n :: ns) in
+ D.push_bind f lenv a bw
+
+let resolve_lref err f id (lenv, ns) =
+ let f i j k = f (List.nth ns k) i j k in
+ D.resolve_lref err f id lenv
+
+let lenv_of_cnt (a, ws, ns) =
+ D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns
+
+(* this is not tail recursive in the GRef branch *)
+let rec xlate_term f st lenv = function
+ | A.Sort s ->
+ let f h = f (N.finite 0) (D.TSort ([], h)) in
+ if s then f 0 else f 1
+ | A.Appl (v, t) ->
+ let f vv n tt = f n (D.TAppl ([], [vv], tt)) in
+ let f _ vv = xlate_term (f vv) st lenv t in
+ xlate_term f st lenv v
+ | A.Abst (name, w, t) ->
+ let f nw ww =
+ let a = [E.Name (name, true)] in
+ let f nt tt =
+ let b = D.Abst (nt, [ww]) in
+ f nt (D.TBind (a, b, tt))
+ in
+ let f lenv = xlate_term f st lenv t in
+ push_abst f lenv a nw ww
+ in
+ xlate_term f st lenv w
+ | A.GRef (name, args) ->
+ let map1 f = function
+ | E.Name (id, _) -> f (A.GRef ((id, true, []), []))
+ | _ -> C.err ()
+ in
+ let map2 f t =
+ let f _ tt = f tt in xlate_term f st lenv t
+ in
+ let g n qid (a, _, _) =
+ let gref = D.TGRef ([], uri_of_qid qid) in
+ match args, a with
+ | [], [] -> f n gref
+ | _ ->
+ let f args = f n (D.TAppl ([], args, gref)) in
+ let f args = C.list_rev_map f map2 args in
+ let f a = C.list_rev_map_append f map1 a ~tail:args in
+ C.list_sub_strict f a args
+ in
+ let g qid = resolve_gref_relaxed g st qid in
+ let err () = complete_qid g st name in
+ resolve_lref err (mk_lref f) (id_of_name name) lenv
+
+let xlate_entity err f st = function
+ | A.Section (Some (_, name)) ->
+ err {st with path = name :: st.path; nodes = st.node :: st.nodes}
+ | A.Section None ->
+ begin match st.path, st.nodes with
+ | _ :: ptl, nhd :: ntl ->
+ err {st with path = ptl; node = nhd; nodes = ntl}
+ | _ -> assert false
+ end
+ | A.Context None ->
+ err {st with node = None}
+ | A.Context (Some name) ->
+ let f name = err {st with node = Some name} in
+ complete_qid f st name
+ | A.Block (name, w) ->
+ let f qid =
+ let f cnt =
+ let lenv = lenv_of_cnt cnt in
+ let f nw ww =
+ K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw);
+ err {st with node = Some qid}
+ in
+ xlate_term f st lenv w
+ in
+ get_cnt_relaxed f st
+ in
+ complete_qid f st (name, true, [])
+ | A.Decl (name, w) ->
+ let f cnt =
+ let a, ws, _ = cnt in
+ let lenv = lenv_of_cnt cnt in
+ let f qid =
+ let f nw ww =
+ K.add henv (uri_of_qid qid) (N.succ nw, cnt);
+ let t = match ws with
+ | [] -> ww
+ | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww)
+ in
+(*
+ print_newline (); CrgOutput.pp_term print_string t;
+*)
+ let b = E.Abst (N.infinite, t) in
+ let entity = [E.Mark st.line], uri_of_qid qid, b in
+ f {st with line = succ st.line} entity
+ in
+ xlate_term f st lenv w
+ in
+ complete_qid f st (name, true, [])
+ in
+ get_cnt_relaxed f st
+ | A.Def (name, w, trans, v) ->
+ let f cnt =
+ let a, ws, _ = cnt in
+ let lenv = lenv_of_cnt cnt in
+ let f qid =
+ let f nw ww =
+ let f nv vv =
+ assert (nv = N.succ nw); (**)
+ K.add henv (uri_of_qid qid) (nv, cnt);
+ let t = match ws with
+ | [] -> D.TCast ([], ww, vv)
+ | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv))
+ in
+(*
+ print_newline (); CrgOutput.pp_term print_string t;
+*)
+ let b = E.Abbr t in
+ let a = E.Mark st.line :: if trans then [] else [E.Priv] in
+ let entity = a, uri_of_qid qid, b in
+ f {st with line = succ st.line} entity
+ in
+ xlate_term f st lenv v
+ in
+ xlate_term f st lenv w
+ in
+ complete_qid f st (name, true, [])
+ in
+ get_cnt_relaxed f st
+
+(* Interface functions ******************************************************)
+
+let initial_status () =
+ K.clear henv; K.clear hcnt; {
+ path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ()
+}
+
+let refresh_status st = {st with
+ mk_uri = G.get_mk_uri ()
+}
+
+let crg_of_aut = xlate_entity
--- /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_______________________________________________________________ *)
+
+type status
+
+val initial_status: unit -> status
+
+val refresh_status: status -> status
+
+val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) ->
+ status -> Aut.command -> 'a
--- /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 C = Cps
+module E = Entity
+module J = Marks
+module N = Level
+module D = Crg
+module Z = Bag
+
+(* internal functions: crg to bag term **************************************)
+
+let rec lenv_fold_left map1 map2 x = function
+ | D.ESort -> x
+ | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
+ | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
+
+let rec xlate_term f = function
+ | D.TSort (a, l) -> f (Z.Sort (a, l))
+ | D.TGRef (a, n) -> f (Z.GRef (a, n))
+ | D.TLRef (a, _, _) -> let f i = f (Z.LRef (a, i)) in E.apix C.err f a
+ | D.TCast (a, u, t) ->
+ let f uu tt = f (Z.Cast (a, uu, tt)) in
+ let f uu = xlate_term (f uu) t in
+ xlate_term f u
+ | D.TAppl (a, vs, t) ->
+ let map f v tt = let f vv = f (Z.Appl (a, vv, tt)) in xlate_term f v in
+ let f tt = C.list_fold_right f map vs tt in
+ xlate_term f t
+ | D.TProj (a, e, t) ->
+ let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
+ xlate_term f t
+ | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
+ xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+ | D.TBind (a, b, t) ->
+ let f tt = f (xlate_bind tt a b) in xlate_term f t
+
+and xlate_bind x a b =
+ let f a ns = a, ns in
+ let a, ns = E.get_names f a in
+ match b with
+ | D.Abst (m, ws) ->
+ let map x n w =
+ let f ww = Z.Bind (n :: J.new_mark () :: a, Z.Abst (m, ww), x) in
+ xlate_term f w
+ in
+ List.fold_left2 map x ns ws
+ | D.Abbr vs ->
+ let map x n v =
+ let f vv = Z.Bind (n :: a, Z.Abbr vv, x) in
+ xlate_term f v
+ in
+ List.fold_left2 map x ns vs
+ | D.Void _ ->
+ let map x n = Z.Bind (n :: a, Z.Void, x) in
+ List.fold_left map x ns
+
+and xlate_proj x _ e =
+ lenv_fold_left xlate_bind xlate_proj x e
+
+(* internal functions: bag to crg term **************************************)
+
+let rec xlate_bk_term f = function
+ | Z.Sort (a, l) -> f (D.TSort (a, l))
+ | Z.GRef (a, n) -> f (D.TGRef (a, n))
+ | Z.LRef (a, i) -> f (D.TLRef (a, i, 0))
+ | Z.Cast (a, u, t) ->
+ let f uu tt = f (D.TCast (a, uu, tt)) in
+ let f uu = xlate_bk_term (f uu) t in
+ xlate_bk_term f u
+ | Z.Appl (a, u, t) ->
+ let f uu tt = f (D.TAppl (a, [uu], tt)) in
+ let f uu = xlate_bk_term (f uu) t in
+ xlate_bk_term f u
+ | Z.Bind (a, b, t) ->
+ let f bb tt = f (D.TBind (a, bb, tt)) in
+ let f bb = xlate_bk_term (f bb) t in
+ xlate_bk_bind f b
+
+and xlate_bk_bind f = function
+ | Z.Abst (n, t) ->
+ let f tt = f (D.Abst (n, [tt])) in
+ xlate_bk_term f t
+ | Z.Abbr t ->
+ let f tt = f (D.Abbr [tt]) in
+ xlate_bk_term f t
+ | Z.Void -> f (D.Void 1)
+
+(* interface functions ******************************************************)
+
+let bag_of_crg f t =
+ f (xlate_term C.start t)
+
+let crg_of_bag = xlate_bk_term
--- /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_______________________________________________________________ *)
+
+val bag_of_crg: (Bag.term -> 'a) -> Crg.term -> 'a
+(*
+val crg_of_bag: (Crg.term -> 'a) -> Bag.term -> 'a
+*)
O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, r2, t)
| _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1),
- _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) ->
- if n1 = n2 && ac {st with S.si = false} m1 w1 m2 w2 then
+ _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)
+ when n1 = n2 || st.S.si ->
+ if ac {st with S.si = false} m1 w1 m2 w2 then
ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
| _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)
- when N.is_zero n && st.S.si ->
+ when N.is_zero n || st.S.si ->
O.add ~si:1 ();
ac st (push m1 a b) u (push m2 a b) t
| _ -> false
-crg crgOutput crgTxt crgAut
+crg crgOutput
+++ /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 U = NUri
-module K = U.UriHash
-module C = Cps
-module G = Options
-module E = Entity
-module N = Level
-module A = Aut
-module D = Crg
-
-(* qualified identifier: uri, name, qualifiers *)
-type qid = D.uri * D.id * D.id list
-
-type context = E.attrs * D.term list
-
-type context_node = qid option (* context node: None = root *)
-
-type status = {
- path: D.id list; (* current section path *)
- node: context_node; (* current context node *)
- nodes: context_node list; (* context node list *)
- line: int; (* line number *)
- mk_uri:G.uri_generator (* uri generator *)
-}
-
-type resolver = Local of int
- | Global of context
-
-let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
-
-let henv = K.create henv_size (* optimized global environment *)
-
-let hcnt = K.create hcnt_size (* optimized context *)
-
-(* Internal functions *******************************************************)
-
-let empty_cnt = [], [], []
-
-let add_abst (a, ws, ns) id w n =
- E.Name (id, true) :: a, w :: ws, N.succ n :: ns
-
-let mk_lref f n i j k = f n (D.TLRef ([E.Apix k], i, j))
-
-let id_of_name (id, _, _) = id
-
-let mk_qid f st id path =
- let str = String.concat "/" path in
- let str = Filename.concat str id in
- let str = st.mk_uri str in
- f (U.uri_of_string str, id, path)
-
-let uri_of_qid (uri, _, _) = uri
-
-let complete_qid f st (id, is_local, qs) =
- let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
- let rec skip f = function
- | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
- | _ :: ptl, _ :: _ -> skip f (ptl, qs)
- | _ -> f []
- in
- if is_local then f st.path else skip f (st.path, qs)
-
-let relax_qid f st (_, id, path) =
- let f = function
- | _ :: tl -> C.list_rev (mk_qid f st id) tl
- | [] -> assert false
- in
- C.list_rev f path
-
-let relax_opt_qid f st = function
- | None -> f None
- | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
-
-let resolve_gref err f st qid =
- try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt
- with Not_found -> err qid
-
-let resolve_gref_relaxed f st qid =
-(* this is not tail recursive *)
- let rec err qid = relax_qid (resolve_gref err f st) st qid in
- resolve_gref err f st qid
-
-let get_cnt err f st = function
- | None -> f empty_cnt
- | Some qid as node ->
- try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
- with Not_found -> err node
-
-let get_cnt_relaxed f st =
-(* this is not tail recursive *)
- let rec err node = relax_opt_qid (get_cnt err f st) st node in
- get_cnt err f st st.node
-
-(****************************************************************************)
-
-let push_abst f (lenv, ns) a n w =
- let bw = D.Abst (N.infinite, [w]) in
- let f lenv = f (lenv, N.succ n :: ns) in
- D.push_bind f lenv a bw
-
-let resolve_lref err f id (lenv, ns) =
- let f i j k = f (List.nth ns k) i j k in
- D.resolve_lref err f id lenv
-
-let lenv_of_cnt (a, ws, ns) =
- D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns
-
-(* this is not tail recursive in the GRef branch *)
-let rec xlate_term f st lenv = function
- | A.Sort s ->
- let f h = f (N.finite 0) (D.TSort ([], h)) in
- if s then f 0 else f 1
- | A.Appl (v, t) ->
- let f vv n tt = f n (D.TAppl ([], [vv], tt)) in
- let f _ vv = xlate_term (f vv) st lenv t in
- xlate_term f st lenv v
- | A.Abst (name, w, t) ->
- let f nw ww =
- let a = [E.Name (name, true)] in
- let f nt tt =
- let b = D.Abst (nt, [ww]) in
- f nt (D.TBind (a, b, tt))
- in
- let f lenv = xlate_term f st lenv t in
- push_abst f lenv a nw ww
- in
- xlate_term f st lenv w
- | A.GRef (name, args) ->
- let map1 f = function
- | E.Name (id, _) -> f (A.GRef ((id, true, []), []))
- | _ -> C.err ()
- in
- let map2 f t =
- let f _ tt = f tt in xlate_term f st lenv t
- in
- let g n qid (a, _, _) =
- let gref = D.TGRef ([], uri_of_qid qid) in
- match args, a with
- | [], [] -> f n gref
- | _ ->
- let f args = f n (D.TAppl ([], args, gref)) in
- let f args = C.list_rev_map f map2 args in
- let f a = C.list_rev_map_append f map1 a ~tail:args in
- C.list_sub_strict f a args
- in
- let g qid = resolve_gref_relaxed g st qid in
- let err () = complete_qid g st name in
- resolve_lref err (mk_lref f) (id_of_name name) lenv
-
-let xlate_entity err f st = function
- | A.Section (Some (_, name)) ->
- err {st with path = name :: st.path; nodes = st.node :: st.nodes}
- | A.Section None ->
- begin match st.path, st.nodes with
- | _ :: ptl, nhd :: ntl ->
- err {st with path = ptl; node = nhd; nodes = ntl}
- | _ -> assert false
- end
- | A.Context None ->
- err {st with node = None}
- | A.Context (Some name) ->
- let f name = err {st with node = Some name} in
- complete_qid f st name
- | A.Block (name, w) ->
- let f qid =
- let f cnt =
- let lenv = lenv_of_cnt cnt in
- let f nw ww =
- K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw);
- err {st with node = Some qid}
- in
- xlate_term f st lenv w
- in
- get_cnt_relaxed f st
- in
- complete_qid f st (name, true, [])
- | A.Decl (name, w) ->
- let f cnt =
- let a, ws, _ = cnt in
- let lenv = lenv_of_cnt cnt in
- let f qid =
- let f nw ww =
- K.add henv (uri_of_qid qid) (N.succ nw, cnt);
- let t = match ws with
- | [] -> ww
- | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww)
- in
-(*
- print_newline (); CrgOutput.pp_term print_string t;
-*)
- let b = E.Abst (N.infinite, t) in
- let entity = [E.Mark st.line], uri_of_qid qid, b in
- f {st with line = succ st.line} entity
- in
- xlate_term f st lenv w
- in
- complete_qid f st (name, true, [])
- in
- get_cnt_relaxed f st
- | A.Def (name, w, trans, v) ->
- let f cnt =
- let a, ws, _ = cnt in
- let lenv = lenv_of_cnt cnt in
- let f qid =
- let f nw ww =
- let f nv vv =
- assert (nv = N.succ nw); (**)
- K.add henv (uri_of_qid qid) (nv, cnt);
- let t = match ws with
- | [] -> D.TCast ([], ww, vv)
- | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv))
- in
-(*
- print_newline (); CrgOutput.pp_term print_string t;
-*)
- let b = E.Abbr t in
- let a = E.Mark st.line :: if trans then [] else [E.Priv] in
- let entity = a, uri_of_qid qid, b in
- f {st with line = succ st.line} entity
- in
- xlate_term f st lenv v
- in
- xlate_term f st lenv w
- in
- complete_qid f st (name, true, [])
- in
- get_cnt_relaxed f st
-
-(* Interface functions ******************************************************)
-
-let initial_status () =
- K.clear henv; K.clear hcnt; {
- path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ()
-}
-
-let refresh_status st = {st with
- mk_uri = G.get_mk_uri ()
-}
-
-let crg_of_aut = xlate_entity
+++ /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_______________________________________________________________ *)
-
-type status
-
-val initial_status: unit -> status
-
-val refresh_status: status -> status
-
-val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) ->
- status -> Aut.command -> 'a
+++ /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 U = NUri
-module H = Hierarchy
-module C = Cps
-module G = Options
-module E = Entity
-module T = Txt
-module TT = TxtTxt
-module D = Crg
-
-type status = {
- path : T.id list; (* current section path *)
- line : int; (* line number *)
- sort : int; (* first default sort index *)
- mk_uri: G.uri_generator (* uri generator *)
-}
-
-let henv_size = 7000 (* hash tables initial size *)
-
-let henv = Hashtbl.create henv_size (* optimized global environment *)
-
-(* Internal functions *******************************************************)
-
-let name_of_id ?(r=true) id = E.Name (id, r)
-
-let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
-
-let mk_gref f uri = f (D.TGRef ([], uri))
-
-let uri_of_id st id path =
- let str = String.concat "/" path in
- let str = Filename.concat str id in
- let str = st.mk_uri str in
- U.uri_of_string str
-
-let resolve_gref err f st id =
- try f (Hashtbl.find henv id)
- with Not_found -> err ()
-
-let rec xlate_term f st lenv = function
- | T.Inst _
- | T.Impl _ -> assert false
- | T.Sort h ->
- f (D.TSort ([], h))
- | T.NSrt id ->
- let f h = f (D.TSort ([], h)) in
- H.sort_of_string C.err f id
- | T.LRef (i, j) ->
- D.get_index C.err (mk_lref f i j) i j lenv
- | T.NRef id ->
- let err () = resolve_gref C.err (mk_gref f) st id in
- D.resolve_lref err (mk_lref f) id lenv
- | T.Cast (u, t) ->
- let f uu tt = f (D.TCast ([], uu, tt)) in
- let f uu = xlate_term (f uu) st lenv t in
- xlate_term f st lenv u
- | T.Appl (vs, t) ->
- let map f = xlate_term f st lenv in
- let f vvs tt = f (D.TAppl ([], vvs, tt)) in
- let f vvs = xlate_term (f vvs) st lenv t in
- C.list_map f map vs
- | T.Bind (n, b, t) ->
- let abst_map (lenv, a, wws) (id, r, w) =
- let attr = name_of_id ~r id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let abbr_map (lenv, a, wws) (id, w) =
- let attr = name_of_id id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let void_map (lenv, a, n) id =
- let attr = name_of_id id in
- D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
- in
- let lenv, aa, bb = match b with
- | T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
- let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
- lenv, aa, D.Abst (n, wws)
- | T.Abbr xvs ->
- let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
- let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
- lenv, aa, D.Abbr vvs
- | T.Void ids ->
- let lenv = D.push_bind C.start lenv [] (D.Void 0) in
- let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
- lenv, aa, D.Void n
- in
- let f tt = f (D.TBind (aa, bb, tt)) in
- xlate_term f st lenv t
-
-let xlate_term f st lenv t =
- TT.contract (xlate_term f st lenv) t
-
-let mk_contents n tt = function
- | T.Decl -> [], E.Abst (n, tt)
- | T.Ax -> [], E.Abst (n, tt)
- | T.Cong -> [], E.Abst (n, tt)
- | T.Def -> [], E.Abbr tt
- | T.Th -> [], E.Abbr tt
-
-let xlate_entity err f gen st = function
- | T.Require _ ->
- err st
- | T.Section (Some name) ->
- err {st with path = name :: st.path}
- | T.Section None ->
- begin match st.path with
- | _ :: ptl ->
- err {st with path = ptl}
- | _ -> assert false
- end
- | T.Sorts sorts ->
- let map st (xix, s) =
- let ix = match xix with
- | None -> st.sort
- | Some ix -> ix
- in
- {st with sort = H.set_sorts ix [s]}
- in
- err (List.fold_left map st sorts)
- | T.Graph id ->
- assert (H.set_graph id); err st
- | T.Entity (kind, n, id, meta, t) ->
- let uri = uri_of_id st id st.path in
- Hashtbl.add henv id uri;
- let tt = xlate_term C.start st D.empty_lenv t in
-(*
- print_newline (); CrgOutput.pp_term print_string tt;
-*)
- let a, b = mk_contents n tt kind in
- let a = if meta <> "" then E.Meta meta :: a else a in
- let entity = E.Mark st.line :: a, uri, b in
- f {st with line = succ st.line} entity
- | T.Generate _ ->
- err st
-
-(* Interface functions ******************************************************)
-
-let initial_status () =
- Hashtbl.clear henv; {
- path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
-}
-
-let refresh_status st = {st with
- mk_uri = G.get_mk_uri ()
-}
-
-let crg_of_txt = xlate_entity
+++ /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_______________________________________________________________ *)
-
-type status
-
-val initial_status: unit -> status
-
-val refresh_status: status -> status
-
-val crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) ->
- (Txt.command -> unit) -> status -> Txt.command -> 'a
-(* free = F I P U V *)
+(* free = F I M P U V *)
module U = NUri
module K = NUri.UriHash
module Q = ccs
module S = status
+module D = crg
+module DO = crgOutput
+
module T = txt
module TP = txtParser
module TL = txtLexer
module TT = txtTxt
+module TD = txtCrg
module A = aut
module AA = autProcess
module AO = autOutput
module AP = autParser
module AL = autLexer
-
-module Z = bag
-module ZO = bagOutput
-module ZE = bagEnvironment
-module ZS = bagSubstitution
-module ZR = bagReduction
-module ZT = bagType
-module ZU = bagUntrusted
-
-module D = crg
-module DO = crgOutput
-module TD = crgTxt
-module AD = crgAut
+module AD = autCrg
module XL = xmlLibrary
module XD = xmlCrg
module BT = brgType
module BU = brgUntrusted
-module M = meta
-module MO = metaOutput
-module MA = metaAut
-module MZ = metaBag
-module MB = metaBrg
+module Z = bag
+module ZD = brgCrg
+module ZO = bagOutput
+module ZE = bagEnvironment
+module ZS = bagSubstitution
+module ZR = bagReduction
+module ZT = bagType
+module ZU = bagUntrusted
(*
top
*)
-txt txtParser txtLexer txtTxt
+txt txtParser txtLexer txtTxt txtCrg
--- /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 U = NUri
+module H = Hierarchy
+module C = Cps
+module G = Options
+module E = Entity
+module T = Txt
+module TT = TxtTxt
+module D = Crg
+
+type status = {
+ path : T.id list; (* current section path *)
+ line : int; (* line number *)
+ sort : int; (* first default sort index *)
+ mk_uri: G.uri_generator (* uri generator *)
+}
+
+let henv_size = 7000 (* hash tables initial size *)
+
+let henv = Hashtbl.create henv_size (* optimized global environment *)
+
+(* Internal functions *******************************************************)
+
+let name_of_id ?(r=true) id = E.Name (id, r)
+
+let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
+
+let mk_gref f uri = f (D.TGRef ([], uri))
+
+let uri_of_id st id path =
+ let str = String.concat "/" path in
+ let str = Filename.concat str id in
+ let str = st.mk_uri str in
+ U.uri_of_string str
+
+let resolve_gref err f st id =
+ try f (Hashtbl.find henv id)
+ with Not_found -> err ()
+
+let rec xlate_term f st lenv = function
+ | T.Inst _
+ | T.Impl _ -> assert false
+ | T.Sort h ->
+ f (D.TSort ([], h))
+ | T.NSrt id ->
+ let f h = f (D.TSort ([], h)) in
+ H.sort_of_string C.err f id
+ | T.LRef (i, j) ->
+ D.get_index C.err (mk_lref f i j) i j lenv
+ | T.NRef id ->
+ let err () = resolve_gref C.err (mk_gref f) st id in
+ D.resolve_lref err (mk_lref f) id lenv
+ | T.Cast (u, t) ->
+ let f uu tt = f (D.TCast ([], uu, tt)) in
+ let f uu = xlate_term (f uu) st lenv t in
+ xlate_term f st lenv u
+ | T.Appl (vs, t) ->
+ let map f = xlate_term f st lenv in
+ let f vvs tt = f (D.TAppl ([], vvs, tt)) in
+ let f vvs = xlate_term (f vvs) st lenv t in
+ C.list_map f map vs
+ | T.Bind (n, b, t) ->
+ let abst_map (lenv, a, wws) (id, r, w) =
+ let attr = name_of_id ~r id in
+ let ww = xlate_term C.start st lenv w in
+ D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
+ in
+ let abbr_map (lenv, a, wws) (id, w) =
+ let attr = name_of_id id in
+ let ww = xlate_term C.start st lenv w in
+ D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
+ in
+ let void_map (lenv, a, n) id =
+ let attr = name_of_id id in
+ D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
+ in
+ let lenv, aa, bb = match b with
+ | T.Abst xws ->
+ let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
+ let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
+ lenv, aa, D.Abst (n, wws)
+ | T.Abbr xvs ->
+ let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
+ let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
+ lenv, aa, D.Abbr vvs
+ | T.Void ids ->
+ let lenv = D.push_bind C.start lenv [] (D.Void 0) in
+ let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
+ lenv, aa, D.Void n
+ in
+ let f tt = f (D.TBind (aa, bb, tt)) in
+ xlate_term f st lenv t
+
+let xlate_term f st lenv t =
+ TT.contract (xlate_term f st lenv) t
+
+let mk_contents n tt = function
+ | T.Decl -> [], E.Abst (n, tt)
+ | T.Ax -> [], E.Abst (n, tt)
+ | T.Cong -> [], E.Abst (n, tt)
+ | T.Def -> [], E.Abbr tt
+ | T.Th -> [], E.Abbr tt
+
+let xlate_entity err f gen st = function
+ | T.Require _ ->
+ err st
+ | T.Section (Some name) ->
+ err {st with path = name :: st.path}
+ | T.Section None ->
+ begin match st.path with
+ | _ :: ptl ->
+ err {st with path = ptl}
+ | _ -> assert false
+ end
+ | T.Sorts sorts ->
+ let map st (xix, s) =
+ let ix = match xix with
+ | None -> st.sort
+ | Some ix -> ix
+ in
+ {st with sort = H.set_sorts ix [s]}
+ in
+ err (List.fold_left map st sorts)
+ | T.Graph id ->
+ assert (H.set_graph id); err st
+ | T.Entity (kind, n, id, meta, t) ->
+ let uri = uri_of_id st id st.path in
+ Hashtbl.add henv id uri;
+ let tt = xlate_term C.start st D.empty_lenv t in
+(*
+ print_newline (); CrgOutput.pp_term print_string tt;
+*)
+ let a, b = mk_contents n tt kind in
+ let a = if meta <> "" then E.Meta meta :: a else a in
+ let entity = E.Mark st.line :: a, uri, b in
+ f {st with line = succ st.line} entity
+ | T.Generate _ ->
+ err st
+
+(* Interface functions ******************************************************)
+
+let initial_status () =
+ Hashtbl.clear henv; {
+ path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+}
+
+let refresh_status st = {st with
+ mk_uri = G.get_mk_uri ()
+}
+
+let crg_of_txt = xlate_entity
--- /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_______________________________________________________________ *)
+
+type status
+
+val initial_status: unit -> status
+
+val refresh_status: status -> status
+
+val crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) ->
+ (Txt.command -> unit) -> status -> Txt.command -> 'a
-meta metaOutput metaAut metaBag metaBrg top
+top
+++ /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 E = Entity
-
-type uri = E.uri
-type id = E.id
-
-type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
- | LRef of int * int (* local reference: local environment length, de bruijn index *)
- | GRef of int * uri * term list (* global reference: local environment length, name, arguments *)
- | Appl of term * term (* application: argument, function *)
- | Abst of id * term * term (* abstraction: name, domain, scope *)
-
-type pars = (id * term) list (* parameter declarations: name, type *)
-
-type entry = pars * term * term option (* parameters, domain, body *)
-
-type entity = entry E.entity
+++ /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 U = NUri
-module K = U.UriHash
-module C = Cps
-module G = Options
-module E = Entity
-module N = Level
-module M = Meta
-module A = Aut
-
-(* qualified identifier: uri, name, qualifiers *)
-type qid = M.uri * M.id * M.id list
-
-type context_node = qid option (* context node: None = root *)
-
-type status = {
- path: M.id list; (* current section path *)
- node: context_node; (* current context node *)
- nodes: context_node list; (* context node list *)
- line: int; (* line number *)
- cover: string (* initial segment of URI hierarchy *)
-}
-
-type resolver = Local of int
- | Global of M.pars
-
-let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
-
-let henv = K.create henv_size (* optimized global environment *)
-
-let hcnt = K.create hcnt_size (* optimized context *)
-
-(* Internal functions *******************************************************)
-
-let id_of_name (id, _, _) = id
-
-let mk_qid st id path =
- let uripath = if st.cover = "" then path else st.cover :: path in
- let str = String.concat "/" uripath in
- let str = Filename.concat str id in
- U.uri_of_string ("ld:/" ^ str ^ ".ld"), id, path
-
-let uri_of_qid (uri, _, _) = uri
-
-let complete_qid f st (id, is_local, qs) =
- let f qs = f (mk_qid st id qs) in
- let f path = C.list_rev_append f path ~tail:qs in
- let rec skip f = function
- | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
- | _ :: ptl, _ :: _ -> skip f (ptl, qs)
- | _ -> f []
- in
- if is_local then f st.path else skip f (st.path, qs)
-
-let relax_qid f st (_, id, path) =
- let f path = f (mk_qid st id path) in
- let f = function
- | _ :: tl -> C.list_rev f tl
- | [] -> assert false
- in
- C.list_rev f path
-
-let relax_opt_qid f st = function
- | None -> f None
- | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
-
-let resolve_lref f st l lenv id =
- let rec aux f i = function
- | [] -> f None
- | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i)))
- | _ :: tl -> aux f (succ i) tl
- in
- aux f 0 lenv
-
-let resolve_lref_strict f st l lenv id =
- let f = function
- | Some t -> f t
- | None -> assert false
- in
- resolve_lref f st l lenv id
-
-let resolve_gref f st qid =
- try let args = K.find henv (uri_of_qid qid) in f qid (Some args)
- with Not_found -> f qid None
-
-let resolve_gref_relaxed f st qid =
-(* this is not tail recursive *)
- let rec g qid = function
- | None -> relax_qid (resolve_gref g st) st qid
- | Some args -> f qid args
- in
- resolve_gref g st qid
-
-let get_pars f st = function
- | None -> f [] None
- | Some qid as node ->
- try let pars = K.find hcnt (uri_of_qid qid) in f pars None
- with Not_found -> f [] (Some node)
-
-let get_pars_relaxed f st =
-(* this is not tail recursive *)
- let rec g pars = function
- | None -> f pars
- | Some node -> relax_opt_qid (get_pars g st) st node
- in
- get_pars g st st.node
-
-(* this is not tail recursive on the GRef branch *)
-let rec xlate_term f st lenv = function
- | A.Sort sort ->
- f (M.Sort sort)
- | A.Appl (v, t) ->
- let f vv tt = f (M.Appl (vv, tt)) in
- let f vv = xlate_term (f vv) st lenv t in
- xlate_term f st lenv v
- | A.Abst (name, w, t) ->
- let add name w lenv = (name, w) :: lenv in
- let f ww tt = f (M.Abst (name, ww, tt)) in
- let f ww = xlate_term (f ww) st (add name ww lenv) t in
- xlate_term f st lenv w
- | A.GRef (name, args) ->
- let l = List.length lenv in
- let g qid defs =
- let map1 f = xlate_term f st lenv in
- let map2 f (id, _) = resolve_lref_strict f st l lenv id in
- let f tail =
- let f args = f (M.GRef (l, uri_of_qid qid, args)) in
- let f defs = C.list_rev_map_append f map2 defs ~tail in
- C.list_sub_strict f defs args
- in
- C.list_map f map1 args
- in
- let g qid = resolve_gref_relaxed g st qid in
- let f = function
- | Some t -> f t
- | None -> complete_qid g st name
- in
- resolve_lref f st l lenv (id_of_name name)
-
-let xlate_entity err f st = function
- | A.Section (Some (_, name)) ->
- err {st with path = name :: st.path; nodes = st.node :: st.nodes}
- | A.Section None ->
- begin match st.path, st.nodes with
- | _ :: ptl, nhd :: ntl ->
- err {st with path = ptl; node = nhd; nodes = ntl}
- | _ -> assert false
- end
- | A.Context None ->
- err {st with node = None}
- | A.Context (Some name) ->
- let f name = err {st with node = Some name} in
- complete_qid f st name
- | A.Block (name, w) ->
- let f qid =
- let f pars =
- let f ww =
- K.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
- err {st with node = Some qid}
- in
- xlate_term f st pars w
- in
- get_pars_relaxed f st
- in
- complete_qid f st (name, true, [])
- | A.Decl (name, w) ->
- let f pars =
- let f qid =
- let f ww =
- K.add henv (uri_of_qid qid) pars;
- let a = [E.Mark st.line] in
- let entry = pars, ww, None in
- let entity = a, uri_of_qid qid, E.Abst (N.infinite, entry) in
- f {st with line = succ st.line} entity
- in
- xlate_term f st pars w
- in
- complete_qid f st (name, true, [])
- in
- get_pars_relaxed f st
- | A.Def (name, w, trans, v) ->
- let f pars =
- let f qid =
- let f ww vv =
- K.add henv (uri_of_qid qid) pars;
- let a = E.Mark st.line :: if trans then [] else [E.Priv] in
- let entry = pars, ww, Some vv in
- let entity = a, uri_of_qid qid, E.Abbr entry in
- f {st with line = succ st.line} entity
- in
- let f ww = xlate_term (f ww) st pars v in
- xlate_term f st pars w
- in
- complete_qid f st (name, true, [])
- in
- get_pars_relaxed f st
-
-(* Interface functions ******************************************************)
-
-let initial_status () =
- K.clear henv; K.clear hcnt; {
- path = []; node = None; nodes = []; line = 1; cover = !G.cover
-}
-
-let refresh_status st = {st with
- cover = !G.cover
-}
-
-let meta_of_aut = xlate_entity
+++ /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_______________________________________________________________ *)
-
-type status
-
-val initial_status: unit -> status
-
-val refresh_status: status -> status
-
-val meta_of_aut:
- (status -> 'a) -> (status -> Meta.entity -> 'a) ->
- status -> Aut.command -> 'a
+++ /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 C = Cps
-module Z = Bag
-module M = Meta
-
-(* Internal functions *******************************************************)
-
-let rec xlate_term c f = function
- | M.Sort s ->
- let f h = f (Z.Sort h) in
- if s then f 0 else f 1
- | M.LRef (_, i) ->
- let l, _, _ = List.nth c i in
- f (Z.LRef l)
- | M.GRef (_, uri, vs) ->
- let map f t v = f (Z.appl v t) in
- let f vs = C.list_fold_left f map (Z.GRef uri) vs in
- C.list_map f (xlate_term c) vs
- | M.Appl (v, t) ->
- let f v t = f (Z.Appl (v, t)) in
- let f v = xlate_term c (f v) t in
- xlate_term c f v
- | M.Abst (id, w, t) ->
- let f w =
- let l = Z.new_location () in
- let f t = f (Z.Bind (l, id, Z.Abst w, t)) in
- let f c = xlate_term c f t in
- Z.push "meta" f c l id (Z.Abst w)
- in
- xlate_term c f w
-
-let xlate_pars f pars =
- let map f (id, w) c =
- let l = Z.new_location () in
- let f w = Z.push "meta" f c l id (Z.Abst w) in
- xlate_term c f w
- in
- C.list_fold_right f map pars Z.empty_lenv
-
-let unwind_to_xlate_term f c t =
- let map f t (l, id, b) = f (Z.bind l id b t) in
- let f t = C.list_fold_left f map t c in
- xlate_term c f t
-
-let xlate_entry f = function
- | pars, u, None ->
- let f c = unwind_to_xlate_term f c u in
- xlate_pars f pars
- | pars, u, Some t ->
- let f u t = f (Z.Cast (u, t)) in
- let f c u = unwind_to_xlate_term (f u) c t in
- let f c = unwind_to_xlate_term (f c) c u in
- xlate_pars f pars
-
-(* Interface functions ******************************************************)
-
-let bag_of_meta = xlate_entry
+++ /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_______________________________________________________________ *)
-
-val bag_of_meta: (Bag.term -> 'a) -> Meta.entry -> 'a
+++ /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 C = Cps
-module E = Entity
-module N = Level
-module B = Brg
-module M = Meta
-
-(* Internal functions *******************************************************)
-
-let rec xlate_term c f = function
- | M.Sort s ->
- let f h = f (B.Sort ([], h)) in
- if s then f 0 else f 1
- | M.LRef (_, i) ->
- f (B.LRef ([], i))
- | M.GRef (_, uri, vs) ->
- let map f t v = f (B.appl [] v t) in
- let f vs = C.list_fold_left f map (B.GRef ([], uri)) vs in
- C.list_map f (xlate_term c) vs
- | M.Appl (v, t) ->
- let f v t = f (B.Appl ([], v, t)) in
- let f v = xlate_term c (f v) t in
- xlate_term c f v
- | M.Abst (id, w, t) ->
- let f w =
- let a = [E.Name (id, true)] in
- let f t = f (B.Bind (a, B.Abst (N.infinite, w), t)) in
- xlate_term (B.push c B.empty a (B.Abst (N.infinite, w))) f t
- in
- xlate_term c f w
-
-let xlate_pars f pars =
- let map f (id, w) c =
- let a = [E.Name (id, true)] in
- let f w = f (B.push c B.empty a (B.Abst (N.infinite, w))) in
- xlate_term c f w
- in
- C.list_fold_right f map pars B.empty
-
-let unwind_to_xlate_term f c t =
- let map t a b = B.bind a b t in
- let f t = f (B.fold_left map t c) in
- xlate_term c f t
-
-let xlate_entry f = function
- | pars, u, None ->
- let f c = unwind_to_xlate_term f c u in
- xlate_pars f pars
- | pars, u, Some t ->
- let f u t = f (B.Cast ([], u, t)) in
- let f c u = unwind_to_xlate_term (f u) c t in
- let f c = unwind_to_xlate_term (f c) c u in
- xlate_pars f pars
-
-(* Interface functions ******************************************************)
-
-let brg_of_meta = xlate_entry
+++ /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_______________________________________________________________ *)
-
-val brg_of_meta: (Brg.term -> 'a) -> Meta.entry -> 'a
+++ /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 P = Printf
-module F = Format
-module U = NUri
-module C = Cps
-module L = Log
-module E = Entity
-module M = Meta
-
-type counters = {
- eabsts: int;
- eabbrs: int;
- pabsts: int;
- tsorts: int;
- tlrefs: int;
- tgrefs: int;
- pappls: int;
- tappls: int;
- tabsts: int;
- uris : U.uri list;
- nodes : int;
- xnodes: int
-}
-
-let initial_counters = {
- eabsts = 0; eabbrs = 0; pabsts = 0; pappls = 0;
- tsorts = 0; tlrefs = 0; tgrefs = 0; tappls = 0; tabsts = 0;
- uris = []; nodes = 0; xnodes = 0
-}
-
-let rec count_term f c = function
- | M.Sort _ ->
- f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
- | M.LRef _ ->
- f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
- | M.GRef (_, u, ts) ->
- let c = {c with tgrefs = succ c.tgrefs} in
- let c = {c with pappls = c.pappls + List.length ts} in
- let c = {c with nodes = c.nodes + List.length ts} in
- let c =
- if Cps.list_mem ~eq:U.eq u c.uris
- then {c with nodes = succ c.nodes}
- else {c with xnodes = succ c.xnodes}
- in
- Cps.list_fold_left f count_term c ts
- | M.Appl (v, t) ->
- let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
- let f c = count_term f c t in
- count_term f c v
- | M.Abst (_, w, t) ->
- let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
- let f c = count_term f c t in
- count_term f c w
-
-let count_par f c (_, w) = count_term f c w
-
-let count_xterm f c = function
- | None -> f c
- | Some v -> count_term f c v
-
-let count_entity f c = function
- | _, u, E.Abst (_, (pars, w, xv)) ->
- let c = {c with eabsts = succ c.eabsts} in
- let c = {c with pabsts = c.pabsts + List.length pars} in
- let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in
- let f c = count_xterm f c xv in
- let f c = count_term f c w in
- Cps.list_fold_left f count_par c pars
- | _, _, E.Abbr (pars, w, xv) ->
- let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
- let c = {c with pabsts = c.pabsts + List.length pars} in
- let c = {c with nodes = c.nodes + List.length pars} in
- let f c = count_xterm f c xv in
- let f c = count_term f c w in
- Cps.list_fold_left f count_par c pars
- | _, _, E.Void -> assert false
-
-let print_counters f c =
- let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
- let pars = c.pabsts + c.pappls in
- let entries = c.eabsts + c.eabbrs in
- let nodes = c.nodes + c.xnodes in
- L.warn (P.sprintf " Intermediate representation summary (meta)");
- L.warn (P.sprintf " Total entries: %7u" entries);
- L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
- L.warn (P.sprintf " Definition items: %7u" c.eabbrs);
- L.warn (P.sprintf " Total parameter items: %7u" pars);
- L.warn (P.sprintf " Application items: %7u" c.pappls);
- L.warn (P.sprintf " Abstraction items: %7u" c.pabsts);
- L.warn (P.sprintf " Total term items: %7u" terms);
- L.warn (P.sprintf " Sort items: %7u" c.tsorts);
- L.warn (P.sprintf " Local reference items: %7u" c.tlrefs);
- L.warn (P.sprintf " Global reference items: %7u" c.tgrefs);
- L.warn (P.sprintf " Application items: %7u" c.tappls);
- L.warn (P.sprintf " Abstraction items: %7u" c.tabsts);
- L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes);
- L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes);
- f ()
+++ /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_______________________________________________________________ *)
-
-type counters
-
-val initial_counters: counters
-
-val count_entity: (counters -> 'a) -> counters -> Meta.entity -> 'a
-
-val print_counters: (unit -> 'a) -> counters -> 'a
module O = Output
module E = Entity
module S = Status
-module TD = CrgTxt
+module DO = CrgOutput
+module TD = TxtCrg
module AA = AutProcess
module AO = AutOutput
-module AD = CrgAut
-module DO = CrgOutput
+module AD = AutCrg
module XL = XmlLibrary
module XD = XmlCrg
module BD = BrgCrg
module ZT = BagType
module ZU = BagUntrusted
-module MA = MetaAut
-module MO = MetaOutput
-module MB = MetaBrg
-module MZ = MetaBag
-
type status = {
kst: S.status;
tst: TD.status;
dc : DO.counters;
bc : BO.counters;
zc : ZO.counters;
- mst: MA.status;
- mc : MO.counters;
}
let flush_all () = L.flush 0; L.flush_err ()
dc = DO.initial_counters;
bc = BO.initial_counters;
zc = ZO.initial_counters;
- mst = MA.initial_status ();
- mc = MO.initial_counters;
}
let refresh_status st = {st with
kst = S.refresh_status st.kst;
tst = TD.refresh_status st.tst;
ast = AD.refresh_status st.ast;
- mst = MA.refresh_status st.mst;
}
(* kernel related ***********************************************************)
-type kernel_entity = BrgEntity of Brg.entity
- | BagEntity of Bag.entity
- | CrgEntity of Crg.entity
- | MetaEntity of Meta.entity
+type kernel_entity = BrgEntity of Brg.entity
+ | BagEntity of Bag.entity
+ | CrgEntity of Crg.entity
let print_counters st = function
| G.Crg -> DO.print_counters C.start st.dc
| G.Bag -> ZO.print_counters C.start st.zc
let xlate_entity entity = match !G.kernel, entity with
- | G.Brg, CrgEntity e ->
+ | G.Brg, CrgEntity e ->
let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
- | G.Brg, MetaEntity e ->
- let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e
- | G.Bag, MetaEntity e ->
- let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e
- | _, entity -> entity
+ | _, entity -> entity
let pp_progress e =
let f a u =
E.mark err f a
in
match e with
- | CrgEntity e -> E.common f e
- | BrgEntity e -> E.common f e
- | BagEntity e -> E.common f e
- | MetaEntity e -> E.common f e
+ | CrgEntity e -> E.common f e
+ | BrgEntity e -> E.common f e
+ | BagEntity e -> E.common f e
let count_entity st = function
- | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e}
- | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e}
- | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
- | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e}
+ | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e}
+ | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e}
+ | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
let export_entity = function
- | CrgEntity e -> XL.export_entity XD.export_term e
- | BrgEntity e -> XL.export_entity BO.export_term e
- | MetaEntity _
- | BagEntity _ -> ()
+ | CrgEntity e -> XL.export_entity XD.export_term e
+ | BrgEntity e -> XL.export_entity BO.export_term e
+ | BagEntity _ -> ()
let type_check st k =
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
match k with
| BrgEntity entity -> BU.type_check brg_err ok st.kst entity
| BagEntity entity -> ZU.type_check ok st.kst entity
- | CrgEntity _
- | MetaEntity _ -> st
+ | CrgEntity _ -> st
(* extended lexer ***********************************************************)
let preprocess = ref false
let root = ref ""
let export = ref false
-let old = ref false
let st = ref (initial_status ())
let streaming = ref false (* parsing style (temporary) *)
let process_0 st entity =
let f st entity =
if !stage = 0 then st else
- match entity, !old with
- | AutEntity e, true ->
- let frr mst = {st with mst = mst} in
- let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
- MA.meta_of_aut frr h st.mst e
- | AutEntity e, false ->
+ match entity with
+ | AutEntity e ->
let err ast = {st with ast = ast} in
let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
AD.crg_of_aut err g st.ast e
- | TxtEntity e, _ ->
+ | TxtEntity e ->
let crr tst = {st with tst = tst} in
let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
TD.crg_of_txt crr d gen_text st.tst e
- | NoEntity, _ -> assert false
+ | NoEntity -> assert false
in
let st = if !L.level > 2 then count_input st entity else st in
if !preprocess then process_input f st entity else f st entity
let main =
try
- let version_string = "Helena 0.8.1 M - October 2010" in
+ let version_string = "Helena 0.8.1 M - November 2010" in
let print_version () = L.warn (version_string ^ "\n"); exit 0 in
let set_hierarchy s =
if H.set_graph s then () else
let set_xdir s = G.xdir := s in
let set_root s = root := s in
let clear_options () =
- progress := false; old := false; export := false; preprocess := false;
+ progress := false; export := false; preprocess := false;
stage := 3; root := "";
st := initial_status ();
L.clear (); G.clear (); H.clear (); O.clear_reductions ();
if !L.level > 2 then begin
AO.print_counters C.start !st.ac;
if !preprocess then AO.print_process_counters C.start !st.pst;
- if !stage > 0 then
- if !old then MO.print_counters C.start !st.mc
- else print_counters !st G.Crg;
+ if !stage > 0 then print_counters !st G.Crg;
if !stage > 1 then print_counters !st !G.kernel;
if !stage > 2 then O.print_reductions ()
end
flush_all ()
in
let help =
- "Usage: helena [ -LPVXcgijopqux1 | -Ss <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
+ "Usage: helena [ -LPVXcgijopqx1 | -Ss <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
"Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
let help_i = " show local references by index" in
let help_j = " show URI of processed kernel objects" in
let help_k = "<string> set kernel version (default: \"brg\")" in
- let help_o = " use old abstract language instead of crg" in
+ let help_o = " activate sort inclusion" in
let help_p = " preprocess source" in
let help_q = " disable quotation of identifiers" in
let help_r = "<string> set initial segment of URI hierarchy (default: empty)" in
let help_s = "<number> set translation stage (see above)" in
- let help_u = " activate sort inclusion" in
let help_x = " export kernel entities (XML)" in
let help_1 = " parse files with streaming policy" in
("-i", Arg.Set G.indexes, help_i);
("-j", Arg.Set progress, help_j);
("-k", Arg.String set_kernel, help_k);
- ("-o", Arg.Set old, help_o);
+ ("-o", Arg.Set G.si, help_o);
("-p", Arg.Set preprocess, help_p);
("-q", Arg.Set G.unquote, help_q);
("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
- ("-u", Arg.Set G.si, help_u);
("-x", Arg.Set export, help_x);
("-1", Arg.Set streaming, help_1);
] process_file help;
projects / helm.git / commitdiff