lambda-delta:

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

diff --git a/helm/software/lambda-delta/lib/output.ml b/helm/software/lambda-delta/lib/output.ml
new file mode 100644 (file)
index 0000000..6dd526b
--- /dev/null
+++ b/helm/software/lambda-delta/lib/output.ml
@@ -0,0 +1,72 @@
+(*
+    ||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
+
+type reductions = {
+   beta   : int;
+   zeta   : int;
+   upsilon: int;
+   tau    : int;
+   ldelta : int;
+   gdelta : int;
+   si     : int;
+   lrt    : int;
+   grt    : int
+}
+
+let initial_reductions = {
+   beta = 0; upsilon = 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) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
+   ?(si=0) ?(lrt=0) ?(grt=0) ()
+= reductions := {
+   beta = !reductions.beta + beta;
+   zeta = !reductions.zeta + zeta;
+   upsilon = !reductions.upsilon + upsilon;
+   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.upsilon + 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 "      Zeta:                   %7u" r.zeta);
+   L.warn (P.sprintf "      Upsilon:                %7u" r.upsilon);
+   L.warn (P.sprintf "      Tau:                    %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)
+
+let indexes = ref false