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.
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_______________________________________________________________ *)
32 let initial_reductions = {
33 beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0;
34 si = 0; lrt = 0; grt = 0; e = 0;
37 let reductions = ref initial_reductions
39 let clear_reductions () = reductions := initial_reductions
42 ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
43 ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
45 beta = !reductions.beta + beta;
46 zeta = !reductions.zeta + zeta;
47 theta = !reductions.theta + theta;
48 epsilon = !reductions.epsilon + epsilon;
49 ldelta = !reductions.ldelta + ldelta;
50 gdelta = !reductions.gdelta + gdelta;
51 si = !reductions.si + si;
52 lrt = !reductions.lrt + lrt;
53 grt = !reductions.grt + grt;
54 e = !reductions.e + e;
57 let print_reductions () =
58 let r = !reductions in
59 let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta in
60 let prs = r.si + r.lrt + r.grt + r.e in
61 let delta = r.ldelta + r.gdelta in
62 let rt = r.lrt + r.grt in
63 L.warn level (P.sprintf "Reductions summary");
64 L.warn level (P.sprintf " Proper reductions: %7u" rs);
65 L.warn level (P.sprintf " Beta: %7u" r.beta);
66 L.warn level (P.sprintf " Delta: %7u" delta);
67 L.warn level (P.sprintf " Local: %7u" r.ldelta);
68 L.warn level (P.sprintf " Global: %7u" r.gdelta);
69 L.warn level (P.sprintf " Theta: %7u" r.theta);
70 L.warn level (P.sprintf " Zeta for abbreviation: %7u" r.zeta);
71 L.warn level (P.sprintf " Zeta for cast: %7u" r.epsilon);
72 L.warn level (P.sprintf " Pseudo reductions: %7u" prs);
73 L.warn level (P.sprintf " Reference typing: %7u" rt);
74 L.warn level (P.sprintf " Local: %7u" r.lrt);
75 L.warn level (P.sprintf " Global: %7u" r.grt);
76 L.warn level (P.sprintf " Cast typing: %7u" r.e);
77 L.warn level (P.sprintf " Sort inclusion: %7u" r.si);
78 L.warn level (P.sprintf "Relocated nodes (icm): %7u" !G.icm)