]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/common/output.ml
update in basic_2
[helm.git] / 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 IFDEF SUMMARY THEN
18
19 type reductions = {
20    beta   : int;
21    zeta   : int;
22    theta  : int;
23    epsilon: int;
24    ldelta : int;
25    gdelta : int;
26    upsilon: int;
27    lrt    : int;
28    grt    : int;
29    e      : int;
30    x      : int;
31 }
32
33 let level = 2
34
35 let initial_reductions = {
36    beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0;
37    lrt = 0; grt = 0; e = 0; x = 0;
38 }
39
40 let reductions = ref initial_reductions
41
42 let clear_reductions () = reductions := initial_reductions
43
44 let add 
45    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
46    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
47 =
48 (*
49    if !G.ct >= level then begin
50       if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
51       if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
52       if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
53       if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
54       if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
55    end;
56 *)
57 reductions := {
58    beta = !reductions.beta + beta;
59    zeta = !reductions.zeta + zeta;
60    theta = !reductions.theta + theta;
61    epsilon = !reductions.epsilon + epsilon;
62    ldelta = !reductions.ldelta + ldelta;
63    gdelta = !reductions.gdelta + gdelta;
64    upsilon = !reductions.upsilon + upsilon;
65    lrt = !reductions.lrt + lrt;
66    grt = !reductions.grt + grt;
67    e = !reductions.e + e;
68    x = !reductions.x + x;
69 }
70
71 let print_reductions () =
72    let r = !reductions in
73    let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta + r.upsilon in
74    let prs = r.lrt + r.grt + r.e + r.x in
75    let delta = r.ldelta + r.gdelta in
76    let rt = r.lrt + r.grt in
77    L.warn level (KP.sprintf "Reductions summary");
78    L.warn level (KP.sprintf "  Proper reductions:        %7u" rs);
79    L.warn level (KP.sprintf "    Beta:                   %7u" r.beta);
80    L.warn level (KP.sprintf "    Delta:                  %7u" delta);
81    L.warn level (KP.sprintf "      Local:                %7u" r.ldelta);
82    L.warn level (KP.sprintf "      Global:               %7u" r.gdelta);
83    L.warn level (KP.sprintf "    Theta:                  %7u" r.theta);
84    L.warn level (KP.sprintf "    Zeta for abbreviation:  %7u" r.zeta);
85    L.warn level (KP.sprintf "    Zeta for cast:          %7u" r.epsilon);
86    L.warn level (KP.sprintf "    Sort inclusion:         %7u" r.upsilon);
87    L.warn level (KP.sprintf "  Pseudo reductions:        %7u" prs);
88    L.warn level (KP.sprintf "    Reference typing:       %7u" rt);
89    L.warn level (KP.sprintf "      Local:                %7u" r.lrt);
90    L.warn level (KP.sprintf "      Global:               %7u" r.grt);
91    L.warn level (KP.sprintf "    Cast typing:            %7u" r.e);
92    L.warn level (KP.sprintf "    Binder typing:          %7u" r.x);
93 IFDEF TYPE THEN
94    L.warn level (KP.sprintf "Relocated nodes (icm):      %7u" !G.icm)
95 ELSE () END
96
97 END