From: Ferruccio Guidi Date: Mon, 5 Oct 2009 16:05:53 +0000 (+0000) Subject: - common/entity: new format for kernel entities X-Git-Tag: make_still_working~3376 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd798346d31b14b8947e5801b87dc4f363607862;p=helm.git - common/entity: new format for kernel entities - common/library: new CPS infrastructure for XML exportation - toplevel/meta: now uses common/entity - dual_rg/drg: some fixes - dual_rg/drgOutput: XML exportation started (alpha-conversion is missing) --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index fe670cb6c..1dbe1c488 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -34,88 +34,103 @@ common/output.cmx: lib/log.cmx common/output.cmi common/entity.cmo: lib/nUri.cmi automath/aut.cmx common/entity.cmx: lib/nUri.cmx automath/aut.cmx common/library.cmi: common/hierarchy.cmi common/entity.cmx -common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi -common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi +common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \ + lib/cps.cmx common/library.cmi +common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/entity.cmx \ + lib/cps.cmx common/library.cmi basic_ag/bag.cmo: lib/log.cmi common/entity.cmx lib/cps.cmx basic_ag/bag.cmx: lib/log.cmx common/entity.cmx lib/cps.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ - common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi + common/hierarchy.cmi common/entity.cmx basic_ag/bag.cmx \ + basic_ag/bagOutput.cmi basic_ag/bagOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ - common/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi + common/hierarchy.cmx common/entity.cmx basic_ag/bag.cmx \ + basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi: basic_ag/bag.cmx -basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \ - basic_ag/bagEnvironment.cmi -basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_ag/bag.cmx \ - basic_ag/bagEnvironment.cmi +basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ + basic_ag/bag.cmx basic_ag/bagEnvironment.cmi +basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ + basic_ag/bag.cmx basic_ag/bagEnvironment.cmi basic_ag/bagSubstitution.cmi: basic_ag/bag.cmx basic_ag/bagSubstitution.cmo: lib/share.cmx basic_ag/bag.cmx \ basic_ag/bagSubstitution.cmi basic_ag/bagSubstitution.cmx: lib/share.cmx basic_ag/bag.cmx \ basic_ag/bagSubstitution.cmi basic_ag/bagReduction.cmi: basic_ag/bag.cmx -basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \ - basic_ag/bagSubstitution.cmi basic_ag/bagOutput.cmi \ +basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ + lib/cps.cmx basic_ag/bagSubstitution.cmi basic_ag/bagOutput.cmi \ basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagReduction.cmi -basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \ - basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \ +basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ + lib/cps.cmx basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi basic_ag/bagType.cmi: common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ - common/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \ - basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \ - basic_ag/bagType.cmi + common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ + basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi \ + basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagType.cmi basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ - common/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \ - basic_ag/bagOutput.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \ - basic_ag/bagType.cmi + common/hierarchy.cmx common/entity.cmx lib/cps.cmx \ + basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx \ + basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagType.cmi basic_ag/bagUntrusted.cmi: common/hierarchy.cmi basic_ag/bag.cmx -basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \ - basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi -basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \ - basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi +basic_ag/bagUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ + basic_ag/bagType.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \ + basic_ag/bagUntrusted.cmi +basic_ag/bagUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ + basic_ag/bagType.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \ + basic_ag/bagUntrusted.cmi basic_rg/brg.cmo: common/entity.cmx basic_rg/brg.cmx: common/entity.cmx -basic_rg/brgOutput.cmi: lib/log.cmi common/entity.cmx basic_rg/brg.cmx +basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ - common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi + common/library.cmi common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ + basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ - common/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi + common/library.cmx common/hierarchy.cmx common/entity.cmx lib/cps.cmx \ + basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: basic_rg/brg.cmx -basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ +basic_rg/brgEnvironment.cmo: lib/nUri.cmi common/entity.cmx basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi -basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ +basic_rg/brgEnvironment.cmx: lib/nUri.cmx common/entity.cmx basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \ - lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \ + lib/log.cmi common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \ - lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ + lib/log.cmx common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi \ basic_rg/brgReduction.cmi basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ - common/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \ - basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ - basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgType.cmi + common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ + basic_rg/brgSubstitution.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ + basic_rg/brgType.cmi basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ - common/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.cmx \ - basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \ - basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgType.cmi + common/hierarchy.cmx common/entity.cmx lib/cps.cmx \ + basic_rg/brgSubstitution.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ + basic_rg/brgType.cmi basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brgType.cmi \ basic_rg/brg.cmx -basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ - basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ - basic_rg/brgUntrusted.cmi -basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \ - basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ - basic_rg/brgUntrusted.cmi +basic_rg/brgUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ + basic_rg/brgType.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi +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: common/library.cmi dual_rg/drg.cmx \ + dual_rg/drgOutput.cmi +dual_rg/drgOutput.cmx: common/library.cmx dual_rg/drg.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 @@ -125,40 +140,42 @@ toplevel/meta.cmo: common/entity.cmx toplevel/meta.cmx: common/entity.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \ - lib/cps.cmx toplevel/metaOutput.cmi + common/entity.cmx lib/cps.cmx toplevel/metaOutput.cmi toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/log.cmx \ - lib/cps.cmx toplevel/metaOutput.cmi + common/entity.cmx lib/cps.cmx toplevel/metaOutput.cmi toplevel/metaLibrary.cmi: toplevel/meta.cmx toplevel/metaLibrary.cmo: toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaLibrary.cmx: toplevel/metaOutput.cmx toplevel/metaLibrary.cmi toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx -toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ - automath/aut.cmx toplevel/metaAut.cmi -toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \ - automath/aut.cmx toplevel/metaAut.cmi +toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx common/entity.cmx \ + lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi +toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx common/entity.cmx \ + lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi toplevel/metaBag.cmi: toplevel/meta.cmx basic_ag/bag.cmx toplevel/metaBag.cmo: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \ toplevel/metaBag.cmi toplevel/metaBag.cmx: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \ toplevel/metaBag.cmi toplevel/metaBrg.cmi: toplevel/meta.cmx basic_rg/brg.cmx -toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ - toplevel/metaBrg.cmi -toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ - toplevel/metaBrg.cmi +toplevel/metaBrg.cmo: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ + basic_rg/brg.cmx toplevel/metaBrg.cmi +toplevel/metaBrg.cmx: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ + basic_rg/brg.cmx toplevel/metaBrg.cmi 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 lib/log.cmi common/library.cmi \ - common/hierarchy.cmi 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 \ - automath/autOutput.cmi automath/autLexer.cmx + common/hierarchy.cmi common/entity.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 automath/autOutput.cmi \ + automath/autLexer.cmx 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 lib/log.cmx common/library.cmx \ - common/hierarchy.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 \ - automath/autOutput.cmx automath/autLexer.cmx + common/hierarchy.cmx common/entity.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 automath/autOutput.cmx \ + automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index c3901db48..19421a032 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -19,12 +19,12 @@ INPUT = automath/grundlagen.aut INPUT-ORIG = automath/grundlagen-orig.aut test: $(MAIN).opt - @echo " HELENA -a -r $(INPUT)" - $(H)./$(MAIN).opt -a -r -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -p -r $(INPUT)" + $(H)./$(MAIN).opt -p -r -S 3 $(O) $(INPUT) > etc/log.txt test-si: $(MAIN).opt - @echo " HELENA -a -r -u $(INPUT)" - $(H)./$(MAIN).opt -a -r -u -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -p -r -u $(INPUT)" + $(H)./$(MAIN).opt -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt @echo " HELENA -r -u $(INPUT)" diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 3649a8b07..cd8713015 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -13,7 +13,7 @@ OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v XMLLINT = xmllint --noout XSLT = xsltproc -TAR = tar -czf $(MAIN:%=%.tgz) +TAR = tar -czf etc/$(MAIN:%=%.tgz) define DIR_TEMPLATE MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make)) diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 79e7a0421..cd8d493f5 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -26,9 +26,7 @@ and term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of int * id * bind * term (* location, name, binder, scope *) -type entry = bind Entity.entry (* age, uri, binder *) - -type entity = bind Entity.entity +type entity = term Entity.entity (* attrs, uri, binder *) type lenv = (int * id * bind) list (* location, name, binder *) diff --git a/helm/software/lambda-delta/basic_ag/bagEnvironment.ml b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml index 35fab4db3..04681cfee 100644 --- a/helm/software/lambda-delta/basic_ag/bagEnvironment.ml +++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml @@ -12,24 +12,28 @@ module U = NUri module L = Log module H = U.UriHash +module Y = Entity module B = Bag exception ObjectNotFound of B.message let hsize = 7000 let env = H.create hsize -let age = ref 1 (* Internal functions *******************************************************) +let get_age = + let age = ref 0 in + fun () -> incr age; !age + let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) (* Interface functions ******************************************************) -let set_entry f entry = - let _, uri, b = entry in - let entry = !age, uri, b in - incr age; H.add env uri entry; f entry +let set_entity f (a, uri, b) = + let age = get_age () in + let entry = (Y.Apix age :: a), uri, b in + H.add env uri entry; f entry -let get_entry f uri = +let get_entity f uri = try f (H.find env uri) with Not_found -> error uri diff --git a/helm/software/lambda-delta/basic_ag/bagEnvironment.mli b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli index ed94f4e8b..4a44c05fe 100644 --- a/helm/software/lambda-delta/basic_ag/bagEnvironment.mli +++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli @@ -11,6 +11,6 @@ exception ObjectNotFound of Bag.message -val set_entry: (Bag.entry -> 'a) -> Bag.entry -> 'a +val set_entity: (Bag.entity -> 'a) -> Bag.entity -> 'a -val get_entry: (Bag.entry -> 'a) -> Bag.uri -> 'a +val get_entity: (Bag.entity -> 'a) -> Bag.uri -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index 400ffc55e..a97219120 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -13,6 +13,7 @@ module P = Printf module F = Format module U = NUri module L = Log +module Y = Entity module H = Hierarchy module O = Output module B = Bag @@ -62,21 +63,13 @@ and count_term f c = function let f c = count_term_binder f c b in count_term f c t -let count_entry_binder f c = function - | B.Abst w -> +let count_entity f c = function + | _, _, Y.Abst w -> let c = {c with eabsts = succ c.eabsts} in count_term f c w - | B.Abbr v -> + | _, _, Y.Abbr v -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v - | B.Void -> f c - -let count_entry f c (_, _, b) = - count_entry_binder f c b - -let count_entity f c = function - | Some entry -> count_entry f c entry - | None -> f c let print_counters f c = let terms = diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index 628968bef..a05d4b5d6 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -12,6 +12,7 @@ module U = NUri module C = Cps module L = Log +module Y = Entity module B = Bag module O = BagOutput module E = BagEnvironment @@ -26,7 +27,7 @@ type machine = { type whd_result = | Sort_ of int | LRef_ of int * B.term option - | GRef_ of B.entry + | GRef_ of B.entity | Bind_ of int * B.id * B.term * B.term type ho_whd_result = @@ -84,7 +85,7 @@ let rec whd f c m x = | B.Sort h -> f m (Sort_ h) | B.GRef uri -> let f entry = f m (GRef_ entry) in - E.get_entry f uri + E.get_entity f uri | B.LRef i -> let f = function | B.Void -> f m (LRef_ (i, None)) @@ -116,10 +117,9 @@ let rec ho_whd f c m x = | Bind_ (_, _, w, _) -> let f w = f (Abst w) in unwind_to_term f m w | LRef_ (_, Some w) -> ho_whd f c m w - | GRef_ (_, _, B.Abst w) -> ho_whd f c m w - | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v + | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w + | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v | LRef_ (_, None) -> assert false - | GRef_ (_, _, B.Void) -> assert false in whd aux c m x @@ -139,9 +139,11 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 = if h1 = h2 then f a else f false | LRef_ (i1, _), LRef_ (i2, _) -> if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false - | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) -> + | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _), + GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) -> if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false - | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) -> + | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1), + GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) -> if a1 = a2 then let f a = if a then f a else are_convertible f ~si true c m1 v1 m2 v2 @@ -150,9 +152,9 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 = else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 - | _, GRef_ (_, _, B.Abbr v2) -> + | _, GRef_ (_, _, Y.Abbr v2) -> whd (aux m1 r1) c m2 v2 - | GRef_ (_, _, B.Abbr v1), _ -> + | GRef_ (_, _, Y.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) -> let l = B.new_location () in diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index da808cd45..1bc6fb225 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -13,6 +13,7 @@ module U = NUri module C = Cps module S = Share module L = Log +module Y = Entity module H = Hierarchy module B = Bag module O = BagOutput @@ -64,13 +65,11 @@ let rec b_type_of f ~si g c x = B.get f c i | B.GRef uri -> let f = function - | _, _, B.Abst w -> f x w - | _, _, B.Abbr (B.Cast (w, v)) -> f x w - | _, _, B.Abbr _ -> assert false - | _, _, B.Void -> - error1 "reference to excluded entry" c x + | _, _, Y.Abst w -> f x w + | _, _, Y.Abbr (B.Cast (w, v)) -> f x w + | _, _, Y.Abbr _ -> assert false in - E.get_entry f uri + E.get_entity f uri | B.Bind (l, id, B.Abbr v, t) -> let f xv xt tt = f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt) diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index ff5478d9f..08a1750c4 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -9,7 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module U = NUri module L = Log +module Y = Entity module B = Bag module E = BagEnvironment module T = BagType @@ -18,15 +20,9 @@ module T = BagType (* to share *) let type_check f ?(si=false) g = function - | None -> f None None - | Some (a, uri, B.Abst t) -> - let f tt entry = f (Some tt) (Some entry) in - let f xt tt = E.set_entry (f tt) (a, uri, B.Abst xt) in - L.loc := a; T.type_of f ~si g B.empty_lenv t - | Some (a, uri, B.Abbr t) -> - let f tt entry = f (Some tt) (Some entry) in - let f xt tt = E.set_entry (f tt) (a, uri, B.Abbr xt) in - L.loc := a; T.type_of f ~si g B.empty_lenv t - | Some (a, uri, B.Void) -> - let f entry = f None (Some entry) in - L.loc := a; E.set_entry f (a, uri, B.Void) + | a, uri, Y.Abst t -> + let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in + L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t + | a, uri, Y.Abbr t -> + let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in + L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli index 9aa4ec575..1d25e3da7 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli @@ -10,5 +10,5 @@ V_______________________________________________________________ *) val type_check: - (Bag.term option -> Bag.entity -> 'a) -> ?si:bool -> + (Bag.term -> Bag.entity -> 'a) -> ?si:bool -> Hierarchy.graph -> Bag.entity -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index e3c586681..373f5342f 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -14,11 +14,7 @@ type uri = Entity.uri type id = Entity.id - -type attr = Name of bool * id (* real?, name *) - | Apix of int (* additional position index *) - -type attrs = attr list +type attrs = Entity.attrs type bind = Void of attrs (* attrs *) | Abst of attrs * term (* attrs, type *) @@ -31,9 +27,7 @@ and term = Sort of attrs * int (* attrs, hierarchy index *) | Appl of attrs * term * term (* attrs, argument, function *) | Bind of bind * term (* binder, scope *) -type entry = bind Entity.entry (* age, uri, binder *) - -type entity = bind Entity.entity +type entity = term Entity.entity (* attrs, uri, binder *) type lenv = Null (* Cons: tail, relative local environment, binder *) @@ -85,13 +79,3 @@ let rec fold_left f map x = function | Cons (tl, _, b) -> let f x = fold_left f map x tl in map f x b - -let rec name err f = function - | [] -> err () - | Name (r, n) :: _ -> f n r - | _ :: tl -> name err f tl - -let rec apix err f = function - | [] -> err () - | Apix i :: _ -> f i - | _ :: tl -> apix err f tl diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml index 1017092d7..5a4cf3cb6 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -11,20 +11,24 @@ module U = NUri module H = U.UriHash +module Y = Entity module B = Brg let hsize = 7000 let env = H.create hsize -let age = ref 1 (* Internal functions *******************************************************) +let get_age = + let age = ref 0 in + fun () -> incr age; !age + (* Interface functions ******************************************************) -let set_entry f entry = - let _, uri, b = entry in - let entry = !age, uri, b in - incr age; H.add env uri entry; f entry +let set_entity f (a, uri, b) = + let age = get_age () in + let entity = (Y.Apix age :: a), uri, b in + H.add env uri entity; f entity -let get_entry err f uri = +let get_entity err f uri = try f (H.find env uri) with Not_found -> err () diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli index 96d6522d9..5f5d86bf3 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val set_entry: (Brg.entry -> 'a) -> Brg.entry -> 'a +val set_entity: (Brg.entity -> 'a) -> Brg.entity -> 'a -val get_entry: (unit -> 'a) -> (Brg.entry -> 'a) -> Brg.uri -> 'a +val get_entity: (unit -> 'a) -> (Brg.entity -> 'a) -> Brg.uri -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 662a71988..7dfb2b937 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -14,6 +14,8 @@ module F = Format module C = Cps module U = NUri module L = Log +module Y = Entity +module X = Library module H = Hierarchy module O = Output module B = Brg @@ -88,24 +90,15 @@ and count_term f c e = function let f c = B.push (f c) e b in count_term_binder f c e b -let count_entry f c = function - | (_, u, B.Abst (_, w)) -> +let count_entity f c = function + | _, u, Y.Abst w -> let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris } in count_term f c B.empty_lenv w - | (_, _, B.Abbr (_, v)) -> + | _, _, Y.Abbr v -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty_lenv v - | (_, u, B.Void _) -> - let c = {c with - evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris - } in - f c - -let count_entity f c = function - | Some entry -> count_entry f c entry - | None -> f c let print_counters f c = let terms = @@ -143,7 +136,7 @@ let rec does_not_occur f n r = function let f n1 r1 = if n1 = n && r1 = r then f false else does_not_occur f n r c in - attrs_of_binder (B.name C.err f) b + attrs_of_binder (Y.name C.err f) b let rename f c a = let rec aux f c n r = @@ -154,10 +147,10 @@ let rename f c a = does_not_occur f n r c in let f n0 r0 = - let f n r = if n = n0 && r = r0 then f a else f (B.Name (r, n) :: a) in + let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in aux f c n0 r0 in - B.name C.err f a + Y.name C.err f a let rename_bind f c = function | B.Abst (a, w) -> let f a = f (B.abst a w) in rename f c a @@ -166,12 +159,12 @@ let rename_bind f c = function (* lenv/term pretty printing ************************************************) -let id frm a = +let name frm a = let f n = function | true -> F.fprintf frm "%s" n | false -> F.fprintf frm "^%s" n in - B.name C.err f a + Y.name C.err f a let rec pp_term c frm = function | B.Sort (_, h) -> @@ -183,7 +176,7 @@ let rec pp_term c frm = function let f _ = function | B.Abst (a, _) | B.Abbr (a, _) - | B.Void a -> F.fprintf frm "@[%a@]" id a + | B.Void a -> F.fprintf frm "@[%a@]" name a in if !O.indexes then err () else B.get err f c i | B.GRef (_, s) -> @@ -194,31 +187,31 @@ let rec pp_term c frm = function F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t | B.Bind (B.Abst (a, w), t) -> let f a cc = - F.fprintf frm "@[[%a:%a].%a@]" id a (pp_term c) w (pp_term cc) t + F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t in let f a = B.push (f a) c (B.abst a w) in rename f c a | B.Bind (B.Abbr (a, v), t) -> let f a cc = - F.fprintf frm "@[[%a=%a].%a@]" id a (pp_term c) v (pp_term cc) t + F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t in let f a = B.push (f a) c (B.abbr a v) in rename f c a | B.Bind (B.Void a, t) -> - let f a cc = F.fprintf frm "@[[%a].%a@]" id a (pp_term cc) t in + let f a cc = F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t in let f a = B.push (f a) c (B.Void a) in rename f c a let pp_lenv frm c = let pp_entry f c = function | B.Abst (a, w) -> - let f a = F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () in + let f a = F.fprintf frm "@,@[%a : %a@]" name a (pp_term c) w; f () in rename f c a | B.Abbr (a, v) -> - let f a = F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f () in + let f a = F.fprintf frm "@,@[%a = %a@]" name a (pp_term c) v; f () in rename f c a | B.Void a -> - let f a = F.fprintf frm "@,%a" id a; f () in + let f a = F.fprintf frm "@,%a" name a; f () in rename f c a in B.rev_iter C.start pp_entry c @@ -229,36 +222,29 @@ let specs = { (* term xml printing ********************************************************) -let id frm a = - let f s = function - | true -> F.fprintf frm " name=%S" s - | false -> F.fprintf frm " name=%S" ("^" ^ s) - in - B.name C.start f a - let rec exp_term c frm = function | B.Sort (a, l) -> let a = let err _ = a in - let f s = B.Name (true, s) :: a in + let f s = Y.Name (s, true) :: a in H.get_sort err f l in - F.fprintf frm "" (string_of_int l) id a + F.fprintf frm "" (string_of_int l) X.old_name a | B.LRef (a, i) -> let a = let err _ = a in - let f n r = B.Name (r, n) :: a in - let f _ b = attrs_of_binder (B.name err f) b in + let f n r = Y.Name (n, r) :: a in + let f _ b = attrs_of_binder (Y.name err f) b in B.get err f c i in - F.fprintf frm "" (string_of_int i) id a + F.fprintf frm "" (string_of_int i) X.old_name a | B.GRef (a, u) -> - let a = B.Name (true, U.name_of_uri u) :: a in - F.fprintf frm "" (U.string_of_uri u) id a + let a = Y.Name (U.name_of_uri u, true) :: a in + F.fprintf frm "" (U.string_of_uri u) X.old_name a | B.Cast (a, w, t) -> - F.fprintf frm "%a@,%a" id a (exp_boxed c) w (exp_term c) t + F.fprintf frm "%a@,%a" X.old_name a (exp_boxed c) w (exp_term c) t | B.Appl (a, v, t) -> - F.fprintf frm "%a@,%a" id a (exp_boxed c) v (exp_term c) t + F.fprintf frm "%a@,%a" X.old_name a (exp_boxed c) v (exp_term c) t | B.Bind (b, t) -> let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in let f b = B.push (f b) c b in @@ -269,25 +255,11 @@ and exp_boxed c frm t = and exp_bind c frm = function | B.Abst (a, w) -> - F.fprintf frm "%a" id a (exp_boxed c) w + F.fprintf frm "%a" X.old_name a (exp_boxed c) w | B.Abbr (a, v) -> - F.fprintf frm "%a" id a (exp_boxed c) v + F.fprintf frm "%a" X.old_name a (exp_boxed c) v | B.Void a -> - F.fprintf frm "" id a - -let exp_entry c frm = function - | _, u, B.Abst (a, w) -> - let str = U.string_of_uri u in - let a = B.Name (true, U.name_of_uri u) :: a in - F.fprintf frm "%a" str id a (exp_boxed c) w - | _, u, B.Abbr (a, v) -> - let str = U.string_of_uri u in - let a = B.Name (true, U.name_of_uri u) :: a in - F.fprintf frm "%a" str id a (exp_boxed c) v - | _, u, B.Void a -> - let str = U.string_of_uri u in - let a = B.Name (true, U.name_of_uri u) :: a in - F.fprintf frm "" str id a + F.fprintf frm "" X.old_name a -let export_entry frm entry = - F.fprintf frm "@,@[ %a@]@," (exp_entry B.empty_lenv) entry +let export_term frm t = + F.fprintf frm "%a" (exp_boxed B.empty_lenv) t diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 0af895dd4..69700febd 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -19,4 +19,4 @@ val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.lenv, Brg.term) Log.specs -val export_entry: Format.formatter -> Brg.bind Entity.entry -> unit +val export_term: Format.formatter -> Brg.term -> unit diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index e6ea50142..12e637659 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -13,6 +13,7 @@ module U = NUri module C = Cps module S = Share module L = Log +module Y = Entity module P = Output module B = Brg module O = BrgOutput @@ -69,16 +70,18 @@ let rec step f ?(delta=false) ?(rt=false) m x = | B.Sort _ -> f m None x | B.GRef (_, uri) -> let f = function - | _, _, B.Abbr (_, v) when delta -> + | _, _, Y.Abbr v when delta -> P.add ~gdelta:1 (); step f ~delta ~rt m v - | _, _, B.Abst (_, w) when rt -> + | _, _, Y.Abst w when rt -> P.add ~grt:1 (); step f ~delta ~rt m w - | _, _, B.Void _ -> - assert false - | e, _, b -> - f m (Some (e, b)) x + | a, _, Y.Abbr v -> + let f e = f m (Some (e, B.Abbr (a, v))) x in + Y.apix C.err f a + | a, _, Y.Abst w -> + let f e = f m (Some (e, B.Abst (a, w))) x in + Y.apix C.err f a in - E.get_entry C.err f uri + E.get_entity C.err f uri | B.LRef (_, i) -> let f c = function | B.Abbr (_, v) -> @@ -91,7 +94,7 @@ let rec step f ?(delta=false) ?(rt=false) m x = assert false | B.Abst (a, _) as b -> let f e = f {m with c = c} (Some (e, b)) x in - B.apix C.err f a + Y.apix C.err f a in get C.err f m i | B.Cast (_, _, t) -> @@ -115,7 +118,7 @@ let rec step f ?(delta=false) ?(rt=false) m x = let push f m b = assert (m.s = []); let b, i = match b with - | B.Abst (a, w) -> B.abst (B.Apix m.i :: a) w, succ m.i + | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i | b -> b, m.i in let f c = f {m with c = c; i = i} in diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index cf997e473..a35a9c32a 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -14,6 +14,7 @@ module C = Cps module A = Share module L = Log module H = Hierarchy +module Y = Entity module B = Brg module O = BrgOutput module E = BrgEnvironment @@ -82,14 +83,12 @@ let rec b_type_of err f ~si g m x = R.get err f m i | B.GRef (_, uri) -> let f = function - | _, _, B.Abst (_, w) -> f x w - | _, _, B.Abbr (_, B.Cast (_, w, _)) -> f x w - | _, _, B.Abbr _ -> assert false - | _, _, B.Void _ -> - error1 err "reference to excluded entry" m x + | _, _, Y.Abst w -> f x w + | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w + | _, _, Y.Abbr _ -> assert false in let err _ = error1 err "reference to unknown entry" m x in - E.get_entry err f uri + E.get_entity err f uri | B.Bind (B.Abbr (a, v), t) -> let f xv xt tt = f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 20b9a5cf1..77098b84e 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -9,7 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module U = NUri module L = Log +module Y = Entity module B = Brg module E = BrgEnvironment module R = BrgReduction @@ -19,15 +21,9 @@ module T = BrgType (* to share *) let type_check err f ?(si=false) g = function - | None -> f None None - | Some (e, uri, B.Abst (a, t)) -> - let f tt entry = f (Some tt) (Some entry) in - let f xt tt = E.set_entry (f tt) (e, uri, B.abst a xt) in - L.loc := e; T.type_of err f ~si g R.empty_kam t - | Some (e, uri, B.Abbr (a, t)) -> - let f tt entry = f (Some tt) (Some entry) in - let f xt tt = E.set_entry (f tt) (e, uri, B.abbr a xt) in - L.loc := e; T.type_of err f ~si g R.empty_kam t - | Some (e, uri, (B.Void _ as b)) -> - let f entry = f None (Some entry) in - L.loc := e; E.set_entry f (e, uri, b) + | a, uri, Y.Abst t -> + let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in + L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t + | a, uri, Y.Abbr t -> + let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in + L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index bab64303e..9c0568f10 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -10,5 +10,5 @@ V_______________________________________________________________ *) val type_check: - (BrgType.message -> 'a) -> (Brg.term option -> Brg.entity -> 'a) -> + (BrgType.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> ?si:bool -> Hierarchy.graph -> Brg.entity -> 'a diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index cd780601a..292b1e921 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -12,8 +12,52 @@ type uri = NUri.uri type id = Aut.id -type 'bind entry = int * uri * 'bind (* age, uri, binder *) +type attr = Name of id * bool (* name, real? *) + | Apix of int (* additional position index *) + | Mark of int (* node marker *) + | Priv (* private global definition *) -type 'bind entity = 'bind entry option +type attrs = attr list (* attributes *) + +type 'term bind = Abst of 'term (* declaration: domain *) + | Abbr of 'term (* definition: body *) + +type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) type 'a uri_generator = (string -> 'a) -> string -> 'a + +(* helpers ******************************************************************) + +let rec name err f = function + | Name (n, r) :: _ -> f n r + | _ :: tl -> name err f tl + | [] -> err () + +let rec apix err f = function + | Apix i :: _ -> f i + | _ :: tl -> apix err f tl + | [] -> err () + +let rec mark err f = function + | Mark i :: _ -> f i + | _ :: tl -> mark err f tl + | [] -> err () + +let rec priv err f = function + | Priv :: _ -> f () + | _ :: tl -> priv err f tl + | [] -> err () + +let resolve err f name a = + let rec aux i = function + | Name (n, true) :: _ when n = name -> f i + | _ :: tl -> aux (succ i) tl + | [] -> err i + in + aux 0 a + +let xlate f xlate_term = function + | a, uri, Abst t -> + let f t = f (a, uri, Abst t) in xlate_term f t + | a, uri, Abbr t -> + let f t = f (a, uri, Abbr t) in xlate_term f t diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 1238c2739..4951e8c60 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -9,11 +9,12 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Filename +module F = Format +module N = Filename module U = NUri +module C = Cps module H = Hierarchy - -type 'a out = (unit -> 'a) -> string -> 'a +module Y = Entity (* internal functions *******************************************************) @@ -21,55 +22,156 @@ let base = "xml" let obj_ext = ".xml" +let root = "ENTITY" + let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd" let path_of_uri uri = - F.concat base (Str.string_after (U.string_of_uri uri) 3) + N.concat base (Str.string_after (U.string_of_uri uri) 3) let pp_head frm = - Format.fprintf frm "@,@," "1.0" "UTF-8" + F.fprintf frm "@,@," "1.0" "UTF-8" let pp_doctype frm = - Format.fprintf frm "@,@," system + F.fprintf frm "@,@," system -let open_entry si g frm = +let open_entity si g frm = let opts = if si then "si" else "" in let f shp = - Format.fprintf frm "" shp opts + F.fprintf frm "" shp opts in H.string_of_graph f g -let close_entry frm = - Format.fprintf frm "" +let close_entity frm = + F.fprintf frm "" + +let name frm a = + let f s = function + | true -> F.fprintf frm " name=%S" s + | false -> F.fprintf frm " name=%S" ("^" ^ s) + in + Y.name C.start f a + +let pp_entity pp_term frm = function + | a, u, Y.Abst w -> + let str = U.string_of_uri u in + let a = Y.Name (U.name_of_uri u, true) :: a in + F.fprintf frm "%a" str name a pp_term w + | a, u, Y.Abbr v -> + let str = U.string_of_uri u in + let a = Y.Name (U.name_of_uri u, true) :: a in + F.fprintf frm "%a" str name a pp_term v + +let pp_boxed pp_term frm entity = + F.fprintf frm "@,@[ %a@]@," (pp_entity pp_term) entity (* interface functions ******************************************************) -let old_export_entity export_entry si g = function - | Some entry -> - let _, uri, bind = entry in - let path = path_of_uri uri in - let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in - let och = open_out (path ^ obj_ext) in - let frm = Format.formatter_of_out_channel och in - Format.pp_set_margin frm max_int; - Format.fprintf frm "@[%t%t%t%a%t@]@." - pp_head pp_doctype (open_entry si g) export_entry entry close_entry; - close_out och - | None -> () +let old_export_entity pp_term si g entity = + let _, uri, _ = entity in + let path = path_of_uri uri in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in + let och = open_out (path ^ obj_ext) in + let frm = F.formatter_of_out_channel och in + F.pp_set_margin frm max_int; + F.fprintf frm "@[%t%t%t%a%t@]@." + pp_head pp_doctype + (open_entity si g) (pp_boxed pp_term) entity close_entity; + close_out och + +let old_name = name (****************************************************************************) -(* -let export_entity export_entry si g = function - | Some entry -> - let _, uri, bind = entry in - let path = path_of_uri root uri in - let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in - let och = open_out (path ^ obj_ext) in - let out f s = output_string och s; f () in - let f () = close_out och in - - Format.fprintf frm "@[%t%t%t%a%t@]@." - pp_head pp_doctype (open_entry si g) export_entry entry close_entry; - close_out och - | None -> () -*) + +type och = string -> unit + +type attr = string * string + +type 'a pp = (och -> int -> 'a) -> och -> int -> 'a + +let attribute out (name, contents) = + if contents <> "" then begin + out " "; out name; out "=\""; out contents; out "\"" + end + +let xml out version encoding = + out "\n\n" + +let doctype out root system = + out "\n\n" + +let tag tag attrs ?contents f out indent = + let spc = String.make indent ' ' in + out spc; out "<"; out "tag"; List.iter (attribute out) attrs; + match contents with + | None -> out "/>\n"; f out indent + | Some cont -> + let f _ _ = out spc; out "\n"; f out indent in + cont f out (indent + 3) + +let sort = "Sort" + +let lref = "LRef" + +let gref = "GRef" + +let cast = "Cast" + +let appl = "Appl" + +let proj = "Proj" + +let abst = "Abst" + +let abbr = "Abbr" + +let void = "Void" + +let position i = + "position", string_of_int i + +let offset j = + let contents = if j > 0 then string_of_int j else "" in + "offset", contents + +let uri u = + "uri", U.string_of_uri u + +let arity n = + let contents = if n > 1 then string_of_int n else "" in + "arity", contents + +let name a = + let err () = "name", "" in + let f s = function + | true -> "name", s + | false -> "name", ("^" ^ s) + in + Y.name err f a + +let mark a = + let err () = "mark", "" in + let f i = "mark", string_of_int i in + Y.mark err f a + +let export_entity f pp_term si g (a, uri, b) = + let path = path_of_uri uri in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in + let och = open_out (path ^ obj_ext) in + let out = output_string och in + let f _ _ = close_out och; f () in + xml out "1.0" "UTF-8"; doctype out root system; + let str = U.string_of_uri uri in + let a = Y.Name (U.name_of_uri uri, true) :: a in + let attrs = ["uri", str; name a] in + let contents = match b with + | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) + | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) + in + let opts = if si then "si" else "" in + let shp = H.string_of_graph C.start g in + let attrs = ["hierarchy", shp; "options", opts] in + tag root attrs ~contents f out 0; diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index bda10346d..95d5ba9b1 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -9,12 +9,50 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type 'a out = (unit -> 'a) -> string -> 'a -(* +type och = string -> unit + +type attr = string * string + +type 'a pp = (och -> int -> 'a) -> och -> int -> 'a + val export_entity: - ('a och -> string -> 'bind Entity.entry -> 'a) -> - string -> bool -> Hierarchy.graph -> 'bind Entity.entity -> 'a -*) + (unit ->'a) -> ('term -> 'a pp) -> + bool -> Hierarchy.graph -> 'term Entity.entity -> 'a + +val tag: string -> attr list -> ?contents:'a pp -> 'a pp + +val sort: string + +val lref: string + +val gref: string + +val cast: string + +val appl: string + +val proj: string + +val abst: string + +val abbr: string + +val void: string + +val position: int -> attr + +val offset: int -> attr + +val uri: Entity.uri -> attr + +val arity: int -> attr + +val name: Entity.attrs -> attr + +val mark: Entity.attrs -> attr + val old_export_entity: - (Format.formatter -> 'bind Entity.entry -> unit) -> - bool -> Hierarchy.graph -> 'bind Entity.entity -> unit + (Format.formatter -> 'term -> unit) -> + bool -> Hierarchy.graph -> 'term Entity.entity -> unit + +val old_name: Format.formatter -> Entity.attrs -> unit diff --git a/helm/software/lambda-delta/dual_rg/Make b/helm/software/lambda-delta/dual_rg/Make index 5020307c3..7d70990f5 100644 --- a/helm/software/lambda-delta/dual_rg/Make +++ b/helm/software/lambda-delta/dual_rg/Make @@ -1 +1 @@ -drg drgAut +drg drgOutput drgAut diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index e598a5986..a30082046 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -14,28 +14,24 @@ type uri = Entity.uri type id = Entity.id +type attrs = Entity.attrs -type attr = Name of id * bool (* name, real? *) - | Priv (* private global definition *) - -type attrs = attr list (* attributes *) - -type bind = Abst of attrs * term (* attrs, domain *) - | Abbr of attrs * term (* attrs, body *) - | Void of attrs (* attrs *) +type bind = Abst of term list (* domains *) + | Abbr of term list (* bodies *) + | Void of int (* number of exclusions *) and term = Sort of attrs * int (* attrs, hierarchy index *) - | LRef of attrs * int (* attrs, position index *) + | LRef of attrs * int * int (* attrs, position indexes *) | GRef of attrs * uri (* attrs, reference *) | Cast of attrs * term * term (* attrs, domain, element *) | Appl of attrs * term list * term (* attrs, arguments, function *) - | Bind of lenv * term (* closure, scope *) - -and lenv = bind list (* local environment *) + | Proj of attrs * lenv * term (* attrs, closure, member *) + | Bind of attrs * bind * term (* attrs, binder, scope *) -type entry = bind Entity.entry (* age, uri, binder *) +and lenv = Null + | Cons of lenv * attrs * bind (* closure, attrs, binder *) -type entity = bind Entity.entity +type entity = term Entity.entity (* helpers ******************************************************************) @@ -43,22 +39,16 @@ let mk_uri root f s = let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in f str -let rec name_of err f = function - | Name (n, r) :: _ -> f n r - | _ :: tl -> name_of err f tl - | [] -> err () +let empty_lenv = Null -let name_of_binder err f = function - | Abst (a, _) -> name_of err f a - | Abbr (a, _) -> name_of err f a - | Void a -> name_of err f a +let push f lenv a b = f (Cons (lenv, a, b)) let resolve_lref err f id lenv = - let rec aux f i = function - | [] -> err () - | b :: tl -> - let err () = aux f (succ i) tl in - let f name _ = if name = id then f i else err () in - name_of_binder err f b + let rec aux f i k = function + | Null -> err () + | Cons (tl, a, _) -> + let err kk = aux f (succ i) (k + kk) tl in + let f j = f i j k in + Entity.resolve err f id a in - aux f 0 lenv + aux f 0 0 lenv diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index 3b371afd7..b6d8b166c 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -12,42 +12,50 @@ module U = NUri module H = U.UriHash module C = Cps -module E = Entity +module Y = Entity module A = Aut module D = Drg (* qualified identifier: uri, name, qualifiers *) type qid = D.uri * D.id * D.id list -type environment = D.lenv H.t +type context = Y.attrs * D.term list + +type environment = context H.t type context_node = qid option (* context node: None = root *) -type 'b status = { +type 'a status = { henv: environment; (* optimized global environment *) path: D.id list; (* current section path *) hcnt: environment; (* optimized context *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - mk_uri:'b E.uri_generator (* uri generator *) + mk_uri:'a Y.uri_generator (* uri generator *) } type resolver = Local of int - | Global of D.lenv + | Global of context -let hsize = 7000 (* hash tables initial size *) +let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) (* Internal functions *******************************************************) -let initial_status size mk_uri = { +let initial_status mk_uri = { path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri; - henv = H.create size; hcnt = H.create size + henv = H.create henv_size; hcnt = H.create hcnt_size } -let mk_lref f i = f (D.LRef ([], i)) +let empty_cnt = [], [] + +let add_abst (a, ws) id w = + Y.Name (id, true) :: a, w :: ws + +let lenv_of_cnt (a, ws) = + D.push C.start D.empty_lenv a (D.Abst ws) -let mk_abst id w = D.Abst ([D.Name (id, true)], w) +let mk_lref f i j k = f (D.LRef ([Y.Apix k], i, j)) let id_of_name (id, _, _) = id @@ -88,7 +96,7 @@ let resolve_gref_relaxed f st qid = resolve_gref err f st qid let get_cnt err f st = function - | None -> f [] + | None -> f empty_cnt | Some qid as node -> try let cnt = H.find st.hcnt (uri_of_qid qid) in f cnt with Not_found -> err node @@ -107,22 +115,23 @@ let rec xlate_term f st lenv = function xlate_term f st lenv v | A.Abst (name, w, t) -> let f ww = - let b = mk_abst name ww in - let f tt = f (D.Bind ([b], tt)) in - xlate_term f st (b :: lenv) t + let a, b = [Y.Name (name, true)], (D.Abst [ww]) in + let f tt = f (D.Bind (a, b, tt)) in + let f lenv = xlate_term f st lenv t in + D.push f lenv a b in xlate_term f st lenv w | A.GRef (name, args) -> - let g qid cnt = + let g qid (a, _) = let map1 f = xlate_term f st lenv in - let map2 f b = - let f id _ = D.resolve_lref Cps.err (mk_lref f) id lenv in - D.name_of_binder C.err f b + let map2 f = function + | Y.Name (id, _) -> D.resolve_lref Cps.err (mk_lref f) id lenv + | _ -> assert false in let f tail = let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in - let f cnt = C.list_rev_map_append f map2 cnt ~tail in - C.list_sub_strict f cnt args + let f a = C.list_rev_map_append f map2 a ~tail in + C.list_sub_strict f a args in C.list_map f map1 args in @@ -130,58 +139,65 @@ let rec xlate_term f st lenv = function let err () = complete_qid g st name in D.resolve_lref err (mk_lref f) (id_of_name name) lenv -let xlate_entity f st = function +let xlate_entity err f st = function | A.Section (Some (_, name)) -> - f {st with path = name :: st.path; nodes = st.node :: st.nodes} None + 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 -> - f {st with path = ptl; node = nhd; nodes = ntl} None + err {st with path = ptl; node = nhd; nodes = ntl} | _ -> assert false end | A.Context None -> - f {st with node = None} None + err {st with node = None} | A.Context (Some name) -> - let f name = f {st with node = Some name} None in + 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 ww = - H.add st.hcnt (uri_of_qid qid) (mk_abst name ww :: cnt); - f {st with node = Some qid} None + H.add st.hcnt (uri_of_qid qid) (add_abst cnt name ww); + err {st with node = Some qid} in - xlate_term f st cnt w + 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 f qid = + let f cnt = + let a, ws = cnt in + let lenv = lenv_of_cnt cnt in + let f qid = let f ww = - let b = D.Abst ([], D.Bind (cnt, ww)) in - let entry = st.line, uri_of_qid qid, b in - H.add st.henv (uri_of_qid qid) cnt; - f {st with line = succ st.line} (Some entry) + H.add st.henv (uri_of_qid qid) cnt; + let b = Y.Abst (D.Bind (a, D.Abst ws, ww)) in + let entity = [Y.Mark st.line], uri_of_qid qid, b in + f {st with line = succ st.line} entity in - xlate_term f st cnt w + 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 ww vv = - let a = if trans then [] else [D.Priv] in - let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in - let entry = st.line, uri_of_qid qid, b in H.add st.henv (uri_of_qid qid) cnt; - f {st with line = succ st.line} (Some entry) + let b = Y.Abbr (D.Bind (a, D.Abst ws, D.Cast ([], ww, vv))) in + let a = + if trans then [Y.Mark st.line] else [Y.Mark st.line; Y.Priv] + in + let entity = a, uri_of_qid qid, b in + f {st with line = succ st.line} entity in - let f ww = xlate_term (f ww) st cnt v in - xlate_term f st cnt w + let f ww = xlate_term (f ww) st lenv v in + xlate_term f st lenv w in complete_qid f st (name, true, []) in @@ -190,6 +206,6 @@ let xlate_entity f st = function (* Interface functions ******************************************************) let initial_status mk_uri = - initial_status hsize mk_uri + initial_status mk_uri let drg_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/dual_rg/drgAut.mli b/helm/software/lambda-delta/dual_rg/drgAut.mli index ea4e4b021..1133f20bd 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.mli +++ b/helm/software/lambda-delta/dual_rg/drgAut.mli @@ -13,5 +13,5 @@ type 'a status val initial_status: 'a Entity.uri_generator -> 'a status -val drg_of_aut: ('a status -> Drg.entity -> 'a) -> +val drg_of_aut: ('a status -> 'a) -> ('a status -> Drg.entity -> 'a) -> 'a status -> Aut.entity -> 'a diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml new file mode 100644 index 000000000..f6782d556 --- /dev/null +++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml @@ -0,0 +1,56 @@ +(* + ||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 X = Library +module D = Drg + +let rec list_iter map l f = match l with + | [] -> f + | hd :: tl -> map hd (list_iter map tl f) + +let rec lenv_iter map l f = match l with + | D.Null -> f + | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b f) + +let rec exp_term t f = match t with + | D.Sort (a, h) -> + let attrs = [X.position h; X.name a] in + X.tag X.sort attrs f + | D.LRef (a, i, j) -> + let attrs = [X.position i; X.offset j; X.name a] in + X.tag X.lref attrs f + | D.GRef (a, n) -> + let attrs = [X.uri n; X.name a] in + X.tag X.gref attrs f + | D.Cast (a, u, t) -> + let attrs = [] in + X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u) + | D.Appl (a, vs, t) -> + let attrs = [X.arity (List.length vs)] in + X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs) + | D.Proj (a, lenv, t) -> + let attrs = [] in + X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv) + | D.Bind (a, b, t) -> + exp_lenv a b (exp_term t f) + +and exp_lenv a b f = match b with + | D.Abst ws -> + let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in + X.tag X.abst attrs f ~contents:(list_iter exp_term ws) + | D.Abbr vs -> + let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in + X.tag X.abbr attrs f ~contents:(list_iter exp_term vs) + | D.Void n -> + let attrs = [X.name a; X.mark a; X.arity n] in + X.tag X.void attrs f + +let export_term = exp_term diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.mli b/helm/software/lambda-delta/dual_rg/drgOutput.mli new file mode 100644 index 000000000..a1b9e6925 --- /dev/null +++ b/helm/software/lambda-delta/dual_rg/drgOutput.mli @@ -0,0 +1,12 @@ +(* + ||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 export_term: Drg.term -> 'a Library.pp diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index e50fa254d..3b93ccedb 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -28,7 +28,7 @@ type ('a, 'b) specs = { let level = ref 0 -let loc = ref 0 +let loc = ref "unknown location" (* Internal functions *******************************************************) @@ -42,7 +42,7 @@ let pp_items frm st l items = | LEnv c -> F.fprintf frm "%a" st.pp_lenv c | Warn s -> F.fprintf frm "@,%s" s | String s -> F.fprintf frm "%s " s - | Loc -> F.fprintf frm " (line %u)" !loc + | Loc -> F.fprintf frm " <%s>" !loc in let iter map frm l = List.iter (map frm) l in if !level >= l then F.fprintf frm "%a" (iter pp_item) items diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 3e093575a..956f91fd8 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -22,7 +22,7 @@ type ('a, 'b) specs = { pp_lenv: Format.formatter -> 'a -> unit } -val loc: int ref +val loc: string ref val level: int ref diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index 563e19b99..553977251 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -10,7 +10,6 @@ V_______________________________________________________________ *) type uri = Entity.uri - type id = Entity.id type term = Sort of bool (* sorts: true = TYPE, false = PROP *) @@ -21,7 +20,6 @@ type term = Sort of bool (* sorts: true = TYPE, false = PROP *) type pars = (id * term) list (* parameter declarations: name, type *) -(* entry: line number, parameters, name, domain, (transparent?, body) *) -type entry = int * pars * uri * term * (bool * term) option +type entry = pars * term * term option (* parameters, domain, body *) -type entity = entry option +type entity = entry Entity.entity diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index db18ade47..75aaa71e6 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -11,11 +11,13 @@ module U = NUri module H = U.UriHash +module C = Cps +module Y = Entity module M = Meta module A = Aut (* qualified identifier: uri, name, qualifiers *) -type qid = U.uri * M.id * M.id list +type qid = M.uri * M.id * M.id list type environment = M.pars H.t @@ -34,13 +36,13 @@ type status = { type resolver = Local of int | Global of M.pars -let hsize = 7000 (* hash tables initial size *) +let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) (* Internal functions *******************************************************) -let initial_status size cover = { +let initial_status cover = { path = []; node = None; nodes = []; line = 1; cover = cover; - henv = H.create size; hcnt = H.create size + henv = H.create henv_size; hcnt = H.create hcnt_size } let id_of_name (id, _, _) = id @@ -55,7 +57,7 @@ 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 = Cps.list_rev_append f path ~tail: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) @@ -66,10 +68,10 @@ let complete_qid f st (id, is_local, qs) = let relax_qid f st (_, id, path) = let f path = f (mk_qid st id path) in let f = function - | _ :: tl -> Cps.list_rev f tl + | _ :: tl -> C.list_rev f tl | [] -> assert false in - Cps.list_rev f path + C.list_rev f path let relax_opt_qid f st = function | None -> f None @@ -133,10 +135,10 @@ let rec xlate_term f st lenv = function 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 = Cps.list_rev_map_append f map2 defs ~tail in - Cps.list_sub_strict f defs args + let f defs = C.list_rev_map_append f map2 defs ~tail in + C.list_sub_strict f defs args in - Cps.list_map f map1 args + C.list_map f map1 args in let g qid = resolve_gref_relaxed g st qid in let f = function @@ -145,26 +147,26 @@ let rec xlate_term f st lenv = function in resolve_lref f st l lenv (id_of_name name) -let xlate_entity f st = function +let xlate_entity err f st = function | A.Section (Some (_, name)) -> - f {st with path = name :: st.path; nodes = st.node :: st.nodes} None + 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 -> - f {st with path = ptl; node = nhd; nodes = ntl} None + err {st with path = ptl; node = nhd; nodes = ntl} | _ -> assert false end | A.Context None -> - f {st with node = None} None + err {st with node = None} | A.Context (Some name) -> - let f name = f {st with node = Some name} None in + 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 = H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars); - f {st with node = Some qid} None + err {st with node = Some qid} in xlate_term f st pars w in @@ -175,9 +177,11 @@ let xlate_entity f st = function let f pars = let f qid = let f ww = - let entry = (st.line, pars, uri_of_qid qid, ww, None) in H.add st.henv (uri_of_qid qid) pars; - f {st with line = succ st.line} (Some entry) + let a = [Y.Mark st.line] in + let entry = pars, ww, None in + let entity = a, uri_of_qid qid, Y.Abst entry in + f {st with line = succ st.line} entity in xlate_term f st pars w in @@ -188,9 +192,11 @@ let xlate_entity f st = function let f pars = let f qid = let f ww vv = - let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in H.add st.henv (uri_of_qid qid) pars; - f {st with line = succ st.line} (Some entry) + let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in + let entry = pars, ww, Some vv in + let entity = a, uri_of_qid qid, Y.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 @@ -202,6 +208,6 @@ let xlate_entity f st = function (* Interface functions ******************************************************) let initial_status ?(cover="") () = - initial_status hsize cover + initial_status cover let meta_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli index cfcb49d0b..977d5ed2f 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.mli +++ b/helm/software/lambda-delta/toplevel/metaAut.mli @@ -13,4 +13,6 @@ type status val initial_status: ?cover:string -> unit -> status -val meta_of_aut: (status -> Meta.entity -> 'a) -> status -> Aut.entity -> 'a +val meta_of_aut: + (status -> 'a) -> (status -> Meta.entity -> 'a) -> + status -> Aut.entity -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml index 67c938df0..991d7e8c2 100644 --- a/helm/software/lambda-delta/toplevel/metaBag.ml +++ b/helm/software/lambda-delta/toplevel/metaBag.ml @@ -52,21 +52,16 @@ let unwind_to_xlate_term f c t = let f t = C.list_fold_left f map t c in xlate_term c f t -let xlate_entry f = function - | e, pars, uri, u, None -> - let f u = f (e, uri, B.Abst u) in +let xlate_entry f = function + | pars, u, None -> let f c = unwind_to_xlate_term f c u in xlate_pars f pars - | e, pars, uri, u, Some (_, t) -> - let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in + | 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 - -let xlate_entity f = function - | None -> f None - | Some e -> let f e = f (Some e) in xlate_entry f e - + (* Interface functions ******************************************************) -let bag_of_meta = xlate_entity +let bag_of_meta = xlate_entry diff --git a/helm/software/lambda-delta/toplevel/metaBag.mli b/helm/software/lambda-delta/toplevel/metaBag.mli index b8e41be04..62ce68f4e 100644 --- a/helm/software/lambda-delta/toplevel/metaBag.mli +++ b/helm/software/lambda-delta/toplevel/metaBag.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val bag_of_meta: (Bag.entity -> 'a) -> Meta.entity -> 'a +val bag_of_meta: (Bag.term -> 'a) -> Meta.entry -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 2fb17262e..4ee25812e 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -10,6 +10,7 @@ V_______________________________________________________________ *) module C = Cps +module Y = Entity module B = Brg module M = Meta @@ -31,7 +32,7 @@ let rec xlate_term c f = function xlate_term c f v | M.Abst (id, w, t) -> let f w = - let a = [B.Name (true, id)] in + let a = [Y.Name (id, true)] in let f t = f (B.Bind (B.abst a w, t)) in let f c = xlate_term c f t in B.push f c (B.abst a w) @@ -40,7 +41,7 @@ let rec xlate_term c f = function let xlate_pars f pars = let map f (id, w) c = - let a = [B.Name (true, id)] in + let a = [Y.Name (id, true)] in let f w = B.push f c (B.abst a w) in xlate_term c f w in @@ -52,20 +53,15 @@ let unwind_to_xlate_term f c t = xlate_term c f t let xlate_entry f = function - | e, pars, uri, u, None -> - let f u = f (e, uri, B.abst [] u) in + | pars, u, None -> let f c = unwind_to_xlate_term f c u in xlate_pars f pars - | e, pars, uri, u, Some (_, t) -> - let f u t = f (e, uri, B.abbr [] (B.Cast ([], u, t))) in + | 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 -let xlate_entity f = function - | None -> f None - | Some e -> let f e = f (Some e) in xlate_entry f e - (* Interface functions ******************************************************) -let brg_of_meta = xlate_entity +let brg_of_meta = xlate_entry diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli index 6a4a7bd2b..4ce275fb8 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.mli +++ b/helm/software/lambda-delta/toplevel/metaBrg.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val brg_of_meta: (Brg.entity -> 'a) -> Meta.entity -> 'a +val brg_of_meta: (Brg.term -> 'a) -> Meta.entry -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 7f62c8abc..caf3cc960 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -12,7 +12,9 @@ module P = Printf module F = Format module U = NUri +module C = Cps module L = Log +module Y = Entity module M = Meta type counters = { @@ -62,25 +64,26 @@ let rec count_term f c = function let count_par f c (_, w) = count_term f c w -let count_entry f c = function - | _, pars, u, w, None -> +let count_xterm f c = function + | None -> f c + | Some v -> count_term f c v + +let count_entity f c = function + | _, u, Y.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 - | _, pars, _, w, Some (_, v) -> + | _, _, Y.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_term f c v 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 -let count_entity f c = function - | Some e -> count_entry f c e - | None -> f c - 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 @@ -107,9 +110,10 @@ let string_of_sort = function | true -> "Type" | false -> "Prop" -let string_of_transparent = function - | true -> "=" - | false -> "~" +let pp_transparent frm a = + let err () = F.fprintf frm "%s" "=" in + let f () = F.fprintf frm "%s" "~" in + Y.priv err f a let pp_list pp opend sep closed frm l = let rec aux frm = function @@ -137,19 +141,20 @@ and pp_term frm = function F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t let pp_par frm (id, w) = - F.fprintf frm "%s:%a" id pp_term w + F.fprintf frm "%s:%a" id pp_term w let pp_pars = pp_rev_list pp_par "[" "," "]" -let pp_body frm = function - | None -> () - | Some (trans, t) -> - F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t +let pp_body a frm = function + | None -> () + | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t -let pp_entry frm (l, pars, uri, u, body) = - F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" - l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u +let pp_entity frm = function + | a, uri, Y.Abst (pars, u, body) + | a, uri, Y.Abbr (pars, u, body) -> + F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" + (Y.mark C.err C.start a) (U.string_of_uri uri) + pp_pars pars (pp_body a) body pp_term u -let pp_entity f frm = function - | Some entry -> pp_entry frm entry; f () - | None -> f () +let pp_entity f frm entity = + pp_entity frm entity; f () diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 869b1386a..2509ffc84 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -16,13 +16,14 @@ module L = Log module T = Time module H = Hierarchy module O = Output +module Y = Entity +module X = Library module AP = AutProcess module AO = AutOutput module MA = MetaAut module MO = MetaOutput module ML = MetaLibrary module MBrg = MetaBrg -module G = Library module BrgO = BrgOutput module BrgR = BrgReduction module BrgU = BrgUntrusted @@ -80,25 +81,22 @@ let print_counters st = match !kernel with let kernel_of_meta f st entity = match !kernel with | Brg -> let f entity = f st (BrgEntity entity) in - MBrg.brg_of_meta f entity + Y.xlate f MBrg.brg_of_meta entity | Bag -> let f entity = f st (BagEntity entity) in - MBag.bag_of_meta f entity + Y.xlate f MBag.bag_of_meta entity let count_entity st = function | BrgEntity entity -> {st with brgc = count BrgO.count_entity st.brgc entity} | BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity} let export_entity si g = function - | BrgEntity entity -> G.old_export_entity BrgO.export_entry si g entity - | BagEntity _ -> () + | BrgEntity entity -> X.old_export_entity BrgO.export_term si g entity + | BagEntity _ -> () let type_check f st si g k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in - let f _ = function - | None -> f st None - | Some (i, u, _) -> f st (Some (i, u)) - in + let f _ (a, u, _) = f st a u in match k with | BrgEntity entity -> BrgU.type_check brg_err f ~si g entity | BagEntity entity -> BagU.type_check f ~si g entity @@ -152,15 +150,17 @@ try close_in ich; if !L.level > 0 then T.utime_stamp "parsed"; let rec aux st = function - | [] -> st + | [] -> st | entity :: tl -> (* stage 3 *) - let f st = function - | None -> st - | Some (i, u) -> - if !progress then - L.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); - st + let f st a u = + if !progress then + let s = U.string_of_uri u in + let err () = L.warn (P.sprintf "%s" s); st in + let f i = L.warn (P.sprintf "[%u] %s" i s); st in + Y.mark err f a + else + st in (* stage 2 *) let f st entity = @@ -181,9 +181,12 @@ try in (* stage 0 *) let st = {st with ac = count AO.count_entity st.ac entity} in + let err st mst = {st with mst = mst} in let f st entity = let st = - if !stage > 0 then MA.meta_of_aut (f st) st.mst entity else st + if !stage > 0 then + MA.meta_of_aut (err st) (f st) st.mst entity + else st in aux st tl in