(*
    ||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 B = Brg

type counters = {
   eabsts: int;
   eabbrs: int;
   tsorts: int;
   tlrefs: int;
   tgrefs: int;
   tcasts: int;
   tappls: int;
   tabsts: int;
   tabbrs: int
}

let initial_counters = {
   eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
   tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
}

let count_term_binder f c = function
   | B.Abst -> f {c with tabsts = succ c.tabsts}
   | B.Abbr -> f {c with tabbrs = succ c.tabbrs}

let rec count_term f c = function
   | B.Sort _            -> 
      f {c with tsorts = succ c.tsorts}
   | B.LRef _            -> 
      f {c with tlrefs = succ c.tlrefs}
   | B.GRef _            -> 
      f {c with tgrefs = succ c.tgrefs}
   | B.Cast (v, t)       -> 
      let c = {c with tcasts = succ c.tcasts} in
      let f c = count_term f c t in
      count_term f c v
   | B.Appl (v, t)       -> 
      let c = {c with tappls = succ c.tappls} in
      let f c = count_term f c t in
      count_term f c v
   | B.Bind (_, b, u, t) -> 
      let f c = count_term_binder f c b in
      let f c = count_term f c t in
      count_term f c u

let count_obj_binder f c = function
   | B.Abst -> f {c with eabsts = succ c.eabsts}
   | B.Abbr -> f {c with eabbrs = succ c.eabbrs}

let count_obj f c (b, t) =
   let f c = count_obj_binder f c b in
   count_term f c t

let count_item f c = function
   | Some (obj, _) -> count_obj f c obj
   | None          -> f c

let print_counters f c =
   let terms =
      c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
      c.tabbrs
   in
   let items = c.eabsts + c.eabbrs in
   L.warn (P.sprintf "  Kernel representation summary (basic_rg)");
   L.warn (P.sprintf "    Total entry items:        %6u" items);
   L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
   L.warn (P.sprintf "      Definition items:       %6u" c.eabbrs);
   L.warn (P.sprintf "    Total term items:         %6u" terms);
   L.warn (P.sprintf "      Sort items:             %6u" c.tsorts);
   L.warn (P.sprintf "      Local reference items:  %6u" c.tlrefs);
   L.warn (P.sprintf "      Global reference items: %6u" c.tgrefs);
   L.warn (P.sprintf "      Explicit Cast items:    %6u" c.tcasts);
   L.warn (P.sprintf "      Application items:      %6u" c.tappls);
   L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
   L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
   f ()