update in helena

[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 7275dd462c604618e6d4242fb6b182134d0a44a7..f068181a789e034488563d970cde256d181d0969 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -47,60 +47,62 @@ let initial_counters = {
    uris = []; nodes = 0; xnodes = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term f c e = function
-   | D.TSort _          -> 
+   | D.TSort _         -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | D.TLRef (_, i)     -> 
+   | D.TLRef (_, i)    -> 
       begin match D.get e i with
-        | _, _, D.Abbr _ ->
+        | _, _, _, 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)     -> 
+   | D.TGRef (_, u)    -> 
       let c =    
         if C.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}
-   | D.TCast (_, v, t)  -> 
+   | D.TCast (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
-   | D.TAppl (_, v, t)  -> 
+   | D.TAppl (_, v, t) -> 
       let c = {c with tappls = succ c.tappls} in
       let f c = count_term f c e t in
       count_term f c e v
-   | D.TProj (_, d, t)  ->
+   | D.TProj (d, t)    ->
       D.shift (count_term f c e) d t
-   | D.TBind (a, b, t)  -> 
+   | D.TBind (y, b, t) -> 
       let f c e = count_term f c e t in
-      count_binder f c e a b
+      count_binder f c e y b
 
-and count_binder f c e a b = match b with
-   | D.Abst (_, w) ->
+and count_binder f c e y 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
+      let f c = D.push_bind (f c) E.empty_node y b e in
       count_term f c e w
-   | D.Abbr v      -> 
+   | 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
+      let f c = D.push_bind (f c) E.empty_node y b e in
       count_term f c e v     
-   | D.Void        ->
+   | D.Void           ->
       let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
-      D.push_bind (f c) a b e
+      D.push_bind (f c) E.empty_node y b e
 
 let count_entity f c = function
-   | _, _, u, E.Abst w -> 
+   | _, _, u, E.Abst (_, w) -> 
       let c = {c with
          eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
       } in
       count_term f c D.ESort w
-   | _, _, _, E.Abbr v ->  
+   | _, _, _, E.Abbr (_, v) ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c D.ESort v
-   | _, _, _, E.Void   -> assert false
+   | _, _, _, E.Void        -> assert false
 
 let print_counters f c =
    let terms =
@@ -127,30 +129,36 @@ let print_counters f c =
    L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" nodes);
    f ()
 
+END
+
 (* term/environment pretty printer ******************************************)
 
-let pp_attrs out a =
+let pp_b_attrs out a =
    let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in
-   E.name ignore f a;
+   E.name ignore f a
+
+let pp_n_attrs out a =
    out (KP.sprintf "+%i;" a.E.n_apix)
 
+let pp_state out x = if x then out "^"
+
 let rec pp_term out st = function
-   | D.TSort (a, l)    -> pp_attrs out a; out (KP.sprintf "*%u" l)
-   | D.TLRef (a, i   ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
-   | D.TGRef (a, u)    -> pp_attrs out a; out (KP.sprintf "$")
-   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
-   | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
-   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
-   | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out st x; out "}."; pp_term out st y
+   | D.TSort k         -> out (KP.sprintf "*%u" k)
+   | D.TLRef (a, i)    -> pp_n_attrs out a; out (KP.sprintf "#%u" i)
+   | D.TGRef (a, u)    -> pp_n_attrs out a; out (KP.sprintf "$")
+   | D.TCast (u, t)    -> out "<"; pp_term out st u; out ">."; pp_term out st t
+   | D.TAppl (_, u, t) -> out "("; pp_term out st u; out ")."; pp_term out st t
+   | D.TBind (y, u, t) -> pp_b_attrs out y; pp_bind out st u; out "."; pp_term out st t
+   | D.TProj (u, t)    -> out "{"; pp_lenv out st u; out "}."; pp_term out st t
 
 and pp_bind out st = function
-   | D.Abst (n, x) ->
-      out "[:"; pp_term out st x; out "]"; out (N.to_string st n)  
-   | D.Abbr x      -> out "[="; pp_term out st x; out "]";
-   | D.Void        -> out "[]"
+   | D.Abst (r, n, u) ->
+      out "[:"; pp_term out st u; out "]"; pp_state out r; out (N.to_string st n); out " "  
+   | D.Abbr u         -> out "[="; pp_term out st u; out "] ";
+   | D.Void           -> out "[] "
 
 and pp_lenv out st = function
-   | D.ESort           -> ()
-   | D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
-   | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ")"
-   | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "}"
+   | D.ESort              -> ()
+   | D.EBind (u, a, y, t) -> pp_lenv out st u; pp_b_attrs out y; pp_n_attrs out a; pp_bind out st t
+   | D.EAppl (u, _, t)    -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+   | D.EProj (u, t)       -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "