summaryrefslogtreecommitdiff
path: root/interpret
diff options
context:
space:
mode:
Diffstat (limited to 'interpret')
-rw-r--r--interpret/interpret.ml17
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