refactoring ...

[helm.git] / helm / software / lambda-delta / src / common / output.ml

diff --git a/helm/software/lambda-delta/src/common/output.ml b/helm/software/lambda-delta/src/common/output.ml
deleted file mode 100644 (file)
index 1124764..0000000
--- a/helm/software/lambda-delta/src/common/output.ml
+++ /dev/null
@@ -1,72 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module P = Printf
-module L = Log
-module G = Options
-
-type reductions = {
-   beta   : int;
-   zeta   : int;
-   theta: int;
-   tau    : int;
-   ldelta : int;
-   gdelta : int;
-   si     : int;
-   lrt    : int;
-   grt    : int
-}
-
-let initial_reductions = {
-   beta = 0; theta = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
-   si = 0; lrt = 0; grt = 0
-}
-
-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) ()
-= reductions := {
-   beta = !reductions.beta + beta;
-   zeta = !reductions.zeta + zeta;
-   theta = !reductions.theta + theta;
-   tau = !reductions.tau + tau;
-   ldelta = !reductions.ldelta + ldelta;
-   gdelta = !reductions.gdelta + gdelta;
-   si = !reductions.si + si;
-   lrt = !reductions.lrt + lrt;
-   grt = !reductions.grt + grt
-}
-
-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 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.tau);
-   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 "      Sort inclusion:         %7u" r.si);
-   L.warn (P.sprintf "  Relocated nodes (icm):      %7u" !G.icm)