From 8659e85d49be1ad72622d4d3a73d384b744c3c08 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 10 Dec 2008 21:25:21 +0000
Subject: [PATCH] - new semantic log system - new brg terms - bug fix im
 MetaOutput and MetaBrg

---
 helm/software/lambda-delta/.depend.opt        |  51 ++++----
 helm/software/lambda-delta/Makefile           |  12 ++
 helm/software/lambda-delta/Makefile.common    |   4 -
 helm/software/lambda-delta/basic_rg/Make      |   2 +-
 helm/software/lambda-delta/basic_rg/brg.ml    |  24 ++--
 .../lambda-delta/basic_rg/brgEnvironment.ml   |   4 +-
 .../lambda-delta/basic_rg/brgOutput.ml        |  69 +++++++++--
 .../lambda-delta/basic_rg/brgOutput.mli       |   2 +
 .../lambda-delta/basic_rg/brgReduction.ml     | 117 ++++++++++--------
 .../lambda-delta/basic_rg/brgReduction.mli    |  10 +-
 .../software/lambda-delta/basic_rg/brgType.ml |  81 ++++++++----
 .../lambda-delta/basic_rg/brgType.mli         |   2 +-
 .../lambda-delta/basic_rg/brgUntrusted.ml     |   7 +-
 helm/software/lambda-delta/lib/cps.ml         |   3 +
 helm/software/lambda-delta/lib/log.ml         |  39 ++++++
 helm/software/lambda-delta/lib/log.mli        |  22 ++++
 helm/software/lambda-delta/lib/share.ml       |   7 +-
 .../software/lambda-delta/toplevel/metaBrg.ml |  16 +--
 .../lambda-delta/toplevel/metaOutput.ml       |   5 +-
 helm/software/lambda-delta/toplevel/top.ml    |  49 ++++----
 20 files changed, 353 insertions(+), 173 deletions(-)

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 418d35ef0..7e884babc 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -1,7 +1,7 @@
 lib/nUri.cmo: lib/nUri.cmi 
 lib/nUri.cmx: lib/nUri.cmi 
-lib/log.cmo: lib/log.cmi 
-lib/log.cmx: lib/log.cmi 
+lib/log.cmo: lib/cps.cmx lib/log.cmi 
+lib/log.cmx: lib/cps.cmx lib/log.cmi 
 lib/time.cmo: lib/log.cmi 
 lib/time.cmx: lib/log.cmx 
 automath/autOutput.cmi: automath/aut.cmx 
@@ -16,29 +16,34 @@ automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi
 automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx 
 basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx 
 basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx 
-basic_rg/brgOutput.cmi: basic_rg/brg.cmx 
-basic_rg/brgOutput.cmo: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi 
-basic_rg/brgOutput.cmx: lib/log.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 basic_rg/brg.cmx \
     basic_rg/brgEnvironment.cmi 
 basic_rg/brgEnvironment.cmx: lib/nUri.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/nUri.cmi lib/cps.cmx \
+basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx 
+basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi lib/cps.cmx \
     basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi 
-basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/cps.cmx \
+basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx lib/cps.cmx \
     basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi 
-basic_rg/brgType.cmi: basic_rg/brgReduction.cmi basic_rg/brg.cmx 
-basic_rg/brgType.cmo: basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi \
-    basic_rg/brg.cmx basic_rg/brgType.cmi 
-basic_rg/brgType.cmx: basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx \
-    basic_rg/brg.cmx basic_rg/brgType.cmi 
+basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brgReduction.cmi \
+    basic_rg/brg.cmx 
+basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \
+    basic_rg/brgReduction.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi 
+basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \
+    basic_rg/brgReduction.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
+basic_rg/brgType.cmi: lib/log.cmi basic_rg/brgReduction.cmi basic_rg/brg.cmx 
+basic_rg/brgType.cmo: lib/log.cmi basic_rg/brgReduction.cmi \
+    basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \
+    basic_rg/brgType.cmi 
+basic_rg/brgType.cmx: lib/log.cmx basic_rg/brgReduction.cmx \
+    basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
+    basic_rg/brgType.cmi 
 basic_rg/brgUntrusted.cmi: basic_rg/brg.cmx 
 basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgReduction.cmi \
-    basic_rg/brgEnvironment.cmi basic_rg/brgUntrusted.cmi 
+    basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi 
 basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgReduction.cmx \
