From 2dc6df301ca3ebf444ec7f767921ee0e57ccd592 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 15 Dec 2014 15:47:41 +0000
Subject: [PATCH] now type inclusion is correctly managed in the RTM

---
 helm/software/helena/src/basic_rg/brgReduction.ml | 10 +++++-----
 helm/software/helena/src/common/layer.ml          |  7 +++++--
 helm/software/helena/src/common/layer.mli         |  3 +++
 3 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 002f12ce1..08f3a3407 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -140,11 +140,7 @@ let rec step st m x =
    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->
-(*      if not !G.cc && st.S.si && N.to_string st.S.lenv n = "0" then begin
-         if !G.summary then O.add ~upsilon:1 ();
-         let e = B.push m.e m.e a B.Void in 
-         step st {m with e = e} t
-      end else *) begin match m.s with
+      if !G.si || N.is_not_zero st n then begin match m.s with
          | []          ->
             let i = tsteps m in
             if i = 0 then m, x, None else
@@ -156,6 +152,10 @@ let rec step st m x =
 	    let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
             let e = B.push m.e c a (B.abbr v) in
 	    step st {m with e = e; s = s} t
+      end else begin
+         if !G.summary then O.add ~upsilon:1 ();
+         let e = B.push m.e m.e a B.Void in 
+         step st {m with e = e} t
       end
    | B.Bind (a, b, t)        ->
       if !G.summary then O.add ~theta:(List.length m.s) ();
diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index 61254620f..d78100324 100644
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -34,10 +34,10 @@ let level = 6
 
 let env_size = 1300
 
-let zero = Fin 0
-
 let warn s = L.warn level s
 
+let zero = Fin 0
+
 let string_of_value k = function
    | Inf        -> ""
    | Fin i      -> string_of_int i
@@ -185,3 +185,6 @@ let assert_equal st n1 n2 =
    if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
       n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
    end; b end
+
+let is_not_zero st n  =
+   let _, n = resolve_layer st n in n.v <> zero
diff --git a/helm/software/helena/src/common/layer.mli b/helm/software/helena/src/common/layer.mli
index 9d8b34e72..7ff8609bd 100644
--- a/helm/software/helena/src/common/layer.mli
+++ b/helm/software/helena/src/common/layer.mli
@@ -36,3 +36,6 @@ val assert_not_zero: status -> layer -> bool
 val assert_zero: status -> layer -> bool
 
 val assert_equal: status -> layer -> layer -> bool
+
+val is_not_zero: status -> layer -> bool
+
-- 
2.39.2