From 0175318715aeb84215a6d3257d417ee5c6091e53 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 10 Nov 2014 17:03:03 +0000 Subject: [PATCH] the partial commit continues with the support for logging the e-reduction steps --- helm/software/helena/src/common/level.ml | 7 +++++- helm/software/helena/src/common/level.mli | 2 ++ helm/software/helena/src/common/output.ml | 27 ++++++++++++---------- helm/software/helena/src/common/output.mli | 4 ++-- helm/software/helena/src/common/status.ml | 4 ++-- 5 files changed, 27 insertions(+), 17 deletions(-) diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml index d33c1be66..b10dda06a 100644 --- a/helm/software/helena/src/common/level.ml +++ b/helm/software/helena/src/common/level.ml @@ -29,7 +29,12 @@ let succ = function let pred = function | None -> None - | Some i when i > 0 -> Some (pred i) + | Some i when i > 1 -> Some (pred i) + | _ -> Some 0 + +let minus n j = match n with + | None -> None + | Some i when i > j -> Some (i - j) | _ -> Some 0 let to_string = function diff --git a/helm/software/helena/src/common/level.mli b/helm/software/helena/src/common/level.mli index 70a49d5e8..9b4955248 100644 --- a/helm/software/helena/src/common/level.mli +++ b/helm/software/helena/src/common/level.mli @@ -23,4 +23,6 @@ val succ: level -> level val pred: level -> level +val minus: level -> int -> level + val to_string: level -> string diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 112476488..2af0b535b 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -16,18 +16,19 @@ module G = Options type reductions = { beta : int; zeta : int; - theta: int; - tau : int; + theta : int; + epsilon: int; ldelta : int; gdelta : int; si : int; lrt : int; - grt : int + grt : int; + e : int; } let initial_reductions = { - beta = 0; theta = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0; - si = 0; lrt = 0; grt = 0 + beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; + si = 0; lrt = 0; grt = 0; e = 0; } let reductions = ref initial_reductions @@ -35,24 +36,25 @@ let reductions = ref initial_reductions let clear_reductions () = reductions := initial_reductions let add - ?(beta=0) ?(theta=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) - ?(si=0) ?(lrt=0) ?(grt=0) () + ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) + ?(si=0) ?(lrt=0) ?(grt=0) ?(e=0) () = reductions := { beta = !reductions.beta + beta; zeta = !reductions.zeta + zeta; theta = !reductions.theta + theta; - tau = !reductions.tau + tau; + epsilon = !reductions.epsilon + epsilon; ldelta = !reductions.ldelta + ldelta; gdelta = !reductions.gdelta + gdelta; si = !reductions.si + si; lrt = !reductions.lrt + lrt; - grt = !reductions.grt + grt + grt = !reductions.grt + grt; + e = !reductions.e + e; } let print_reductions () = let r = !reductions 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 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 delta = r.ldelta + r.gdelta in let rt = r.lrt + r.grt in L.warn (P.sprintf " Reductions summary"); @@ -63,10 +65,11 @@ let print_reductions () = L.warn (P.sprintf " Global: %7u" r.gdelta); 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 " Zeta for cast: %7u" r.epsilon); L.warn (P.sprintf " Pseudo reductions: %7u" prs); L.warn (P.sprintf " Reference typing: %7u" rt); L.warn (P.sprintf " Local: %7u" r.lrt); L.warn (P.sprintf " Global: %7u" r.grt); + L.warn (P.sprintf " Cast typing: %7u" r.e); L.warn (P.sprintf " Sort inclusion: %7u" r.si); L.warn (P.sprintf " Relocated nodes (icm): %7u" !G.icm) diff --git a/helm/software/helena/src/common/output.mli b/helm/software/helena/src/common/output.mli index 5cfe82b43..ba2d294da 100644 --- a/helm/software/helena/src/common/output.mli +++ b/helm/software/helena/src/common/output.mli @@ -12,8 +12,8 @@ val clear_reductions: unit -> unit val add: - ?beta:int -> ?theta:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> - ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> + ?beta:int -> ?theta:int -> ?epsilon:int -> ?ldelta:int -> ?gdelta:int -> + ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> ?e:int -> unit -> unit val print_reductions: unit -> unit diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml index 3da988f84..ec7f8a65c 100644 --- a/helm/software/helena/src/common/status.ml +++ b/helm/software/helena/src/common/status.ml @@ -14,7 +14,7 @@ module Q = Ccs type status = { delta: bool; (* global delta-expansion *) - rt: bool; (* reference typing *) +(* rt: bool; (* reference typing *) *) si: bool; (* sort inclusion *) expand: bool; (* always expand global definitions *) cc: Q.csys; (* conversion constraints *) @@ -23,7 +23,7 @@ type status = { (* helpers ******************************************************************) let initial_status () = { - delta = false; rt = false; + delta = false; (* rt = false; *) si = !G.si; expand = !G.expand; cc = Q.init () } -- 2.39.2