From a5709dff43233c041f77a4ee4b7f2df1a3c51ab6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 2 Nov 2010 22:06:52 +0000 Subject: [PATCH] - the connections between the intermediate language and the "bag" kernel were missing - the connections between the intermediate language and the "bag" kernel are now tail recursive - the dtd now declares the "level" attribute - some "assert false" removed in crg - xml exportation of the data processed by the "bag" kernel is now available - the "bag" kernel now uses Entity names rather than identifiers --- helm/software/lambda-delta/.depend.opt | 45 ++++-- helm/software/lambda-delta/Makefile | 9 +- helm/software/lambda-delta/Makefile.common | 14 +- helm/software/lambda-delta/src/basic_ag/Make | 2 +- .../software/lambda-delta/src/basic_ag/bag.ml | 50 +++---- .../lambda-delta/src/basic_ag/bagCrg.ml | 141 +++++++++--------- .../lambda-delta/src/basic_ag/bagCrg.mli | 3 +- .../lambda-delta/src/basic_ag/bagOutput.ml | 76 ++++++---- .../lambda-delta/src/basic_ag/bagOutput.mli | 2 + .../lambda-delta/src/basic_ag/bagReduction.ml | 42 +++--- .../src/basic_ag/bagSubstitution.ml | 4 +- .../lambda-delta/src/basic_ag/bagType.ml | 34 ++--- .../software/lambda-delta/src/basic_rg/brg.ml | 6 - .../lambda-delta/src/basic_rg/brgCrg.ml | 40 ++--- .../lambda-delta/src/basic_rg/brgOutput.mli | 3 - .../software/lambda-delta/src/common/marks.ml | 9 +- .../lambda-delta/src/common/marks.mli | 16 ++ .../lambda-delta/src/complete_rg/crg.ml | 19 ++- .../lambda-delta/src/complete_rg/crgOutput.ml | 7 +- helm/software/lambda-delta/src/lib/cps.ml | 5 + .../software/lambda-delta/src/toplevel/top.ml | 5 +- helm/software/lambda-delta/xml/ld.dtd | 12 +- 22 files changed, 292 insertions(+), 252 deletions(-) create mode 100644 helm/software/lambda-delta/src/common/marks.mli diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 97e811578..ab31669d6 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -22,8 +22,9 @@ src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \ src/common/output.cmi src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \ src/common/output.cmi -src/common/marks.cmo: src/common/entity.cmx -src/common/marks.cmx: src/common/entity.cmx +src/common/marks.cmi: src/common/entity.cmx +src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmi +src/common/marks.cmx: src/common/entity.cmx src/common/marks.cmi src/common/alpha.cmi: src/common/entity.cmx src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi @@ -34,8 +35,10 @@ src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \ src/lib/cps.cmx src/common/ccs.cmi src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx -src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx -src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx +src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx \ + src/lib/cps.cmx +src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ @@ -110,7 +113,7 @@ src/xml/xmlCrg.cmx: src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \ src/basic_rg/brg.cmo: src/common/level.cmi src/common/entity.cmx src/basic_rg/brg.cmx: src/common/level.cmx src/common/entity.cmx src/basic_rg/brgCrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx -src/basic_rg/brgCrg.cmo: src/common/marks.cmx src/common/level.cmi \ +src/basic_rg/brgCrg.cmo: src/common/marks.cmi src/common/level.cmi \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/level.cmx \ @@ -172,12 +175,22 @@ src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ src/basic_rg/brgUntrusted.cmi src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx -src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \ +src/basic_ag/bagCrg.cmi: src/complete_rg/crg.cmx src/basic_ag/bag.cmx +src/basic_ag/bagCrg.cmo: src/common/marks.cmi src/common/level.cmi \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi +src/basic_ag/bagCrg.cmx: src/common/marks.cmx src/common/level.cmx \ + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi +src/basic_ag/bagOutput.cmi: src/xml/xmlLibrary.cmi src/lib/log.cmi \ + src/basic_ag/bag.cmx +src/basic_ag/bagOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \ + src/common/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \ + src/common/entity.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \ src/basic_ag/bagOutput.cmi -src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \ +src/basic_ag/bagOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \ + src/common/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \ + src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi: src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \ @@ -190,12 +203,12 @@ src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx -src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \ +src/basic_ag/bagReduction.cmo: src/common/marks.cmi src/lib/log.cmi \ + src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \ src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \ src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi -src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \ +src/basic_ag/bagReduction.cmx: src/common/marks.cmx src/lib/log.cmx \ + src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \ src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx @@ -225,7 +238,7 @@ src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ - src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \ + src/basic_ag/bagOutput.cmi src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \ src/automath/autProcess.cmi src/automath/autParser.cmi \ src/automath/autOutput.cmi src/automath/autLexer.cmx \ src/automath/autCrg.cmi src/automath/aut.cmx @@ -238,7 +251,7 @@ src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ - src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagOutput.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ src/automath/autProcess.cmx src/automath/autParser.cmx \ src/automath/autOutput.cmx src/automath/autLexer.cmx \ src/automath/autCrg.cmx src/automath/aut.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 9d55e6292..daabc346d 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -10,9 +10,9 @@ KEEP = README CLEAN = etc/log.txt etc/profile.txt -TAGS = test-si test-si-fast xml-si-crg xml-si profile +TAGS = test-si test-si-fast profile xml-si xml-si-crg html test-html \ + install-html install-lddl install-dtd install-xml -XMLLINTLOCAL = --nonet --path xml --dtdvalid ld.dtd XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ xml/brg-si/grundlagen/l/et.ld.xml \ @@ -21,9 +21,8 @@ XMLS = xml/brg-si/grundlagen/l/not.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 - -LOCALXMLS = xml/brg-si/grundlagen/ccs.ldc.xml + xml/crg-si/grundlagen/l/e/pairis1.ld.xml \ + xml/brg-si/grundlagen/ccs.ldc.xml include Makefile.common diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index 5d007032e..7bf33007d 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -20,10 +20,8 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(I OCAMLLEX = ocamllex.opt OCAMLYACC = ocamlyacc -v XMLLINT = xmllint --noout - - XSLT = xsltproc -#TAR = tar -czf etc/$(MAIN:%=%.tgz) +TAR = tar -czf etc/$(MAIN:%=%.tgz) define DIR_TEMPLATE MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make)) @@ -73,13 +71,9 @@ lint-xml: $(XMLS) @echo XMLLINT --valid $(H)$(XMLLINT) --valid $^ -lint-xml-local: $(LOCALXMLS) - @echo XMLLINT --valid - $(H)$(XMLLINT) $(XMLLINTLOCAL) --valid $^ - -#tgz: clean -# @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)" -# $(H)find -name "Make*" | xargs $(TAR) $(KEEP) +tgz: clean + @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)" + $(H)find -name "Make*" | xargs $(TAR) $(KEEP) %.ml %.mli: %.mly @echo " OCAMLYACC $<" diff --git a/helm/software/lambda-delta/src/basic_ag/Make b/helm/software/lambda-delta/src/basic_ag/Make index 1d2286b52..74961c692 100644 --- a/helm/software/lambda-delta/src/basic_ag/Make +++ b/helm/software/lambda-delta/src/basic_ag/Make @@ -1,2 +1,2 @@ -bag bagOutput +bag bagCrg bagOutput bagEnvironment bagSubstitution bagReduction bagType bagUntrusted diff --git a/helm/software/lambda-delta/src/basic_ag/bag.ml b/helm/software/lambda-delta/src/basic_ag/bag.ml index d6432863d..fc0f72f9a 100644 --- a/helm/software/lambda-delta/src/basic_ag/bag.ml +++ b/helm/software/lambda-delta/src/basic_ag/bag.ml @@ -15,22 +15,22 @@ module E = Entity type uri = E.uri -type id = E.id +type attrs = E.attrs type bind = Void (* exclusion *) | Abst of term (* abstraction *) | Abbr of term (* abbreviation *) -and term = Sort of int (* hierarchy index *) - | LRef of int (* location *) - | GRef of uri (* reference *) - | Cast of term * term (* domain, element *) - | Appl of term * term (* argument, function *) - | Bind of int * id * bind * term (* location, name, binder, scope *) +and term = Sort of int (* hierarchy index *) + | LRef of int (* location *) + | GRef of uri (* reference *) + | Cast of term * term (* domain, element *) + | Appl of term * term (* argument, function *) + | Bind of attrs * int * bind * term (* name, location, binder, scope *) type entity = term E.entity (* attrs, uri, binder *) -type lenv = (int * id * bind) list (* location, name, binder *) +type lenv = (attrs * int * bind) list (* location, name, binder *) type message = (lenv, term) Log.item list @@ -46,32 +46,24 @@ let cast u t = Cast (u, t) let appl u t = Appl (u, t) -let bind l id b t = Bind (l, id, b, t) +let bind a l b t = Bind (a, l, b, t) -let bind_abst l id u t = Bind (l, id, Abst u, t) +let bind_abst a l u t = Bind (a, l, Abst u, t) -let bind_abbr l id v t = Bind (l, id, Abbr v, t) - -(* location handling functions **********************************************) - -let location = ref 0 - -let new_location () = let loc = !location in incr location; loc - -let locations () = !location +let bind_abbr a l v t = Bind (a, l, Abbr v, t) (* local environment handling functions *************************************) let empty_lenv = [] -let push msg f es l id b = +let push msg f es a l b = let rec does_not_occur loc = function | [] -> true - | (l, _, _) :: _ when l = loc -> false + | (_, l, _) :: _ when l = loc -> false | _ :: es -> does_not_occur l es in if not (does_not_occur l es) then failwith msg else - let c = (l, id, b) :: es in f c + let c = (a, l, b) :: es in f c let append f es1 es2 = f (List.append es2 es1) @@ -81,9 +73,17 @@ let map f map es = let contents f es = f es -let get f es i = +let get err f es i = let rec aux = function - | [] -> f None - | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl + | [] -> err () + | (a, l, b) :: tl -> if l = i then f a b else aux tl in aux es + +let nth err f loc e = + let rec aux n = function + | [] -> err loc + | (_, l, _) :: _ when l = loc -> f n + | _ :: e -> aux (succ n) e + in + aux 0 e diff --git a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml index d4366b60b..dcc495232 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagCrg.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.ml @@ -18,85 +18,90 @@ module Z = Bag (* internal functions: crg to bag term **************************************) -let rec lenv_fold_left map1 map2 x = function - | D.ESort -> x - | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl - | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl +let rec shift t = function + | _, [] -> t + | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns) + | _ -> assert false -let rec xlate_term f = function - | D.TSort (a, l) -> f (Z.Sort (a, l)) - | D.TGRef (a, n) -> f (Z.GRef (a, n)) - | D.TLRef (a, _, _) -> let f i = f (Z.LRef (a, i)) in E.apix C.err f a - | D.TCast (a, u, t) -> - let f uu tt = f (Z.Cast (a, uu, tt)) in - let f uu = xlate_term (f uu) t in - xlate_term f u - | D.TAppl (a, vs, t) -> - let map f v tt = let f vv = f (Z.Appl (a, vv, tt)) in xlate_term f v in +let rec xlate_term xlate_bind f c = function + | D.TSort (_, h) -> f (Z.Sort h) + | D.TGRef (_, s) -> f (Z.GRef s) + | D.TLRef (a, _, _) -> + let f i = + let _, l, _ = List.nth c i in + f (Z.LRef l) + in + E.apix C.err f a + | D.TCast (_, u, t) -> + let f tt uu = f (Z.Cast (uu, tt)) in + let f tt = xlate_term xlate_bind (f tt) c u in + xlate_term xlate_bind f c t + | D.TAppl (_, vs, t) -> + let map f v tt = let f vv = f (Z.Appl (vv, tt)) in xlate_term xlate_bind f c v in let f tt = C.list_fold_right f map vs tt in - xlate_term f t - | D.TProj (a, e, t) -> - let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in - xlate_term f t + xlate_term xlate_bind f c t + | D.TProj (_, e, t) -> + xlate_term xlate_bind f c (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))) + 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) -> - let f tt = f (xlate_bind tt a b) in xlate_term f t + let g _ ns = ns in + let ns = E.get_names g a in + let cc = xlate_bind C.start c ns b in + let f tt = f (shift tt (cc, ns)) in + xlate_term xlate_bind f cc t -and xlate_bind x a b = - let f a ns = a, ns in - let a, ns = E.get_names f a in - match b with - | D.Abst (m, ws) -> - let map x n w = - let f ww = Z.Bind (n :: J.new_mark () :: a, Z.Abst (m, ww), x) in - xlate_term f w - in - List.fold_left2 map x ns ws - | D.Abbr vs -> - let map x n v = - let f vv = Z.Bind (n :: a, Z.Abbr vv, x) in - xlate_term f v - in - List.fold_left2 map x ns vs - | D.Void _ -> - let map x n = Z.Bind (n :: a, Z.Void, x) in - List.fold_left map x ns - -and xlate_proj x _ e = - lenv_fold_left xlate_bind xlate_proj x e +let rec xlate_bind f c ns = function + | D.Abst (_, ws) -> + let map f n w c = + let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in + xlate_term xlate_bind f c w + in + C.list_fold_right2 f map ns ws c + | D.Abbr vs -> + let map f n v c = + let f vv = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abbr vv) in + xlate_term xlate_bind f c v + in + C.list_fold_right2 f map ns vs c + | D.Void _ -> + let map f n c = Z.push "xlate_bind" f c [n] (J.new_location ()) Z.Void in + C.list_fold_right f map ns c (* internal functions: bag to crg term **************************************) -let rec xlate_bk_term f = function - | Z.Sort (a, l) -> f (D.TSort (a, l)) - | Z.GRef (a, n) -> f (D.TGRef (a, n)) - | Z.LRef (a, i) -> f (D.TLRef (a, i, 0)) - | Z.Cast (a, u, t) -> - let f uu tt = f (D.TCast (a, uu, tt)) in - let f uu = xlate_bk_term (f uu) t in - xlate_bk_term f u - | Z.Appl (a, u, t) -> - let f uu tt = f (D.TAppl (a, [uu], tt)) in - let f uu = xlate_bk_term (f uu) t in - xlate_bk_term f u - | Z.Bind (a, b, t) -> - let f bb tt = f (D.TBind (a, bb, tt)) in - let f bb = xlate_bk_term (f bb) t in - xlate_bk_bind f b +let rec xlate_bk_term f c = function + | Z.Sort h -> f (D.TSort ([], h)) + | Z.GRef s -> f (D.TGRef ([], s)) + | Z.LRef l -> + let f i = f (D.TLRef ([], i, 0)) in + Z.nth C.err f l c + | Z.Cast (u, t) -> + let f tt uu = f (D.TCast ([], uu, tt)) in + let f tt = xlate_bk_term (f tt) c u in + xlate_bk_term f c t + | Z.Appl (u, t) -> + let f tt uu = f (D.TAppl ([], [uu], tt)) in + let f tt = xlate_bk_term (f tt) c u in + xlate_bk_term f c t + | Z.Bind (a, l, b, t) -> + let f tt bb = f (D.TBind (a, bb, tt)) in + let f tt = xlate_bk_bind (f tt) c b in + let cc = Z.push "xlate_bk_term" C.start c a l b in + xlate_bk_term f cc t -and xlate_bk_bind f = function - | Z.Abst (n, t) -> - let f tt = f (D.Abst (n, [tt])) in - xlate_bk_term f t - | Z.Abbr t -> +and xlate_bk_bind f c = function + | Z.Abst t -> + let f tt = f (D.Abst (N.infinite, [tt])) in + xlate_bk_term f c t + | Z.Abbr t -> let f tt = f (D.Abbr [tt]) in - xlate_bk_term f t - | Z.Void -> f (D.Void 1) - + xlate_bk_term f c t + | Z.Void -> f (D.Void 1) + (* interface functions ******************************************************) let bag_of_crg f t = - f (xlate_term C.start t) + xlate_term xlate_bind f Z.empty_lenv t -let crg_of_bag = xlate_bk_term +let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t diff --git a/helm/software/lambda-delta/src/basic_ag/bagCrg.mli b/helm/software/lambda-delta/src/basic_ag/bagCrg.mli index aae9eb280..5c7b41bec 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagCrg.mli +++ b/helm/software/lambda-delta/src/basic_ag/bagCrg.mli @@ -10,6 +10,5 @@ V_______________________________________________________________ *) val bag_of_crg: (Bag.term -> 'a) -> Crg.term -> 'a -(* + val crg_of_bag: (Crg.term -> 'a) -> Bag.term -> 'a -*) diff --git a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml index dfdc6e116..feebca464 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml @@ -9,14 +9,17 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf -module F = Format -module U = NUri -module L = Log -module G = Options -module E = Entity -module H = Hierarchy -module Z = Bag +module P = Printf +module F = Format +module U = NUri +module L = Log +module G = Options +module E = Entity +module J = Marks +module H = Hierarchy +module XD = XmlCrg +module Z = Bag +module ZD = BagCrg type counters = { eabsts: int; @@ -78,7 +81,7 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in - let locations = Z.locations () in + let locations = J.locations () in L.warn (P.sprintf " Kernel representation summary (basic_ag)"); L.warn (P.sprintf " Total entry items: %7u" items); L.warn (P.sprintf " Declaration items: %7u" c.eabsts); @@ -94,8 +97,16 @@ let print_counters f c = L.warn (P.sprintf " Total binder locations: %7u" locations); f () -let res l id = - if !G.indexes then P.sprintf "#%u" l else id +let name err frm a = + let f n = function + | true -> F.fprintf frm "%s" n + | false -> F.fprintf frm "-%s" n + in + E.name err f a + +let res a l frm = + let err () = F.fprintf frm "@[#%u@]" l in + if !G.indexes then err () else name err frm a let rec pp_term c frm = function | Z.Sort h -> @@ -103,38 +114,36 @@ let rec pp_term c frm = function let f s = F.fprintf frm "@[%s@]" s in H.string_of_sort err f h | Z.LRef i -> - let f = function - | Some (id, _) -> F.fprintf frm "@[%s@]" id - | None -> F.fprintf frm "@[#%u@]" i - in - if !G.indexes then f None else Z.get f c i + let err () = F.fprintf frm "@[#%u@]" i in + let f a _ = name err frm a in + if !G.indexes then err () else Z.get err f c i | Z.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) | Z.Cast (u, t) -> F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t | Z.Appl (v, t) -> F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t - | Z.Bind (l, id, Z.Abst w, t) -> + | Z.Bind (a, l, Z.Abst w, t) -> let f cc = - F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t + F.fprintf frm "@[[%t:%a].%a@]" (res a l) (pp_term c) w (pp_term cc) t in - Z.push "output abst" f c l id (Z.Abst w) - | Z.Bind (l, id, Z.Abbr v, t) -> + Z.push "output abst" f c a l (Z.Abst w) + | Z.Bind (a, l, Z.Abbr v, t) -> let f cc = - F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t + F.fprintf frm "@[[%t=%a].%a@]" (res a l) (pp_term c) v (pp_term cc) t in - Z.push "output abbr" f c l id (Z.Abbr v) - | Z.Bind (l, id, Z.Void, t) -> - let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in - Z.push "output void" f c l id Z.Void + Z.push "output abbr" f c a l (Z.Abbr v) + | Z.Bind (a, l, Z.Void, t) -> + let f cc = F.fprintf frm "@[[%t].%a@]" (res a l) (pp_term cc) t in + Z.push "output void" f c a l Z.Void let pp_lenv frm c = let pp_entry frm = function - | l, id, Z.Abst w -> - F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w - | l, id, Z.Abbr v -> - F.fprintf frm "@,@[%s = %a@]" (res l id) (pp_term c) v - | l, id, Z.Void -> - F.fprintf frm "@,%s" (res l id) + | a, l, Z.Abst w -> + F.fprintf frm "@,@[%t : %a@]" (res a l) (pp_term c) w + | a, l, Z.Abbr v -> + F.fprintf frm "@,@[%t = %a@]" (res a l) (pp_term c) v + | a, l, Z.Void -> + F.fprintf frm "@,%t" (res a l) in let iter map frm l = List.iter (map frm) l in let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in @@ -143,3 +152,8 @@ let pp_lenv frm c = let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv } + +(* term xml printing ********************************************************) + +let export_term = + ZD.crg_of_bag XD.export_term diff --git a/helm/software/lambda-delta/src/basic_ag/bagOutput.mli b/helm/software/lambda-delta/src/basic_ag/bagOutput.mli index daa07a6d1..90ae4c977 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagOutput.mli +++ b/helm/software/lambda-delta/src/basic_ag/bagOutput.mli @@ -18,3 +18,5 @@ val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Bag.lenv, Bag.term) Log.specs + +val export_term: Bag.term -> XmlLibrary.pp diff --git a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml index 52f04bf0e..d22d2c730 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml @@ -13,6 +13,7 @@ module U = NUri module C = Cps module L = Log module E = Entity +module J = Marks module Z = Bag module ZO = BagOutput module ZE = BagEnvironment @@ -28,7 +29,7 @@ type whd_result = | Sort_ of int | LRef_ of int * Z.term option | GRef_ of Z.entity - | Bind_ of int * Z.id * Z.term * Z.term + | Bind_ of Z.attrs * int * Z.term * Z.term type ho_whd_result = | Sort of int @@ -40,7 +41,7 @@ let term_of_whdr = function | Sort_ h -> Z.Sort h | LRef_ (i, _) -> Z.LRef i | GRef_ (_, uri, _) -> Z.GRef uri - | Bind_ (l, id, w, t) -> Z.bind_abst l id w t + | Bind_ (a, l, w, t) -> Z.bind_abst a l w t let level = 5 @@ -57,7 +58,7 @@ let empty_machine = {i = 0; c = Z.empty_lenv; s = []} let inc m = {m with i = succ m.i} let unwind_to_term f m t = - let map f t (l, id, b) = f (Z.Bind (l, id, b, t)) in + let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in let f mc = C.list_fold_left f map t mc in Z.contents f m.c @@ -66,16 +67,13 @@ let unwind_stack f m = C.list_map f map m.s let get f c m i = - let f = function - | Some (_, b) -> f b - | None -> assert false - in - let f c = Z.get f c i in + let f _ b = f b in + let f c = Z.get C.err f c i in Z.append f c m.c -let push msg f c m l id w = +let push msg f c m a l w = assert (m.s = []); - let f w = Z.push msg f c l id (Z.Abst w) in + let f w = Z.push msg f c a l (Z.Abst w) in unwind_to_term f m w (* to share *) @@ -95,18 +93,18 @@ let rec whd f c m x = get f c m i | Z.Cast (_, t) -> whd f c m t | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t - | Z.Bind (l, id, Z.Abst w, t) -> + | Z.Bind (a, l, Z.Abst w, t) -> begin match m.s with - | [] -> f m (Bind_ (l, id, w, t)) + | [] -> f m (Bind_ (a, l, w, t)) | v :: tl -> - let nl = Z.new_location () in + let nl = J.new_location () in let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in - Z.push "!" f m.c nl id (Z.Abbr (Z.Cast (w, v))) + Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v))) end - | Z.Bind (l, id, b, t) -> - let nl = Z.new_location () in + | Z.Bind (a, l, b, t) -> + let nl = J.new_location () in let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in - Z.push "!" f m.c nl id b + Z.push "!" f m.c a nl b (* Interface functions ******************************************************) @@ -157,20 +155,20 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 = whd (aux m1 r1) c m2 v2 | GRef_ (_, _, E.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 - | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) -> - let l = Z.new_location () in + | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) -> + let l = J.new_location () in let h c = let m1, m2 = inc m1, inc m2 in let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in ZS.subst f l l1 t1 in - let f r = if r then push "!" h c m1 l id1 w1 else f false in + let f r = if r then push "!" h c m1 a1 l w1 else f false in are_convertible f ~si a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) - | Sort_ _, Bind_ (l2, id2, w2, t2) when si -> + | Sort_ _, Bind_ (a2, l2, w2, t2) when si -> let m1, m2 = inc m1, inc m2 in let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in - push "nsi" f c m2 l2 id2 w2 + push "nsi" f c m2 a2 l2 w2 | _ -> f false and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in let g m1 r1 = whd (aux m1 r1) c m2 t2 in diff --git a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml index 7a341783c..f8c347892 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml @@ -36,8 +36,8 @@ and lref_map f map t = match t with let f w' u' = f (W.sh2 w w' u u' t Z.appl) in let f w' = lref_map (f w') map u in lref_map f map w - | Z.Bind (l, id, b, u) -> - let f b' u' = f (W.sh2 b b' u u' t (Z.bind l id)) in + | Z.Bind (a, l, b, u) -> + let f b' u' = f (W.sh2 b b' u u' t (Z.bind a l)) in let f b' = lref_map (f b') map u in lref_map_bind f map b diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.ml b/helm/software/lambda-delta/src/basic_ag/bagType.ml index 906904011..4f447276b 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagType.ml @@ -54,16 +54,14 @@ let rec b_type_of f st c x = | Z.Sort h -> let h = H.apply h in f x (Z.Sort h) | Z.LRef i -> - let f = function - | Some (_, Z.Abst w) -> f x w - | Some (_, Z.Abbr (Z.Cast (w, v))) -> f x w - | Some (_, Z.Abbr _) -> assert false - | Some (_, Z.Void) -> - error1 "reference to excluded variable" c x - | None -> - error1 "variable not found" c x + let err () = error1 "variable not found" c x in + let f _ = function + | Z.Abst w -> f x w + | Z.Abbr (Z.Cast (w, v)) -> f x w + | Z.Abbr _ -> assert false + | Z.Void -> error1 "reference to excluded variable" c x in - Z.get f c i + Z.get err f c i | Z.GRef uri -> let f = function | _, _, E.Abst (_, w) -> f x w @@ -72,30 +70,30 @@ let rec b_type_of f st c x = | _, _, E.Void -> assert false in ZE.get_entity f uri - | Z.Bind (l, id, Z.Abbr v, t) -> + | Z.Bind (a, l, Z.Abbr v, t) -> let f xv xt tt = - f (W.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt) + f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt) in let f xv cc = b_type_of (f xv) st cc t in - let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in + let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in let f xv vv = match xv with | Z.Cast _ -> f xv | _ -> f (Z.Cast (vv, xv)) in type_of f st c v - | Z.Bind (l, id, Z.Abst u, t) -> + | Z.Bind (a, l, Z.Abst u, t) -> let f xu xt tt = - f (W.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt) + f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt) in let f xu cc = b_type_of (f xu) st cc t in - let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in + let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in type_of f st c u - | Z.Bind (l, id, Z.Void, t) -> + | Z.Bind (a, l, Z.Void, t) -> let f xt tt = - f (W.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt) + f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt) in let f cc = b_type_of f st cc t in - Z.push "type void" f c l id Z.Void + Z.push "type void" f c a l Z.Void | Z.Appl (v, t) -> let f xv vv xt tt = function | ZR.Abst w -> diff --git a/helm/software/lambda-delta/src/basic_rg/brg.ml b/helm/software/lambda-delta/src/basic_rg/brg.ml index 038652309..be4e6f9b9 100644 --- a/helm/software/lambda-delta/src/basic_rg/brg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brg.ml @@ -16,7 +16,6 @@ module E = Entity module N = Level type uri = E.uri -type id = E.id type attrs = E.attrs type bind = Void (* *) @@ -73,8 +72,3 @@ let get e i = get i e let rec fold_right f map e x = match e with | Null -> f x | Cons (e, c, a, b) -> fold_right (map f e c a b) map e x - -(* used in MetaBrg.unwind_to_xlate_term *) -let rec fold_left map x = function - | Null -> x - | Cons (e, _, a, b) -> fold_left map (map x a b) e diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml index f844c2e51..490125095 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml @@ -18,26 +18,20 @@ module B = Brg (* internal functions: crg to brg term **************************************) -let rec lenv_fold_left map1 map2 x = function - | D.ESort -> x - | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl - | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl - let rec xlate_term f = function | D.TSort (a, l) -> f (B.Sort (a, l)) | D.TGRef (a, n) -> f (B.GRef (a, n)) | D.TLRef (a, _, _) -> let f i = f (B.LRef (a, i)) in E.apix C.err f a | D.TCast (a, u, t) -> - let f uu tt = f (B.Cast (a, uu, tt)) in - let f uu = xlate_term (f uu) t in - xlate_term f u + let f tt uu = f (B.Cast (a, uu, tt)) in + let f tt = xlate_term (f tt) u in + xlate_term f t | D.TAppl (a, vs, t) -> let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in let f tt = C.list_fold_right f map vs tt in xlate_term f t - | D.TProj (a, e, t) -> - let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in - xlate_term f t + | D.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) -> @@ -63,9 +57,6 @@ and xlate_bind x a b = let map x n = B.Bind (n :: a, B.Void, x) in List.fold_left map x ns -and xlate_proj x _ e = - lenv_fold_left xlate_bind xlate_proj x e - (* internal functions: brg to crg term **************************************) let rec xlate_bk_term f = function @@ -73,17 +64,17 @@ let rec xlate_bk_term f = function | B.GRef (a, n) -> f (D.TGRef (a, n)) | B.LRef (a, i) -> f (D.TLRef (a, i, 0)) | B.Cast (a, u, t) -> - let f uu tt = f (D.TCast (a, uu, tt)) in - let f uu = xlate_bk_term (f uu) t in - xlate_bk_term f u + let f tt uu = f (D.TCast (a, uu, tt)) in + let f tt = xlate_bk_term (f tt) u in + xlate_bk_term f t | B.Appl (a, u, t) -> - let f uu tt = f (D.TAppl (a, [uu], tt)) in - let f uu = xlate_bk_term (f uu) t in - xlate_bk_term f u + let f tt uu = f (D.TAppl (a, [uu], tt)) in + let f tt = xlate_bk_term (f tt) u in + xlate_bk_term f t | B.Bind (a, b, t) -> - let f bb tt = f (D.TBind (a, bb, tt)) in - let f bb = xlate_bk_term (f bb) t in - xlate_bk_bind f b + let f tt bb = f (D.TBind (a, bb, tt)) in + let f tt = xlate_bk_bind (f tt) b in + xlate_bk_term f t and xlate_bk_bind f = function | B.Abst (n, t) -> @@ -96,7 +87,6 @@ and xlate_bk_bind f = function (* interface functions ******************************************************) -let brg_of_crg f t = - f (xlate_term C.start t) +let brg_of_crg f t = f (xlate_term C.start t) let crg_of_brg = xlate_bk_term diff --git a/helm/software/lambda-delta/src/basic_rg/brgOutput.mli b/helm/software/lambda-delta/src/basic_rg/brgOutput.mli index 556439a99..f0b0aa543 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/src/basic_rg/brgOutput.mli @@ -20,6 +20,3 @@ val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.lenv, Brg.term) Log.specs val export_term: Brg.term -> XmlLibrary.pp -(* -val export_term: Format.formatter -> Brg.term -> unit -*) diff --git a/helm/software/lambda-delta/src/common/marks.ml b/helm/software/lambda-delta/src/common/marks.ml index a9b78762a..fba716b37 100644 --- a/helm/software/lambda-delta/src/common/marks.ml +++ b/helm/software/lambda-delta/src/common/marks.ml @@ -11,11 +11,14 @@ module E = Entity +let location = ref 0 + (* interface functions ******************************************************) -let new_location = - let location = ref 0 in - fun () -> incr location; !location +let locations () = !location + +let new_location () = + incr location; !location let new_mark () = E.Mark (new_location ()) diff --git a/helm/software/lambda-delta/src/common/marks.mli b/helm/software/lambda-delta/src/common/marks.mli new file mode 100644 index 000000000..ff5a68109 --- /dev/null +++ b/helm/software/lambda-delta/src/common/marks.mli @@ -0,0 +1,16 @@ +(* + ||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 locations: unit -> int + +val new_location: unit -> int + +val new_mark: unit -> Entity.attr diff --git a/helm/software/lambda-delta/src/complete_rg/crg.ml b/helm/software/lambda-delta/src/complete_rg/crg.ml index 07305e9c1..5a394f4f8 100644 --- a/helm/software/lambda-delta/src/complete_rg/crg.ml +++ b/helm/software/lambda-delta/src/complete_rg/crg.ml @@ -12,6 +12,7 @@ (* kernel version: complete, relative, global *) (* note : fragment of complete lambda-delta serving as abstract layer *) +module C = Cps module E = Entity module N = Level @@ -39,6 +40,18 @@ type entity = term E.entity (* helpers ******************************************************************) +let rec tshift t = function + | ESort -> t + | EBind (e, a, b) -> tshift (TBind (a, b, t)) e + | EProj (e, a, d) -> tshift (TProj (a, d, t)) e + +let tshift c t = tshift t c + +let rec eshift f c = function + | ESort -> f c + | EBind (e, a, b) -> let f ee = f (EBind (ee, a, b)) in eshift f c e + | EProj (e, a, d) -> let f ee = f (EProj (ee, a, d)) in eshift f c e + let empty_lenv = ESort let push_bind f lenv a b = f (EBind (lenv, a, b)) @@ -71,7 +84,7 @@ let resolve_lref err f id lenv = let err kk = aux f (succ i) (k + kk) tl in let f j = f i j (k + j) in E.resolve err f id a - | EProj _ -> assert false (* TODO *) + | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) in aux f 0 0 lenv @@ -99,7 +112,7 @@ let get_index err f i j lenv = if E.count_names a > j then f (k + j) else err i | EBind (tl, a, _) -> aux f (pred i) (k + E.count_names a) tl - | EProj _ -> assert false (* TODO *) + | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) in aux f i 0 lenv @@ -115,6 +128,6 @@ let rec get i = function | EBind (e, _, Void 0) -> get i e | EBind (e, a, b) when i = 0 -> e, a, b | EBind (e, _, _) -> get (pred i) e - | EProj _ -> assert false (* TODO *) + | EProj (e, _, d) -> get i (eshift C.start e d) let get e i = get i e diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml index c8d3bad88..5d2faf900 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml @@ -44,11 +44,6 @@ let initial_counters = { uris = []; nodes = 0; xnodes = 0 } -let rec shift t = function - | D.ESort -> t - | D.EBind (e, a, b) -> shift (D.TBind (a, b, t)) e - | D.EProj (e, a, d) -> shift (D.TProj (a, d, t)) e - let rec count_term f c e = function | D.TSort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} @@ -75,7 +70,7 @@ let rec count_term f c e = function let f c = count_term f c e t in C.list_fold_right f (map1 e) vs c | D.TProj (a, d, t) -> - count_term f c e (shift t d) + count_term f c e (D.tshift d t) | D.TBind (a, b, t) -> let f c e = count_term f c e t in count_binder f c e a b diff --git a/helm/software/lambda-delta/src/lib/cps.ml b/helm/software/lambda-delta/src/lib/cps.ml index 10ec62376..f993ffb04 100644 --- a/helm/software/lambda-delta/src/lib/cps.ml +++ b/helm/software/lambda-delta/src/lib/cps.ml @@ -71,6 +71,11 @@ let rec list_fold_right f map l a = match l with | [] -> f a | hd :: tl -> list_fold_right (map f hd) map tl a +let rec list_fold_right2 f map l1 l2 a = match l1, l2 with + | [], [] -> f a + | hd1 :: tl1, hd2 :: tl2 -> list_fold_right2 (map f hd1 hd2) map tl1 tl2 a + | _ -> failwith "Cps.list_fold_right2" + let list_map f map l = let map f hd a = let f hd = f (hd :: a) in map f hd diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index b47d00725..aad48387e 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -31,6 +31,7 @@ module BD = BrgCrg module BO = BrgOutput module BR = BrgReduction module BU = BrgUntrusted +module ZD = BagCrg module ZO = BagOutput module ZT = BagType module ZU = BagUntrusted @@ -85,6 +86,8 @@ let print_counters st = function let xlate_entity entity = match !G.kernel, entity with | G.Brg, CrgEntity e -> let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e + | G.Bag, CrgEntity e -> + let f e = (BagEntity e) in E.xlate f ZD.bag_of_crg e | _, entity -> entity let pp_progress e = @@ -107,7 +110,7 @@ let count_entity st = function let export_entity = function | CrgEntity e -> XL.export_entity XD.export_term e | BrgEntity e -> XL.export_entity BO.export_term e - | BagEntity _ -> () + | BagEntity e -> XL.export_entity ZO.export_term e let type_check st k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index d97173d82..539e8a28f 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -53,7 +53,8 @@ -- 2.39.2