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