now type inclusion is correctly managed in the RTM

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 002f12ce11e028bf01dcbc7e89b1c7c9add21a29..08f3a340756e8187297fa966e38e54e5394f1b36 100644 (file)
--- 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 61254620f192ecd21edad2a1c0a13476a8654a37..d781003249fb355d458cc647d7c3ac7644db642b 100644 (file)
--- 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 9d8b34e724c3c2c0709fabfa7aec4c41140cdf18..7ff8609bde734fc4f76f208a84a77ca952715285 100644 (file)
--- 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
+