helm/software/lambda-delta/lib/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 P = Printf
  13 module L = Log
  14
  15 type reductions = {
  16    beta   : int;
  17    zeta   : int;
  18    upsilon: int;
  19    tau    : int;
  20    ldelta : int;
  21    gdelta : int;
  22    si     : int;
  23    lrt    : int;
  24    grt    : int
  25 }
  26
  27 let initial_reductions = {
  28    beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
  29    si = 0; lrt = 0; grt = 0
  30 }
  31
  32 let reductions = ref initial_reductions
  33
  34 let clear_reductions () = reductions := initial_reductions
  35
  36 let add
  37    ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
  38    ?(si=0) ?(lrt=0) ?(grt=0) ()
  39 = reductions := {
  40    beta = !reductions.beta + beta;
  41    zeta = !reductions.zeta + zeta;
  42    upsilon = !reductions.upsilon + upsilon;
  43    tau = !reductions.tau + tau;
  44    ldelta = !reductions.ldelta + ldelta;
  45    gdelta = !reductions.gdelta + gdelta;
  46    si = !reductions.si + si;
  47    lrt = !reductions.lrt + lrt;
  48    grt = !reductions.grt + grt
  49 }
  50
  51 let print_reductions () =
  52    let r = !reductions in
  53    let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in
  54    let prs = r.si + r.lrt + r.grt in
  55    let delta = r.ldelta + r.gdelta in
  56    let rt = r.lrt + r.grt in
  57    L.warn (P.sprintf "  Reductions summary");
  58    L.warn (P.sprintf "    Proper reductions:        %7u" rs);
  59    L.warn (P.sprintf "      Beta:                   %7u" r.beta);
  60    L.warn (P.sprintf "      Delta:                  %7u" delta);
  61    L.warn (P.sprintf "        Local:                %7u" r.ldelta);
  62    L.warn (P.sprintf "        Global:               %7u" r.gdelta);
  63    L.warn (P.sprintf "      Zeta:                   %7u" r.zeta);
  64    L.warn (P.sprintf "      Upsilon:                %7u" r.upsilon);
  65    L.warn (P.sprintf "      Tau:                    %7u" r.tau);
  66    L.warn (P.sprintf "    Pseudo reductions:        %7u" prs);
  67    L.warn (P.sprintf "      Reference typing:       %7u" rt);
  68    L.warn (P.sprintf "        Local:                %7u" r.lrt);
  69    L.warn (P.sprintf "        Global:               %7u" r.grt);
  70    L.warn (P.sprintf "      Sort inclusion:         %7u" r.si)
  71
  72 let indexes = ref false