new message reporting system improves performance significatively

[helm.git] / helm / software / helena / src / common / output.ml

diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml
index 2af0b535bb1f9e07bcbea5c3e1a7d63be445dd52..7b9bd109b03a7f8fe64633cd6559bc3a5ccf12a0 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -26,6 +26,8 @@ type reductions = {
    e      : int;
 }
 
+let level = 2
+
 let initial_reductions = {
    beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0;
    si = 0; lrt = 0; grt = 0; e = 0;
@@ -56,20 +58,20 @@ let print_reductions () =
    let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta in
    let prs = r.si + r.lrt + r.grt + r.e in
    let delta = r.ldelta + r.gdelta in
-   let rt = r.lrt + r.grt in   
-   L.warn (P.sprintf "  Reductions summary");
-   L.warn (P.sprintf "    Proper reductions:        %7u" rs);
-   L.warn (P.sprintf "      Beta:                   %7u" r.beta);
-   L.warn (P.sprintf "      Delta:                  %7u" delta);
-   L.warn (P.sprintf "        Local:                %7u" r.ldelta);
-   L.warn (P.sprintf "        Global:               %7u" r.gdelta);
-   L.warn (P.sprintf "      Theta:                  %7u" r.theta);
-   L.warn (P.sprintf "      Zeta for abbreviation:  %7u" r.zeta);
-   L.warn (P.sprintf "      Zeta for cast:          %7u" r.epsilon);
-   L.warn (P.sprintf "    Pseudo reductions:        %7u" prs);
-   L.warn (P.sprintf "      Reference typing:       %7u" rt);
-   L.warn (P.sprintf "        Local:                %7u" r.lrt);
-   L.warn (P.sprintf "        Global:               %7u" r.grt);
-   L.warn (P.sprintf "      Cast typing:            %7u" r.e);  
-   L.warn (P.sprintf "      Sort inclusion:         %7u" r.si);
-   L.warn (P.sprintf "  Relocated nodes (icm):      %7u" !G.icm)
+   let rt = r.lrt + r.grt in
+   L.warn level (P.sprintf "Reductions summary");
+   L.warn level (P.sprintf "  Proper reductions:        %7u" rs);
+   L.warn level (P.sprintf "    Beta:                   %7u" r.beta);
+   L.warn level (P.sprintf "    Delta:                  %7u" delta);
+   L.warn level (P.sprintf "      Local:                %7u" r.ldelta);
+   L.warn level (P.sprintf "      Global:               %7u" r.gdelta);
+   L.warn level (P.sprintf "    Theta:                  %7u" r.theta);
+   L.warn level (P.sprintf "    Zeta for abbreviation:  %7u" r.zeta);
+   L.warn level (P.sprintf "    Zeta for cast:          %7u" r.epsilon);
+   L.warn level (P.sprintf "  Pseudo reductions:        %7u" prs);
+   L.warn level (P.sprintf "    Reference typing:       %7u" rt);
+   L.warn level (P.sprintf "      Local:                %7u" r.lrt);
+   L.warn level (P.sprintf "      Global:               %7u" r.grt);
+   L.warn level (P.sprintf "    Cast typing:            %7u" r.e);  
+   L.warn level (P.sprintf "    Sort inclusion:         %7u" r.si);
+   L.warn level (P.sprintf "Relocated nodes (icm):      %7u" !G.icm)