(*
    ||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 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_entry_binder f c = function
   | B.Abst -> f {c with eabsts = succ c.eabsts}
   | B.Abbr -> f {c with eabbrs = succ c.eabbrs}

let count_entry f c (_, b, t) =
   let f c = count_entry_binder f c b in
   count_term f c t

let count_item f c = function
   | Some e -> count_entry f c e
   | 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
   Printf.printf "  Kernel representation summary (basic_rg)\n";
   Printf.printf "    Total entry items:        %6u\n" items;
   Printf.printf "      Declaration items:      %6u\n" c.eabsts;
   Printf.printf "      Definition items:       %6u\n" c.eabbrs;
   Printf.printf "    Total term items:         %6u\n" terms;
   Printf.printf "      Sort items:             %6u\n" c.tsorts;
   Printf.printf "      Local reference items:  %6u\n" c.tlrefs;
   Printf.printf "      Global reference items: %6u\n" c.tgrefs;
   Printf.printf "      Explicit Cast items:    %6u\n" c.tcasts;
   Printf.printf "      Application items:      %6u\n" c.tappls;
   Printf.printf "      Abstraction items:      %6u\n" c.tabsts;
   Printf.printf "      Abbreviation items:     %6u\n" c.tabbrs;
   flush stdout; f ()