the partial commit continues

[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 1124764885c871d364e7cfd3d6d3c048a17a77ec..2af0b535bb1f9e07bcbea5c3e1a7d63be445dd52 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -16,18 +16,19 @@ module G = Options
 type reductions = {
    beta   : int;
    zeta   : int;
-   theta: int;
-   tau    : int;
+   theta  : int;
+   epsilon: int;
    ldelta : int;
    gdelta : int;
    si     : int;
    lrt    : int;
-   grt    : int
+   grt    : int;
+   e      : int;
 }
 
 let initial_reductions = {
-   beta = 0; theta = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
-   si = 0; lrt = 0; grt = 0
+   beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0;
+   si = 0; lrt = 0; grt = 0; e = 0;
 }
 
 let reductions = ref initial_reductions
@@ -35,24 +36,25 @@ let reductions = ref initial_reductions
 let clear_reductions () = reductions := initial_reductions
 
 let add 
-   ?(beta=0) ?(theta=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
-   ?(si=0) ?(lrt=0) ?(grt=0) ()
+   ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
+   ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
 = reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
    theta = !reductions.theta + theta;
-   tau = !reductions.tau + tau;
+   epsilon = !reductions.epsilon + epsilon;
    ldelta = !reductions.ldelta + ldelta;
    gdelta = !reductions.gdelta + gdelta;
    si = !reductions.si + si;
    lrt = !reductions.lrt + lrt;
-   grt = !reductions.grt + grt
+   grt = !reductions.grt + grt;
+   e = !reductions.e + e;
 }
 
 let print_reductions () =
    let r = !reductions in
-   let rs = r.beta + r.ldelta + r.zeta + r.theta + r.tau + r.gdelta in
-   let prs = r.si + r.lrt + r.grt 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 delta = r.ldelta + r.gdelta in
    let rt = r.lrt + r.grt in   
    L.warn (P.sprintf "  Reductions summary");
@@ -63,10 +65,11 @@ let print_reductions () =
    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.tau);
+   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)