From 338e3e5c639fbcfeeb347a0121cacc6c0f1fc42a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 14 Dec 2008 19:34:19 +0000
Subject: [PATCH] new kernel basic_ag (with absolute local references)

---
 helm/software/lambda-delta/.depend.opt        |  93 ++++----
 helm/software/lambda-delta/Make               |   1 +
 helm/software/lambda-delta/Makefile           |   2 -
 helm/software/lambda-delta/Makefile.common    |   2 +
 helm/software/lambda-delta/basic_ag/Make      |   3 +-
 .../lambda-delta/basic_ag/{brg.ml => bag.ml}  |  55 ++---
 .../{brgEnvironment.ml => bagEnvironment.ml}  |   2 +-
 ...{brgEnvironment.mli => bagEnvironment.mli} |   6 +-
 .../basic_ag/{brgOutput.ml => bagOutput.ml}   |  51 ++---
 .../basic_ag/{brgOutput.mli => bagOutput.mli} |   4 +-
 .../lambda-delta/basic_ag/bagReduction.ml     | 154 +++++++++++++
 .../{brgReduction.mli => bagReduction.mli}    |   8 +-
 .../lambda-delta/basic_ag/bagSubstitution.ml  |  48 +++++
 .../lambda-delta/basic_ag/bagSubstitution.mli |  12 ++
 .../basic_ag/{brgType.ml => bagType.ml}       |  36 ++--
 .../basic_ag/{brgType.mli => bagType.mli}     |   6 +-
 .../{brgUntrusted.ml => bagUntrusted.ml}      |   6 +-
 .../{brgUntrusted.mli => bagUntrusted.mli}    |   2 +-
 .../lambda-delta/basic_ag/brgReduction.ml     | 203 ------------------
 helm/software/lambda-delta/lib/cps.ml         |   4 +
 helm/software/lambda-delta/toplevel/Make      |   2 +-
 .../toplevel/{metaBrg.ml => metaBag.ml}       |  63 +++---
 .../toplevel/{metaBrg.mli => metaBag.mli}     |   2 +-
 helm/software/lambda-delta/toplevel/top.ml    |  32 +--
 24 files changed, 419 insertions(+), 378 deletions(-)
 create mode 100644 helm/software/lambda-delta/Make
 rename helm/software/lambda-delta/basic_ag/{brg.ml => bag.ml} (53%)
 rename helm/software/lambda-delta/basic_ag/{brgEnvironment.ml => bagEnvironment.ml} (98%)
 rename helm/software/lambda-delta/basic_ag/{brgEnvironment.mli => bagEnvironment.mli} (83%)
 rename helm/software/lambda-delta/basic_ag/{brgOutput.ml => bagOutput.ml} (78%)
 rename helm/software/lambda-delta/basic_ag/{brgOutput.mli => bagOutput.mli} (88%)
 create mode 100644 helm/software/lambda-delta/basic_ag/bagReduction.ml
 rename helm/software/lambda-delta/basic_ag/{brgReduction.mli => bagReduction.mli} (80%)
 create mode 100644 helm/software/lambda-delta/basic_ag/bagSubstitution.ml
 create mode 100644 helm/software/lambda-delta/basic_ag/bagSubstitution.mli
 rename helm/software/lambda-delta/basic_ag/{brgType.ml => bagType.ml} (81%)
 rename helm/software/lambda-delta/basic_ag/{brgType.mli => bagType.mli} (84%)
 rename helm/software/lambda-delta/basic_ag/{brgUntrusted.ml => bagUntrusted.ml} (95%)
 rename helm/software/lambda-delta/basic_ag/{brgUntrusted.mli => bagUntrusted.mli} (91%)
 delete mode 100644 helm/software/lambda-delta/basic_ag/brgReduction.ml
 rename helm/software/lambda-delta/toplevel/{metaBrg.ml => metaBag.ml} (54%)
 rename helm/software/lambda-delta/toplevel/{metaBrg.mli => metaBag.mli} (92%)

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index ae6e441cc..88f23f93e 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -18,39 +18,44 @@ automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi
 automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx 
 automath/autItem.cmo: lib/nUri.cmi 
 automath/autItem.cmx: lib/nUri.cmx 
-basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx 
-basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx 
-basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx 
-basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \
-    lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
-basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \
-    lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
-basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx 
-basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \
-    basic_rg/brgEnvironment.cmi 
-basic_rg/brgEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_rg/brg.cmx \
-    basic_rg/brgEnvironment.cmi 
-basic_rg/brgReduction.cmi: basic_rg/brg.cmx 
-basic_rg/brgReduction.cmo: lib/share.cmx lib/log.cmi 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 lib/log.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/hierarchy.cmi basic_rg/brg.cmx 
-basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
-    lib/hierarchy.cmi basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \
-    basic_rg/brgEnvironment.cmi basic_rg/brg.cmx automath/autItem.cmx \
-    basic_rg/brgType.cmi 
-basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
-    lib/hierarchy.cmx basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \
-    basic_rg/brgEnvironment.cmx basic_rg/brg.cmx automath/autItem.cmx \
-    basic_rg/brgType.cmi 
-basic_rg/brgUntrusted.cmi: lib/hierarchy.cmi basic_rg/brg.cmx 
-basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgEnvironment.cmi \
-    basic_rg/brg.cmx basic_rg/brgUntrusted.cmi 
-basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgEnvironment.cmx \
-    basic_rg/brg.cmx basic_rg/brgUntrusted.cmi 
+basic_ag/bag.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx 
+basic_ag/bag.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx 
+basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx 
+basic_ag/bagOutput.cmo: lib/nUri.cmi lib/log.cmi lib/hierarchy.cmi \
+    lib/cps.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi 
+basic_ag/bagOutput.cmx: lib/nUri.cmx lib/log.cmx lib/hierarchy.cmx \
+    lib/cps.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi 
+basic_ag/bagEnvironment.cmi: lib/nUri.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/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/log.cmi 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/log.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: lib/hierarchy.cmi basic_ag/bag.cmx 
+basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
+    lib/hierarchy.cmi basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi \
+    basic_ag/bagEnvironment.cmi basic_ag/bag.cmx automath/autItem.cmx \
+    basic_ag/bagType.cmi 
+basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
+    lib/hierarchy.cmx basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx \
+    basic_ag/bagEnvironment.cmx basic_ag/bag.cmx automath/autItem.cmx \
+    basic_ag/bagType.cmi 
+basic_ag/bagUntrusted.cmi: lib/hierarchy.cmi basic_ag/bag.cmx 
+basic_ag/bagUntrusted.cmo: basic_ag/bagType.cmi basic_ag/bagEnvironment.cmi \
+    basic_ag/bag.cmx basic_ag/bagUntrusted.cmi 
+basic_ag/bagUntrusted.cmx: basic_ag/bagType.cmx basic_ag/bagEnvironment.cmx \
+    basic_ag/bag.cmx basic_ag/bagUntrusted.cmi 
 toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx 
 toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx 
 toplevel/metaOutput.cmi: toplevel/meta.cmx 
