From cee0c3ca597ebbff2250674c255ed1bc909521fb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 3 Nov 2010 21:02:44 +0000 Subject: [PATCH] last commit for helena 0.8.1 - xsl : we can render the levels of the abstractions - ccs : we output three kinds of constraints - Makefiles: we automatized the relising process - brgCrg : all abstractions have infinite level for now --- helm/software/lambda-delta/Make | 11 ++++++++ helm/software/lambda-delta/MakeVersion | 1 + helm/software/lambda-delta/Makefile | 8 +++++- helm/software/lambda-delta/Makefile.common | 13 ++++++++-- helm/software/lambda-delta/README | 6 ++--- .../lambda-delta/src/automath/autCrg.ml | 3 ++- .../lambda-delta/src/basic_ag/bagCrg.ml | 1 + .../lambda-delta/src/basic_rg/brgCrg.ml | 2 -- .../lambda-delta/src/basic_rg/brgReduction.ml | 10 ++++---- helm/software/lambda-delta/src/common/ccs.ml | 22 +++++++++++++--- helm/software/lambda-delta/src/common/ccs.mli | 10 ++++++-- .../lambda-delta/src/xml/xmlLibrary.ml | 18 ++++++++++++- .../lambda-delta/xml/ld-html-library.xsl | 25 ++++++++++++++++--- helm/software/lambda-delta/xml/ld.dtd | 21 +++++++++++++--- 14 files changed, 124 insertions(+), 27 deletions(-) create mode 100644 helm/software/lambda-delta/Make create mode 100644 helm/software/lambda-delta/MakeVersion diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make new file mode 100644 index 000000000..f5f4524de --- /dev/null +++ b/helm/software/lambda-delta/Make @@ -0,0 +1,11 @@ +.depend.opt +Make* +README +examples/grundlagen/*.aut +icons/*.ico +icons/*.png +src/*.ml +src/Make* +src/*/* +xml/*.dtd +xml/*.xsl diff --git a/helm/software/lambda-delta/MakeVersion b/helm/software/lambda-delta/MakeVersion new file mode 100644 index 000000000..6f4eebdf6 --- /dev/null +++ b/helm/software/lambda-delta/MakeVersion @@ -0,0 +1 @@ +0.8.1 diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index daabc346d..7ee8e5f58 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -18,10 +18,12 @@ 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 \ xml/brg-si/grundlagen/l/e/pairis1.ld.xml \ + xml/brg-si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ xml/crg-si/grundlagen/l/not.ld.xml \ xml/crg-si/grundlagen/l/et.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 \ + xml/crg-si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ xml/brg-si/grundlagen/ccs.ldc.xml include Makefile.common @@ -61,6 +63,9 @@ etc: $(H)mkdir -p $(LOCALLDDLDIR)/$(@D) $(H)$(XSLT) -o $(LOCALLDDLDIR)/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml +%.ldc: + @echo " SKIP $@" + etc/make-html.sh xml/index.txt index: @echo " GENERATE INDEXES" $(H)find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt @@ -79,7 +84,8 @@ install-html: etc/make-html.sh install-lddl: index @echo " INSTALL lddl.tar.bz2" - $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml + $(H)tar -cjf etc/lddl.tar.bz2 -X etc/exclude.txt xml + $(H)scp etc/lddl.tar.bz2 $(DOWNDIR) install-dtd: xml/ld.dtd @echo " INSTALL $<" diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 7bf33007d..806379008 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -1,15 +1,17 @@ H=@ ifeq ($(origin OCAMLPATH), undefined) - OCAMLFIND = OCAMLPATH=../components/METAS ocamlfind + OCAMLFIND = OCAMLPATH=$(HOME)/svn/software/components/METAS ocamlfind else OCAMLFIND = ocamlfind endif +RELISE = $(MAIN:%=%_$(shell cat MakeVersion)) + LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl LDDLDIR = mowgli:/projects/helm/public_html/lambda-delta/static/lddl DOWNDIR = mowgli:/projects/helm/public_html/lambda-delta/download XMLDIR = mowgli:/projects/helm/public_html/lambda-delta/xml -LOCALLDDLDIR = ../../../public_html/lddl +LOCALLDDLDIR = $(HOME)/public_html/lddl DIRECTORIES = $(addprefix $(SRC)/,$(shell cat $(SRC)/Make)) @@ -71,6 +73,13 @@ lint-xml: $(XMLS) @echo XMLLINT --valid $(H)$(XMLLINT) --valid $^ +relise: clean + @echo " RELISE $(RELISE)" + $(H)mkdir -p $(RELISE) + $(H)$(foreach FILE, $(shell cat Make), cp --parents $(FILE) $(RELISE);) + $(H)tar -czf etc/$(RELISE).tar.gz $(RELISE) + $(H)scp etc/$(RELISE).tar.gz $(DOWNDIR) + tgz: clean @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)" $(H)find -name "Make*" | xargs $(TAR) $(KEEP) diff --git a/helm/software/lambda-delta/README b/helm/software/lambda-delta/README index 8a0f0d674..a21142fea 100644 --- a/helm/software/lambda-delta/README +++ b/helm/software/lambda-delta/README @@ -4,7 +4,7 @@ Helena 0.8.1 M * type "make test-si" to parse the grundlagen it generates a log.txt with the grundlagen contents statistics - -* type "make clean" to remove the products of compilation -* type "make tgz" to make a tar.gz of the source files +* type "make test-si-fast" to parse the grundlagen with minimum logging + +* type "make clean" to remove the products of compilation diff --git a/helm/software/lambda-delta/src/automath/autCrg.ml b/helm/software/lambda-delta/src/automath/autCrg.ml index 388b0c2b9..66de6c3d3 100644 --- a/helm/software/lambda-delta/src/automath/autCrg.ml +++ b/helm/software/lambda-delta/src/automath/autCrg.ml @@ -128,7 +128,8 @@ let rec xlate_term f st lenv = function let f nw ww = let a = [E.Name (name, true)] in let f nt tt = - let b = D.Abst (nt, [ww]) in + let nnt = N.infinite (* if N.is_zero nt then N.infinite else nt *) in + let b = D.Abst (nnt, [ww]) in f nt (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in diff --git a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml index dcc495232..8fbf7cf79 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml @@ -42,6 +42,7 @@ let rec xlate_term xlate_bind f c = function xlate_term xlate_bind f c t | D.TProj (_, e, t) -> xlate_term xlate_bind f c (D.tshift e t) +(* this case should be removed by improving alpha-conversion *) | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) -> xlate_term xlate_bind f c (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) -> diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml index 490125095..8514de641 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml @@ -32,8 +32,6 @@ let rec xlate_term f = function xlate_term f t | D.TProj (_, e, t) -> xlate_term f (D.tshift e 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 diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index 5f73a4fc0..c4b2e9c15 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -114,7 +114,7 @@ let rec step st m x = begin match m.s with | [] -> m, None, x | (c, v) :: s -> - if N.is_zero n then Q.add_infinite st.S.cc a; + if N.is_zero n then Q.add_nonzero 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 @@ -159,13 +159,13 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) = 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) - when n1 = n2 || st.S.si -> + _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) -> + if n1 = n2 then () else Q.add_equal st.S.cc a1 a2; 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 -> + | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t) -> + if N.is_zero n then () else Q.add_zero st.S.cc a; O.add ~si:1 (); ac st (push m1 a b) u (push m2 a b) t | _ -> false diff --git a/helm/software/lambda-delta/src/common/ccs.ml b/helm/software/lambda-delta/src/common/ccs.ml index ca27ff93d..db8a77865 100644 --- a/helm/software/lambda-delta/src/common/ccs.ml +++ b/helm/software/lambda-delta/src/common/ccs.ml @@ -17,7 +17,9 @@ module G = Options type csys = { uri: E.uri; - mutable is : int list + mutable tp : int list; + mutable t1 : int list; + mutable tn : (int * int) list; } let mark a = E.mark C.err C.start a @@ -26,11 +28,23 @@ let mark a = E.mark C.err C.start a let init () = { uri = U.uri_of_string (G.get_baseuri ()); - is = []; + tp = []; t1 = []; tn = [] } -let add_infinite s a = +let add_nonzero 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 + if L.mem i s.tp then () else s.tp <- i :: s.tp + else () + +let add_zero s a = + if !G.si && !G.cc then + let i = abs (mark a) in + if L.mem i s.t1 then () else s.t1 <- i :: s.t1 + else () + +let add_equal s xa ia = + if !G.si && !G.cc then + let i = abs (mark xa), abs (mark ia) in + if L.mem i s.tn then () else s.tn <- i :: s.tn else () diff --git a/helm/software/lambda-delta/src/common/ccs.mli b/helm/software/lambda-delta/src/common/ccs.mli index d94406d7b..4d11ddd7c 100644 --- a/helm/software/lambda-delta/src/common/ccs.mli +++ b/helm/software/lambda-delta/src/common/ccs.mli @@ -11,9 +11,15 @@ type csys = { uri: Entity.uri; - mutable is : int list + mutable tp : int list; + mutable t1 : int list; + mutable tn : (int * int) list; } val init: unit -> csys -val add_infinite: csys -> Entity.attrs -> unit +val add_nonzero: csys -> Entity.attrs -> unit + +val add_zero: csys -> Entity.attrs -> unit + +val add_equal: csys -> Entity.attrs -> Entity.attrs -> unit diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml index 3bc0c54e0..7355c98a7 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml @@ -145,10 +145,22 @@ let export_entity pp_term (a, u, b) = tag obj_root attrs ~contents out 0; close_out och +let prec_map (i, _) = string_of_int i + +let next_map (_, i) = string_of_int i + let marks = function | [] -> "mark", "" | l -> "mark", String.concat " " (List.rev_map string_of_int l) +let precs = function + | [] -> "prec", "" + | l -> "prec", String.concat " " (List.rev_map prec_map l) + +let nexts = function + | [] -> "next", "" + | l -> "next", String.concat " " (List.rev_map next_map 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 @@ -157,6 +169,10 @@ let export_csys s = 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 + let contents out tab = + tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab; + tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab; + tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab + in tag ccs_root attrs ~contents out 0; close_out och diff --git a/helm/software/lambda-delta/xml/ld-html-library.xsl b/helm/software/lambda-delta/xml/ld-html-library.xsl index 2094c2a87..3120f0960 100644 --- a/helm/software/lambda-delta/xml/ld-html-library.xsl +++ b/helm/software/lambda-delta/xml/ld-html-library.xsl @@ -85,7 +85,26 @@ - &lambda; + + + &Pi; + + + + &Pi; + + + &lambda; + + + &lambda; + &infin; + + + &lambda; + + + @@ -110,8 +129,8 @@ - - + + diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index 539e8a28f..0378bb397 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -105,14 +105,29 @@ - + - - + + + + + + + + +