-    basic_rg/brgEnvironment.cmx basic_rg/brgUntrusted.cmi 
+    basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.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 
@@ -56,11 +61,11 @@ 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/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaBrg.cmi \
-    toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \
-    basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \
-    automath/autLexer.cmx 
-toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \
-    toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
-    basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \
-    automath/autLexer.cmx 
+toplevel/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.cmi \
+    toplevel/metaBrg.cmi toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx \
+    basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.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/cps.cmx \
+    basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \
+    automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx 
diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index 2b218865e..a568047d9 100644
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -13,3 +13,15 @@ include Makefile.common
 test: $(MAIN).opt
 	@echo "  HELENA automath/*.aut"
 	$(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt
+
+meta: $(MAIN).opt
+	@echo "  HELENA -m meta.txt automath/*.aut"
+	$(H)./$(MAIN).opt -m meta.txt -s 1 -S 3 automath/*.aut > /dev/null
+
+ifeq ($(MAKECMDGOALS), test)
+  include .depend.opt
+endif
+
+ifeq ($(MAKECMDGOALS), meta)
+  include .depend.opt
+endif
diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common
index c4a276b82..c9173f76c 100644
--- a/helm/software/lambda-delta/Makefile.common
+++ b/helm/software/lambda-delta/Makefile.common
@@ -66,7 +66,3 @@ tgz: clean
 ifeq ($(MAKECMDGOALS), $(MAIN).opt)
   include .depend.opt
 endif
-
-ifeq ($(MAKECMDGOALS), test)
-  include .depend.opt
-endif
diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make
index eb1c64a66..7085d3b57 100644
--- a/helm/software/lambda-delta/basic_rg/Make
+++ b/helm/software/lambda-delta/basic_rg/Make
@@ -1 +1 @@
-brg brgOutput brgEnvironment brgReduction brgType brgUntrusted
+brg brgEnvironment brgReduction brgOutput brgType brgUntrusted
diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index 36e4fefe8..e9897c08a 100644
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -12,16 +12,18 @@
 type uri = NUri.uri
 type id = Aut.id
 
-type bind = Abst | Abbr (* abstraction, abbreviation *)
+type bind = Void         (* exclusion *)
+          | Abst of term (* abstraction *)
+          | Abbr of term (* abbreviation *)
 
-type 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 * term (* name, binder, content, scope *)
+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 *)
 
-type obj = int * uri * bind * term (* age, uri, binder, contents *)
+type obj = int * uri * bind (* age, uri, binder, contents *)
 
 type item = obj option
 
@@ -29,8 +31,12 @@ type hierarchy = int -> int
 
 (* Currified constructors ***************************************************)
 
+let abst w = Abst w
+
+let abbr v = Abbr v
+
 let cast u t = Cast (u, t)
 
 let appl u t = Appl (u, t)
 
-let bind id b u t = Bind (id, b, u, t)
+let bind id b t = Bind (id, b, t)
diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml
index b0cb9596e..e640c865b 100644
--- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml
+++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml
@@ -24,8 +24,8 @@ let entry = ref 0
 (* Interface functions ******************************************************)
 
 let set_obj f obj =
-   let _, uri, b, t = obj in
-   let obj = !entry, uri, b, t in
+   let _, uri, b = obj in
+   let obj = !entry, uri, b in
    incr entry; H.add env uri obj; f obj
 
 let get_obj f uri =
diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index e29b3f495..4c100375d 100644
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -10,8 +10,12 @@
       V_______________________________________________________________ *)
 
 module P = Printf
+module F = Format
+module U = NUri
+module C = Cps
 module L = Log
 module B = Brg
+module R = BrgReduction
 
 type counters = {
    eabsts: int;
@@ -30,11 +34,16 @@ let initial_counters = {
    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
 }
 
-let count_term_binder f c = function
-   | B.Abst -> f {c with tabsts = succ c.tabsts}
-   | B.Abbr -> f {c with tabbrs = succ c.tabbrs}
+let rec count_term_binder f c = function
+   | B.Abst w ->
+      let c = {c with tabsts = succ c.tabsts} in
+      count_term f c w
+   | B.Abbr v -> 
+      let c = {c with tabbrs = succ c.tabbrs} in
+      count_term f c v
+   | B.Void   -> f c
 
-let rec count_term f c = function
+and count_term f c = function
    | B.Sort _            -> 
       f {c with tsorts = succ c.tsorts}
    | B.LRef _            -> 
@@ -49,18 +58,21 @@ let rec 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, u, t) -> 
+   | B.Bind (_, b, t) -> 
       let f c = count_term_binder f c b in
-      let f c = count_term f c t in
-      count_term f c u
+      count_term f c t
 
 let count_obj_binder f c = function
-   | B.Abst -> f {c with eabsts = succ c.eabsts}
-   | B.Abbr -> f {c with eabbrs = succ c.eabbrs}
+   | B.Abst w -> 
+      let c = {c with eabsts = succ c.eabsts} in
+      count_term f c w
+   | B.Abbr v -> 
+      let c = {c with eabbrs = succ c.eabbrs} in
+      count_term f c v
+   | B.Void   -> f c
 
-let count_obj f c (_, _, b, t) =
-   let f c = count_obj_binder f c b in
-   count_term f c t
+let count_obj f c (_, _, b) =
+   count_obj_binder f c b
 
 let count_item f c = function
    | Some obj -> count_obj f c obj
@@ -85,3 +97,36 @@ let print_counters f c =
    L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
    L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
    f ()
+
+let rec pp_term c frm = function
+   | B.Sort h                 -> F.fprintf frm "@[*%u@]" h
+   | B.LRef i                 -> F.fprintf frm "@[#%u@]" i
+   | 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)            ->
+      F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
+   | B.Bind (id, B.Abst w, t) ->
+      F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term c) t
+   | B.Bind (id, B.Abbr v, t) ->
+      F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term c) t
+   | B.Bind (id, B.Void, t)   ->
+      F.fprintf frm "@[[%s].%a@]" id (pp_term c) t
+
+let pp_context frm c =
+   let pp_entry f = function
+      | B.Abst w -> 
+         F.fprintf frm "%s %a\n%!" "\\decl" (pp_term c) w; f ()
+      | B.Abbr v -> 
+         F.fprintf frm "%s %a\n%!" "\\def " (pp_term c) v; f ()
+      | B.Void   -> 
+         F.fprintf frm "%s\n%!" "\\void"; f ()
+   in
+   R.iter C.start pp_entry c
+
+let pp_term frm c t = 
+   F.fprintf frm "%a\n%!" (pp_term c) t
+
+let specs = {
+   L.pp_term = pp_term; L.pp_context = pp_context
+}
diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli
index 49b5064d1..cd7e49dc5 100644
--- a/helm/software/lambda-delta/basic_rg/brgOutput.mli
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli
@@ -16,3 +16,5 @@ val initial_counters: counters
 val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a
 
 val print_counters: (unit -> 'a) -> counters -> 'a
+
+val specs: (BrgReduction.context, Brg.term) Log.specs
diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index aced1a22e..74f6a5048 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -12,16 +12,11 @@
 module U = NUri
 module C = Cps
 module S = Share
+module L = Log
 module B = Brg
 module E = BrgEnvironment
 
-exception LRefNotFound of string Lazy.t
-
-type bind = Void_
-          | Abst_ of B.term
-          | Abbr_ of B.term
-
-type environment = int * bind list
+type environment = int * B.bind list
 
 type stack = B.term list
 
@@ -31,10 +26,12 @@ type context = {
    s: stack
 }
 
+exception LRefNotFound of (context, B.term) L.item list
+
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of int * B.bind * B.term
+   | GRef_ of int * B.bind
    | Bind_ of B.term * B.term
 
 type ho_whd_result =
@@ -43,6 +40,8 @@ type ho_whd_result =
 
 (* Internal functions *******************************************************)
 
+let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
+
 let empty_e = 0, []
 
 let push_e f b (l, e) =
@@ -50,36 +49,45 @@ let push_e f b (l, e) =
 
 let get_e f c i =
    let (gl, ge), (ll, le) = c.g, c.l in
-   if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i)));
+   if i >= gl + ll then error i;
    let b =
       if i < gl then List.nth ge (gl - (succ i)) 
       else List.nth le (gl + ll - (succ i))
    in
    f b
 
-let rec 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 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)        ->
+   | 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, w, u) ->
-      let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) 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 = 
    let (gl, _), (ll, le) = c.g, c.l in
    let map i = if i >= gl then succ i else i in
    let map f = function
-      | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t
+      | B.Abbr t -> let f t' = f (B.Abbr t') in lref_map f map t
       | _       -> assert false
    in
    let f le' = f {c with l = (ll, le')} in
@@ -97,52 +105,52 @@ let xchg f c t =
 let rec whd f c t = match t with
    | B.Sort h                 -> f c (Sort_ h)
    | B.GRef uri               ->
-      let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
+      let f (i, _, b) = f c (GRef_ (i, b)) in
       E.get_obj f uri
-   | B.LRef i                 ->
+   | B.LRef i                ->
       let f = function
-         | Void_   -> f c (LRef_ (i, None))
-	 | Abst_ t -> f c (LRef_ (i, Some t))
-	 | Abbr_ t -> whd f c t
+         | B.Void   -> f c (LRef_ (i, None))
+	 | B.Abst t -> f c (LRef_ (i, Some t))
+	 | B.Abbr t -> whd f c t
       in
       get_e f c i
-   | B.Appl (v, t)            -> whd f {c with s = v :: c.s} t   
-   | B.Bind (_, B.Abbr, v, t) -> 
-      let f l = whd f {c with l = l} t in
-      push_e f (Abbr_ v) c.l
-   | B.Bind (_, B.Abst, w, t) -> 
+   | B.Cast (_, t)           -> whd f c t
+   | B.Appl (v, t)           -> whd f {c with s = v :: c.s} t   
+   | B.Bind (_, B.Abst w, t) -> 
       begin match c.s with
          | []      -> f c (Bind_ (w, t))
 	 | v :: tl -> 
 	    let f tl l = whd f {c with l = l; s = tl} t in
-	    push_e (f tl) (Abbr_ v) c.l
+	    push_e (f tl) (B.Abbr v) c.l
       end
-   | B.Cast (_, t)            -> whd f c t
+   | B.Bind (_, b, t) -> 
+      let f l = whd f {c with l = l} t in
+      push_e f b c.l
 
 let push f c t = 
    assert (c.s = []);
    let f c g = xchg f {c with g = g} t in
-   let f c = push_e (f c) Void_ c.g in
+   let f c = push_e (f c) B.Void c.g in
    lift f c 
 
 (* Interface functions ******************************************************)
 
 let rec are_convertible f c1 t1 c2 t2 =
    let rec aux c1' r1 c2' r2 = match r1, r2 with
-      | Sort_ h1, Sort_ h2                             -> f (h1 = h2)
-      | LRef_ (i1, _), LRef_ (i2, _)                   ->
+      | Sort_ h1, Sort_ h2                           -> f (h1 = h2)
+      | LRef_ (i1, _), LRef_ (i2, _)                 ->
          if i1 = i2 then are_convertible_stacks f c1' c2' else f false
-      | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _)   ->
+      | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _)   ->
          if a1 = a2 then are_convertible_stacks f c1' c2' else f false
-      | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) ->
+      | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
          if a1 = a2 then are_convertible_stacks f c1' c2' else
 	 if a1 < a2 then whd (aux c1' r1) c2' v2 else
 	 whd (aux_rev c2' r2) c1' v1
-      | _, GRef_ (_, B.Abbr, v2)                       ->
+      | _, GRef_ (_, B.Abbr v2)                      ->
          whd (aux c1' r1) c2' v2
-      | GRef_ (_, B.Abbr, v1), _                       ->
+      | GRef_ (_, B.Abbr v1), _                      ->
 	 whd (aux_rev c2' r2) c1' v1
-      | Bind_ (w1, t1), Bind_ (w2, t2)                 ->
+      | Bind_ (w1, t1), Bind_ (w2, t2)               ->
          let f b = 
 	    if b then 
 	       let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
@@ -164,31 +172,30 @@ let are_convertible f c t1 t2 = are_convertible f c t1 c t2
 
 let rec ho_whd f c t =
    let aux c' = function
-      | Sort_ h           -> f c' (Sort h)
-      | Bind_ (w, t)      -> f c' (Abst w)
-      | LRef_ (_, Some w) -> ho_whd f c w
-      | GRef_ (_, _, u)   -> ho_whd f c u
-      | LRef_ (_, None)   -> assert false
+      | Sort_ h             -> f c' (Sort h)
+      | Bind_ (w, t)        -> f c' (Abst w)
+      | LRef_ (_, Some w)   -> ho_whd f c w
+      | GRef_ (_, B.Abst u) -> ho_whd f c u
+      | GRef_ (_, B.Abbr u) -> ho_whd f c u
+      | LRef_ (_, None)     -> assert false
+      | GRef_ (_, B.Void)   -> assert false
    in
    whd aux c t
 
-let push f c b t = 
+let push f c b = 
    assert (c.l = empty_e && c.s = []);
    let f g = f {c with g = g} in
-   let b = match b with
-      | B.Abbr -> Abbr_ t
-      | B.Abst -> Abst_ t
-   in
    push_e f b c.g
 
 let get f c i =
    let gl, ge = c.g in
-   if i >= gl then raise (LRefNotFound (lazy (string_of_int i)));
-   match List.nth ge (gl - (succ i)) with
-      | Abbr_ v -> f (B.Abbr, v)
-      | Abst_ w -> f (B.Abst, w)
-      | Void_   -> assert false
+   if i >= gl then error i;
+   f (List.nth ge (gl - (succ i)))
 
 let empty_context = {
    g = empty_e; l = empty_e; s = []
 }
+
+let iter f map c =
+   let _, ge = c.g in   
+   C.list_iter f map ge
diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli
index a8320ed55..b3a79ecae 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.mli
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli
@@ -9,19 +9,21 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-exception LRefNotFound of string Lazy.t
-
 type context
 
+exception LRefNotFound of (context, Brg.term) Log.item list
+
 type ho_whd_result =
    | Sort of int
    | Abst of Brg.term
 
 val empty_context: context
 
-val push: (context -> 'a) -> context -> Brg.bind -> Brg.term -> 'a
+val push: (context -> 'a) -> context -> Brg.bind -> 'a
+
+val get: (Brg.bind -> 'a) -> context -> int -> 'a
 
-val get: (Brg.bind * Brg.term -> 'a) -> context -> int -> 'a
+val iter: (unit -> 'a) -> ((unit -> 'a) -> Brg.bind -> 'a) -> context -> 'a
 
 val are_convertible: (bool -> 'a) -> context -> Brg.term -> Brg.term -> 'a
 
diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index d10ddefaa..60b5b75bc 100644
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -9,53 +9,82 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module L = Log
 module B = Brg
+module O = BrgOutput
 module E = BrgEnvironment
 module R = BrgReduction
 
-exception TypeError of string Lazy.t
+exception TypeError of (R.context, B.term) Log.item list
 
 (* Internal functions *******************************************************)
 
-let error msg = raise (TypeError (lazy msg))
+let error1 s c t =
+   raise (TypeError (L.ct_items1 s c t))
+
+let error2 s1 c1 t1 s2 c2 t2 =
+   raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2))
+
+let are_convertible f c t1 t2 =
+   L.log O.specs 4 (L.ct_items2 "Now converting" c t1 "and" c t2);
+   R.are_convertible f c t1 t2
 
 (* Interface functions ******************************************************)
 
-let rec type_of f g c = function
-   | B.Sort h             -> f (B.Sort (g h))
-   | B.LRef i             ->
+let rec type_of f g c x = 
+   L.log O.specs 5 (L.ct_items1 "now checking" c x);
+   match x with
+   | B.Sort h                 -> f (B.Sort (g h))
+   | B.LRef i                 ->
       let f = function
-         | B.Abst, w             -> f w
-	 | B.Abbr, B.Cast (w, v) -> f w
-	 | B.Abbr, _             -> error "lref"
+         | B.Abst w               -> f w
+	 | B.Abbr (B.Cast (w, v)) -> f w
+	 | B.Abbr _               -> assert false
+	 | B.Void                 -> assert false
       in
       R.get f c i
-   | B.GRef uri           ->
+   | B.GRef uri               ->
       let f = function
-         | _, _, B.Abst, w             -> f w
-	 | _, _, B.Abbr, B.Cast (w, v) -> f w
-	 | _, _, B.Abbr, _             -> error "gref"
+         | _, _, B.Abst w               -> f w
+	 | _, _, B.Abbr (B.Cast (w, v)) -> f w
+	 | _, _, B.Abbr _               -> assert false
+	 | _, _, B.Void                 -> assert false
       in
       E.get_obj f uri
-   | B.Bind (id, b, u, t) ->
-      let f uu tt = match b, t with 
-         | B.Abst, _ 
-	 | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt))
-         | _                -> f (B.Bind (id, b, B.Cast (uu, u), tt))
+   | B.Bind (id, B.Abbr u, t) ->
+      let f tt = f (B.Bind (id, B.Abbr u, tt)) in
+      let f cc = type_of f g cc t in
+      let f u = R.push f c (B.Abbr u) in
+      let f uu = match u with 
+	 | B.Cast _ -> f u
+         | _        -> f (B.Cast (uu, u))
       in
-      let f uu cc = type_of (f uu) g cc t in
-      let f uu = R.push (f uu) c b u in
       type_of f g c u
-   | B.Appl (v, t)        ->
+   | B.Bind (id, B.Abst u, t) ->
+      let f tt = f (B.Bind (id, B.Abst u, tt)) in
+      let f cc = type_of f g cc t in
+      let f _ = R.push f c (B.Abst u) in
+      type_of f g c u
+   | B.Bind (id, B.Void, t)   ->
+      let f tt = f (B.Bind (id, B.Void, tt)) in
+      let f cc = type_of f g cc t in
+      R.push f c B.Void
+   | B.Appl (v, t)            ->
       let f tt cc = function
-         | R.Sort _ -> error "appl"
+         | R.Sort _ -> error1 "not a function" c t
 	 | R.Abst w -> 
-	    let f b = if b then f (B.Appl (v, tt)) else error "appl_cast" in
-	    type_of (R.are_convertible f cc w) g c v
+	    let f b =
+	       if b then f (B.Appl (v, tt)) else
+	       error2 "the term" c v "must be of type" cc w
+	    in
+	    type_of (are_convertible f cc w) g c v
       in
       let f tt = R.ho_whd (f tt) c t in
       type_of f g c t 
-   | B.Cast (u, t)        ->
-      let f b = if b then f u else error "cast" in
-      let f _ = type_of (R.are_convertible f c u) g c t in
+   | B.Cast (u, t)            ->
+      let f b = 
+         if b then f u else
+	 error2 "the term" c t "must be of type" c u
+      in
+      let f _ = type_of (are_convertible f c u) g c t in
       type_of f g c u
diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli
index 5b351cca4..dc6fc998d 100644
--- a/helm/software/lambda-delta/basic_rg/brgType.mli
+++ b/helm/software/lambda-delta/basic_rg/brgType.mli
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-exception TypeError of string Lazy.t
+exception TypeError of (BrgReduction.context, Brg.term) Log.item list
 
 val type_of: (Brg.term -> 'a) -> 
              Brg.hierarchy -> BrgReduction.context -> Brg.term -> 'a
diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml
index c9f425f88..d08209f12 100644
--- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml
+++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml
@@ -9,6 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module B = Brg
 module E = BrgEnvironment
 module R = BrgReduction
 module T = BrgType
@@ -16,8 +17,10 @@ module T = BrgType
 (* Interface functions ******************************************************)
 
 let type_check f g = function
-   | None                       -> f None
-   | Some ((_, _, _, t) as obj) ->
+   | None                           -> f None
+   | Some ((_, _, B.Abst t) as obj)
+   | Some ((_, _, B.Abbr t) as obj) ->
        let f tt obj = f (Some (tt, obj)) in
        let f tt = E.set_obj (f tt) obj in
        T.type_of f g R.empty_context t
+   | Some (_, _, B.Void)            -> assert false
diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml
index c235197d9..2e8b2c715 100644
--- a/helm/software/lambda-delta/lib/cps.ml
+++ b/helm/software/lambda-delta/lib/cps.ml
@@ -49,3 +49,6 @@ let list_rev =
 let list_map f =
    list_rev_map (list_rev f)
    
+let list_iter f map l =
+   let map f () x = map f x in
+   list_fold_left f map () l
diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml
index 667fef534..78e57fdfa 100644
--- a/helm/software/lambda-delta/lib/log.ml
+++ b/helm/software/lambda-delta/lib/log.ml
@@ -10,6 +10,22 @@
       V_______________________________________________________________ *)
 
 module P = Printf
+module F = Format
+module C = Cps
+
+type ('a, 'b) item = Term of 'a * 'b
+                   | Context of 'a
+                   | Warn of string
+		   | String of string
+
+type ('a, 'b) specs = {
+   pp_term   : F.formatter -> 'a -> 'b -> unit;
+   pp_context: F.formatter -> 'a -> unit
+}
+
+let level = ref 0
+
+(* Internal functions *******************************************************)
 
 let init =
    let started = ref false in
@@ -17,5 +33,28 @@ let init =
       if !started then () else 
       begin P.printf "\n"; started := true end
 
+let pp_items frm st l items =   
+   let pp_item = function
+      | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t
+      | Context c   -> st.pp_context frm c
+      | Warn s      -> F.fprintf frm "@[%s\n@]" s
+      | String s    -> F.fprintf frm "@[%s @]" s
+   in
+   if !level >= l then List.iter pp_item items
+
+(* Interface functions ******************************************************)
+
 let warn msg = 
    init (); P.printf " %s\n" msg; flush stdout
+
+let log st l items = pp_items F.std_formatter st l items
+
+let error st items = pp_items F.err_formatter st 0 items
+
+let items1 s = [Warn s]
+
+let ct_items1 s c t =
+   [Warn s; Term (c, t)]
+
+let ct_items2 s1 c1 t1 s2 c2 t2 =
+   [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)]
diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli
index e32f6e0fd..184594077 100644
--- a/helm/software/lambda-delta/lib/log.mli
+++ b/helm/software/lambda-delta/lib/log.mli
@@ -9,4 +9,26 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+type ('a, 'b) item = Term of 'a * 'b
+                   | Context of 'a
+                   | Warn of string
+		   | String of string
+
+type ('a, 'b) specs = {
+   pp_term   : Format.formatter -> 'a -> 'b -> unit;
+   pp_context: Format.formatter -> 'a -> unit
+}
+
+val level: int ref
+
 val warn: string -> unit
+
+val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit
+
+val error: ('a, 'b) specs -> ('a, 'b) item list -> unit
+
+val items1: string -> ('a, 'b) item list
+
+val ct_items1: string -> 'a -> 'b -> ('a, 'b) item list
+
+val ct_items2: string -> 'a -> 'b -> string -> 'a -> 'b -> ('a, 'b) item list
diff --git a/helm/software/lambda-delta/lib/share.ml b/helm/software/lambda-delta/lib/share.ml
index 019cca982..c8097d568 100644
--- a/helm/software/lambda-delta/lib/share.ml
+++ b/helm/software/lambda-delta/lib/share.ml
@@ -11,6 +11,9 @@
 
 let sh a b =
    if a == b then a else b
-   
-let sh2 a1 b1 a2 b2 c1 c2 =
+
+let sh1 a1 a2 b1 b2 =
+   if a1 == a2 then b1 else b2 (sh a1 a2)
+
+let sh2 a1 a2 b1 b2 c1 c2 =
    if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2)
diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml
index 4088c2982..192613264 100644
--- a/helm/software/lambda-delta/toplevel/metaBrg.ml
+++ b/helm/software/lambda-delta/toplevel/metaBrg.ml
@@ -20,23 +20,23 @@ let map_fold_left f map1 map2 a l =
 
 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 map_pars f t (id, w) = f (B.Bind (id, B.Abst w, t))
 
 let rec xlate_term 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 - i))
+      f (B.LRef (l - succ i))
    | M.GRef (_, uri, vs) ->
       let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in
-      Cps.list_rev_map f xlate_term vs
+      Cps.list_map f xlate_term 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
    | M.Abst (id, w, t)   ->
-      let f w t = f (B.Bind (id, B.Abst, w, t)) in
+      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
 
@@ -46,14 +46,14 @@ let xlate_pars f (id, w) =
 
 let xlate_entry f = function
    | e, pars, uri, u, None        ->
-      let f u = f (e, uri, B.Abst, u) in
+      let f u = f (e, uri, B.Abst u) in
       let f pars = map_fold_left f xlate_term map_pars u pars in      
-      Cps.list_rev_map f xlate_pars pars
+      Cps.list_map f xlate_pars pars
    | e, pars, uri, u, Some (_, t) ->
-      let f u t = f (e, uri, B.Abbr, (B.Cast (u, t))) in
+      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
-      Cps.list_rev_map f xlate_pars pars
+      Cps.list_map f xlate_pars pars
 
 let xlate_item f = function
    | None   -> f None
diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml
index 2d5bc3ad5..03995e153 100644
--- a/helm/software/lambda-delta/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/toplevel/metaOutput.ml
@@ -104,6 +104,9 @@ let pp_list pp opend sep closed frm l =
    in
    if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
 
+let pp_rev_list pp opend sep closed frm l =
+   pp_list pp opend sep closed frm (List.rev l)
+
 let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
 
 and pp_term frm = function
@@ -121,7 +124,7 @@ and pp_term frm = function
 let pp_par frm (id, w) =
     F.fprintf frm "%s:%a" id pp_term w
 
-let pp_pars = pp_list pp_par "[" "," "]"
+let pp_pars = pp_rev_list pp_par "[" "," "]"
 
 let pp_body frm = function
    | None            -> ()
diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 92840d54a..7504e2c0b 100644
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 module P    = Printf
+module U    = NUri
 module L    = Log
 module AO   = AutOutput
 module MA   = MetaAut
@@ -19,31 +20,32 @@ module BrgO = BrgOutput
 module BrgU = BrgUntrusted
 
 type status = {
-   summary: int;
    mst : MA.status;
    ac  : AO.counters;
    mc  : MO.counters;
    brgc: BrgO.counters
 }
 
-let initial_status summary = {
-   summary = summary;
+let initial_status = {
    ac = AO.initial_counters;
    mc = MO.initial_counters;
    brgc= BrgO.initial_counters;
    mst = MA.initial_status
 }
 
-let count st count_fun c item =
-   if st.summary > 2 then count_fun Cps.start c item else c
+let count count_fun c item =
+   if !L.level > 2 then count_fun Cps.start c item else c
+
+let brg_error s msg =
+   L.error BrgO.specs (L.Warn s :: msg) 
 
 let main =
+try 
    let version_string = "Helena Checker 0.8.0 M - December 2008" in
-   let summary = ref 0 in
    let stage = ref 3 in
    let meta_file = ref None in
    let hierarchy = ref (fun h -> h + 2) in
-   let set_summary i = summary := i in
+   let set_summary i = L.level := i in
    let print_version () = L.warn version_string; exit 0 in
    let set_stage i = stage := i in
    let close = function
@@ -58,33 +60,33 @@ let main =
       meta_file := Some (och, frm)
    in
    let read_file name =
-      if !summary > 0 then Time.gmtime version_string;      
-      if !summary > 1 then
+      if !L.level > 0 then Time.gmtime version_string;      
+      if !L.level > 1 then
          L.warn (P.sprintf "Processing file: %s" name);
-      if !summary > 0 then Time.utime_stamp "started";
+      if !L.level > 0 then Time.utime_stamp "started";
       let ich = open_in name in
       let lexbuf = Lexing.from_channel ich in
       let book = AutParser.book AutLexer.token lexbuf in
       close_in ich;
-      if !summary > 0 then Time.utime_stamp "parsed";
+      if !L.level > 0 then Time.utime_stamp "parsed";
       let rec aux st = function
          | []         -> st
 	 | item :: tl ->
 (* stage 3 *)
 	    let f st = function
-	       | None                   -> st
-	       | Some (_, (i, _, _, _)) ->
-	          Log.warn (string_of_int i); st
+	       | None                -> st
+	       | Some (_, (i, u, _)) -> 
+	          Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st
 	    in
 (* stage 2 *)	    
 	    let f st item =
-	       let st = {st with brgc = count st BrgO.count_item st.brgc item} in
+	       let st = {st with brgc = count BrgO.count_item st.brgc item} in
 	       if !stage > 2 then BrgU.type_check (f st) !hierarchy item else st
 	    in
 (* stage 1 *)	    
 	    let f mst item = 
 	       let st = {st with
-	          mst = mst; mc = count st MO.count_item st.mc item
+	          mst = mst; mc = count MO.count_item st.mc item
 	       } in
 	       begin match !meta_file with
 	          | None          -> ()
@@ -93,17 +95,17 @@ let main =
 	       if !stage > 1 then MBrg.brg_of_meta (f st) item else st 
 	    in  
 (* stage 0 *)	    
-            let st = {st with ac = count st AO.count_item st.ac item} in
+            let st = {st with ac = count AO.count_item st.ac item} in
 	    let st =
 	       if !stage > 0 then MA.meta_of_aut f st.mst item else st
 	    in
 	    aux st tl
       in 
-      let st = aux (initial_status !summary) book in
-      if !summary > 0 then Time.utime_stamp "processed";
-      if !summary > 2 then AO.print_counters Cps.start st.ac;
-      if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
-      if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
+      let st = aux initial_status book in
+      if !L.level > 0 then Time.utime_stamp "processed";
+      if !L.level > 2 then AO.print_counters Cps.start st.ac;
+      if !L.level > 2 && !stage > 0 then MO.print_counters Cps.start st.mc;
+      if !L.level > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc;
    in
    let help = "Usage: helena [ -V | -Ss <number> | -m <file> ] <file> ..." in
    let help_S = "<number>  Set summary level" in
@@ -116,4 +118,5 @@ let main =
       ("-m", Arg.String set_meta_file, help_m); 
       ("-s", Arg.Int set_stage, help_s);
    ] read_file help;
-   if !summary > 0 then Time.utime_stamp "at exit"
+   if !L.level > 0 then Time.utime_stamp "at exit"
+with BrgType.TypeError msg -> brg_error "Type Error" msg
-- 
2.39.2