@@ -63,18 +68,18 @@ 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/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/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/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.cmi \
-    toplevel/metaBrg.cmi toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi \
-    lib/cps.cmx basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi \
-    basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \
+    toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi \
+    lib/cps.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \
+    basic_ag/bagOutput.cmi automath/autParser.cmi automath/autOutput.cmi \
     automath/autLexer.cmx 
 toplevel/top.cmx: lib/time.cmx lib/nUri.cmx toplevel/metaOutput.cmx \
-    toplevel/metaBrg.cmx toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx \
-    lib/cps.cmx basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx \
-    basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \
+    toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx \
+    lib/cps.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \
+    basic_ag/bagOutput.cmx automath/autParser.cmx automath/autOutput.cmx \
     automath/autLexer.cmx 
diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make
new file mode 100644
index 000000000..5c7f64d02
--- /dev/null
+++ b/helm/software/lambda-delta/Make
@@ -0,0 +1 @@
+lib automath basic_ag toplevel
diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index 2be69cba3..3b212fa94 100644
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -1,7 +1,5 @@
 MAIN = helena
 
-DIRECTORIES = lib automath basic_rg toplevel
-
 REQUIRES = unix
 
 KEEP = README automath/*.aut
diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common
index e4489040d..cf15ef85d 100644
--- a/helm/software/lambda-delta/Makefile.common
+++ b/helm/software/lambda-delta/Makefile.common
@@ -1,5 +1,7 @@
 H=@
 
+DIRECTORIES = $(shell cat Make)
+
 INCLUDES = $(DIRECTORIES:%=-I %) 
 
 OCAMLDEP  = ocamlfind ocamldep -native $(INCLUDES)
diff --git a/helm/software/lambda-delta/basic_ag/Make b/helm/software/lambda-delta/basic_ag/Make
index eb1c64a66..1d2286b52 100644
--- a/helm/software/lambda-delta/basic_ag/Make
+++ b/helm/software/lambda-delta/basic_ag/Make
@@ -1 +1,2 @@
-brg brgOutput brgEnvironment brgReduction brgType brgUntrusted
+bag bagOutput 
+bagEnvironment bagSubstitution bagReduction bagType bagUntrusted
diff --git a/helm/software/lambda-delta/basic_ag/brg.ml b/helm/software/lambda-delta/basic_ag/bag.ml
similarity index 53%
rename from helm/software/lambda-delta/basic_ag/brg.ml
rename to helm/software/lambda-delta/basic_ag/bag.ml
index 73da25b2d..d0c193a2a 100644
--- a/helm/software/lambda-delta/basic_ag/brg.ml
+++ b/helm/software/lambda-delta/basic_ag/bag.ml
@@ -16,18 +16,18 @@ type bind = Void         (* exclusion *)
           | Abst of term (* abstraction *)
           | Abbr of term (* abbreviation *)
 
-and term = Sort of int              (* hierarchy index *)
-         | LRef of int              (* reverse de Bruijn index *)
-         | GRef of uri              (* reference *)
-         | Cast of term * term      (* type, term *)
-         | Appl of term * term      (* argument, function *)
-         | Bind of id * bind * term (* name, binder, scope *)
+and term = Sort of int                    (* hierarchy index *)
+         | LRef of int                    (* location *)
+         | GRef of uri                    (* reference *)
+         | Cast of term * term            (* type, term *)
+         | Appl of term * term            (* argument, function *)
+         | Bind of int * id * bind * term (* location, name, binder, scope *)
 
 type obj = int * uri * bind (* age, uri, binder, contents *)
 
 type item = obj option
 
-type context = int * (id * bind) list
+type context = (int * id * bind) list (* location, name, binder *) 
 
 type message = (context, term) Log.item list
 
@@ -37,35 +37,42 @@ let abst w = Abst w
 
 let abbr v = Abbr v
 
+let lref i = LRef i
+
 let cast u t = Cast (u, t)
 
 let appl u t = Appl (u, t)
 
-let bind id b t = Bind (id, b, t)
+let bind l id b t = Bind (l, id, b, t)
+
+let bind_abst l id u t = Bind (l, id, Abst u, t)
+
+let bind_abbr l id v t = Bind (l, id, Abbr v, t)
 
-let bind_abst id u t = Bind (id, Abst u, t)
+(* location handling functions **********************************************)
 
-let bind_abbr id v t = Bind (id, Abbr v, t)
+let location = ref 0
+
+let new_location () = let loc = !location in incr location; loc
 
 (* context handling functions ***********************************************)
 
-let empty_context = 0, []
+let empty_context = []
 
-let push f (l, es) id b =
-   let c = succ l, (id, b) :: es in 
-   f c
+let push f es l id b =
+   let c = (l, id, b) :: es in f c
 
-let append f (l1, es1) (l2, es2) =
-   f (l2 + l1, List.append es2 es1)
+let append f es1 es2 = 
+   f (List.append es2 es1)
 
-let map f map (l, es) =
-   let f es = f (l, es) in
+let map f map es =
    Cps.list_map f map es
 
-let contents f (l, es) = f l es
-
-let get f (l, es) i =
-   if i < 0 || i >= l then f None else 
-   let result = List.nth es (l - succ i) in
-   f (Some result)
+let contents f es = f es
 
+let get f es i =
+   let rec aux = function
+      | []               -> f None
+      | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl
+   in
+   aux es
diff --git a/helm/software/lambda-delta/basic_ag/brgEnvironment.ml b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml
similarity index 98%
rename from helm/software/lambda-delta/basic_ag/brgEnvironment.ml
rename to helm/software/lambda-delta/basic_ag/bagEnvironment.ml
index fb4243c74..5e6c9f1a0 100644
--- a/helm/software/lambda-delta/basic_ag/brgEnvironment.ml
+++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml
@@ -12,7 +12,7 @@
 module U = NUri
 module L = Log
 module H = U.UriHash
-module B = Brg
+module B = Bag
 
 exception ObjectNotFound of B.message
 
diff --git a/helm/software/lambda-delta/basic_ag/brgEnvironment.mli b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli
similarity index 83%
rename from helm/software/lambda-delta/basic_ag/brgEnvironment.mli
rename to helm/software/lambda-delta/basic_ag/bagEnvironment.mli
index 8f9f8b1b0..6dc2330c1 100644
--- a/helm/software/lambda-delta/basic_ag/brgEnvironment.mli
+++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli
@@ -9,8 +9,8 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-exception ObjectNotFound of Brg.message
+exception ObjectNotFound of Bag.message
 
-val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a
+val set_obj: (Bag.obj -> 'a) -> Bag.obj -> 'a
 
-val get_obj: (Brg.obj -> 'a) -> NUri.uri -> 'a
+val get_obj: (Bag.obj -> 'a) -> NUri.uri -> 'a
diff --git a/helm/software/lambda-delta/basic_ag/brgOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml
similarity index 78%
rename from helm/software/lambda-delta/basic_ag/brgOutput.ml
rename to helm/software/lambda-delta/basic_ag/bagOutput.ml
index 66c7ed3d8..589ce60f0 100644
--- a/helm/software/lambda-delta/basic_ag/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml
@@ -15,7 +15,7 @@ module U = NUri
 module C = Cps
 module L = Log
 module H = Hierarchy
-module B = Brg
+module B = Bag
 
 type counters = {
    eabsts: int;
@@ -29,8 +29,6 @@ type counters = {
    tabbrs: int
 }
 
-let indexes = ref false
-
 let initial_counters = {
    eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
@@ -60,7 +58,7 @@ and count_term f c = function
       let c = {c with tappls = succ c.tappls} in
       let f c = count_term f c t in
       count_term f c v
-   | B.Bind (_, b, t) -> 
+   | B.Bind (_, _, b, t) -> 
       let f c = count_term_binder f c b in
       count_term f c t
 
@@ -86,7 +84,7 @@ let print_counters f c =
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
-   L.warn (P.sprintf "  Kernel representation summary (basic_rg)");
+   L.warn (P.sprintf "  Kernel representation summary (basic_ag)");
    L.warn (P.sprintf "    Total entry items:        %6u" items);
    L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
    L.warn (P.sprintf "      Definition items:       %6u" c.eabbrs);
@@ -100,6 +98,11 @@ let print_counters f c =
    L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
    f ()
 
+let indexes = ref false
+
+let res l id =
+   if !indexes then P.sprintf "#%u" l else id
+
 let rec pp_term c frm = function
    | B.Sort h                 -> 
       let f = function 
@@ -113,36 +116,36 @@ let rec pp_term c frm = function
          | None         -> F.fprintf frm "@[#%u@]" i
       in
       if !indexes then f None else B.get f c i
-   | B.GRef s                 -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
-   | B.Cast (u, t)            ->
+   | B.GRef s                    -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+   | B.Cast (u, t)               ->
       F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
-   | B.Appl (v, t)            ->
+   | B.Appl (v, t)               ->
       F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
-   | B.Bind (id, B.Abst w, t) ->
+   | B.Bind (l, id, B.Abst w, t) ->
       let f cc =
-         F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term cc) t
+         F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t
       in
-      B.push f c id (B.Abst w)
-   | B.Bind (id, B.Abbr v, t) ->
+      B.push f c l id (B.Abst w)
+   | B.Bind (l, id, B.Abbr v, t) ->
       let f cc = 
-         F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term cc) t
+         F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t
       in
-      B.push f c id (B.Abbr v)
-   | B.Bind (id, B.Void, t)   ->
-      let f cc = F.fprintf frm "@[[%s].%a@]" id (pp_term cc) t in
-      B.push f c id B.Void
+      B.push f c l id (B.Abbr v)
+   | B.Bind (l, id, B.Void, t)   ->
+      let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
+      B.push f c l id B.Void
 
 let pp_context frm c =
    let pp_entry frm = function
-      | id, B.Abst w -> 
-         F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w
-      | id, B.Abbr v -> 
-         F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v
-      | id, B.Void   -> 
-         F.fprintf frm "@,%s" id
+      | l, id, B.Abst w -> 
+         F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w
+      | l, id, B.Abbr v -> 
+         F.fprintf frm "@,@[%s = %a@]" (res l id) (pp_term c) v
+      | l, id, B.Void   -> 
+         F.fprintf frm "@,%s" (res l id)
    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
+   let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
    B.contents f c
 
 let specs = {
diff --git a/helm/software/lambda-delta/basic_ag/brgOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli
similarity index 88%
rename from helm/software/lambda-delta/basic_ag/brgOutput.mli
rename to helm/software/lambda-delta/basic_ag/bagOutput.mli
index 566dfe8f3..fe4d9f344 100644
--- a/helm/software/lambda-delta/basic_ag/brgOutput.mli
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.mli
@@ -13,10 +13,10 @@ type counters
 
 val initial_counters: counters
 
-val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a
+val count_item: (counters -> 'a) -> counters -> Bag.item -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
 
-val specs: (Brg.context, Brg.term) Log.specs
+val specs: (Bag.context, Bag.term) Log.specs
 
 val indexes: bool ref
diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
new file mode 100644
index 000000000..0310e8d28
--- /dev/null
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -0,0 +1,154 @@
+(*
+    ||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 C = Cps
+module L = Log
+module B = Bag
+module O = BagOutput
+module E = BagEnvironment
+module S = BagSubstitution
+
+exception LRefNotFound of B.message
+
+type machine = {
+   c: B.context;
+   s: B.term list
+}
+
+type whd_result =
+   | Sort_ of int
+   | LRef_ of int * B.term option
+   | GRef_ of int * B.bind
+   | Bind_ of int * B.id * B.term * B.term
+
+type ho_whd_result =
+   | Sort of int
+   | Abst of B.term
+
+(* Internal functions *******************************************************)
+
+let level = 5
+
+let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
+
+let empty_machine = {c = B.empty_context; s = []}
+
+let contents f c m =
+   let f gl ges = B.contents (f gl ges) m.c in
+   B.contents f c
+
+let unwind_to_context f c m = B.append f c m.c
+
+let unwind_to_term f m t =
+   let map f t (l, id, b) = f (B.Bind (l, id, b, t)) in
+   let f mc = C.list_fold_left f map t mc in
+   B.contents f m.c
+
+let get f c m i =
+   let f = function
+      | Some (_, b) -> f b
+      | None        -> error i
+   in
+   let f c = B.get f c i in
+   unwind_to_context f c m
+
+let push f c m l id w = 
+   assert (m.s = []);
+   let f w = B.push f c l id (B.Abst w) in
+   unwind_to_term f m w
+
+(* to share *)
+let rec whd f c m x = match x with
+   | B.Sort h                    -> f m (Sort_ h)
+   | B.GRef uri                  ->
+      let f (i, _, b) = f m (GRef_ (i, b)) in
+      E.get_obj f uri
+   | B.LRef i                    ->
+      let f = function
+         | B.Void   -> f m (LRef_ (i, None))
+	 | B.Abst t -> f m (LRef_ (i, Some t))
+	 | B.Abbr t -> whd f c m t
+      in
+      get f c m i
+   | B.Cast (_, t)               -> whd f c m t
+   | B.Appl (v, t)               -> whd f c {m with s = v :: m.s} t   
+   | B.Bind (l, id, B.Abst w, t) -> 
+      begin match m.s with
+         | []      -> f m (Bind_ (l, id, w, t))
+	 | v :: tl -> 
+	    let f mc = whd f c {c = mc; s = tl} t in
+	    B.push f m.c l id (B.Abbr (B.Cast (w, v)))
+      end
+   | B.Bind (l, id, b, t)         -> 
+      let f mc = whd f c {m with c = mc} t in
+      B.push f m.c l id b
+
+(* Interface functions ******************************************************)
+
+let rec ho_whd f c m x =
+   let aux m = function
+      | Sort_ h             -> f c (Sort h)
+      | Bind_ (_, _, w, _)  -> 
+         let f c = f c (Abst w) in unwind_to_context f c m
+      | LRef_ (_, Some w)   -> ho_whd f c m w
+      | GRef_ (_, B.Abst u) -> ho_whd f c m u
+      | GRef_ (_, B.Abbr t) -> ho_whd f c m t
+      | LRef_ (_, None)     -> assert false
+      | GRef_ (_, B.Void)   -> assert false
+   in
+   whd aux c m x
+   
+let ho_whd f c t =
+   let f c r = L.unbox (); f c r in
+   L.box (); L.log O.specs level (L.ct_items1 "Now scanning" c t);
+   ho_whd f c empty_machine t
+
+let rec are_convertible f c m1 t1 m2 t2 =
+   let rec aux m1 r1 m2 r2 = match r1, r2 with
+      | Sort_ h1, Sort_ h2                               -> f (h1 = h2)
+      | LRef_ (i1, _), LRef_ (i2, _)                     ->
+         if i1 = i2 then are_convertible_stacks f c m1 m2 else f false
+      | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _)       ->
+         if a1 = a2 then are_convertible_stacks f c m1 m2 else f false
+      | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2)     ->
+         if a1 = a2 then are_convertible_stacks f c m1 m2 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)                          ->
+         whd (aux m1 r1) c m2 v2
+      | GRef_ (_, B.Abbr v1), _                          ->
+	 whd (aux_rev m2 r2) c m1 v1      
+      | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) ->
+         let f b = 
+	    if b then 
+	       let f c = 
+	          S.subst (are_convertible f c m1 t1 m2) l1 l2 t2
+	       in
+               push f c m1 l1 id1 w1
+	    else f false
+	 in
+	 are_convertible f c m1 w1 m2 w2
+      | _                                                -> f false
+   and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
+   let f m1 r1 = whd (aux m1 r1) c m2 t2 in 
+   whd f c m1 t1
+
+and are_convertible_stacks f c m1 m2 =
+   let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
+   let map f v1 v2 = are_convertible f c mm1 v1 mm2 v2 in
+   if List.length m1.s <> List.length m2.s then f false else
+   C.forall2 f map m1.s m2.s
+
+let are_convertible f c t1 t2 = 
+   let f b = L.unbox (); f b in
+   L.box ();
+   L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2);
+   are_convertible f c empty_machine t1 empty_machine t2
diff --git a/helm/software/lambda-delta/basic_ag/brgReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli
similarity index 80%
rename from helm/software/lambda-delta/basic_ag/brgReduction.mli
rename to helm/software/lambda-delta/basic_ag/bagReduction.mli
index 91a0289bb..2b5f02e71 100644
--- a/helm/software/lambda-delta/basic_ag/brgReduction.mli
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli
@@ -10,14 +10,14 @@
       V_______________________________________________________________ *)
 
 
-exception LRefNotFound of Brg.message
+exception LRefNotFound of Bag.message
 
 type ho_whd_result =
    | Sort of int
-   | Abst of Brg.term
+   | Abst of Bag.term
 
 val ho_whd: 
-   (Brg.context -> ho_whd_result -> 'a) -> Brg.context -> Brg.term -> 'a
+   (Bag.context -> ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a
 
 val are_convertible:
-   (bool -> 'a) -> Brg.context -> Brg.term -> Brg.term -> 'a
+   (bool -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a
diff --git a/helm/software/lambda-delta/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
new file mode 100644
index 000000000..25725520d
--- /dev/null
+++ b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
@@ -0,0 +1,48 @@
+(*
+    ||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 S = Share
+module B = Bag
+
+(* Internal functions *******************************************************)
+
+let rec lref_map_bind f map b = match b with
+   | B.Abbr v ->
+      let f v' = f (S.sh1 v v' b B.abbr) in
+      lref_map f map v      
+   | B.Abst w ->
+      let f w' = f (S.sh1 w w' b B.abst) in
+      lref_map f map w
+   | B.Void   -> f b
+
+and lref_map f map t = match t with
+   | B.LRef i            -> 
+      let ii = map i in f (S.sh1 i ii t B.lref)
+   | B.GRef _            -> f t
+   | B.Sort _            -> f t
+   | B.Cast (w, u)       ->
+      let f w' u' = f (S.sh2 w w' u u' t B.cast) in
+      let f w' = lref_map (f w') map u in 
+      lref_map f map w
+   | B.Appl (w, u)       ->
+      let f w' u' = f (S.sh2 w w' u u' t B.appl) in
+      let f w' = lref_map (f w') map u in 
+      lref_map f map w
+   | B.Bind (l, id, b, u) ->
+      let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in
+      let f b' = lref_map (f b') map u in 
+      lref_map_bind f map b
+
+(* Interface functions ******************************************************)
+
+let subst f new_l old_l t =
+   let map i = if i = old_l then new_l else i in
+   lref_map f map t
diff --git a/helm/software/lambda-delta/basic_ag/bagSubstitution.mli b/helm/software/lambda-delta/basic_ag/bagSubstitution.mli
new file mode 100644
index 000000000..b48c056df
--- /dev/null
+++ b/helm/software/lambda-delta/basic_ag/bagSubstitution.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 subst: (Bag.term -> 'a) -> int -> int -> Bag.term -> 'a
diff --git a/helm/software/lambda-delta/basic_ag/brgType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml
similarity index 81%
rename from helm/software/lambda-delta/basic_ag/brgType.ml
rename to helm/software/lambda-delta/basic_ag/bagType.ml
index fb7862c24..a651c6e33 100644
--- a/helm/software/lambda-delta/basic_ag/brgType.ml
+++ b/helm/software/lambda-delta/basic_ag/bagType.ml
@@ -14,10 +14,10 @@ module S = Share
 module L = Log
 module H = Hierarchy
 module I = AutItem
-module B = Brg
-module O = BrgOutput
-module E = BrgEnvironment
-module R = BrgReduction
+module B = Bag
+module O = BagOutput
+module E = BagEnvironment
+module R = BagReduction
 
 exception TypeError of B.message
 
@@ -40,9 +40,9 @@ let mk_gref u l =
 let rec b_type_of f g c x = 
    L.log O.specs level (L.ct_items1 "Now checking" c x);
    match x with
-   | B.Sort h                 ->
+   | B.Sort h                    ->
       let f h = f x (B.Sort h) in H.apply f g h
-   | B.LRef i                 ->
+   | B.LRef i                    ->
       let f = function
          | Some (_, B.Abst w)               -> f x w
 	 | Some (_, B.Abbr (B.Cast (w, v))) -> f x w
@@ -53,7 +53,7 @@ let rec b_type_of f g c x =
 	    error1 "variable not found" c x	 
       in
       B.get f c i
-   | B.GRef uri               ->
+   | B.GRef uri                  ->
       let f = function
          | _, _, B.Abst w               -> f x w
 	 | _, _, B.Abbr (B.Cast (w, v)) -> f x w
@@ -62,35 +62,37 @@ let rec b_type_of f g c x =
 	    error1 "reference to excluded object" c x
       in
       E.get_obj f uri   
-   | B.Bind (id, B.Abbr v, t) ->
+   | B.Bind (l, id, B.Abbr v, t) ->
       let f xv xt tt =
-         f (S.sh2 v xv t xt x (B.bind_abbr id)) (B.bind_abbr id xv tt)
+         f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt)
       in
       let f xv cc = b_type_of (f xv) g cc t in
-      let f xv = B.push (f xv) c id (B.Abbr xv) in
+      let f xv = B.push (f xv) c l id (B.Abbr xv) in
       let f xv vv = match xv with 
 	 | B.Cast _ -> f xv
          | _        -> f (B.Cast (vv, xv))
       in
       type_of f g c v
-   | B.Bind (id, B.Abst u, t) ->
+   | B.Bind (l, id, B.Abst u, t) ->
       let f xu xt tt =
-	 f (S.sh2 u xu t xt x (B.bind_abst id)) (B.bind_abst id xu tt)
+	 f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt)
       in
       let f xu cc = b_type_of (f xu) g cc t in
-      let f xu _ = B.push (f xu) c id (B.Abst xu) in
+      let f xu _ = B.push (f xu) c l id (B.Abst xu) in
       type_of f g c u
-   | B.Bind (id, B.Void, t)   ->
+   | B.Bind (l, id, B.Void, t)   ->
       let f xt tt = 
-         f (S.sh1 t xt x (B.bind id B.Void)) (B.bind id B.Void tt)
+         f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt)
       in
       let f cc = b_type_of f g cc t in
-      B.push f c id B.Void   
+      B.push f c l id B.Void   
    | B.Appl (v, t)            ->
       let h xv vv xt tt cc = function
          | R.Sort _ -> error1 "not a function" c xt
 	 | R.Abst w -> 
-            L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w);
+            L.box ();
+	    L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w);
+	    L.unbox ();
 	    let f b =
 	       if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else
 	       error2 "the term" cc xv "must be of type" cc w
diff --git a/helm/software/lambda-delta/basic_ag/brgType.mli b/helm/software/lambda-delta/basic_ag/bagType.mli
similarity index 84%
rename from helm/software/lambda-delta/basic_ag/brgType.mli
rename to helm/software/lambda-delta/basic_ag/bagType.mli
index e7e2d7ed7..24d1f57a2 100644
--- a/helm/software/lambda-delta/basic_ag/brgType.mli
+++ b/helm/software/lambda-delta/basic_ag/bagType.mli
@@ -9,8 +9,8 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-exception TypeError of Brg.message
+exception TypeError of Bag.message
 
 val type_of: 
-   (Brg.term -> Brg.term -> 'a) -> 
-   Hierarchy.graph -> Brg.context -> Brg.term -> 'a
+   (Bag.term -> Bag.term -> 'a) -> 
+   Hierarchy.graph -> Bag.context -> Bag.term -> 'a
diff --git a/helm/software/lambda-delta/basic_ag/brgUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml
similarity index 95%
rename from helm/software/lambda-delta/basic_ag/brgUntrusted.ml
rename to helm/software/lambda-delta/basic_ag/bagUntrusted.ml
index 96be16217..e80a06125 100644
--- a/helm/software/lambda-delta/basic_ag/brgUntrusted.ml
+++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml
@@ -9,9 +9,9 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module B = Brg
-module E = BrgEnvironment
-module T = BrgType
+module B = Bag
+module E = BagEnvironment
+module T = BagType
 
 (* Interface functions ******************************************************)
 
diff --git a/helm/software/lambda-delta/basic_ag/brgUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli
similarity index 91%
rename from helm/software/lambda-delta/basic_ag/brgUntrusted.mli
rename to helm/software/lambda-delta/basic_ag/bagUntrusted.mli
index 92e401e7d..54ae7717c 100644
--- a/helm/software/lambda-delta/basic_ag/brgUntrusted.mli
+++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli
@@ -10,4 +10,4 @@
       V_______________________________________________________________ *)
 
 val type_check:
-   (Brg.term option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a
+   (Bag.term option -> Bag.item -> 'a) -> Hierarchy.graph -> Bag.item -> 'a
diff --git a/helm/software/lambda-delta/basic_ag/brgReduction.ml b/helm/software/lambda-delta/basic_ag/brgReduction.ml
deleted file mode 100644
index 4cfd5260d..000000000
--- a/helm/software/lambda-delta/basic_ag/brgReduction.ml
+++ /dev/null
@@ -1,203 +0,0 @@
-(*
-    ||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 C = Cps
-module S = Share
-module L = Log
-module B = Brg
-module O = BrgOutput
-module E = BrgEnvironment
-
-exception LRefNotFound of B.message
-
-type machine = {
-   c: B.context;
-   s: B.term list
-}
-
-type whd_result =
-   | Sort_ of int
-   | LRef_ of int * B.term option
-   | GRef_ of int * B.bind
-   | Bind_ of B.id * B.term * B.term
-
-type ho_whd_result =
-   | Sort of int
-   | Abst of B.term
-
-(* Internal functions *******************************************************)
-
-let level = 5
-
-let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
-
-let empty_machine = {c = B.empty_context; s = []}
-
-let get f c m i =
-   let f = function
-      | Some (_, b) -> f b
-      | None        -> error i
-   in
-   let f gl _ = if i < gl then B.get f c i else B.get f m.c (i - gl) in
-   B.contents f c 
-
-let contents f c m =
-   let f gl ges = B.contents (f gl ges) m.c in
-   B.contents f c
-
-let unwind_to_context f c m = B.append f c m.c
-
-let unwind_to_term f m t =
-   let map f t (id, b) = f (B.Bind (id, b, t)) in
-   let f _ mc = C.list_fold_left f map t mc in
-   B.contents f m.c
-
-let rec lref_map_bind f map b = match b with
-   | B.Abbr v ->
-      let f v' = f (S.sh1 v v' b B.abbr) in
-      lref_map f map v      
-   | B.Abst w ->
-      let f w' = f (S.sh1 w w' b B.abst) in
-      lref_map f map w
-   | B.Void   -> f b
-
-and lref_map f map t = match t with
-   | B.LRef i          -> f (B.LRef (map i))
-   | B.GRef _          -> f t
-   | B.Sort _          -> f t
-   | B.Cast (w, u)     ->
-      let f w' u' = f (S.sh2 w w' u u' t B.cast) in
-      let f w' = lref_map (f w') map u in 
-      lref_map f map w
-   | B.Appl (w, u)     ->
-      let f w' u' = f (S.sh2 w w' u u' t B.appl) in
-      let f w' = lref_map (f w') map u in 
-      lref_map f map w
-   | B.Bind (id, b, u) ->
-      let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in
-      let f b' = lref_map (f b') map u in 
-      lref_map_bind f map b
-
-(* to share *)
-let lift f c m = 
-   let f gl _ =
-      let map i = if i >= gl then succ i else i in
-      let map f = function
-         | id, B.Abbr t -> let f t = f (id, B.Abbr t) in lref_map f map t
-         | _            -> assert false
-      in
-      let f mc = f {m with c = mc} in
-      B.map f map m.c
-   in
-   B.contents f c
-
-(* to share *)
-let xchg f c m t =
-   let f gl _ ll _ =
-      let map i =
-         if i < gl || i > gl + ll then i else
-         if i >= gl && i < gl + ll then succ i else gl
-      in
-      lref_map f map t
-   in
-   contents f c m
-
-let push f c m id w t = 
-   assert (m.s = []);   
-   let f c m = xchg (f c m) c m t in  
-   let f c = lift (f c) c m in
-   let f w = B.push f c id (B.Abst w) in
-   unwind_to_term f m w
-
-(* to share *)
-let rec whd f c m x = match x with
-   | B.Sort h                 -> f m (Sort_ h)
-   | B.GRef uri               ->
-      let f (i, _, b) = f m (GRef_ (i, b)) in
-      E.get_obj f uri
-   | B.LRef i                 ->
-      let f = function
-         | B.Void   -> f m (LRef_ (i, None))
-	 | B.Abst t -> f m (LRef_ (i, Some t))
-	 | B.Abbr t -> whd f c m t
-      in
-      get f c m i
-   | B.Cast (_, t)            -> whd f c m t
-   | B.Appl (v, t)            -> whd f c {m with s = v :: m.s} t   
-   | B.Bind (id, B.Abst w, t) -> 
-      begin match m.s with
-         | []      -> f m (Bind_ (id, w, t))
-	 | v :: tl -> 
-	    let f mc = whd f c {c = mc; s = tl} t in
-	    B.push f m.c id (B.Abbr (B.Cast (w, v)))
-      end
-   | B.Bind (id, b, t)        -> 
-      let f mc = whd f c {m with c = mc} t in
-      B.push f m.c id b
-
-(* Interface functions ******************************************************)
-
-let rec ho_whd f c m x =
-   let aux m = function
-      | Sort_ h             -> f c (Sort h)
-      | Bind_ (_, w, _)     -> 
-         let f c = f c (Abst w) in unwind_to_context f c m
-      | LRef_ (_, Some w)   -> ho_whd f c m w
-      | GRef_ (_, B.Abst u) -> ho_whd f c m u
-      | GRef_ (_, B.Abbr t) -> ho_whd f c m t
-      | LRef_ (_, None)     -> assert false
-      | GRef_ (_, B.Void)   -> assert false
-   in
-   whd aux c m x
-   
-let ho_whd f c t =
-   L.log O.specs level (L.ct_items1 "Now scanning" c t);
-   ho_whd f c empty_machine t
-
-let rec are_convertible f c1 m1 t1 c2 m2 t2 =
-   let rec aux m1 r1 m2 r2 = match r1, r2 with
-      | Sort_ h1, Sort_ h2                           -> f (h1 = h2)
-      | LRef_ (i1, _), LRef_ (i2, _)                 ->
-         if i1 = i2 then are_convertible_stacks f c1 m1 c2 m2 else f false
-      | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _)   ->
-         if a1 = a2 then are_convertible_stacks f c1 m1 c2 m2 else f false
-      | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
-         if a1 = a2 then are_convertible_stacks f c1 m1 c2 m2 else
-	 if a1 < a2 then whd (aux m1 r1) c2 m2 v2 else
-	 whd (aux_rev m2 r2) c1 m1 v1
-      | _, GRef_ (_, B.Abbr v2)                      ->
-         whd (aux m1 r1) c2 m2 v2
-      | GRef_ (_, B.Abbr v1), _                      ->
-	 whd (aux_rev m2 r2) c1 m1 v1
-      | Bind_ (id1, w1, t1), Bind_ (id2, w2, t2)     ->
-         let f b = 
-	    if b then 
-	       let f c1 m1 t1 = 
-	          push (are_convertible f c1 m1 t1) c2 m2 id2 w2 t2
-	       in
-               push f c1 m1 id1 w1 t1
-	    else f false
-	 in
-	 are_convertible f c1 m1 w1 c2 m2 w2
-      | _                                              -> f false
-   and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
-   let f m1 r1 = whd (aux m1 r1) c2 m2 t2 in 
-   whd f c1 m1 t1
-
-and are_convertible_stacks f c1 m1 c2 m2 =
-   let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
-   let map f v1 v2 = are_convertible f c1 mm1 v1 c2 mm2 v2 in
-   if List.length m1.s <> List.length m2.s then f false else
-   C.forall2 f map m1.s m2.s
-
-let are_convertible f c t1 t2 = 
-   L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2);
-   are_convertible f c empty_machine t1 c empty_machine t2
diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml
index 2e8b2c715..9fc5dc9b2 100644
--- a/helm/software/lambda-delta/lib/cps.ml
+++ b/helm/software/lambda-delta/lib/cps.ml
@@ -46,6 +46,10 @@ let list_rev_map =
 let list_rev =
    list_rev_append ~tail:[]
 
+let list_fold_right f map l a =
+   let map f a m = map f m a in
+   list_rev (list_fold_left f map a) l
+
 let list_map f =
    list_rev_map (list_rev f)
    
diff --git a/helm/software/lambda-delta/toplevel/Make b/helm/software/lambda-delta/toplevel/Make
index 7b8610821..b185d6004 100644
--- a/helm/software/lambda-delta/toplevel/Make
+++ b/helm/software/lambda-delta/toplevel/Make
@@ -1 +1 @@
-meta metaOutput metaAut metaBrg top
+meta metaOutput metaAut metaBag top
diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBag.ml
similarity index 54%
rename from helm/software/lambda-delta/toplevel/metaBrg.ml
rename to helm/software/lambda-delta/toplevel/metaBag.ml
index dfc7e8b56..cf2c009f4 100644
--- a/helm/software/lambda-delta/toplevel/metaBrg.ml
+++ b/helm/software/lambda-delta/toplevel/metaBag.ml
@@ -10,51 +10,58 @@
       V_______________________________________________________________ *)
 
 module C = Cps
-module B = Brg
+module B = Bag
 module M = Meta
 
 (* Internal functions *******************************************************)
 
-let map_fold_left f map1 map2 a l =
-   let f a = C.list_fold_left f map2 a l in
-   map1 f a 
-
-let map_args f t v = f (B.Appl (v, t))
-
-let map_pars f t (id, w) = f (B.Bind (id, B.Abst w, t))
-
-let rec xlate_term f = function
+let rec xlate_term c f = function
    | M.Sort s            -> 
       let f h = f (B.Sort h) in
       if s then f 0 else f 1
-   | M.LRef (l, i)       ->
-      f (B.LRef (l - succ i))
+   | M.LRef (_, i)       ->
+      let l, _, _ = List.nth c i in
+      f (B.LRef l)
    | M.GRef (_, uri, vs) ->
-      let f vs = map_fold_left f C.id map_args (B.GRef uri) vs in
-      C.list_map f xlate_term vs
+      let map f t v = f (B.appl v t) in
+      let f vs = C.list_fold_left f map (B.GRef uri) vs in
+      C.list_map f (xlate_term c) vs
    | M.Appl (v, t)       ->
       let f v t = f (B.Appl (v, t)) in
-      let f v = xlate_term (f v) t in
-      xlate_term f v
+      let f v = xlate_term c (f v) t in
+      xlate_term c f v
    | M.Abst (id, w, t)   ->
-      let f w t = f (B.Bind (id, B.Abst w, t)) in
-      let f w = xlate_term (f w) t in
-      xlate_term f w
+      let f w = 
+         let l = B.new_location () in
+         let f t = f (B.Bind (l, id, B.Abst w, t)) in
+         let f c = xlate_term c f t in
+         B.push f c l id (B.Abst w)
+      in
+      xlate_term c f w
+
+let xlate_pars f pars =
+   let map f (id, w) c =
+      let l = B.new_location () in
+      let f w = B.push f c l id (B.Abst w) in
+      xlate_term c f w
+   in
+   C.list_fold_right f map pars B.empty_context
 
-let xlate_pars f (id, w) =
-   let f w = f (id, w) in
-   xlate_term f w
+let unwind_to_xlate_term f c t =
+   let map f t (l, id, b) = f (B.bind l id b t) in
+   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 f pars = map_fold_left f xlate_term map_pars u pars in      
-      C.list_map f xlate_pars pars
+      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
-      let f pars u = map_fold_left (f u) xlate_term map_pars t pars in      
-      let f pars = map_fold_left (f pars) xlate_term map_pars u pars in
-      C.list_map f xlate_pars pars
+      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_item f = function
    | None   -> f None
@@ -62,4 +69,4 @@ let xlate_item f = function
 
 (* Interface functions ******************************************************)
 
-let brg_of_meta = xlate_item
+let bag_of_meta = xlate_item
diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBag.mli
similarity index 92%
rename from helm/software/lambda-delta/toplevel/metaBrg.mli
rename to helm/software/lambda-delta/toplevel/metaBag.mli
index cb47bc9c1..87e341692 100644
--- a/helm/software/lambda-delta/toplevel/metaBrg.mli
+++ b/helm/software/lambda-delta/toplevel/metaBag.mli
@@ -9,4 +9,4 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val brg_of_meta: (Brg.item -> 'a) -> Meta.item -> 'a
+val bag_of_meta: (Bag.item -> 'a) -> Meta.item -> 'a
diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 06df1ab03..1286db0bb 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -17,22 +17,22 @@ module H    = Hierarchy
 module AO   = AutOutput
 module MA   = MetaAut
 module MO   = MetaOutput
-module MBrg = MetaBrg
-module BrgO = BrgOutput
-module BrgU = BrgUntrusted
+module MBag = MetaBag
+module BagO = BagOutput
+module BagU = BagUntrusted
 
 type status = {
    mst : MA.status;
    ac  : AO.counters;
    mc  : MO.counters;
-   brgc: BrgO.counters
+   bagc: BagO.counters
 }
 
 let initial_status = {
-   ac = AO.initial_counters;
-   mc = MO.initial_counters;
-   brgc= BrgO.initial_counters;
-   mst = MA.initial_status
+   ac   = AO.initial_counters;
+   mc   = MO.initial_counters;
+   bagc = BagO.initial_counters;
+   mst  = MA.initial_status
 }
 
 let count count_fun c item =
@@ -40,8 +40,8 @@ let count count_fun c item =
 
 let flush () = L.flush (); L.flush_err ()
 
-let brg_error s msg =
-   L.error BrgO.specs (L.Warn s :: msg); flush () 
+let bag_error s msg =
+   L.error BagO.specs (L.Warn s :: msg); flush () 
 
 let main =
 try 
@@ -90,8 +90,8 @@ try
 	    in
 (* stage 2 *)	    
 	    let f st item =
-	       let st = {st with brgc = count BrgO.count_item st.brgc item} in
-	       if !stage > 2 then BrgU.type_check (f st) !H.graph item else st
+	       let st = {st with bagc = count BagO.count_item st.bagc item} in
+	       if !stage > 2 then BagU.type_check (f st) !H.graph item else st
 	    in
 (* stage 1 *)	    
 	    let f mst item = 
@@ -102,7 +102,7 @@ try
 	          | None          -> ()
 		  | Some (_, frm) -> MO.pp_item C.start frm item
 	       end;
-	       if !stage > 1 then MBrg.brg_of_meta (f st) item else st 
+	       if !stage > 1 then MBag.bag_of_meta (f st) item else st 
 	    in  
 (* stage 0 *)	    
             let st = {st with ac = count AO.count_item st.ac item} in
@@ -115,7 +115,7 @@ try
       if !L.level > 0 then Time.utime_stamp "processed";
       if !L.level > 2 then AO.print_counters C.start st.ac;
       if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
-      if !L.level > 2 && !stage > 1 then BrgO.print_counters C.start st.brgc;
+      if !L.level > 2 && !stage > 1 then BagO.print_counters C.start st.bagc;
    in
    let help = 
       "Usage: helena [ -Vi | -Ss <number> | -m <file> | -h <string> ] <file> ...\n\n" ^
@@ -135,10 +135,10 @@ try
       ("-S", Arg.Int set_summary, help_S);
       ("-V", Arg.Unit print_version, help_V);
       ("-h", Arg.String set_hierarchy, help_h);
-      ("-i", Arg.Set BrgO.indexes, help_i);
+      ("-i", Arg.Set BagO.indexes, help_i);
       ("-m", Arg.String set_meta_file, help_m); 
       ("-s", Arg.Int set_stage, help_s);
    ] read_file help;
    if !L.level > 0 then Time.utime_stamp "at exit";
    flush ()
-with BrgType.TypeError msg -> brg_error "Type Error" msg
+with BagType.TypeError msg -> bag_error "Type Error" msg
-- 
2.39.2