From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 20 Nov 2014 16:02:51 +0000 (+0000)
Subject: new intermediate language complete_rg,
X-Git-Tag: make_still_working~796
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=251534dbf294c645d2121df2d9ce240011fa0c91;p=helm.git

new intermediate language complete_rg,
more similar to what lambdadelta version 4 should be
---

diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt
index b2015af33..22608ffa0 100644
--- a/helm/software/helena/.depend.opt
+++ b/helm/software/helena/.depend.opt
@@ -41,11 +41,11 @@ 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 \
-    src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+    src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/complete_rg/crgOutput.cmi
 src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \
-    src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
-    src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+    src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+    src/complete_rg/crgOutput.cmi
 src/text/txt.cmo: src/common/level.cmi
 src/text/txt.cmx: src/common/level.cmx
 src/text/txtParser.cmi: src/text/txt.cmx
diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index dfd51aa47..025459d2e 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -44,12 +44,12 @@ let hcnt = K.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
-let empty_cnt = [], []
+let empty_cnt = D.ESort
 
-let add_abst (a, ws) id w = 
-   E.Name (id, true) :: a, w :: ws 
+let add_abst cnt id w = 
+   D.EBind (cnt, [E.Name (id, true)], D.Abst (N.infinite, w)) 
 
-let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
+let mk_lref f i = f (D.TLRef ([], i))
 
 let id_of_name (id, _, _) = id
 
@@ -82,7 +82,7 @@ let relax_opt_qid f st = function
    | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
 
 let resolve_gref err f st qid =
-   try let cnt = K.find henv (uri_of_qid qid) in f qid cnt
+   try let age, cnt = K.find henv (uri_of_qid qid) in f qid age cnt
    with Not_found -> err qid 
 
 let resolve_gref_relaxed f st qid =
@@ -101,15 +101,16 @@ let get_cnt_relaxed f st =
    let rec err node = relax_opt_qid (get_cnt err f st) st node in
    get_cnt err f st st.node
 
-(****************************************************************************)
+let push_abst f a w lenv =
+   let bw = D.Abst (N.infinite, w) in
+   D.push_bind f a bw lenv
 
-let push_abst f lenv a w =
-   let bw = D.Abst (N.infinite, [w]) in
-   let f lenv = f lenv in
-   D.push_bind f lenv a bw
+let add_proj e t = match e with
+   | D.ESort                 -> t
+   | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t) 
+   | _                       -> D.TProj ([], e, t)
 
-let lenv_of_cnt (a, ws) = 
-   D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws))
+let lenv_of_cnt cnt = cnt
 
 (* this is not tail recursive in the GRef branch *)
 let rec xlate_term f st lenv = function
@@ -117,36 +118,38 @@ let rec xlate_term f st lenv = function
       let f h = f (D.TSort ([], h)) in
       if s then f 0 else f 1
    | A.Appl (v, t)       ->
-      let f vv tt = f (D.TAppl ([], [vv], tt)) in
+      let f vv tt = f (D.TAppl ([], vv, tt)) in
       let f vv = xlate_term (f vv) st lenv t in
       xlate_term f st lenv v
    | A.Abst (name, w, t) ->
       let f ww = 
          let a = [E.Name (name, true)] in
 	 let f tt =
-	    let b = D.Abst (N.infinite, [ww]) in
+	    let b = D.Abst (N.infinite, ww) in
 	    f (D.TBind (a, b, tt))
 	 in
          let f lenv = xlate_term f st lenv t in
-	 push_abst f lenv a ww
+	 push_abst f a ww lenv
       in
       xlate_term f st lenv w
    | A.GRef (name, args) ->
-      let map1 f = function
-	    | E.Name (id, _) -> f (A.GRef ((id, true, []), []))
-	    | _              -> C.err ()
+      let map1 args a =
+         let f id _ = A.GRef ((id, true, []), []) :: args in
+         E.name C.err f a
       in
