- bug fix in the RTM

[helm.git] / helm / software / helena / src / common / layer.ml

diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index 494b3915937027a1ee5f96227416edb3f0cd6708..ed2b140e4a339b823a68e9e1c7004487be6487f1 100644 (file)
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -44,8 +44,9 @@ let string_of_value k = function
    | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
    | Unk        -> "-" ^ J.string_of_mark k
 
+(* Note: remove assigned variables *)
 let pp_table st =
-   let map k n =
+   let map k n = 
       warn (Printf.sprintf "%s: v %s (s:%b b:%b)" 
          (J.string_of_mark k) (string_of_value k n.v) n.s n.b
       )
@@ -81,10 +82,11 @@ let resolve_layer st = function
 let rec generated st h i =
    let default = dynamic h i in
    let k = J.new_mark () in
-   match resolve_key_with_default st default k with
-      | k, n when n = default   -> if !G.trace >= level then pp_table st; n
-      | _, n when n.s = true -> generated st h i
-      | _                    -> assert false
+   let k, n = resolve_key_with_default st default k in 
+   if n.s then generated st h i else begin
+      if n <> default then H.replace st k default;
+      if !G.trace >= level then pp_table st; default
+   end
 
 let assert_finite st n j =
    if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
@@ -133,11 +135,14 @@ let rec unknown st =
    if !G.trace >= level then warn "UNKNOWN";
    let default = empty () in
    let k = J.new_mark () in
-   match resolve_key_with_default st default k with
-      | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
-      | _, n when n.s = true  -> n
-      | _                     -> unknown st
-
+   let k, n = resolve_key_with_default st default k in
+   if n.s then match n.v with
+      | Inf
+      | Fin _ -> n
+      | Unk   -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+      | Ref _ -> assert false
+   else unknown st
+ 
 let minus st n j =
    if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
    let rec aux k n j = match n.v with
@@ -188,3 +193,4 @@ let assert_equal st n1 n2 =
 
 let is_not_zero st n  =
    let _, n = resolve_layer st n in n.v <> zero
+