type reductions = {
beta : int;
zeta : int;
- upsilon: int;
+ theta: int;
tau : int;
ldelta : int;
gdelta : int;
}
let initial_reductions = {
- beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
+ beta = 0; theta = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
si = 0; lrt = 0; grt = 0
}
let clear_reductions () = reductions := initial_reductions
let add
- ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
+ ?(beta=0) ?(theta=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
?(si=0) ?(lrt=0) ?(grt=0) ()
= reductions := {
beta = !reductions.beta + beta;
zeta = !reductions.zeta + zeta;
- upsilon = !reductions.upsilon + upsilon;
+ theta = !reductions.theta + theta;
tau = !reductions.tau + tau;
ldelta = !reductions.ldelta + ldelta;
gdelta = !reductions.gdelta + gdelta;
let print_reductions () =
let r = !reductions in
- let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in
+ let rs = r.beta + r.ldelta + r.zeta + r.theta + r.tau + r.gdelta in
let prs = r.si + r.lrt + r.grt in
let delta = r.ldelta + r.gdelta in
let rt = r.lrt + r.grt in
L.warn (P.sprintf " Delta: %7u" delta);
L.warn (P.sprintf " Local: %7u" r.ldelta);
L.warn (P.sprintf " Global: %7u" r.gdelta);
- L.warn (P.sprintf " Zeta: %7u" r.zeta);
- L.warn (P.sprintf " Upsilon: %7u" r.upsilon);
- L.warn (P.sprintf " Tau: %7u" r.tau);
+ L.warn (P.sprintf " Theta: %7u" r.theta);
+ L.warn (P.sprintf " Zeta for abbreviation: %7u" r.zeta);
+ L.warn (P.sprintf " Zeta for cast: %7u" r.tau);
L.warn (P.sprintf " Pseudo reductions: %7u" prs);
L.warn (P.sprintf " Reference typing: %7u" rt);
L.warn (P.sprintf " Local: %7u" r.lrt);