helm/software/helena/src/common/output.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 KP = Printf
  13
  14 module L  = Log
  15 module G  = Options
  16
  17 type reductions = {
  18    beta   : int;
  19    zeta   : int;
  20    theta  : int;
  21    epsilon: int;
  22    ldelta : int;
  23    gdelta : int;
  24    upsilon: int;
  25    lrt    : int;
  26    grt    : int;
  27    e      : int;
  28    x      : int;
  29 }
  30
  31 let level = 2
  32
  33 let initial_reductions = {
  34    beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0;
  35    lrt = 0; grt = 0; e = 0; x = 0;
  36 }
  37
  38 let reductions = ref initial_reductions
  39
  40 let clear_reductions () = reductions := initial_reductions
  41
  42 let add
  43    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
  44    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
  45 =
  46  if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
  47  if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
  48  if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
  49  if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
  50  if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
  51 reductions := {
  52    beta = !reductions.beta + beta;
  53    zeta = !reductions.zeta + zeta;
  54    theta = !reductions.theta + theta;
  55    epsilon = !reductions.epsilon + epsilon;
  56    ldelta = !reductions.ldelta + ldelta;
  57    gdelta = !reductions.gdelta + gdelta;
  58    upsilon = !reductions.upsilon + upsilon;
  59    lrt = !reductions.lrt + lrt;
  60    grt = !reductions.grt + grt;
  61    e = !reductions.e + e;
  62    x = !reductions.x + x;
  63 }
  64
  65 let print_reductions () =
  66    let r = !reductions in
  67    let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta + r.upsilon in
  68    let prs = r.lrt + r.grt + r.e + r.x in
  69    let delta = r.ldelta + r.gdelta in
  70    let rt = r.lrt + r.grt in
  71    L.warn level (KP.sprintf "Reductions summary");
  72    L.warn level (KP.sprintf "  Proper reductions:        %7u" rs);
  73    L.warn level (KP.sprintf "    Beta:                   %7u" r.beta);
  74    L.warn level (KP.sprintf "    Delta:                  %7u" delta);
  75    L.warn level (KP.sprintf "      Local:                %7u" r.ldelta);
  76    L.warn level (KP.sprintf "      Global:               %7u" r.gdelta);
  77    L.warn level (KP.sprintf "    Theta:                  %7u" r.theta);
  78    L.warn level (KP.sprintf "    Zeta for abbreviation:  %7u" r.zeta);
  79    L.warn level (KP.sprintf "    Zeta for cast:          %7u" r.epsilon);
  80    L.warn level (KP.sprintf "    Sort inclusion:         %7u" r.upsilon);
  81    L.warn level (KP.sprintf "  Pseudo reductions:        %7u" prs);
  82    L.warn level (KP.sprintf "    Reference typing:       %7u" rt);
  83    L.warn level (KP.sprintf "      Local:                %7u" r.lrt);
  84    L.warn level (KP.sprintf "      Global:               %7u" r.grt);
  85    L.warn level (KP.sprintf "    Cast typing:            %7u" r.e);
  86    L.warn level (KP.sprintf "    Binder typing:          %7u" r.x);
  87    L.warn level (KP.sprintf "Relocated nodes (icm):      %7u" !G.icm)