- siimplifified RTM (one register less) now counts x-steps.

[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 a72f94318d785686562302c3ddb80d04c4b0157a..013287243d5e1e0aaebe03b5b0390492a49909c8 100644 (file)
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -25,13 +25,14 @@ type reductions = {
    lrt    : int;
    grt    : int;
    e      : int;
+   x      : int;
 }
 
 let level = 2
 
 let initial_reductions = {
    beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0;
-   lrt = 0; grt = 0; e = 0;
+   lrt = 0; grt = 0; e = 0; x = 0;
 }
 
 let reductions = ref initial_reductions
@@ -40,7 +41,7 @@ let clear_reductions () = reductions := initial_reductions
 
 let add 
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
-   ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
+   ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
 =
 (*
  if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
@@ -60,12 +61,13 @@ reductions := {
    lrt = !reductions.lrt + lrt;
    grt = !reductions.grt + grt;
    e = !reductions.e + e;
+   x = !reductions.x + x;
 }
 
 let print_reductions () =
    let r = !reductions 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 prs = r.lrt + r.grt + r.e + r.x in
    let delta = r.ldelta + r.gdelta in
    let rt = r.lrt + r.grt in
    L.warn level (KP.sprintf "Reductions summary");
@@ -82,5 +84,6 @@ let print_reductions () =
    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 "    Cast typing:            %7u" r.e);
+   L.warn level (KP.sprintf "    Binder typing:          %7u" r.x);  
    L.warn level (KP.sprintf "Relocated nodes (icm):      %7u" !G.icm)