-      let map2 f t = xlate_term f st lenv t in
-      let g qid (a, _) =
-         let gref age = D.TGRef ([age], uri_of_qid qid) in
-	 match args, a with
-	    | [], [age]    -> f (gref age)
-	    | _ , age :: a ->
-	       let f args = f (D.TAppl ([], args, gref age)) in
-	       let f args = C.list_rev_map f map2 args in
-	       let f a = C.list_rev_map_append f map1 a ~tail:args in
-	       C.list_sub_strict f a args
-            | _             -> assert false
+      let map2 f arg args = 
+         let f arg = f (D.EAppl (args, [], arg)) in 
+         xlate_term f st lenv arg
+      in
+      let g qid age cnt =
+         let gref = D.TGRef ([age], uri_of_qid qid) in
+	 if cnt = D.ESort then f gref else
+	 let f = function 
+            | D.EAppl (D.ESort, a, v) -> f (D.TAppl (a, v, gref))
+            | args                    -> f (D.TProj ([], args, gref))
+         in
+	 let f args = C.list_fold_right f map2 args D.ESort in
+	 D.sub_list_strict (D.fold_attrs f map1 args) cnt args
       in
       let g qid = resolve_gref_relaxed g st qid in
       let err () = complete_qid g st name in
@@ -169,28 +172,23 @@ let xlate_entity err f st = function
    | A.Block (name, w)         ->
       let f qid = 
          let f cnt =
-	    let lenv = lenv_of_cnt cnt in
 	    let f ww = 
 	       K.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
 	       err {st with node = Some qid}
 	    in
-	    xlate_term f st lenv w
+	    xlate_term f st cnt w
 	 in
          get_cnt_relaxed f st
       in
       complete_qid f st (name, true, [])
    | A.Decl (name, w)          ->
       let f cnt =
-         let a, ws = cnt in
          let lenv = lenv_of_cnt cnt in
 	 let f qid = 
             let f ww =
                let age = E.Apix st.line in
-               K.add henv (uri_of_qid qid) (age :: a, ws);
-	       let t = match ws with
-	          | [] -> ww
-	          | _  -> D.TBind (a, D.Abst (N.infinite, ws), ww)
-	       in
+               K.add henv (uri_of_qid qid) (age, cnt);
+	       let t = add_proj lenv ww in
 (*
 	    print_newline (); CrgOutput.pp_term print_string t;
 *)
@@ -204,18 +202,14 @@ let xlate_entity err f st = function
       in
       get_cnt_relaxed f st
    | A.Def (name, w, trans, v) ->
-      let f cnt = 
-	 let a, ws = cnt in
+      let f cnt =
 	 let lenv = lenv_of_cnt cnt in
          let f qid = 
             let f ww =
 	       let f vv =
                   let age = E.Apix st.line in
-                  K.add henv (uri_of_qid qid) (age :: a, ws);
-                  let t = match ws with
-	             | [] -> D.TCast ([], ww, vv)
-	             | _  -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv))
-	          in
+                  K.add henv (uri_of_qid qid) (age, cnt);
+                  let t = add_proj lenv (D.TCast ([], ww, vv)) in
 (*
 	    print_newline (); CrgOutput.pp_term print_string t;
 *)
diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml
index fc0f72f9a..5e7c07b5b 100644
--- a/helm/software/helena/src/basic_ag/bag.ml
+++ b/helm/software/helena/src/basic_ag/bag.ml
@@ -30,7 +30,7 @@ and term = Sort of int                       (* hierarchy index *)
 
 type entity = term E.entity (* attrs, uri, binder *)
 
-type lenv = (attrs * int * bind) list (* location, name, binder *) 
+type lenv = (attrs * int * bind) list (* name, location, binder *) 
 
 type message = (lenv, term) Log.item list
 
diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml
index 8fbf7cf79..1bd594503 100644
--- a/helm/software/helena/src/basic_ag/bagCrg.ml
+++ b/helm/software/helena/src/basic_ag/bagCrg.ml
@@ -18,56 +18,41 @@ module Z = Bag
 
 (* internal functions: crg to bag term **************************************)
 
