- revision of ground_2 and basic_2

[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 51d6ddfc107df8323632f3f09a7abe9a389266f6..23829c095ff543aedfe7afe9db4eaf6e88a79776 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -9,10 +9,10 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P = Printf
+module KP = Printf
 
-module L = Log
-module G = Options
+module L  = Log
+module G  = Options
 
 type reductions = {
    beta   : int;
@@ -21,7 +21,7 @@ type reductions = {
    epsilon: int;
    ldelta : int;
    gdelta : int;
-   si     : int;
+   upsilon: int;
    lrt    : int;
    grt    : int;
    e      : int;
@@ -30,8 +30,8 @@ type reductions = {
 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;
+   beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0;
+   lrt = 0; grt = 0; e = 0;
 }
 
 let reductions = ref initial_reductions
@@ -40,7 +40,7 @@ let clear_reductions () = reductions := initial_reductions
 
 let add 
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
-   ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
+   ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
 = reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
@@ -48,7 +48,7 @@ let add
    epsilon = !reductions.epsilon + epsilon;
    ldelta = !reductions.ldelta + ldelta;
    gdelta = !reductions.gdelta + gdelta;
-   si = !reductions.si + si;
+   upsilon = !reductions.upsilon + upsilon;
    lrt = !reductions.lrt + lrt;
    grt = !reductions.grt + grt;
    e = !reductions.e + e;
@@ -56,23 +56,23 @@ let add
 
 let print_reductions () =
    let r = !reductions in
-   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 rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta + r.upsilon in
+   let prs = r.lrt + r.grt + r.e in
    let delta = r.ldelta + r.gdelta in
    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)
+   L.warn level (KP.sprintf "Reductions summary");
+   L.warn level (KP.sprintf "  Proper reductions:        %7u" rs);
+   L.warn level (KP.sprintf "    Beta:                   %7u" r.beta);
+   L.warn level (KP.sprintf "    Delta:                  %7u" delta);
+   L.warn level (KP.sprintf "      Local:                %7u" r.ldelta);
+   L.warn level (KP.sprintf "      Global:               %7u" r.gdelta);
+   L.warn level (KP.sprintf "    Theta:                  %7u" r.theta);
+   L.warn level (KP.sprintf "    Zeta for abbreviation:  %7u" r.zeta);
+   L.warn level (KP.sprintf "    Zeta for cast:          %7u" r.epsilon);
+   L.warn level (KP.sprintf "    Sort inclusion:         %7u" r.upsilon);
+   L.warn level (KP.sprintf "  Pseudo reductions:        %7u" prs);
+   L.warn level (KP.sprintf "    Reference typing:       %7u" rt);
+   L.warn level (KP.sprintf "      Local:                %7u" r.lrt);
+   L.warn level (KP.sprintf "      Global:               %7u" r.grt);
+   L.warn level (KP.sprintf "    Cast typing:            %7u" r.e);  
+   L.warn level (KP.sprintf "Relocated nodes (icm):      %7u" !G.icm)