From da715664068e859d20ab81fd6969e64d58c0f57e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 29 Oct 2009 19:50:22 +0000 Subject: [PATCH] - dual_rg: renamed to complete_rg [as suggested in the ToCL documentation] - Makefile: "lddl" entry generates lddl.tar.bz2 --- helm/software/lambda-delta/.depend.opt | 45 ++++++++++--------- helm/software/lambda-delta/Makefile | 6 ++- helm/software/lambda-delta/Makefile.common | 1 + .../complete_rg/{drg.ml => crg.ml} | 4 +- .../complete_rg/{drgAut.ml => crgAut.ml} | 8 ++-- .../complete_rg/{drgAut.mli => crgAut.mli} | 2 +- .../complete_rg/{drgBrg.ml => crgBrg.ml} | 7 +-- .../complete_rg/{drgBrg.mli => crgBrg.mli} | 2 +- .../{drgOutput.ml => crgOutput.ml} | 2 +- .../{drgOutput.mli => crgOutput.mli} | 4 +- helm/software/lambda-delta/toplevel/top.ml | 36 +++++++-------- 11 files changed, 61 insertions(+), 56 deletions(-) rename helm/software/lambda-delta/complete_rg/{drg.ml => crg.ml} (95%) rename helm/software/lambda-delta/complete_rg/{drgAut.ml => crgAut.ml} (97%) rename helm/software/lambda-delta/complete_rg/{drgAut.mli => crgAut.mli} (92%) rename helm/software/lambda-delta/complete_rg/{drgBrg.ml => crgBrg.ml} (95%) rename helm/software/lambda-delta/complete_rg/{drgBrg.mli => crgBrg.mli} (92%) rename helm/software/lambda-delta/complete_rg/{drgOutput.ml => crgOutput.ml} (99%) rename helm/software/lambda-delta/complete_rg/{drgOutput.mli => crgOutput.mli} (88%) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 1cf0b734e..00b1db36f 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -114,23 +114,26 @@ basic_rg/brgUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ basic_rg/brgUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ basic_rg/brgType.cmx basic_rg/brgReduction.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi -dual_rg/drg.cmo: common/entity.cmx -dual_rg/drg.cmx: common/entity.cmx -dual_rg/drgOutput.cmi: common/library.cmi dual_rg/drg.cmx -dual_rg/drgOutput.cmo: lib/nUri.cmi common/library.cmi common/hierarchy.cmi \ - common/entity.cmx dual_rg/drg.cmx lib/cps.cmx dual_rg/drgOutput.cmi -dual_rg/drgOutput.cmx: lib/nUri.cmx common/library.cmx common/hierarchy.cmx \ - common/entity.cmx dual_rg/drg.cmx lib/cps.cmx dual_rg/drgOutput.cmi -dual_rg/drgAut.cmi: common/entity.cmx dual_rg/drg.cmx automath/aut.cmx -dual_rg/drgAut.cmo: lib/nUri.cmi common/entity.cmx dual_rg/drg.cmx \ - lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi -dual_rg/drgAut.cmx: lib/nUri.cmx common/entity.cmx dual_rg/drg.cmx \ - lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi -dual_rg/drgBrg.cmi: dual_rg/drg.cmx basic_rg/brg.cmx -dual_rg/drgBrg.cmo: common/entity.cmx dual_rg/drg.cmx lib/cps.cmx \ - basic_rg/brg.cmx dual_rg/drgBrg.cmi -dual_rg/drgBrg.cmx: common/entity.cmx dual_rg/drg.cmx lib/cps.cmx \ - basic_rg/brg.cmx dual_rg/drgBrg.cmi +complete_rg/crg.cmo: common/entity.cmx +complete_rg/crg.cmx: common/entity.cmx +complete_rg/crgOutput.cmi: common/library.cmi complete_rg/crg.cmx +complete_rg/crgOutput.cmo: lib/nUri.cmi common/library.cmi \ + common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ + complete_rg/crgOutput.cmi +complete_rg/crgOutput.cmx: lib/nUri.cmx common/library.cmx \ + common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ + complete_rg/crgOutput.cmi +complete_rg/crgAut.cmi: common/entity.cmx complete_rg/crg.cmx \ + automath/aut.cmx +complete_rg/crgAut.cmo: lib/nUri.cmi common/entity.cmx complete_rg/crg.cmx \ + lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi +complete_rg/crgAut.cmx: lib/nUri.cmx common/entity.cmx complete_rg/crg.cmx \ + lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi +complete_rg/crgBrg.cmi: complete_rg/crg.cmx basic_rg/brg.cmx +complete_rg/crgBrg.cmo: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ + basic_rg/brg.cmx complete_rg/crgBrg.cmi +complete_rg/crgBrg.cmx: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ + basic_rg/brg.cmx complete_rg/crgBrg.cmi toplevel/meta.cmo: common/entity.cmx toplevel/meta.cmx: common/entity.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx @@ -160,8 +163,8 @@ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \ common/library.cmi common/hierarchy.cmi common/entity.cmx \ - dual_rg/drgOutput.cmi dual_rg/drgBrg.cmi dual_rg/drgAut.cmi \ - dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \ + complete_rg/crgOutput.cmi complete_rg/crgBrg.cmi complete_rg/crgAut.cmi \ + complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \ basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \ basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \ @@ -170,8 +173,8 @@ toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \ toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \ common/library.cmx common/hierarchy.cmx common/entity.cmx \ - dual_rg/drgOutput.cmx dual_rg/drgBrg.cmx dual_rg/drgAut.cmx \ - dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ + complete_rg/crgOutput.cmx complete_rg/crgBrg.cmx complete_rg/crgAut.cmx \ + complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \ basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \ diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index d2edae23b..98a1c59c6 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -50,7 +50,7 @@ xml-si-drg: $(MAIN).opt $(H)$(XSLT) -o $(LDDLDIR)/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml etc/make-html.sh xml/index.txt index: - @echo " GENERATING INDEXES" + @echo " GENERATE INDEXES" $(H)find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt $(H)sed "s/^/make --no-print-directory /" xml/index.txt | sed s.ld:/.. > etc/make-html.sh @@ -60,3 +60,7 @@ html: etc/make-html.sh test-html: @$(MAKE) --no-print-directory $(XMLS:xml/%.xml=%) + +lddl: index + @echo " GENERATE lddl.tar.bz2" + $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index cd8713015..ca219ca66 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -2,6 +2,7 @@ H=@ LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl LDDLDIR = /projects/helm/public_html/lambda-delta/static/lddl +DOWNDIR = /projects/helm/public_html/lambda-delta/download DIRECTORIES = $(shell cat Make) diff --git a/helm/software/lambda-delta/complete_rg/drg.ml b/helm/software/lambda-delta/complete_rg/crg.ml similarity index 95% rename from helm/software/lambda-delta/complete_rg/drg.ml rename to helm/software/lambda-delta/complete_rg/crg.ml index 87e973ca8..6db1b5481 100644 --- a/helm/software/lambda-delta/complete_rg/drg.ml +++ b/helm/software/lambda-delta/complete_rg/crg.ml @@ -9,8 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -(* kernel version: dual, relative, global *) -(* note : fragment of dual lambda-delta serving as abstract layer *) +(* kernel version: complete, relative, global *) +(* note : fragment of complete lambda-delta serving as abstract layer *) type uri = Entity.uri type id = Entity.id diff --git a/helm/software/lambda-delta/complete_rg/drgAut.ml b/helm/software/lambda-delta/complete_rg/crgAut.ml similarity index 97% rename from helm/software/lambda-delta/complete_rg/drgAut.ml rename to helm/software/lambda-delta/complete_rg/crgAut.ml index 4b17faaa1..267e2b403 100644 --- a/helm/software/lambda-delta/complete_rg/drgAut.ml +++ b/helm/software/lambda-delta/complete_rg/crgAut.ml @@ -14,7 +14,7 @@ module H = U.UriHash module C = Cps module Y = Entity module A = Aut -module D = Drg +module D = Crg (* qualified identifier: uri, name, qualifiers *) type qid = D.uri * D.id * D.id list @@ -181,7 +181,7 @@ let xlate_entity err f st = function | _ -> D.TBind (a, D.Abst ws, ww) in (* - DrgOutput.pp_term print_string t; print_newline (); + print_newline (); CrgOutput.pp_term print_string t; *) let b = Y.Abst t in let entity = [Y.Mark st.line], uri_of_qid qid, b in @@ -203,7 +203,7 @@ let xlate_entity err f st = function | _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv)) in (* - Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid)); + print_newline (); CrgOutput.pp_term print_string t; *) let b = Y.Abbr t in let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in @@ -219,4 +219,4 @@ let xlate_entity err f st = function let initial_status mk_uri = initial_status mk_uri -let drg_of_aut = xlate_entity +let crg_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/complete_rg/drgAut.mli b/helm/software/lambda-delta/complete_rg/crgAut.mli similarity index 92% rename from helm/software/lambda-delta/complete_rg/drgAut.mli rename to helm/software/lambda-delta/complete_rg/crgAut.mli index 5de7f7e85..3f416a033 100644 --- a/helm/software/lambda-delta/complete_rg/drgAut.mli +++ b/helm/software/lambda-delta/complete_rg/crgAut.mli @@ -13,5 +13,5 @@ type status val initial_status: Entity.uri_generator -> status -val drg_of_aut: (status -> 'a) -> (status -> Drg.entity -> 'a) -> +val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> status -> Aut.entity -> 'a diff --git a/helm/software/lambda-delta/complete_rg/drgBrg.ml b/helm/software/lambda-delta/complete_rg/crgBrg.ml similarity index 95% rename from helm/software/lambda-delta/complete_rg/drgBrg.ml rename to helm/software/lambda-delta/complete_rg/crgBrg.ml index 9ff63fb7c..d07e6efbf 100644 --- a/helm/software/lambda-delta/complete_rg/drgBrg.ml +++ b/helm/software/lambda-delta/complete_rg/crgBrg.ml @@ -11,7 +11,7 @@ module C = Cps module Y = Entity -module D = Drg +module D = Crg module B = Brg let rec lenv_fold_left map1 map2 x = function @@ -60,8 +60,5 @@ and xlate_bind x a b = and xlate_proj x _ e = lenv_fold_left xlate_bind xlate_proj x e -let brg_of_drg f t = -(* - print_newline (); DrgOutput.pp_term print_string t; -*) +let brg_of_crg f t = f (xlate_term C.start t) diff --git a/helm/software/lambda-delta/complete_rg/drgBrg.mli b/helm/software/lambda-delta/complete_rg/crgBrg.mli similarity index 92% rename from helm/software/lambda-delta/complete_rg/drgBrg.mli rename to helm/software/lambda-delta/complete_rg/crgBrg.mli index 900dad95a..db4e54221 100644 --- a/helm/software/lambda-delta/complete_rg/drgBrg.mli +++ b/helm/software/lambda-delta/complete_rg/crgBrg.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val brg_of_drg: (Brg.term -> 'a) -> Drg.term -> 'a +val brg_of_crg: (Brg.term -> 'a) -> Crg.term -> 'a diff --git a/helm/software/lambda-delta/complete_rg/drgOutput.ml b/helm/software/lambda-delta/complete_rg/crgOutput.ml similarity index 99% rename from helm/software/lambda-delta/complete_rg/drgOutput.ml rename to helm/software/lambda-delta/complete_rg/crgOutput.ml index 5cb9538dd..ecc4a33b1 100644 --- a/helm/software/lambda-delta/complete_rg/drgOutput.ml +++ b/helm/software/lambda-delta/complete_rg/crgOutput.ml @@ -15,7 +15,7 @@ module C = Cps module H = Hierarchy module Y = Entity module X = Library -module D = Drg +module D = Crg (****************************************************************************) diff --git a/helm/software/lambda-delta/complete_rg/drgOutput.mli b/helm/software/lambda-delta/complete_rg/crgOutput.mli similarity index 88% rename from helm/software/lambda-delta/complete_rg/drgOutput.mli rename to helm/software/lambda-delta/complete_rg/crgOutput.mli index e02161b13..4d3f747fd 100644 --- a/helm/software/lambda-delta/complete_rg/drgOutput.mli +++ b/helm/software/lambda-delta/complete_rg/crgOutput.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val export_term: Drg.term -> Library.pp +val export_term: Crg.term -> Library.pp -val pp_term: (string -> unit) -> Drg.term -> unit +val pp_term: (string -> unit) -> Crg.term -> unit diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 6f7d60e9c..12e639c56 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -20,12 +20,12 @@ module Y = Entity module X = Library module AP = AutProcess module AO = AutOutput -module DA = DrgAut +module DA = CrgAut module MA = MetaAut module MO = MetaOutput module ML = MetaLibrary -module DO = DrgOutput -module DBrg = DrgBrg +module DO = CrgOutput +module DBrg = CrgBrg module MBrg = MetaBrg module BrgO = BrgOutput module BrgR = BrgReduction @@ -76,7 +76,7 @@ type kernel = Brg | Bag type kernel_entity = BrgEntity of Brg.entity | BagEntity of Bag.entity - | DrgEntity of Drg.entity + | CrgEntity of Crg.entity | MetaEntity of Meta.entity let kernel = ref Brg @@ -86,8 +86,8 @@ let print_counters st = match !kernel with | Bag -> BagO.print_counters C.start st.bagc let xlate f st entity = match !kernel, entity with - | Brg, DrgEntity e -> - let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_drg e + | Brg, CrgEntity e -> + let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e | Brg, MetaEntity e -> let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e | Bag, MetaEntity e -> @@ -102,7 +102,7 @@ let pp_progress e = Y.mark err f a in match e with - | DrgEntity e -> Y.common f e + | CrgEntity e -> Y.common f e | BrgEntity e -> Y.common f e | BagEntity e -> Y.common f e | MetaEntity e -> Y.common f e @@ -114,7 +114,7 @@ let count_entity st = function | _ -> st let export_entity si g moch = function - | DrgEntity e -> X.export_entity DO.export_term si g e + | CrgEntity e -> X.export_entity DO.export_term si g e | BrgEntity e -> X.export_entity BrgO.export_term si g e | MetaEntity e -> begin match moch with @@ -125,12 +125,12 @@ let export_entity si g moch = function let type_check f st si g k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in - let ok _ (a, u, _) = f st a u in + let ok _ _ = f st in match k with - | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity - | BagEntity entity -> BagU.type_check ok ~si g entity - | DrgEntity (a, u, _) - | MetaEntity (a, u, _) -> f st a u + | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity + | BagEntity entity -> BagU.type_check ok ~si g entity + | CrgEntity _ + | MetaEntity _ -> f st (****************************************************************************) @@ -146,7 +146,7 @@ let export = ref false let graph = ref (H.graph_of_string C.err C.start "Z2") let old = ref false -let process_3 f st a u = +let process_3 f st = f st let process_2 f st entity = @@ -166,9 +166,9 @@ let process_0 f st entity = let frr mst = f {st with mst = mst} in let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in let err dst = f {st with dst = dst} in - let g dst e = process_1 f {st with dst = dst} (DrgEntity e) in + let g dst e = process_1 f {st with dst = dst} (CrgEntity e) in if !old then MA.meta_of_aut frr h st.mst entity else - DA.drg_of_aut err g st.dst entity + DA.crg_of_aut err g st.dst entity in let st = {st with ac = count AO.count_entity st.ac entity} in if !preprocess then process_entity f st entity else f st entity @@ -219,7 +219,7 @@ try if !L.level > 0 then T.utime_stamp "parsed"; O.clear_reductions (); let mk_uri = - if !stage < 2 then Drg.mk_uri else + if !stage < 2 then Crg.mk_uri else match !kernel with | Brg -> Brg.mk_uri | Bag -> Bag.mk_uri @@ -255,7 +255,7 @@ try let help_j = " show URI of processed kernel objects" in let help_k = " set kernel version (default: brg)" in let help_m = " output intermediate representation (HAL)" in - let help_o = " use old abstract language instead of drg" in + let help_o = " use old abstract language instead of crg" in let help_p = " preprocess Automath source" in let help_r = " disable initial segment of URI hierarchy" in let help_s = " set translation stage (see above)" in -- 2.39.2