-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 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 rec xlate_term f c = function
+   | D.TSort (_, h)    -> f (Z.Sort h)
+   | D.TGRef (_, s)    -> f (Z.GRef s)
+   | D.TLRef (a, i)    ->
+      let _, l, _ = List.nth c i in f (Z.LRef l)
+   | 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 xlate_bind f c t
-   | D.TProj (_, e, t)  ->
-      xlate_term xlate_bind f c (D.tshift e t)
+      let f tt = xlate_term (f tt) c u in
+      xlate_term f c t
+   | D.TAppl (_, v, t) ->
+      let f tt vv = f (Z.Appl (vv, tt)) in
+      let f tt = xlate_term (f tt) c v in
+      xlate_term f c t
+   | D.TProj (_, e, t) ->
+      D.shift (xlate_term f c) e t
 (* this case should be removed by improving alpha-conversion *)
    | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
-      xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
-   | D.TBind (a, b, t)  ->
-      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
-
-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
+      xlate_term 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 cc =
+         let a, l, b = List.hd cc in
+         let f tt = f (Z.Bind (a, l, b, tt)) in
+         xlate_term f cc t
       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
+      xlate_bind f c a b
+
+and xlate_bind f c a = function
+   | D.Abst (_, w) ->
+      let f ww = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abst ww) in 
+      xlate_term f c w
+   | D.Abbr v      -> 
+      let f vv = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abbr vv) in
+      xlate_term f c v
+   | D.Void        ->
+      Z.push "xlate_bind" f c a (J.new_location ()) Z.Void
 
 (* internal functions: bag to crg term **************************************)
 
@@ -75,14 +60,14 @@ 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
+       let f i = f (D.TLRef ([], i)) 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 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) ->
@@ -93,16 +78,16 @@ let rec xlate_bk_term f c = function
 
 and xlate_bk_bind f c = function
    | Z.Abst t ->
-      let f tt = f (D.Abst (N.infinite, [tt])) in
+      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
+      let f tt = f (D.Abbr tt) in
       xlate_bk_term f c t
-   | Z.Void   -> f (D.Void 1)
+   | Z.Void   -> f D.Void
 
 (* interface functions ******************************************************)
 
 let bag_of_crg f t =
-   xlate_term xlate_bind f Z.empty_lenv t
+   xlate_term f Z.empty_lenv t
 
 let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t 
diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml
index 8514de641..f646145ed 100644
--- a/helm/software/helena/src/basic_rg/brgCrg.ml
+++ b/helm/software/helena/src/basic_rg/brgCrg.ml
@@ -21,52 +21,42 @@ module B = Brg
 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.TLRef (a, i)     -> f (B.LRef (a, i))
    | D.TCast (a, u, t)  ->
       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.TAppl (a, v, t) ->
+      let f tt vv = f (B.Appl (a, vv, tt)) in
+      let f tt = xlate_term (f tt) v in
+      xlate_term f t 
    | D.TProj (_, e, t)  -> 
-      xlate_term f (D.tshift e t)
-   | D.TBind (a, b, t)  ->
-      let f tt = f (xlate_bind tt a b) in xlate_term f t
+      D.shift (xlate_term f) e t
+   | D.TBind (a, b, t)  -> 
+      xlate_term (xlate_bind f a b) 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 = B.Bind (n :: J.new_mark () :: a, B.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 = B.Bind (n :: a, B.Abbr vv, x) in 
-	    xlate_term f v
-	 in
-	 List.fold_left2 map x ns vs
-      | D.Void _       ->
-         let map x n = B.Bind (n :: a, B.Void, x) in
-	 List.fold_left map x ns
+and xlate_bind f a b x = match b with
+   | D.Abst (n, w) ->
+      let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in 
+      xlate_term f w
+   | D.Abbr v      ->
+      let f vv = f (B.Bind (a, B.Abbr vv, x)) in 
+      xlate_term f v
+   | D.Void        ->
+      f (B.Bind (a, B.Void, x))
 
 (* internal functions: brg to crg term **************************************)
 
 let rec xlate_bk_term f = function
    | B.Sort (a, l)     -> f (D.TSort (a, l))
    | B.GRef (a, n)     -> f (D.TGRef (a, n))
-   | B.LRef (a, i)     -> f (D.TLRef (a, i, 0))
+   | B.LRef (a, i)     -> f (D.TLRef (a, i))
    | B.Cast (a, u, t)  ->
       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 tt uu = f (D.TAppl (a, [uu], tt)) in
+      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)  ->
@@ -76,12 +66,12 @@ let rec xlate_bk_term f = function
 
 and xlate_bk_bind f = function
    | B.Abst (n, t) ->
