open Ast
open Util
open Ast_util
open Interface
module I : INTERPRET = struct
(* Values for variables *)
exception Bad_datatype
type value =
| VInt of int
| VBool of bool
| VReal of float
| VState of id
| VPrevious of value list
| VBusy (* intermediate value : calculating ! *)
| VCalc of (unit -> value)
let int_value i = VInt i
let bool_value b = VBool b
let real_value r = VReal r
let as_int = function
| VInt i -> i
| _ -> raise Bad_datatype
let as_bool = function
| VBool b -> b
| _ -> raise Bad_datatype
let as_real = function
| VReal r -> r
| _ -> raise Bad_datatype
let rec str_repr_of_val = function
| VInt i -> string_of_int i
| VReal r -> string_of_float r
| VBool b -> if b then "true" else "false"
| VState s -> "state " ^ s
| VPrevious p ->
"[" ^
List.fold_left (fun s v ->
(if s = "" then "" else s ^ ", ") ^ str_repr_of_val v)
"" p
^ "]"
| VBusy -> "#"
| VCalc _ -> "()"
(* States of the interpret *)
(* path to node * subscope prefix in node * equations in scope *)
type scope = id * id * eqn ext list
type state = {
p : prog;
root_scope : scope;
outputs : id list;
save : value VarMap.t;
}
let print_state fmt st =
VarMap.iter
(fun id v -> Format.fprintf fmt "%s = %s@." id (str_repr_of_val v))
st.save
type io = (id * value) list
(* Internal type env : contains the environment for state calculation *)
type env = {
st : state;
vars : (id, value) Hashtbl.t;
}
(*
get_var : env -> id -> id -> value
Gets the value of a variable relative to a node path.
*)
let get_var env node id =
let p = node^"/"^id in
try match Hashtbl.find env.vars p with
| VCalc f ->
Hashtbl.replace env.vars p VBusy;
f ()
| VBusy -> combinatorial_cycle p
| x -> x
with
| Not_found -> no_variable p
(*
eval_expr : env -> (id * id) -> expr ext -> value list
*)
let rec eval_expr env (node, prefix) exp =
let sub_eval = eval_expr env (node, prefix) in
match fst exp with
| AST_identifier (id, _) ->
[loc_error (snd exp) (get_var env node) id]
| AST_idconst (id, _) ->
begin try [VarMap.find ("cst/"^id) env.st.save]
with Not_found -> loc_error (snd exp) no_variable id end
(* on numerical values *)
| AST_int_const (i, _) -> [VInt (int_of_string i)]
| AST_real_const (r, _) -> [VReal (float_of_string r)]
| AST_unary(AST_UPLUS, e) -> sub_eval e
| AST_unary(AST_UMINUS, e) ->
begin match sub_eval e with
| [VInt x] -> [VInt (-x)]
| [VReal x] -> [VReal(-. x)]
| _ -> type_error "Unary on non-numerical."
end
| AST_binary(op, e1, e2) ->
let iop, fop = match op with
| AST_PLUS -> (+), (+.)
| AST_MINUS -> (-), (-.)
| AST_MUL -> ( * ), ( *. )
| AST_DIV -> (/), (/.)
| AST_MOD -> (mod), mod_float
in
begin match sub_eval e1, sub_eval e2 with
| [VInt a], [VInt b] -> [VInt (iop a b)]
| [VReal a], [VReal b] -> [VReal(fop a b)]
| _ -> type_error "Invalid arguments for numerical binary."
end
(* on boolean values *)
| AST_bool_const b -> [VBool b]
| AST_binary_rel(op, e1, e2) ->
let r = match op with
| AST_EQ -> (=) | AST_NE -> (<>)
| AST_LT -> (<) | AST_LE -> (<=)
| AST_GT -> (>) | AST_GE -> (>=)
in
begin match sub_eval e1, sub_eval e2 with
| [VInt a], [VInt b] -> [VBool (r a b)]
| [VReal a], [VReal b] -> [VBool (r a b)]
| [VBool a], [VBool b] -> [VBool (r a b)]
| _ -> type_error "Invalid arguments for binary relation."
end
| AST_binary_bool(op, e1, e2) ->
let r = match op with
| AST_AND -> (&&) | AST_OR -> (||)
in
begin match sub_eval e1, sub_eval e2 with
| [VBool a], [VBool b] -> [VBool (r a b)]
| _ -> type_error "Invalid arguments for boolean relation."
end
| AST_not(e) ->
begin match sub_eval e with
| [VBool b] -> [VBool (not b)]
| _ -> type_error "Invalid arguments for boolean negation."
end
(* temporal primitives *)
| AST_pre(exp, n) ->
begin try match VarMap.find (node^"/"^prefix^n) env.st.save with
| VPrevious x -> x
| _ -> assert false
with Not_found -> []
end
| AST_arrow(before, after) ->
begin try match VarMap.find (node^"/"^prefix^"init") env.st.save with
| VBool true -> sub_eval before
| VBool false -> sub_eval after
| _ -> assert false
with Not_found -> assert false
end
(* other *)
| AST_if(cond, a, b) ->
begin match sub_eval cond with
| [VBool true] -> sub_eval a
| [VBool false] -> sub_eval b
| _ -> type_error "Invalid condition in if."
end
| AST_instance((f, _), args, nid) ->
let (n, _) = find_node_decl env.st.p f in
List.map
(fun (_, (id, _), _) -> get_var env (node^"/"^nid) id)
n.ret
(*
reset_scope : env -> scope -> unit
Sets all the init variables to true, and all the state variables
to initial state. Does this recursively.
*)
let rec reset_scope env (node, prefix, eqs) =
Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true);
let do_exp e =
List.iter
(fun (id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs))
(extract_instances env.st.p e)
in
let do_eq (e, _) = match e with
| AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e
| AST_automaton (aid, states, _) ->
let (init_state, _) = List.find (fun (st, _) -> st.initial) states in
Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name);
List.iter
(fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body))
states
| AST_activate (x, _) ->
let rec aux = function
| AST_activate_if (_, a, b) -> aux a; aux b
| AST_activate_body b ->
reset_scope env (node, b.act_id^".", b.body)
in aux x
in
List.iter do_eq eqs
(*
activate_scope : env -> scope -> unit
Adds functions for calculating the variables in this scope.
For assign : simple !
For automaton : lazily select+activate automaton state (would enable
implementation of strong transitions)
For activate : lazily select+activate active block
*)
let rec activate_scope env (node, prefix, eqs) =
Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true);
let do_expr e =
List.iter
(fun (id, eqs, args) ->
activate_scope env (node^"/"^id, "", eqs);
let do_arg ((_,(name,_),_), expr) =
let apath = node^"/"^id^"/"^name in
let calc () =
match eval_expr env (node, prefix) expr with
| [v] -> Hashtbl.replace env.vars apath v; v
| _ -> loc_error (snd expr) error "Unsupported arity for argument."
in
Hashtbl.replace env.vars apath (VCalc calc)
in
List.iter do_arg args)
(extract_instances env.st.p e)
in
let do_eq (e, _) = match e with
| AST_assign(vars, e) ->
do_expr e;
let calc i () =
let vals = eval_expr env (node, prefix) e in
List.iter2 (fun (id, _) v ->
Hashtbl.replace env.vars (node^"/"^id) v) vars vals;
List.nth vals i
in
List.iteri
(fun i (id, _) ->
Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc i)))
vars
| AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e
| _ -> not_implemented "activate_scope"
in
List.iter do_eq eqs
(*
is_scope_active : env -> scope -> bool
*)
let is_scope_active env (node, prefix, _) =
try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act"))
with Not_found -> false
(*
do_weak_transitions : env -> scope -> unit
*)
let do_weak_transitions env (node, prefix, eqs) =
not_implemented "do_weak_transitions"
(*
extract_st : env -> state
*)
let extract_st env =
let rec aux (node, prefix, eqs) save =
let init =
try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init"))
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)))
in
let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in
let save_expr save e =
let save = List.fold_left
(fun save (id, expr) ->
VarMap.add
(node^"/"^prefix^id)
(VPrevious (eval_expr env (node, prefix) expr))
save)
save (extract_pre e) in
let save = List.fold_left
(fun save (n, eqs, _) ->
aux (node^"/"^n, "", eqs) save)
save (extract_instances env.st.p e)
in save
in
let save_eq save eq = match fst eq with
| AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
save_expr save e
| AST_automaton(aid, states, _) -> not_implemented "save_eq automaton"
| AST_activate(r, _) -> not_implemented "save_eq activate"
in
List.fold_left save_eq save eqs
in
let consts = VarMap.filter (fun k _ -> k.[0] <> '/') env.st.save in
{ env.st with save = aux env.st.root_scope consts }
(*
init_state : prog -> id -> state
*)
let init_state p root =
let (n, _) = find_node_decl p root in
let root_scope = ("", "", n.body) in
let st = {
p = p;
root_scope = root_scope;
save = VarMap.empty;
outputs = (List.map (fun (_,(n,_),_) -> n) n.ret);
} in
let env = { st = st; vars = Hashtbl.create 42 } in
(* calculate constants *)
List.iter (function
| AST_const_decl(d, l) ->
let cpath = "cst/" ^ d.c_name in
Hashtbl.replace env.vars cpath (VCalc (fun () ->
match eval_expr env ("cst", "") d.value with
| [v] -> Hashtbl.replace env.vars cpath v; v
| _ -> loc_error l error "Arity error in constant expression."))
| _ -> ())
p;
List.iter (function
| AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name)
| _ -> ())
p;
reset_scope env root_scope;
{ st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
(*
step : state -> io -> (state * io)
*)
let step st i =
let vars = Hashtbl.create 10 in
List.iter (fun (k, v) -> Hashtbl.replace vars ("/"^k) v) i;
let env = { st = st; vars = vars } in
activate_scope env st.root_scope;
(*
Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars;
*)
let out = List.map (fun id -> id, get_var env "" id) st.outputs in
(* do_weak_transitions env st.root_scope; *)
extract_st env, out
end
