+(*
+ ||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