-      let f tt = f (D.Abst (n, [tt])) in
+      let f tt = f (D.Abst (n, tt)) in
       xlate_bk_term f t
    | B.Abbr t      ->
-      let f tt = f (D.Abbr [tt]) in
+      let f tt = f (D.Abbr tt) in
       xlate_bk_term f t
-   | B.Void        -> f (D.Void 1)
+   | B.Void        -> f D.Void
    
 (* interface functions ******************************************************)
 
diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index c3ef9795b..09e262d12 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -181,7 +181,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
          let e2 = E.apix C.err C.start a2 in
 	 if e1 = e2 then ac_stacks st m1 m2 else false
       | B.GRef (_, u1), None, B.GRef (_, u2), None          ->
-	 if U.eq u1 u2 & assert_iterations m1 m2 then ac_stacks st m1 m2 else false
+	 if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
       | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2  ->
          let e1 = E.apix C.err C.start a1 in
          let e2 = E.apix C.err C.start a2 in
@@ -191,7 +191,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
 	 end else if e2 < e1 then begin
 	    if !G.summary then O.add ~gdelta:1 ();
 	    ac_nfs st (step st m1 v1) (m2, t2, r2) 
-         end else if U.eq u1 u2 & assert_iterations m1 m2 && ac_stacks st m1 m2 then true
+         end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
          else begin
 	    if !G.summary then O.add ~gdelta:2 ();
 	    ac st m1 v1 m2 v2
diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml
index 9518ff60b..7ba80ddfb 100644
--- a/helm/software/helena/src/complete_rg/crg.ml
+++ b/helm/software/helena/src/complete_rg/crg.ml
@@ -20,44 +20,76 @@ type uri = E.uri
 type id = E.id
 type attrs = E.attrs
 
-type bind = Abst of N.level * term list (* level, domains *)
-          | Abbr of term list           (* bodies *)
-          | Void of int                 (* number of exclusions *)
-
-and term = TSort of attrs * int              (* attrs, hierarchy index *)
-         | TLRef of attrs * int * int        (* attrs, position indexes *)
-         | TGRef of attrs * uri              (* attrs, reference *)
-         | TCast of attrs * term * term      (* attrs, domain, element *)
-         | TAppl of attrs * term list * term (* attrs, arguments, function *)
-	 | TProj of attrs * lenv * term      (* attrs, closure, member *)
-	 | TBind of attrs * bind * term      (* attrs, binder, scope *)
+type bind = Abst of N.level * term      (* level, type *)
+          | Abbr of term                (* body *)
+          | Void                        (* *)
+
+and term = TSort of attrs * int         (* attrs, hierarchy index *)
+         | TLRef of attrs * int         (* attrs, position indexe *)
+         | TGRef of attrs * uri         (* attrs, reference *)
+         | TCast of attrs * term * term (* attrs, domain, element *)
+         | TAppl of attrs * term * term (* attrs, argument, function *)
+	 | TBind of attrs * bind * term (* attrs, binder, scope *)
+	 | TProj of attrs * lenv * term (* attrs, closure, member *)
 
 and lenv = ESort                        (* top *)
-         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
          | EBind of lenv * attrs * bind (* environment, attrs, binder *)
+         | EAppl of lenv * attrs * term (* environment, attrs, argument *)
+         | EProj of lenv * attrs * lenv (* environment, attrs, closure *) 
 
 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 empty_lenv = ESort
 
-let tshift c t = tshift t c
+let push_bind f a b lenv = f (EBind (lenv, a, b))
 
-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 push_appl f a t lenv = f (EAppl (lenv, a, t))
 
-let empty_lenv = ESort
+let push_proj f a e lenv = f (EProj (lenv, a, e))
+
+let add_bind f a b t = f (TBind (a, b, t))
+
+let add_appl f a v t = f (TAppl (a, v, t))
 
