- simpler attribute system

[helm.git] / helm / software / helena / src / basic_rg / brgOutput.ml

diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml
index 6a40aecd4df2c87a09a596cf5378e0352bdb7229..0c692045ed7db3e6c7f13a9ffc7e196ee65e18d0 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgOutput.ml
+++ b/helm/software/helena/src/basic_rg/brgOutput.ml
@@ -64,33 +64,33 @@ let rec count_term_binder f c e = function
       f c
 
 and count_term f c e = function
-   | B.Sort _            ->
+   | B.Sort _         ->
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | B.LRef (_, i)       ->
+   | B.LRef (_, i)    ->
       begin match B.get e i with
-        | _, _, _, B.Abst _
-        | _, _, _, B.Void   ->
+        | _, _, _, _, B.Abst _
+        | _, _, _, _, B.Void   ->
            f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
-        | _, _, _, B.Abbr _ ->
+        | _, _, _, _, B.Abbr _ ->
            f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
       end      
-   | B.GRef (_, u)       -> 
+   | B.GRef (_, u)    -> 
       let c =    
         if Cps.list_mem ~eq:U.eq u c.uris
         then {c with nodes = succ c.nodes}
         else {c with xnodes = succ c.xnodes}
       in
       f {c with tgrefs = succ c.tgrefs}
-   | B.Cast (_, v, t)    -> 
+   | B.Cast (v, t)    -> 
       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
-   | B.Appl (_, _, v, t) -> 
+   | B.Appl (_, v, t) -> 
       let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
       let f c = count_term f c e t in
       count_term f c e v
-   | B.Bind (a, b, t)    -> 
-      let f c = count_term f c (B.push e B.empty a b) t in
+   | B.Bind (y, b, t) -> 
+      let f c = count_term f c (B.push e B.empty E.empty_node y b) t in
       count_term_binder f c e b
 
 let count_entity f c = function
@@ -106,7 +106,7 @@ let count_entity f c = function
 
 let print_counters f c =
    let terms =
-      c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
+      c.tsorts + c.tlrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
@@ -143,46 +143,46 @@ let pp_level st och n =
    KP.fprintf och "%s" (N.to_string st n)
 
 let rec pp_term st e och = function
-   | B.Sort (_, h)                   -> 
-      let err _ = KP.fprintf och "*%u" h in
+   | B.Sort k                        -> 
+      let err _ = KP.fprintf och "*%u" k in
       let f s = KP.fprintf och "%s" s in
-      H.string_of_sort err f h 
+      H.string_of_sort err f k 
    | B.LRef (_, i)                   -> 
       let err _ = KP.fprintf och "#%u" i in
       if !G.indexes then err () else      
-      let _, _, a, b = B.get e i in
-      KP.fprintf och "%a" (name err) a
+      let _, _, _, y, b = B.get e i in
+      KP.fprintf och "%a" (name err) y
    | B.GRef (_, s)                   ->
       let u = U.string_of_uri s in
       KP.fprintf och "$%s" (if !G.short then KF.basename u else u)
-   | B.Cast (_, u, t)                ->
+   | B.Cast (u, t)                   ->
       KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t
-   | B.Appl (_, _, v, t)             ->
+   | B.Appl (_, v, t)                ->
       KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
-   | B.Bind (a, B.Abst (r, n, w), t) ->
-      let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst r n w) in
-      KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t
-   | B.Bind (a, B.Abbr v, t)         ->
-      let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abbr v) in
-      KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t
-   | B.Bind (a, B.Void, t)           ->
-      let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a B.Void in
-      KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t
+   | B.Bind (y, B.Abst (r, n, w), t) ->
+      let y = R.alpha B.mem e y in
+      let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
+      KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) y (pp_term st e) w (pp_term st ee) t
+   | B.Bind (y, B.Abbr v, t)         ->
+      let y = R.alpha B.mem e y in
+      let ee = B.push e B.empty E.empty_node y (B.abbr v) in
+      KP.fprintf och "[%a=%a].%a" (name C.start) y (pp_term st e) v (pp_term st ee) t
+   | B.Bind (y, B.Void, t)           ->
+      let y = R.alpha B.mem e y in
+      let ee = B.push e B.empty E.empty_node y B.Void in
+      KP.fprintf och "[%a].%a" (name C.start) y (pp_term st ee) t
 
 let pp_lenv st och e =
-   let pp_entry f c a b x =
-      let a = R.alpha B.mem e a in
-      let x = B.push x c a b in
+   let pp_entry f c a y b x =
+      let y = R.alpha B.mem e y in
+      let x = B.push x c a y b in
       match b with
          | B.Abst (_, _, w) ->
-            KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x
+            KP.fprintf och "[%a : %a] " (name C.start) y (pp_term st c) w; f x
          | B.Abbr v            ->
-            KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x
+            KP.fprintf och "[%a = %a] " (name C.start) y (pp_term st c) v; f x
          | B.Void           ->
-            KP.fprintf och "[%a]" (name C.start) a; f x
+            KP.fprintf och "[%a]" (name C.start) y; f x
    in
    if e = B.empty then KP.fprintf och "%s" "empty" else
    B.fold_right ignore pp_entry e B.empty