\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
-module L = Log
-module G = Options
+module L = Log
+module G = Options
+
+IFDEF SUMMARY THEN
type reductions = {
beta : int;
epsilon: int;
ldelta : int;
gdelta : int;
- si : int;
+ upsilon: int;
lrt : int;
grt : int;
e : int;
+ x : int;
}
let level = 2
let initial_reductions = {
- beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0;
- si = 0; lrt = 0; grt = 0; e = 0;
+ beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; upsilon = 0;
+ lrt = 0; grt = 0; e = 0; x = 0;
}
let reductions = ref initial_reductions
let add
?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
- ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) ()
-= reductions := {
+ ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
+=
+(*
+ if !G.ct >= level then begin
+ if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
+ if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
+ if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
+ if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
+ if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
+ end;
+*)
+reductions := {
beta = !reductions.beta + beta;
zeta = !reductions.zeta + zeta;
theta = !reductions.theta + theta;
epsilon = !reductions.epsilon + epsilon;
ldelta = !reductions.ldelta + ldelta;
gdelta = !reductions.gdelta + gdelta;
- si = !reductions.si + si;
+ upsilon = !reductions.upsilon + upsilon;
lrt = !reductions.lrt + lrt;
grt = !reductions.grt + grt;
e = !reductions.e + e;
+ x = !reductions.x + x;
}
let print_reductions () =
let r = !reductions in
- let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta in
- let prs = r.si + r.lrt + r.grt + r.e in
+ let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta + r.upsilon in
+ let prs = r.lrt + r.grt + r.e + r.x in
let delta = r.ldelta + r.gdelta in
let rt = r.lrt + r.grt in
- L.warn level (P.sprintf "Reductions summary");
- L.warn level (P.sprintf " Proper reductions: %7u" rs);
- L.warn level (P.sprintf " Beta: %7u" r.beta);
- L.warn level (P.sprintf " Delta: %7u" delta);
- L.warn level (P.sprintf " Local: %7u" r.ldelta);
- L.warn level (P.sprintf " Global: %7u" r.gdelta);
- L.warn level (P.sprintf " Theta: %7u" r.theta);
- L.warn level (P.sprintf " Zeta for abbreviation: %7u" r.zeta);
- L.warn level (P.sprintf " Zeta for cast: %7u" r.epsilon);
- L.warn level (P.sprintf " Pseudo reductions: %7u" prs);
- L.warn level (P.sprintf " Reference typing: %7u" rt);
- L.warn level (P.sprintf " Local: %7u" r.lrt);
- L.warn level (P.sprintf " Global: %7u" r.grt);
- L.warn level (P.sprintf " Cast typing: %7u" r.e);
- L.warn level (P.sprintf " Sort inclusion: %7u" r.si);
- L.warn level (P.sprintf "Relocated nodes (icm): %7u" !G.icm)
+ L.warn level (KP.sprintf "Reductions summary");
+ L.warn level (KP.sprintf " Proper reductions: %7u" rs);
+ L.warn level (KP.sprintf " Beta: %7u" r.beta);
+ L.warn level (KP.sprintf " Delta: %7u" delta);
+ L.warn level (KP.sprintf " Local: %7u" r.ldelta);
+ L.warn level (KP.sprintf " Global: %7u" r.gdelta);
+ L.warn level (KP.sprintf " Theta: %7u" r.theta);
+ L.warn level (KP.sprintf " Zeta for abbreviation: %7u" r.zeta);
+ L.warn level (KP.sprintf " Zeta for cast: %7u" r.epsilon);
+ L.warn level (KP.sprintf " Sort inclusion: %7u" r.upsilon);
+ L.warn level (KP.sprintf " Pseudo reductions: %7u" prs);
+ L.warn level (KP.sprintf " Reference typing: %7u" rt);
+ L.warn level (KP.sprintf " Local: %7u" r.lrt);
+ L.warn level (KP.sprintf " Global: %7u" r.grt);
+ L.warn level (KP.sprintf " Cast typing: %7u" r.e);
+ L.warn level (KP.sprintf " Binder typing: %7u" r.x);
+IFDEF TYPE THEN
+ L.warn level (KP.sprintf "Relocated nodes (icm): %7u" !G.icm)
+ELSE () END
+
+END