helm/software/lambda-delta/basic_rg/brgOutput.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module P = Printf
  13 module L = Log
  14 module B = Brg
  15
  16 type counters = {
  17    eabsts: int;
  18    eabbrs: int;
  19    tsorts: int;
  20    tlrefs: int;
  21    tgrefs: int;
  22    tcasts: int;
  23    tappls: int;
  24    tabsts: int;
  25    tabbrs: int
  26 }
  27
  28 let initial_counters = {
  29    eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
  30    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
  31 }
  32
  33 let count_term_binder f c = function
  34    | B.Abst -> f {c with tabsts = succ c.tabsts}
  35    | B.Abbr -> f {c with tabbrs = succ c.tabbrs}
  36
  37 let rec count_term f c = function
  38    | B.Sort _            ->
  39       f {c with tsorts = succ c.tsorts}
  40    | B.LRef _            ->
  41       f {c with tlrefs = succ c.tlrefs}
  42    | B.GRef _            ->
  43       f {c with tgrefs = succ c.tgrefs}
  44    | B.Cast (v, t)       ->
  45       let c = {c with tcasts = succ c.tcasts} in
  46       let f c = count_term f c t in
  47       count_term f c v
  48    | B.Appl (v, t)       ->
  49       let c = {c with tappls = succ c.tappls} in
  50       let f c = count_term f c t in
  51       count_term f c v
  52    | B.Bind (_, b, u, t) ->
  53       let f c = count_term_binder f c b in
  54       let f c = count_term f c t in
  55       count_term f c u
  56
  57 let count_obj_binder f c = function
  58    | B.Abst -> f {c with eabsts = succ c.eabsts}
  59    | B.Abbr -> f {c with eabbrs = succ c.eabbrs}
  60
  61 let count_obj f c (_, _, b, t) =
  62    let f c = count_obj_binder f c b in
  63    count_term f c t
  64
  65 let count_item f c = function
  66    | Some obj -> count_obj f c obj
  67    | None     -> f c
  68
  69 let print_counters f c =
  70    let terms =
  71       c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
  72       c.tabbrs
  73    in
  74    let items = c.eabsts + c.eabbrs in
  75    L.warn (P.sprintf "  Kernel representation summary (basic_rg)");
  76    L.warn (P.sprintf "    Total entry items:        %6u" items);
  77    L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
  78    L.warn (P.sprintf "      Definition items:       %6u" c.eabbrs);
  79    L.warn (P.sprintf "    Total term items:         %6u" terms);
  80    L.warn (P.sprintf "      Sort items:             %6u" c.tsorts);
  81    L.warn (P.sprintf "      Local reference items:  %6u" c.tlrefs);
  82    L.warn (P.sprintf "      Global reference items: %6u" c.tgrefs);
  83    L.warn (P.sprintf "      Explicit Cast items:    %6u" c.tcasts);
  84    L.warn (P.sprintf "      Application items:      %6u" c.tappls);
  85    L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
  86    L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
  87    f ()