-let push_bind f lenv a b = f (EBind (lenv, a, b))
+let add_proj f a e t = f (TProj (a, e, t))
 
-let push_proj f lenv a e = f (EProj (lenv, a, e))
+let rec shift f c t = match c with
+   | ESort           -> f t
+   | EBind (e, a, b) -> add_bind (shift f e) a b t
+   | EAppl (e, a, v) -> add_appl (shift f e) a v t
+   | EProj (e, a, d) -> add_proj (shift f e) a d t
+
+let rec append f c = function
+   | ESort           -> f c
+   | EBind (e, a, b) -> append (push_bind f a b) c e
+   | EAppl (e, a, t) -> append (push_appl f a t) c e
+   | EProj (e, a, d) -> append (push_proj f a d) c e
+
+let resolve_lref err f id lenv =
+   let rec aux i = function
+     | ESort             -> err ()
+     | EAppl (tl, _, _)  -> aux i tl
+     | EBind (tl, a, _)  ->
+        let f id0 _ = if id0 = id then f i else aux (succ i) tl in
+        E.name err f a 
+     | EProj (tl, _, d)  -> append (aux i) tl d
+   in
+   aux 0 lenv
+
+let rec get_name err f i = function
+   | ESort                      -> err i
+   | EAppl (tl, _, _)           -> get_name err f i tl
+   | EBind (_, a, _) when i = 0 -> 
+      let err () = err i in
+      E.name err f a
+   | EBind (tl, _, _)           -> get_name err f (pred i) tl
+   | EProj (tl, _, e)           ->
+      let err i = get_name err f i tl in 
+      get_name err f i e
 
+(*
 let push2 err f lenv ?attr ?t () = match lenv, attr, t with
    | EBind (e, a, Abst (n, ws)), Some attr, Some t -> 
       f (EBind (e, (attr :: a), Abst (n, t :: ws)))
@@ -73,35 +105,6 @@ let push2 err f lenv ?attr ?t () = match lenv, attr, t with
       f (EBind (e, a, Void (succ n)))
    | _                                             -> err ()
 
-(* this id not tail recursive *)
-let resolve_lref err f id lenv =
-   let rec aux f i k = function
-     | ESort                  -> err ()
-     | EBind (tl, _, Abst (_, []))
-     | EBind (tl, _, Abbr [])
-     | EBind (tl, _, Void 0)  -> aux f i k tl
-     | EBind (tl, a, b)       ->
-	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 (tl, _, d)       -> aux f i k (eshift C.start tl d)
-   in
-   aux f 0 0 lenv
-
-let rec get_name err f i j = function
-   | ESort                      -> err i
-   | EBind (tl, _, Abst (_, []))
-   | EBind (tl, _, Abbr [])
-   | EBind (tl, _, Void 0)      -> get_name err f i j tl
-   | EBind (_, a, _) when i = 0 -> 
-      let err () = err i in
-      E.get_name err f j a
-   | EBind (tl, _, _)           -> 
-      get_name err f (pred i) j tl
-   | EProj (tl, _, e)           ->
-      let err i = get_name err f i j tl in 
-      get_name err f i j e
-
 let get_index err f i j lenv =
    let rec aux f i k = function
       | ESort                      -> err i
@@ -115,19 +118,26 @@ let get_index err f i j lenv =
       | EProj (tl, _, d)           -> aux f i k (eshift C.start tl d)
    in
    aux f i 0 lenv
-
+*)
 let rec names_of_lenv ns = function
    | ESort            -> ns
    | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
+   | EAppl (tl, _, _) -> names_of_lenv ns tl
    | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
 
-let rec get i = function
-   | ESort                      -> ESort, [], Void 0 
-   | EBind (e, _, Abst (_, []))
-   | EBind (e, _, Abbr [])
-   | EBind (e, _, Void 0)       -> get i e
+let rec get e i = match e with 
+   | ESort                      -> ESort, [], Void
    | EBind (e, a, b) when i = 0 -> e, a, b
