Adapt for real type with Apron ; not very efficient ATM.

1 files changed, 15 insertions, 2 deletions

diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 27cecdb..dd0ffb0 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -162,6 +162,14 @@ end = struct
       | [VReal a], [VReal b] -> [VReal(fop a b)]
       | _ -> type_error "Invalid arguments for numerical binary."
       end
+    | AST_cast(e, ty) ->
+      begin match sub_eval e, ty with
+      | [VInt i], AST_TINT -> [VInt i]
+      | [VReal r], AST_TINT -> [VInt (int_of_float r)]
+      | [VInt i], AST_TREAL -> [VReal (float_of_int i)]
+      | [VReal r], AST_TREAL -> [VReal r]
+      | _ -> type_error "Invalid arguments in cast."
+      end
     (* on boolean values *)
     | AST_bool_const b -> [VBool b]
     | AST_binary_rel(op, e1, e2) ->
@@ -324,7 +332,7 @@ end = struct
   *)
   let is_scope_active env (node, prefix, _) =
     try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act"))
-    with Not_found -> false
+    with Not_found -> false | Bad_datatype -> assert false
 
   (*
     do_weak_transitions : env -> scope -> unit
@@ -382,9 +390,14 @@ end = struct
 
       let init =
         try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init"))
-        with Not_found ->
+        with
+        | Not_found ->
           let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save)
           in pre_init && (not (is_scope_active env (node, prefix, eqs)))
+        | Bad_datatype ->
+            Format.eprintf "%s@."
+              (str_repr_of_val (Hashtbl.find env.vars (node^"/"^prefix^"init")));
+            assert false
       in
       let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in