From f97a886970bef9e1d6e8a1e217732d6ef8be087e Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 1 Jul 2014 15:42:57 +0200 Subject: Adapt for real type with Apron ; not very efficient ATM. --- interpret/interpret.ml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) (limited to 'interpret') 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 -- cgit v1.2.3