-   | EBind (e, _, _)            -> get (pred i) e
-   | EProj (e, _, d)            -> get i (eshift C.start e d)
- 
-let get e i = get i e
+   | EBind (e, _, _)            -> get e (pred i)
+   | EAppl (e, _, _)            -> get e i
+   | EProj (e, _, d)            -> get (append C.start e d) i
+
+let rec sub_list_strict f e l = match e, l with
+   | _, []                         -> f e
+   | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
+   | _                             -> assert false
+
+let rec fold_attrs f map a0 = function
+   | ESort                -> f a0
+   | EBind (e, a, Abst _) -> fold_attrs f map (map a0 a) e
+   | _                    -> assert false
diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 49acbb49b..d5f639b39 100644
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -13,7 +13,6 @@ module P = Printf
 module U = NUri
 module C = Cps
 module L = Log
-module H = Hierarchy
 module E = Entity
 module N = Level
 module D = Crg
@@ -49,11 +48,11 @@ let initial_counters = {
 let rec count_term f c e = function
    | D.TSort _          -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | D.TLRef (_, i, j)  -> 
+   | D.TLRef (_, i)     -> 
       begin match D.get e i with
-	 | _, _, D.Abbr vs when j < List.length vs ->
+	 | _, _, D.Abbr _ ->
 	    f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
-	 | _                                       ->
+	 | _              ->
 	    f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
       end      
    | D.TGRef (_, u)     -> 
@@ -67,40 +66,28 @@ let rec count_term f c e = function
       let c = {c with tcasts = succ c.tcasts} in
       let f c = count_term f c e t in
       count_term f c e v
-   | D.TAppl (_, vs, t) -> 
-      let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
+   | D.TAppl (_, v, t)  -> 
+      let c = {c with tappls = succ c.tappls} in
       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 (D.tshift d t)
+      count_term f c e v
+   | D.TProj (_, d, t)  ->
+      D.shift (count_term f c e) 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
 
-and count_binder f c e a = function
-   | D.Abst (n, ws) ->      
-      let k = List.length ws in
-      let c = {c with tabsts = c.tabsts + k; nodes = c.nodes + k} in
-      let e = D.push_bind C.start e a (D.Abst (n, [])) in
-      let f (c, e) = f c e in
-      C.list_fold_right f map2 ws (c, e)
-   | D.Abbr vs      -> 
-      let k = List.length vs in
-      let c = {c with tabbrs = c.tabbrs + k; xnodes = c.xnodes + k} in
-      let e = D.push_bind C.start e a (D.Abbr []) in
-      let f (c, e) = f c e in
-      C.list_fold_right f map2 vs (c, e)
-   | D.Void k       ->
-      let c = {c with tvoids = c.tvoids + k; xnodes = c.xnodes + k} in   
-      let e = D.push_bind C.start e a (D.Void k) in
-      f c e
-
-and map1 e f t c = count_term f c e t
-
-and map2 f t (c, e) =
-   let f c e = f (c, e) in
-   let f c = D.push2 C.err (f c) e ~t () in
-   count_term f c e t
+and count_binder f c e a b = match b with
+   | D.Abst (_, w) ->
+      let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
+      let f c = D.push_bind (f c) a b e in
+      count_term f c e w
+   | D.Abbr v      -> 
+      let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
+      let f c = D.push_bind (f c) a b e in
+      count_term f c e v     
+   | D.Void        ->
+      let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
+      D.push_bind (f c) a b e
 
 let count_entity f c = function
    | _, u, E.Abst (_, w) -> 
@@ -151,29 +138,22 @@ let pp_attrs out a =
 
 let rec pp_term out = function
    | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
-   | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
+   | D.TLRef (a, i   ) -> pp_attrs out a; out (P.sprintf "#%u" i)
    | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
    | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
-   | D.TProj (a, x, y) -> assert false
-   | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
-   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
-
-and pp_terms bg eg out vs =
-   let rec aux = function
-      | []      -> ()
-      | [v]     -> pp_term out v
-      | v :: vs -> pp_term out v; out ", "; aux vs
-   in
-   out bg; aux vs; out (eg ^ ".")
+   | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out x; out ")."; pp_term out y
+   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; out "."; pp_term out y
+   | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out x; out "}."; pp_term out y
 
 and pp_bind out = function
-   | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x
-   | D.Abst (n, x)                      -> 
-      pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x
-   | D.Abbr x                           -> pp_terms "[=" "]" out x
-   | D.Void x                           -> out (P.sprintf "[%u]" x)
+   | D.Abst (n, x) ->
+      out "[:"; pp_term out x; out "]";
+      if N.is_infinite n then () else out (N.to_string n)  
+   | D.Abbr x      -> out "[="; pp_term out x; out "]";
+   | D.Void        -> out "[]"
 
-let rec pp_lenv out = function
+and pp_lenv out = function
    | D.ESort           -> ()
-   | D.EProj (x, a, y) -> assert false
    | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
+   | D.EAppl (x, a, y) -> pp_lenv out x; out "("; pp_term out y; out ")"
+   | D.EProj (x, a, y) -> pp_lenv out x; out "{"; pp_lenv out y; out "}"
diff --git a/helm/software/helena/src/lib/cps.ml b/helm/software/helena/src/lib/cps.ml
index f993ffb04..0ce60a8f0 100644
--- a/helm/software/helena/src/lib/cps.ml
+++ b/helm/software/helena/src/lib/cps.ml
@@ -20,6 +20,10 @@ let rec list_sub_strict f l1 l2 = match l1, l2 with
    | _ :: tl1, _ :: tl2 -> list_sub_strict f tl1 tl2
    | _                  -> assert false
 
+let rec list_fold f map a = function
+   | []       -> f a
+   | hd :: tl -> list_fold f map (map a hd) tl
+
 (* this is not tail recursive *)
 let rec list_fold_left f map a = function
    | []       -> f a
diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml
index ce3853fcb..a6839b89c 100644
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -32,7 +32,7 @@ let henv = Hashtbl.create henv_size (* optimized global environment *)
 (* Internal functions *******************************************************)
 
 let name_of_id ?(r=true) id = E.Name (id, r)
-
+(*
 let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
 
 let mk_gref f uri = f (D.TGRef ([], uri))
@@ -151,7 +151,7 @@ let xlate_entity err f gen st = function
       err st
 
 (* Interface functions ******************************************************)
-
+*)
 let initial_status () =
    Hashtbl.clear henv; {
    path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
@@ -161,4 +161,4 @@ let refresh_status st = {st with
    mk_uri = G.get_mk_uri ()
 }
 
-let crg_of_txt = xlate_entity
+let crg_of_txt _ _ = assert false (* xlate_entity *)
diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index c11614af5..ce14855e0 100644
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -19,33 +19,20 @@ module D  = Crg
 
 (* internal functions *******************************************************)
 
-let rec list_iter map l out tab = match l with
-   | []       -> ()
-   | hd :: tl -> map hd out tab; list_iter map tl out tab
-
-let list_rev_iter map e ns l out tab =
-   let rec aux err f e = function
-      | [], []            -> f e
-      | n :: ns, hd :: tl -> 
-        let f e =
-(*	
-           pp_lenv print_string e; print_string " |- "; 
-	   pp_term print_string hd; print_newline ();
-*)
-	   map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ())
-	in
-	aux err f e (ns, tl) 
-      | _                 -> err ()
+let lenv_iter map_bind map_appl map_proj e lenv out tab = 
+   let rec aux = function
+      | D.ESort           -> e
+      | D.EBind (e, a, b) -> 
+         let e = aux e in
+         map_bind e a b out tab; D.EBind (e, a, b)
+      | D.EAppl (e, a, v) ->
+         let e = aux e in
+         map_appl e a v out tab; D.EAppl (e, a, v)
+      | D.EProj (e, a, d) ->
+         let e = aux e in
+         map_proj e a d out tab; D.EProj (e, a, d)
    in
-   ignore (aux C.err C.start e (ns, l))
-
-let lenv_iter map1 map2 l out tab = 
-   let rec aux f = function
-      | D.ESort              -> f ()
-      | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
-      | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
-   in 
-   aux C.start l
+   ignore (aux lenv)
 
 let rec exp_term e t out tab = match t with
    | D.TSort (a, l)       ->
@@ -56,13 +43,13 @@ let rec exp_term e t out tab = match t with
       in
       let attrs = [XL.position l; XL.name a] in
       XL.tag XL.sort attrs out tab
-   | D.TLRef (a, i, j)    ->
+   | D.TLRef (a, i)       ->
       let a = 
          let err _ = a in
 	 let f n r = Y.Name (n, r) :: a in
-         D.get_name err f i j e
+         D.get_name err f i e
       in
-      let attrs = [XL.position i; XL.offset j; XL.name a] in
+      let attrs = [XL.position i; XL.name a] in
       XL.tag XL.lref attrs out tab
    | D.TGRef (a, n)       ->
       let a = Y.Name (U.name_of_uri n, true) :: a in
@@ -72,39 +59,38 @@ let rec exp_term e t out tab = match t with
       let attrs = [] in
       XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
       exp_term e t out tab
-   | D.TAppl (a, vs, t)   ->
-      let attrs = [XL.arity vs] in
-      XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+   | D.TAppl (a, v, t)    ->
+      let attrs = [] in
+      XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
       exp_term e t out tab
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
-      XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
-      exp_term (D.push_proj C.start e a lenv) t out tab
+      XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab;
+      exp_term (D.push_proj C.start a lenv e) t out tab
    | D.TBind (a, b, t) ->
 (* NOTE: the inner binders are alpha-converted first *)
       let a = R.alpha (D.names_of_lenv [] e) a in
       exp_bind e a b out tab; 
-      exp_term (D.push_bind C.start e a b) t out tab 
+      exp_term (D.push_bind C.start a b e) t out tab 
+
+and exp_appl e a v out tab =
+   let attrs = [] in
+   XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
 
-and exp_bind e a b out tab = 
-   let f a ns = a, ns in
-   let a, ns = Y.get_names f a in 
-   match b with
-      | D.Abst (n, ws) ->
-	 let e = D.push_bind C.start e a (D.Abst (n, [])) in
-	 let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
-         XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
-      | D.Abbr vs      ->
-         let e = D.push_bind C.start e a (D.Abbr []) in
-         let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
-         XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
-      | D.Void n       ->
-         let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in
-         XL.tag XL.void attrs out tab
+and exp_bind e a b out tab = match b with
+   | D.Abst (n, w) ->
+      let attrs = [XL.level n; XL.name a; XL.mark a] in
+      XL.tag XL.abst attrs ~contents:(exp_term e w) out tab
+   | D.Abbr v      ->
+      let attrs = [XL.name a] in
+      XL.tag XL.abbr attrs ~contents:(exp_term e v) out tab
+   | D.Void        ->
+      let attrs = [XL.name a] in
+      XL.tag XL.void attrs out tab
 
-and exp_eproj e a lenv out tab =
+and exp_proj e a lenv out tab =
    let attrs = [] in
-   XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab
 
 (* interface functions ******************************************************)
 
diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index a7f5ae29a..e182ab9a3 100644
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -92,21 +92,9 @@ 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 l =
-   let n = match n with 
-      | None   -> List.length l
-      | Some n -> n   
-   in
-   let contents = if n > 1 then string_of_int n else "" in
-   "arity", contents
-
 let name a =
    let map f i n r s =
       let n = if r then n else "-" ^ n in 
@@ -140,6 +128,9 @@ let meta a =
    let f ms = "meta", String.concat " " (List.rev_map map ms) in
    E.meta err f a
 
+let arity l =
+   "arity", string_of_int (List.length l)
+
 (* TODO: the string tx must be quoted *)
 let info a =
    let err () = ["lang", ""; "info", ""] in
diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli
index 7b3a476c3..9db373c47 100644
--- a/helm/software/helena/src/xml/xmlLibrary.mli
+++ b/helm/software/helena/src/xml/xmlLibrary.mli
@@ -41,12 +41,8 @@ val void: string
 
 val position: int -> attr
 
-val offset: int -> attr
-
 val uri: Entity.uri -> attr
 
-val arity: ?n:int -> 'a list -> attr
-
 val level: Level.level -> attr
 
 val name: Entity.attrs -> attr