(*
    ||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 KP = Printf

module L  = Log
module G  = Options

IFDEF SUMMARY THEN

type reductions = {
   beta   : int;
   zeta   : int;
   theta  : int;
   epsilon: int;
   ldelta : int;
   gdelta : int;
   upsilon: int;
   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; x = 0;
}

let reductions = ref initial_reductions

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) ?(x=0) ()
=
(*
   if !G.ct >= level then begin
      if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
      if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
      if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
      if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
      if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
   end;
*)
reductions := {
   beta = !reductions.beta + beta;
   zeta = !reductions.zeta + zeta;
   theta = !reductions.theta + theta;
   epsilon = !reductions.epsilon + epsilon;
   ldelta = !reductions.ldelta + ldelta;
   gdelta = !reductions.gdelta + gdelta;
   upsilon = !reductions.upsilon + upsilon;
   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 + r.x in
   let delta = r.ldelta + r.gdelta in
   let rt = r.lrt + r.grt in
   L.warn level (KP.sprintf "Reductions summary");
   L.warn level (KP.sprintf "  Proper reductions:        %7u" rs);
   L.warn level (KP.sprintf "    Beta:                   %7u" r.beta);
   L.warn level (KP.sprintf "    Delta:                  %7u" delta);
   L.warn level (KP.sprintf "      Local:                %7u" r.ldelta);
   L.warn level (KP.sprintf "      Global:               %7u" r.gdelta);
   L.warn level (KP.sprintf "    Theta:                  %7u" r.theta);
   L.warn level (KP.sprintf "    Zeta for abbreviation:  %7u" r.zeta);
   L.warn level (KP.sprintf "    Zeta for cast:          %7u" r.epsilon);
   L.warn level (KP.sprintf "    Sort inclusion:         %7u" r.upsilon);
   L.warn level (KP.sprintf "  Pseudo reductions:        %7u" prs);
   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 "    Binder typing:          %7u" r.x);
IFDEF TYPE THEN
   L.warn level (KP.sprintf "Relocated nodes (icm):      %7u" !G.icm)
ELSE () END

END