new message reporting system improves performance significatively

[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 ed024a68e8faeb50c6901ce118e9cd1a6e3ce0a4..978658caa0cd6fbf87d144a1275b3e1e877dccbe 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgOutput.ml
+++ b/helm/software/helena/src/basic_rg/brgOutput.ml
@@ -10,7 +10,6 @@
       V_______________________________________________________________ *)
 
 module P  = Printf
-module F  = Format
 module C  = Cps
 module U  = NUri
 module L  = Log
@@ -41,6 +40,8 @@ type counters = {
    xnodes: int
 }
 
+let level = 2
+
 let initial_counters = {
    eabsts = 0; eabbrs = 0; evoids = 0; 
    tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0;
@@ -107,20 +108,20 @@ let print_counters f c =
    in
    let items = c.eabsts + c.eabbrs in
    let nodes = c.nodes + c.xnodes in
-   L.warn (P.sprintf "  Kernel representation summary (basic_rg)");
-   L.warn (P.sprintf "    Total entry items:        %7u" items);
-   L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
-   L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
-   L.warn (P.sprintf "    Total term items:         %7u" terms);
-   L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
-   L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
-   L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
-   L.warn (P.sprintf "      Explicit Cast items:    %7u" c.tcasts);
-   L.warn (P.sprintf "      Application items:      %7u" c.tappls);
-   L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
-   L.warn (P.sprintf "      Abbreviation items:     %7u" c.tabbrs);
-   L.warn (P.sprintf "    Global Int. Complexity:   %7u" c.nodes);
-   L.warn (P.sprintf "      + Abbreviation nodes:   %7u" nodes);
+   L.warn level (P.sprintf "Kernel representation summary (basic_rg)");
+   L.warn level (P.sprintf "  Total entry items:        %7u" items);
+   L.warn level (P.sprintf "    Declaration items:      %7u" c.eabsts);
+   L.warn level (P.sprintf "    Definition items:       %7u" c.eabbrs);
+   L.warn level (P.sprintf "  Total term items:         %7u" terms);
+   L.warn level (P.sprintf "    Sort items:             %7u" c.tsorts);
+   L.warn level (P.sprintf "    Local reference items:  %7u" c.tlrefs);
+   L.warn level (P.sprintf "    Global reference items: %7u" c.tgrefs);
+   L.warn level (P.sprintf "    Explicit Cast items:    %7u" c.tcasts);
+   L.warn level (P.sprintf "    Application items:      %7u" c.tappls);
+   L.warn level (P.sprintf "    Abstraction items:      %7u" c.tabsts);
+   L.warn level (P.sprintf "    Abbreviation items:     %7u" c.tabbrs);
+   L.warn level (P.sprintf "  Global Int. Complexity:   %7u" c.nodes);
+   L.warn level (P.sprintf "    + Abbreviation nodes:   %7u" nodes);
    f ()
 
 (* supplementary annotation *************************************************)
@@ -149,63 +150,65 @@ let rename f e a =
 
 (* lenv/term pretty printing ************************************************)
 
-let name err frm a =
+let name err och a =
    let f n = function 
-      | true  -> F.fprintf frm "%s" n
-      | false -> F.fprintf frm "-%s" n
+      | true  -> P.fprintf och "%s" n
+      | false -> P.fprintf och "-%s" n
    in      
    E.name err f a
 
-let pp_level frm n =
-   if N.is_infinite n then () else F.fprintf frm "^%s" (N.to_string n)
+let pp_level och n =
+   if N.is_infinite n then () else P.fprintf och "^%s" (N.to_string n)
 
-let rec pp_term e frm = function
+let rec pp_term e och = function
    | B.Sort (_, h)           -> 
-      let err _ = F.fprintf frm "@[*%u@]" h in
-      let f s = F.fprintf frm "@[%s@]" s in
+      let err _ = P.fprintf och "*%u" h in
+      let f s = P.fprintf och "%s" s in
       H.string_of_sort err f h 
    | B.LRef (_, i)           -> 
-      let err _ = F.fprintf frm "@[#%u@]" i in
+      let err _ = P.fprintf och "#%u" i in
       if !G.indexes then err () else      
       let _, _, a, b = B.get e i in
-      F.fprintf frm "@[%a@]" (name err) a
+      P.fprintf och "%a" (name err) a
    | B.GRef (_, s)           ->
-      F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+      P.fprintf och "$%s" (U.string_of_uri s)
    | B.Cast (_, u, t)        ->
-      F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t
+      P.fprintf och "{%a}.%a" (pp_term e) u (pp_term e) t
    | B.Appl (_, v, t)        ->
-      F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t
+      P.fprintf och "(%a).%a" (pp_term e) v (pp_term e) t
    | B.Bind (a, B.Abst (n, w), t) ->
       let f a =
          let ee = B.push e B.empty a (B.abst n w) in
-        F.fprintf frm "@[[%a:%a]%a.%a@]" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t
+        P.fprintf och "[%a:%a]%a.%a" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t
       in
       rename f e a
    | B.Bind (a, B.Abbr v, t) ->
       let f a = 
          let ee = B.push e B.empty a (B.abbr v) in
-        F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t
+        P.fprintf och "[%a=%a].%a" (name C.err) a (pp_term e) v (pp_term ee) t
       in
       rename f e a
    | B.Bind (a, B.Void, t)   ->
       let f a = 
          let ee = B.push e B.empty a B.Void in
-         F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t
+         P.fprintf och "[%a].%a" (name C.err) a (pp_term ee) t
       in
       rename f e a
 
-let pp_lenv frm e =
-   let pp_entry f e c a b x = f x (*match b with
+let pp_lenv och e =
+   let pp_entry f e c a b x = f x (* match b with
       | B.Abst (a, w) -> 
-         let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in
+         let f a = P.fprintf och "%a : %a\n" (name C.err) a (pp_term e) w; f a in
          rename f x a
       | B.Abbr (a, v) -> 
-         let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in
+         let f a = P.fprintf och "%a = %a\n" (name C.err) a (pp_term e) v; f a in
         rename f c a
       | B.Void a      -> 
-         let f a = F.fprintf frm "@,%a" (name C.err) a; f a in
+         let f a = P.fprintf och "%a\n" (name C.err) a; f a in
         rename f c a
 *)   in
+   let e = B.empty in
+   if e = B.empty then P.fprintf och "%s\n" "not shown" else
    B.fold_right ignore pp_entry e B.empty
 
 let specs = {