From: Ferruccio Guidi Date: Sun, 31 Oct 2010 15:13:37 +0000 (+0000) Subject: when sort inclusion is enabled, we can produce conversion constraints in xml X-Git-Tag: make_still_working~2746 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7988fc51f7c96617aa2b3320628645480af681a;p=helm.git when sort inclusion is enabled, we can produce conversion constraints in xml format --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index b71db9944..94d36ea3f 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -7,26 +7,33 @@ src/lib/log.cmo: src/lib/cps.cmx src/lib/log.cmi src/lib/log.cmx: src/lib/cps.cmx src/lib/log.cmi src/lib/time.cmo: src/lib/log.cmi src/lib/time.cmx: src/lib/log.cmx -src/common/options.cmo: src/lib/cps.cmx -src/common/options.cmx: src/lib/cps.cmx src/common/hierarchy.cmi: src/common/hierarchy.cmo: src/lib/cps.cmx src/common/hierarchy.cmi src/common/hierarchy.cmx: src/lib/cps.cmx src/common/hierarchy.cmi +src/common/level.cmi: +src/common/level.cmo: src/common/level.cmi +src/common/level.cmx: src/common/level.cmi +src/common/entity.cmo: src/common/level.cmi +src/common/entity.cmx: src/common/level.cmx +src/common/options.cmo: src/lib/cps.cmx +src/common/options.cmx: src/lib/cps.cmx src/common/output.cmi: src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \ src/common/output.cmi src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \ src/common/output.cmi -src/common/level.cmi: -src/common/level.cmo: src/common/level.cmi -src/common/level.cmx: src/common/level.cmi -src/common/entity.cmo: src/common/options.cmx src/common/level.cmi -src/common/entity.cmx: src/common/options.cmx src/common/level.cmx src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmx: src/common/entity.cmx src/common/alpha.cmi: src/common/entity.cmx src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi +src/common/ccs.cmi: src/common/entity.cmx +src/common/ccs.cmo: src/common/options.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/common/ccs.cmi +src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/common/ccs.cmi +src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi +src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx src/text/txt.cmo: src/common/level.cmi src/text/txt.cmx: src/common/level.cmx src/text/txtParser.cmi: src/text/txt.cmx @@ -90,18 +97,18 @@ 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/entity.cmx src/basic_ag/bag.cmx -src/basic_ag/bagType.cmo: 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/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/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/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/entity.cmx src/basic_ag/bag.cmx +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 @@ -131,11 +138,14 @@ src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/level.cmi \ src/complete_rg/crgAut.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/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx -src/xml/xmlLibrary.cmo: src/common/level.cmi src/common/hierarchy.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi -src/xml/xmlLibrary.cmx: src/common/level.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.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/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ + src/common/ccs.cmi src/xml/xmlLibrary.cmi +src/xml/xmlLibrary.cmx: src/common/options.cmx src/common/level.cmx \ + src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ + src/common/ccs.cmx src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi: src/xml/xmlLibrary.cmi src/complete_rg/crg.cmx src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ @@ -172,17 +182,19 @@ src/basic_rg/brgSubstitution.cmo: src/basic_rg/brg.cmx \ src/basic_rg/brgSubstitution.cmi src/basic_rg/brgSubstitution.cmx: src/basic_rg/brg.cmx \ src/basic_rg/brgSubstitution.cmi -src/basic_rg/brgReduction.cmi: src/lib/log.cmi src/common/entity.cmx \ - src/basic_rg/brg.cmx -src/basic_rg/brgReduction.cmo: src/lib/share.cmx src/common/output.cmi \ - src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx \ +src/basic_rg/brgReduction.cmi: src/common/status.cmx src/lib/log.cmi \ + src/common/entity.cmx src/basic_rg/brg.cmx +src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \ + src/common/output.cmi src/lib/log.cmi src/common/level.cmi \ + src/common/entity.cmx src/lib/cps.cmx src/common/ccs.cmi \ src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi -src/basic_rg/brgReduction.cmx: src/lib/share.cmx src/common/output.cmx \ - src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx \ +src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \ + src/common/output.cmx src/lib/log.cmx src/common/level.cmx \ + src/common/entity.cmx src/lib/cps.cmx src/common/ccs.cmx \ src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi -src/basic_rg/brgType.cmi: src/lib/log.cmi src/common/entity.cmx \ +src/basic_rg/brgType.cmi: src/common/status.cmx src/lib/log.cmi \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \ src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \ @@ -194,7 +206,7 @@ src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \ src/lib/cps.cmx src/basic_rg/brgSubstitution.cmx \ src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgType.cmi -src/basic_rg/brgUntrusted.cmi: src/common/entity.cmx src/basic_rg/brgType.cmi \ +src/basic_rg/brgUntrusted.cmi: src/common/status.cmx src/basic_rg/brgType.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ src/basic_rg/brgType.cmi src/basic_rg/brgReduction.cmi \ @@ -232,28 +244,28 @@ src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/level.cmx \ src/toplevel/metaBrg.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/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/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/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/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/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/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/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/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/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/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/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 \ diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 683e422a4..c5992e90a 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -12,6 +12,8 @@ CLEAN = etc/log.txt etc/profile.txt TAGS = test-si test-si-fast hal xml-si-crg xml-si profile +XMLLINTLOCAL = --nonet --path xml --dtdvalid ld.dtd + XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ xml/brg-si/grundlagen/l/et.ld.xml \ xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ @@ -21,15 +23,15 @@ XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ xml/crg-si/grundlagen/l/e/pairis1.ld.xml -include Makefile.common +LOCALXMLS = xml/brg-si/grundlagen/ccs.ldc.xml -HOME = . +include Makefile.common INPUT = examples/grundlagen/grundlagen.aut test-si: $(MAIN).opt etc - @echo " HELENA -p -u $(INPUT)" - $(H)./$(MAIN).opt -p -u -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -p -u -c $(INPUT)" + $(H)./$(MAIN).opt -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt etc @echo " HELENA -u -q $(INPUT)" @@ -43,11 +45,11 @@ profile: $(MAIN).opt etc xml-si: $(MAIN).opt etc @echo " HELENA -u -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -u -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 $(HOME) -s 1 -S 1 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt etc: @echo " MKDIR etc" @@ -104,4 +106,4 @@ test-si-fast-old: $(MAIN).opt etc xml-si-old: $(MAIN).opt etc @echo " HELENA -o -u -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -o -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 434ece82f..5d007032e 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -20,6 +20,8 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(I OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v XMLLINT = xmllint --noout + + XSLT = xsltproc #TAR = tar -czf etc/$(MAIN:%=%.tgz) @@ -71,6 +73,10 @@ lint-xml: $(XMLS) @echo XMLLINT --valid $(H)$(XMLLINT) --valid $^ +lint-xml-local: $(LOCALXMLS) + @echo XMLLINT --valid + $(H)$(XMLLINT) $(XMLLINTLOCAL) --valid $^ + #tgz: clean # @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)" # $(H)find -name "Make*" | xargs $(TAR) $(KEEP) diff --git a/helm/software/lambda-delta/src/basic_ag/bag.ml b/helm/software/lambda-delta/src/basic_ag/bag.ml index d3ac2c8ee..d6432863d 100644 --- a/helm/software/lambda-delta/src/basic_ag/bag.ml +++ b/helm/software/lambda-delta/src/basic_ag/bag.ml @@ -34,12 +34,6 @@ type lenv = (int * id * bind) list (* location, name, binder *) type message = (lenv, term) Log.item list -(* helpers ******************************************************************) - -let mk_uri si root s = - let kernel = if si then "bag-si" else "bag" in - String.concat "/" ["ld:"; kernel; root; s ^ ".ld"] - (* Currified constructors ***************************************************) let abst w = Abst w diff --git a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml index 46cd95c14..7a341783c 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml @@ -9,35 +9,35 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module S = Share +module W = Share module Z = Bag (* Internal functions *******************************************************) let rec lref_map_bind f map b = match b with | Z.Abbr v -> - let f v' = f (S.sh1 v v' b Z.abbr) in + let f v' = f (W.sh1 v v' b Z.abbr) in lref_map f map v | Z.Abst w -> - let f w' = f (S.sh1 w w' b Z.abst) in + let f w' = f (W.sh1 w w' b Z.abst) in lref_map f map w | Z.Void -> f b and lref_map f map t = match t with | Z.LRef i -> - let ii = map i in f (S.sh1 i ii t Z.lref) + let ii = map i in f (W.sh1 i ii t Z.lref) | Z.GRef _ -> f t | Z.Sort _ -> f t | Z.Cast (w, u) -> - let f w' u' = f (S.sh2 w w' u u' t Z.cast) in + let f w' u' = f (W.sh2 w w' u u' t Z.cast) in let f w' = lref_map (f w') map u in lref_map f map w | Z.Appl (w, u) -> - let f w' u' = f (S.sh2 w w' u u' t Z.appl) in + let f w' u' = f (W.sh2 w w' u u' t Z.appl) in let f w' = lref_map (f w') map u in lref_map f map w | Z.Bind (l, id, b, u) -> - let f b' u' = f (S.sh2 b b' u u' t (Z.bind l id)) in + let f b' u' = f (W.sh2 b b' u u' t (Z.bind l id)) in let f b' = lref_map (f b') map u in lref_map_bind f map b diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.ml b/helm/software/lambda-delta/src/basic_ag/bagType.ml index 1314218d3..906904011 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagType.ml @@ -11,10 +11,11 @@ module U = NUri module C = Cps -module S = Share +module W = Share module L = Log module E = Entity module H = Hierarchy +module S = Status module Z = Bag module ZO = BagOutput module ZE = BagEnvironment @@ -73,7 +74,7 @@ let rec b_type_of f st c x = ZE.get_entity f uri | Z.Bind (l, id, Z.Abbr v, t) -> let f xv xt tt = - f (S.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt) + f (W.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt) in let f xv cc = b_type_of (f xv) st cc t in let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in @@ -84,14 +85,14 @@ let rec b_type_of f st c x = type_of f st c v | Z.Bind (l, id, Z.Abst u, t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt) + f (W.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt) in let f xu cc = b_type_of (f xu) st cc t in let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in type_of f st c u | Z.Bind (l, id, Z.Void, t) -> let f xt tt = - f (S.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt) + f (W.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt) in let f cc = b_type_of f st cc t in Z.push "type void" f c l id Z.Void @@ -103,10 +104,10 @@ let rec b_type_of f st c x = L.unbox (succ level); let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt) + if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt) else error3 c xv vv w in - ZR.are_convertible f ~si:st.E.si c w vv + ZR.are_convertible f ~si:st.S.si c w vv | _ -> error1 "not a function" c xt in @@ -116,9 +117,9 @@ let rec b_type_of f st c x = | Z.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu + if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu in - let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.E.si c xu tt in + let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.S.si c xu tt in let f xu _ = b_type_of (f xu) st c t in type_of f st c u diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.mli b/helm/software/lambda-delta/src/basic_ag/bagType.mli index 31a421bda..ba0268e9c 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagType.mli +++ b/helm/software/lambda-delta/src/basic_ag/bagType.mli @@ -13,4 +13,4 @@ exception TypeError of Bag.message val type_of: (Bag.term -> Bag.term -> 'a) -> - Entity.status -> Bag.lenv -> Bag.term -> 'a + Status.status -> Bag.lenv -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/src/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/src/basic_ag/bagUntrusted.mli index af967408e..5c609e804 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagUntrusted.mli +++ b/helm/software/lambda-delta/src/basic_ag/bagUntrusted.mli @@ -10,4 +10,4 @@ V_______________________________________________________________ *) val type_check: - (Bag.term -> Bag.entity -> 'a) -> Entity.status -> Bag.entity -> 'a + (Bag.term -> Bag.entity -> 'a) -> Status.status -> Bag.entity -> 'a diff --git a/helm/software/lambda-delta/src/basic_rg/brg.ml b/helm/software/lambda-delta/src/basic_rg/brg.ml index bc6eb5727..038652309 100644 --- a/helm/software/lambda-delta/src/basic_rg/brg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brg.ml @@ -36,12 +36,6 @@ type lenv = Null (* Cons: tail, relative local environment, attrs, binder *) | Cons of lenv * lenv * attrs * bind -(* helpers ******************************************************************) - -let mk_uri si root s = - let kernel = if si then "brg-si" else "brg" in - String.concat "/" ["ld:"; kernel; root; s ^ ".ld"] - (* Currified constructors ***************************************************) let abst n w = Abst (n, w) diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index 5a5559f7c..79ffcb32f 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -11,10 +11,13 @@ module U = NUri module C = Cps -module S = Share +module W = Share module L = Log module E = Entity +module N = Level module O = Output +module Q = Ccs +module S = Status module B = Brg module BO = BrgOutput module BE = BrgEnvironment @@ -64,7 +67,7 @@ let are_alpha_convertible err f t1 t2 = | B.Void, B.Void -> f () | _ -> err () in - if S.eq t1 t2 then f () else aux f (t1, t2) + if W.eq t1 t2 then f () else aux f (t1, t2) let get m i = let _, c, a, b = B.get m.e i in c, a, b @@ -76,9 +79,9 @@ let rec step st m x = | B.Sort _ -> m, None, x | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, E.Abbr v when st.E.delta -> + | _, _, E.Abbr v when st.S.delta -> O.add ~gdelta:1 (); step st m v - | _, _, E.Abst (_, w) when st.E.rt -> + | _, _, E.Abst (_, w) when st.S.rt -> O.add ~grt:1 (); step st m w | a, _, E.Abbr v -> let e = E.apix C.err C.start a in @@ -93,7 +96,7 @@ let rec step st m x = | c, _, B.Abbr v -> O.add ~ldelta:1 (); step st {m with e = c} v - | c, _, B.Abst (_, w) when st.E.rt -> + | c, _, B.Abst (_, w) when st.S.rt -> O.add ~lrt:1 (); step st {m with e = c} w | c, _, B.Void -> @@ -111,7 +114,8 @@ let rec step st m x = begin match m.s with | [] -> m, None, x | (c, v) :: s -> - O.add ~beta:1 ~upsilon:(List.length s) (); + if N.is_zero n then Q.add_infinite st.S.cc a; + O.add ~beta:1 ~upsilon:(List.length s) (); let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in step st {m with e = e; s = s} t end @@ -156,10 +160,11 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) = 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 E.si = false} m1 w1 m2 w2 then + if n1 = n2 && 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, t) when st.E.si -> + | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t) + 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 @@ -173,7 +178,7 @@ and ac_stacks st m1 m2 = if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in - ac {st with E.si = false} m1 v1 m2 v2 + ac {st with S.si = false} m1 v1 m2 v2 in list_and map (m1.s, m2.s) @@ -189,15 +194,15 @@ let get m i = let xwhd st m t = L.box level; log1 "Now scanning" m.e t; - let m, _, t = step {st with E.delta = true; E.rt = true} m t in + let m, _, t = step {st with S.delta = true; S.rt = true} m t in L.unbox level; m, t let are_convertible st mu u mw w = L.box level; log2 "Now converting" mu.e u mw.e w; - let r = ac {st with E.delta = st.E.expand; E.rt = false} mu u mw w in + let r = ac {st with S.delta = st.S.expand; S.rt = false} mu u mw w in L.unbox level; r (* let err _ = in - if S.eq mu mw then are_alpha_convertible err f u w else err () *) + if W.eq mu mw then are_alpha_convertible err f u w else err () *) (* error reporting **********************************************************) diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.mli b/helm/software/lambda-delta/src/basic_rg/brgReduction.mli index eebb15725..e8df9f7aa 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.mli @@ -17,10 +17,10 @@ val get: kam -> int -> Brg.bind val push: kam -> Entity.attrs -> Brg.bind -> kam -val xwhd: Entity.status -> kam -> Brg.term -> kam * Brg.term +val xwhd: Status.status -> kam -> Brg.term -> kam * Brg.term (* arguments: expected type, inferred type *) val are_convertible: - Entity.status -> kam -> Brg.term -> kam -> Brg.term -> bool + Status.status -> kam -> Brg.term -> kam -> Brg.term -> bool val specs: (kam, Brg.term) Log.specs diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml index 2bead2d33..f23da87d0 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgType.ml @@ -11,7 +11,7 @@ module U = NUri module C = Cps -module S = Share +module W = Share module L = Log module H = Hierarchy module E = Entity @@ -88,7 +88,7 @@ let rec b_type_of err f st m x = end | B.Bind (a, B.Abbr v, t) -> let f xv xt tt = - f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) + f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in let f xv m = b_type_of err (f xv) st m t in let f xv = f xv (BR.push m a (B.abbr xv)) in @@ -99,27 +99,27 @@ let rec b_type_of err f st m x = type_of err f st m v | B.Bind (a, B.Abst (n, u), t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt) + f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt) in let f xu m = b_type_of err (f xu) st m t in let f xu _ = f xu (BR.push m a (B.abst n xu)) in type_of err f st m u | B.Bind (a, B.Void, t) -> let f xt tt = - f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) + f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) in b_type_of err f st (BR.push m a B.Void) t | B.Appl (a, v, t) -> let f xv vv xt tt = - let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in + let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in assert_applicability err f st m tt vv xv in let f xv vv = b_type_of err (f xv vv) st m t in type_of err f st m v | B.Cast (a, u, t) -> let f xu xt tt = - let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in + let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in assert_convertibility err f st m xu tt xt in let f xu _ = b_type_of err (f xu) st m t in diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.mli b/helm/software/lambda-delta/src/basic_rg/brgType.mli index 5d9350b49..169267662 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/src/basic_rg/brgType.mli @@ -13,4 +13,4 @@ type message = (BrgReduction.kam, Brg.term) Log.message val type_of: (message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> - Entity.status -> BrgReduction.kam -> Brg.term -> 'a + Status.status -> BrgReduction.kam -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/src/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/src/basic_rg/brgUntrusted.mli index d395eb535..eb3136da2 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/src/basic_rg/brgUntrusted.mli @@ -11,4 +11,4 @@ val type_check: (BrgType.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> - Entity.status -> Brg.entity -> 'a + Status.status -> Brg.entity -> 'a diff --git a/helm/software/lambda-delta/src/common/Make b/helm/software/lambda-delta/src/common/Make index 5052ac0f3..7be0f01c2 100644 --- a/helm/software/lambda-delta/src/common/Make +++ b/helm/software/lambda-delta/src/common/Make @@ -1 +1 @@ -options hierarchy output level entity marks alpha +hierarchy level entity options output marks alpha ccs status diff --git a/helm/software/lambda-delta/src/common/ccs.ml b/helm/software/lambda-delta/src/common/ccs.ml new file mode 100644 index 000000000..ca27ff93d --- /dev/null +++ b/helm/software/lambda-delta/src/common/ccs.ml @@ -0,0 +1,36 @@ +(* + ||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 L = List +module U = NUri +module C = Cps +module E = Entity +module G = Options + +type csys = { + uri: E.uri; + mutable is : int list +} + +let mark a = E.mark C.err C.start a + +(* interface functions ******************************************************) + +let init () = { + uri = U.uri_of_string (G.get_baseuri ()); + is = []; +} + +let add_infinite s a = + if !G.si && !G.cc then + let i = abs (mark a) in + if L.mem i s.is then () else s.is <- i :: s.is + else () diff --git a/helm/software/lambda-delta/src/common/ccs.mli b/helm/software/lambda-delta/src/common/ccs.mli new file mode 100644 index 000000000..d94406d7b --- /dev/null +++ b/helm/software/lambda-delta/src/common/ccs.mli @@ -0,0 +1,19 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +type csys = { + uri: Entity.uri; + mutable is : int list +} + +val init: unit -> csys + +val add_infinite: csys -> Entity.attrs -> unit diff --git a/helm/software/lambda-delta/src/common/entity.ml b/helm/software/lambda-delta/src/common/entity.ml index f587a8d54..b88af255c 100644 --- a/helm/software/lambda-delta/src/common/entity.ml +++ b/helm/software/lambda-delta/src/common/entity.ml @@ -10,7 +10,6 @@ V_______________________________________________________________ *) module U = NUri -module G = Options module N = Level type uri = U.uri @@ -35,13 +34,6 @@ type 'term bind = Abst of N.level * 'term (* declaration: level, domain *) type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) -type status = { - delta: bool; (* global delta-expansion *) - rt: bool; (* reference typing *) - si: bool; (* sort inclusion *) - expand: bool (* always expand global definitions *) -} - (* helpers ******************************************************************) let common f (a, u, _) = f a u @@ -120,12 +112,3 @@ let xlate f xlate_term = function let f t = f (a, uri, Abbr t) in xlate_term f t | _, _, Void -> assert false - -let initial_status () = { - delta = false; rt = false; si = !G.si; expand = !G.expand -} - -let refresh_status st = {st with - si = !G.si; expand = !G.expand -} - diff --git a/helm/software/lambda-delta/src/common/options.ml b/helm/software/lambda-delta/src/common/options.ml index d9783c766..c133bed7c 100644 --- a/helm/software/lambda-delta/src/common/options.ml +++ b/helm/software/lambda-delta/src/common/options.ml @@ -13,30 +13,49 @@ module C = Cps type uri_generator = string -> string +type kernel = Crg | Brg | Bag + (* interface functions ******************************************************) -let indexes = ref false (* show de Bruijn indexes *) +let xdir = ref "" -let expand = ref false (* always expand global definitions *) +let kernel = ref Brg let si = ref false (* use sort inclusion *) -let unquote = ref false (* do not quote identifiers when lexing *) +let cover = ref "" (* initial uri segment *) + +let cc = ref false (* activate conversion constraints *) + +let expand = ref false (* always expand global definitions *) + +let indexes = ref false (* show de Bruijn indexes *) let icm = ref 0 (* complexity measure of relocated terms *) -let cover = ref "" (* initial uri segment *) +let unquote = ref false (* do not quote identifiers when lexing *) let debug_parser = ref false (* output parser debug information *) let debug_lexer = ref false (* output lexer debug information *) -let mk_uri = ref (fun _ _ -> C.err : bool -> string -> uri_generator) +let kernel_id () = + let id = match !kernel with + | Crg -> "crg" + | Brg -> "brg" + | Bag -> "bag" + in + let si = if !si then "-si" else "" in + id ^ si + +let get_baseuri () = + String.concat "/" ["ld:"; kernel_id (); !cover ] let get_mk_uri () = - !mk_uri !si !cover + let bu = get_baseuri () in + fun s -> bu ^ "/" ^ s ^ ".ld" let clear () = - expand := false; si := false; cover := ""; indexes := false; icm := 0; - debug_parser := false; debug_lexer := false; - mk_uri := fun _ _ -> C.err + xdir := ""; kernel := Brg; si := false; cover := ""; + expand := false; indexes := false; icm := 0; unquote := false; + debug_parser := false; debug_lexer := false diff --git a/helm/software/lambda-delta/src/common/status.ml b/helm/software/lambda-delta/src/common/status.ml new file mode 100644 index 000000000..3da988f84 --- /dev/null +++ b/helm/software/lambda-delta/src/common/status.ml @@ -0,0 +1,33 @@ +(* + ||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 G = Options +module Q = Ccs + +type status = { + delta: bool; (* global delta-expansion *) + rt: bool; (* reference typing *) + si: bool; (* sort inclusion *) + expand: bool; (* always expand global definitions *) + cc: Q.csys; (* conversion constraints *) +} + +(* helpers ******************************************************************) + +let initial_status () = { + delta = false; rt = false; + si = !G.si; expand = !G.expand; cc = Q.init () +} + +let refresh_status st = {st with + si = !G.si; expand = !G.expand; cc = Q.init () +} + diff --git a/helm/software/lambda-delta/src/complete_rg/crg.ml b/helm/software/lambda-delta/src/complete_rg/crg.ml index d272bdea8..9020048af 100644 --- a/helm/software/lambda-delta/src/complete_rg/crg.ml +++ b/helm/software/lambda-delta/src/complete_rg/crg.ml @@ -39,10 +39,6 @@ type entity = term E.entity (* helpers ******************************************************************) -let mk_uri si root s = - let kernel = if si then "crg-si" else "crg" in - String.concat "/" ["ld:"; kernel; root; s ^ ".ld"] - let empty_lenv = ESort let push_bind f lenv a b = f (EBind (lenv, a, b)) diff --git a/helm/software/lambda-delta/src/modules.ml b/helm/software/lambda-delta/src/modules.ml index 51b98a29d..619a6cce6 100644 --- a/helm/software/lambda-delta/src/modules.ml +++ b/helm/software/lambda-delta/src/modules.ml @@ -1,20 +1,22 @@ -(* free = F I P Q U V W *) +(* free = F I P U V *) module U = NUri module K = NUri.UriHash module C = cps -module S = share +module W = share (**) module L = log module Y = time (**) -module G = options module H = hierarchy -module O = output +module N = level module E = entity +module G = options +module O = output module J = marks (**) module R = alpha -module N = level +module Q = ccs +module S = status module T = txt module TP = txtParser diff --git a/helm/software/lambda-delta/src/text/txtTxt.ml b/helm/software/lambda-delta/src/text/txtTxt.ml index d2c85cb92..fe0988401 100644 --- a/helm/software/lambda-delta/src/text/txtTxt.ml +++ b/helm/software/lambda-delta/src/text/txtTxt.ml @@ -23,7 +23,7 @@ let rec contract f = function contract f tt | T.Impl (n, true, id, w, t) -> let f = function - | T.Bind (n, T.Abst [xw], T.Bind (_, T.Abst xws, tt)) -> + | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) -> f (T.Bind (n, T.Abst (xw :: xws), tt)) | tt -> f tt in diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 95ff41df3..4a1446734 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -19,6 +19,7 @@ module G = Options module H = Hierarchy module O = Output module E = Entity +module S = Status module XL = XmlLibrary module XD = XmlCrg module AA = AutProcess @@ -46,7 +47,7 @@ type status = { mc : MO.counters; brgc: BO.counters; bagc: ZO.counters; - kst : E.status + kst : S.status } let flush_all () = L.flush 0; L.flush_err () @@ -66,37 +67,34 @@ let initial_status () = { dst = AD.initial_status (); tst = TD.initial_status (); ast = AA.initial_status (); - kst = E.initial_status () + kst = S.initial_status () } let refresh_status st = {st with mst = MA.refresh_status st.mst; dst = AD.refresh_status st.dst; tst = TD.refresh_status st.tst; - kst = E.refresh_status st.kst + kst = S.refresh_status st.kst } (* kernel related ***********************************************************) -type kernel = Brg | Bag - type kernel_entity = BrgEntity of Brg.entity | BagEntity of Bag.entity | CrgEntity of Crg.entity | MetaEntity of Meta.entity -let kernel = ref Brg - -let print_counters st = match !kernel with - | Brg -> BO.print_counters C.start st.brgc - | Bag -> ZO.print_counters C.start st.bagc +let print_counters st = function + | G.Brg -> BO.print_counters C.start st.brgc + | G.Bag -> ZO.print_counters C.start st.bagc + | G.Crg -> () -let xlate_entity entity = match !kernel, entity with - | Brg, CrgEntity e -> +let xlate_entity entity = match !G.kernel, entity with + | G.Brg, CrgEntity e -> let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e - | Brg, MetaEntity e -> + | G.Brg, MetaEntity e -> let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e - | Bag, MetaEntity e -> + | G.Bag, MetaEntity e -> let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e | _, entity -> entity @@ -119,9 +117,9 @@ let count_entity st = function | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e} | _ -> st -let export_entity si xdir = function - | CrgEntity e -> XL.export_entity XD.export_term si xdir e - | BrgEntity e -> XL.export_entity BO.export_term si xdir 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 _ -> () @@ -210,21 +208,20 @@ let stage = ref 3 let progress = ref false let preprocess = ref false let root = ref "" -let cc = ref false -let export = ref "" +let export = ref false let old = ref false let st = ref (initial_status ()) let streaming = ref false (* parsing style (temporary) *) let process_2 st entity = let st = if !L.level > 2 then count_entity st entity else st in - if !export <> "" then export_entity !G.si !export entity; + if !export then export_entity entity; if !stage > 2 then type_check st entity else st let process_1 st entity = if !progress then pp_progress entity; let st = if !L.level > 2 then count_entity st entity else st in - if !export <> "" && !stage = 1 then export_entity !G.si !export entity; + if !export && !stage = 1 then export_entity entity; if !stage > 1 then process_2 st (xlate_entity entity) else st let process_0 st entity = @@ -275,7 +272,9 @@ let process st name = 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 + close_in ich; + if !stage > 2 && !G.cc && !G.si then XL.export_csys st.kst.S.cc; + st, input let main = try @@ -286,18 +285,18 @@ try L.warn (P.sprintf "Unknown type hierarchy: %s" s) in let set_kernel = function - | "brg" -> kernel := Brg - | "bag" -> kernel := Bag + | "brg" -> G.kernel := G.Brg + | "bag" -> G.kernel := G.Bag | s -> L.warn (P.sprintf "Unknown kernel version: %s" s) in let set_summary i = L.level := i in let set_stage i = stage := i in - let set_xdir s = export := s in + let set_xdir s = G.xdir := s in let set_root s = root := s in let clear_options () = - stage := 3; progress := false; old := false; - preprocess := false; root := ""; cc := false; export := ""; - kernel := Brg; st := initial_status (); + progress := false; old := false; export := false; preprocess := false; + stage := 3; root := ""; + st := initial_status (); L.clear (); G.clear (); H.clear (); O.clear_reductions (); streaming := false; in @@ -307,14 +306,9 @@ try L.warn (P.sprintf "Processing file: %s" name); if !L.level > 0 then Y.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in - let mk_uri = - if !stage < 2 then Crg.mk_uri else - match !kernel with - | Brg -> Brg.mk_uri - | Bag -> Bag.mk_uri - in let cover = F.concat !root base_name in - G.mk_uri := mk_uri; G.cover := cover; + if !stage < 2 then G.kernel := G.Crg; + G.cover := cover; let sst, input = process (refresh_status !st) name in st := sst; if !L.level > 0 then Y.utime_stamp "processed"; @@ -322,7 +316,7 @@ try AO.print_counters C.start !st.ac; if !preprocess then AO.print_process_counters C.start !st.ast; if !stage > 0 then MO.print_counters C.start !st.mc; - if !stage > 1 then print_counters !st; + if !stage > 1 then print_counters !st !G.kernel; if !stage > 2 then O.print_reductions () end in @@ -331,41 +325,43 @@ try flush_all () in let help = - "Usage: helena [ -LPVXcgijopqu1 | -Ss | -x | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXcgijopqux1 | -Ss | -O | -hkr ]* [ ]*\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" in let help_L = " show lexer debug information" in + let help_O = " set location of output directory (XML) to (default: current directory)" in let help_P = " show parser debug information" in let help_S = " set summary level (see above)" in let help_V = " show version information" in let help_X = " clear options" in - let help_c = " output conversion constraints" in + let help_c = " read/write conversion constraints" in let help_g = " always expand global definitions" in - let help_h = " set type hierarchy (default: Z1)" in + let help_h = " set type hierarchy (default: \"Z1\")" in let help_i = " show local references by index" in let help_j = " show URI of processed kernel objects" in - let help_k = " set kernel version (default: brg)" in + let help_k = " set kernel version (default: \"brg\")" in let help_o = " use old abstract language instead of crg" in let help_p = " preprocess source" in let help_q = " disable quotation of identifiers" in - let help_r = " set initial segment of URI hierarchy" in + let help_r = " set initial segment of URI hierarchy (default: empty)" in let help_s = " set translation stage (see above)" in let help_u = " activate sort inclusion" in - let help_x = " export kernel entities (XML) to " in + let help_x = " export kernel entities (XML)" in let help_1 = " parse files with streaming policy" in L.box 0; L.box_err (); at_exit exit; Arg.parse [ ("-L", Arg.Set G.debug_lexer, help_L); + ("-O", Arg.String set_xdir, help_O); ("-P", Arg.Set G.debug_parser, help_P); ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); ("-X", Arg.Unit clear_options, help_X); - ("-c", Arg.Set cc, help_c); + ("-c", Arg.Set G.cc, help_c); ("-g", Arg.Set G.expand, help_g); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set G.indexes, help_i); @@ -377,7 +373,7 @@ try ("-r", Arg.String set_root, help_r); ("-s", Arg.Int set_stage, help_s); ("-u", Arg.Set G.si, help_u); - ("-x", Arg.String set_xdir, help_x); + ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help; with ZT.TypeError msg -> bag_error "Type Error" msg diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml index 7b5dd8ddc..3eea8cd87 100644 --- a/helm/software/lambda-delta/src/xml/xmlCrg.ml +++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml @@ -73,7 +73,7 @@ let rec exp_term e t out tab = match t with XL.tag XL.cast attrs ~contents:(exp_term e u) out tab; exp_term e t out tab | D.TAppl (a, vs, t) -> - let attrs = [XL.arity (List.length vs)] in + let attrs = [XL.arity vs] in XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; exp_term e t out tab | D.TProj (a, lenv, t) -> @@ -92,14 +92,14 @@ and exp_bind e a b out tab = match b with | D.Abst (n, ws) -> let e = D.push_bind C.start e a (D.Abst (n, ws)) in - let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity (List.length ws)] in + let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab | D.Abbr vs -> let e = D.push_bind C.start e a (D.Abbr vs) in - let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in + let attrs = [XL.name ns; XL.mark a; XL.arity vs] in XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab | D.Void n -> - let attrs = [XL.name a; XL.mark a; XL.arity n] in + let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in XL.tag XL.void attrs out tab and exp_eproj e a lenv out tab = diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml index af6245c9f..3bc0c54e0 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml @@ -13,16 +13,22 @@ module F = Filename module U = NUri module C = Cps module H = Hierarchy +module G = Options module E = Entity module N = Level +module Q = Ccs (* internal functions *******************************************************) let base = "xml" -let obj_ext = ".xml" +let ext = ".xml" -let root = "ENTITY" +let obj_root = "ENTITY" + +let ccs_name = "ccs.ldc" + +let ccs_root = "CCS" let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd" @@ -89,7 +95,11 @@ let offset j = let uri u = "uri", U.string_of_uri u -let arity n = +let arity ?n l = + let n = match n with + | None -> List.length l + | Some n -> n + in let contents = if n > 1 then string_of_int n else "" in "arity", contents @@ -116,12 +126,12 @@ let meta a = let f s = "meta", s in E.meta err f a -let export_entity pp_term si xdir (a, u, b) = - let path = path_of_uri xdir u in +let export_entity pp_term (a, u, b) = + let path = path_of_uri !G.xdir u in let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in - let och = open_out (path ^ obj_ext) in + let och = open_out (path ^ ext) in let out = output_string och in - xml out "1.0" "UTF-8"; doctype out root system; + xml out "1.0" "UTF-8"; doctype out obj_root system; let a = E.Name (U.name_of_uri u, true) :: a in let attrs = [uri u; name a; mark a; meta a] in let contents = match b with @@ -129,8 +139,24 @@ let export_entity pp_term si xdir (a, u, b) = | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) | E.Void -> assert false in - let opts = if si then "si" else "" in + let opts = if !G.si then "si" else "" in let shp = H.string_of_graph () in let attrs = ["hierarchy", shp; "options", opts] in - tag root attrs ~contents out 0; + tag obj_root attrs ~contents out 0; + close_out och + +let marks = function + | [] -> "mark", "" + | l -> "mark", String.concat " " (List.rev_map string_of_int l) + +let export_csys s = + let path = path_of_uri !G.xdir s.Q.uri in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in + let name = F.concat path (ccs_name ^ ext) in + let och = open_out name in + let out = output_string och in + xml out "1.0" "UTF-8"; doctype out ccs_root system; + let attrs = [uri s.Q.uri] in + let contents = tag "ToInfinity" [arity s.Q.is; marks s.Q.is] in + tag ccs_root attrs ~contents out 0; close_out och diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.mli b/helm/software/lambda-delta/src/xml/xmlLibrary.mli index 28f056f06..ebd4157d9 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.mli +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.mli @@ -15,8 +15,9 @@ type attr = string * string type pp = och -> int -> unit -val export_entity: - ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit +val export_entity: ('term -> pp) -> 'term Entity.entity -> unit + +val export_csys: Ccs.csys -> unit val tag: string -> attr list -> ?contents:pp -> pp @@ -44,7 +45,7 @@ val offset: int -> attr val uri: Entity.uri -> attr -val arity: int -> attr +val arity: ?n:int -> 'a list -> attr val level: Level.level -> attr diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index e6e90f738..d97173d82 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -95,10 +95,23 @@ meta CDATA #IMPLIED > - - + + + + + + + + + +