the partial commit continues

with the support for logging the e-reduction steps

diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml
index d33c1be662deda6db265f7169c0795b57913cf7f..b10dda06a4b83f30618790322dd2e5459c3bf49f 100644 (file)
--- 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 70a49d5e8a6814ad481796accc82bb465d36a8ec..9b4955248726eaffd5689491ee31e6af2af79227 100644 (file)
--- 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 1124764885c871d364e7cfd3d6d3c048a17a77ec..2af0b535bb1f9e07bcbea5c3e1a7d63be445dd52 100644 (file)
--- 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 5cfe82b4368d6f0505616b220bf66cba19d57cf5..ba2d294da73ca496c4604cdaeb076c35b7a945f0 100644 (file)
--- 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 3da988f8441eca5db3bc9f5aa687041ccc14087b..ec7f8a65c9bc1e3ee5dde0d9b49e8ee749b7008a 100644 (file)
--- 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 ()
 }