new message reporting system improves performance significatively

[helm.git] / helm / software / helena / src / basic_ag / bagOutput.ml

diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml
index feebca464a05bf92fbd2af4d78381dd639511e7a..4d0a1c07b1b2e834fed3861c84535459ab4a202e 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagOutput.ml
+++ b/helm/software/helena/src/basic_ag/bagOutput.ml
@@ -10,7 +10,6 @@
       V_______________________________________________________________ *)
 
 module P  = Printf
-module F  = Format
 module U  = NUri
 module L  = Log
 module G  = Options
@@ -33,6 +32,8 @@ type counters = {
    tabbrs: int
 }
 
+let level = 2
+
 let initial_counters = {
    eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
@@ -82,71 +83,71 @@ let print_counters f c =
    in
    let items = c.eabsts + c.eabbrs in
    let locations = J.locations () in
-   L.warn (P.sprintf "  Kernel representation summary (basic_ag)");
-   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 "    Total binder locations:   %7u" locations);   
+   L.warn level (P.sprintf "Kernel representation summary (basic_ag)");
+   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 "  Total binder locations:   %7u" locations);   
    f ()
 
-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 res a l frm =
-   let err () = F.fprintf frm "@[#%u@]" l in
-   if !G.indexes then err () else name err frm a
+let res a l och =
+   let err () = P.fprintf och "#%u" l in
+   if !G.indexes then err () else name err och a
 
-let rec pp_term c frm = function
+let rec pp_term c och = function
    | Z.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 
    | Z.LRef i                 -> 
-      let err () = F.fprintf frm "@[#%u@]" i in
-      let f a _ = name err frm a in
+      let err () = P.fprintf och "#%u" i in
+      let f a _ = name err och a in
       if !G.indexes then err () else Z.get err f c i
-   | Z.GRef s                    -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+   | Z.GRef s                    -> P.fprintf och "$%s" (U.string_of_uri s)
    | Z.Cast (u, t)               ->
-      F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
+      P.fprintf och "{%a}.%a" (pp_term c) u (pp_term c) t
    | Z.Appl (v, t)               ->
-      F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
+      P.fprintf och "(%a).%a" (pp_term c) v (pp_term c) t
    | Z.Bind (a, l, Z.Abst w, t) ->
       let f cc =
-         F.fprintf frm "@[[%t:%a].%a@]" (res a l) (pp_term c) w (pp_term cc) t
+         P.fprintf och "[%t:%a].%a" (res a l) (pp_term c) w (pp_term cc) t
       in
       Z.push "output abst" f c a l (Z.Abst w)
    | Z.Bind (a, l, Z.Abbr v, t) ->
       let f cc = 
-         F.fprintf frm "@[[%t=%a].%a@]" (res a l) (pp_term c) v (pp_term cc) t
+         P.fprintf och "[%t=%a].%a" (res a l) (pp_term c) v (pp_term cc) t
       in
       Z.push "output abbr" f c a l (Z.Abbr v)
    | Z.Bind (a, l, Z.Void, t)   ->
-      let f cc = F.fprintf frm "@[[%t].%a@]" (res a l) (pp_term cc) t in
+      let f cc = P.fprintf och "[%t].%a" (res a l) (pp_term cc) t in
       Z.push "output void" f c a l Z.Void
 
-let pp_lenv frm c =
-   let pp_entry frm = function
+let pp_lenv och c =
+   let pp_entry och = function
       | a, l, Z.Abst w -> 
-         F.fprintf frm "@,@[%t : %a@]" (res a l) (pp_term c) w
+         P.fprintf och "%t : %a\n" (res a l) (pp_term c) w
       | a, l, Z.Abbr v -> 
-         F.fprintf frm "@,@[%t = %a@]" (res a l) (pp_term c) v
+         P.fprintf och "%t = %a\n" (res a l) (pp_term c) v
       | a, l, Z.Void   -> 
-         F.fprintf frm "@,%t" (res a l)
+         P.fprintf och "%t\n" (res a l)
    in
-   let iter map frm l = List.iter (map frm) l in
-   let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
+   let iter map och l = List.iter (map och) l in
+   let f es = P.fprintf och "%a" (iter pp_entry) (List.rev es) in
    Z.contents f c
 
 let specs = {