open Ast
open Data
open Util
open Ast_util
(* Utility : extract subscopes of equation ; extract pre declarations *)
(* subscopes :
prog -> expr ext -> (id * eqs * (id * expr ext) list) list
*)
let rec subscopes p e = match fst e with
| AST_idconst _ | AST_identifier _
| AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
| AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e'
| AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
| AST_arrow(e1, e2) ->
subscopes p e1 @ subscopes p e2
| AST_if(e1, e2, e3) ->
subscopes p e1 @ subscopes p e2 @ subscopes p e3
| AST_instance((f, _), args, id) ->
let more = List.flatten (List.map (subscopes p) args) in
let (node, _) = find_node_decl p f in
let args_x = List.map2 (fun id arg -> id, arg) node.args args in
(id, node.body, args_x)::more
(* extract_pre : expr ext -> (id * expr ext) list *)
let rec extract_pre e = match fst e with
| AST_identifier _ | AST_idconst _
| AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
| AST_unary (_, e') | AST_not e' -> extract_pre e'
| AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
| AST_arrow(e1, e2) ->
extract_pre e1 @ extract_pre e2
| AST_if(e1, e2, e3) ->
extract_pre e1 @ extract_pre e2 @ extract_pre e3
| AST_instance((f, _), args, id) ->
List.flatten (List.map extract_pre args)
| AST_pre(e', n) ->
(n, e')::(extract_pre e')
(* Expression evaluation *)
type eval_env = {
p: prog;
c: calc_map;
scopes: string list;
}
(*
eval_expr : eval_env -> string -> expr ext -> (state * value)
*)
let rec eval_expr env st exp =
let sub_eval = eval_expr env in
let scope = List.hd env.scopes in
match fst exp with
| AST_identifier (id, _) | AST_idconst(id, _) ->
let rec aux = function
| [] ->
let st, v = get_var st env.c ("cst/"^id) in st, [v]
| sc::q ->
try let st, v = get_var st env.c (sc^"/"^id) in st, [v]
with _ -> aux q
in aux env.scopes
(* on numerical values *)
| AST_int_const (i, _) -> st, [VInt (int_of_string i)]
| AST_real_const (r, _) -> st, [VReal (float_of_string r)]
| AST_unary(AST_UPLUS, e) -> sub_eval st e
| AST_unary(AST_UMINUS, e) ->
begin match sub_eval st e with
| st, [VInt x] -> st, [VInt (-x)]
| st, [VReal x] -> st, [VReal(-. x)]
| _ -> type_error "Unary on non-numerical."
end
| AST_binary(op, e1, e2) ->
let st, v1 = sub_eval st e1 in
let st, v2 = sub_eval st e2 in
let iop, fop = match op with
| AST_PLUS -> (+), (+.)
| AST_MINUS -> (-), (-.)
| AST_MUL -> ( * ), ( *. )
| AST_DIV -> (/), (/.)
| AST_MOD -> (mod), mod_float
in
begin match v1, v2 with
| [VInt a], [VInt b] -> st, [VInt (iop a b)]
| [VReal a], [VReal b] -> st, [VReal(fop a b)]
| _ -> type_error "Invalid arguments for numerical binary."
end
(* on boolean values *)
| AST_bool_const b -> st, [VBool b]
| AST_binary_rel(op, e1, e2) ->
let st, v1 = sub_eval st e1 in
let st, v2 = sub_eval st e2 in
let r = match op with
| AST_EQ -> (=) | AST_NE -> (<>)
| AST_LT -> (<) | AST_LE -> (<=)
| AST_GT -> (>) | AST_GE -> (>=)
in
begin match v1, v2 with
| [VInt a], [VInt b] -> st, [VBool (r a b)]
| [VReal a], [VReal b] -> st, [VBool (r a b)]
| [VBool a], [VBool b] -> st, [VBool (r a b)]
| _ -> type_error "Invalid arguments for binary relation."
end
| AST_binary_bool(op, e1, e2) ->
let st, v1 = sub_eval st e1 in
let st, v2 = sub_eval st e2 in
let r = match op with
| AST_AND -> (&&) | AST_OR -> (||)
in
begin match v1, v2 with
| [VBool a], [VBool b] -> st, [VBool (r a b)]
| _ -> type_error "Invalid arguments for boolean relation."
end
| AST_not(e) ->
begin match sub_eval st e with
| st, [VBool b] -> st, [VBool (not b)]
| _ -> type_error "Invalid arguments for boolean negation."
end
(* temporal primitives *)
| AST_pre(exp, n) ->
begin try match VarMap.find (scope^"/"^n) st with
| VPrevious x -> st, x
| _ -> st, []
with Not_found -> st, []
end
| AST_arrow(before, after) ->
begin try match VarMap.find (scope^"/init") st with
| VBool true -> sub_eval st before
| VBool false -> sub_eval st after
| _ -> assert false
with Not_found -> assert false
end
(* other *)
| AST_if(cond, a, b) ->
let st, cv = sub_eval st cond in
begin match cv with
| [VBool true] -> sub_eval st a
| [VBool false] -> sub_eval st b
| _ -> type_error "Invalid condition in if."
end
| AST_instance((f, _), args, nid) ->
let (n, _) = find_node_decl env.p f in
List.fold_left
(fun (st, vs) (_, (id,_), _) ->
let st, v = get_var st env.c (scope^"/"^nid^"/"^id) in
st, vs @ [v])
(st, []) n.ret
(* Constant calculation *)
let rec calc_const p d st c =
let env = { p = p; c = c; scopes = ["cst"] } in
match eval_expr env st d.value with
| st, [v] -> VarMap.add ("cst/"^d.name) v st
| _ -> type_error ("Cannot assign tuple to constant" ^ d.name)
let program_consts p =
let cdecl = extract_const_decls p in
let ccmap = List.fold_left
(fun c (d, _) -> VarMap.add ("cst/"^d.name) (F (calc_const p d)) c)
VarMap.empty cdecl
in
List.fold_left
(fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.name) in st)
VarMap.empty
cdecl
(* get initial state for program *)
let program_init_state p root_node =
let (n, _) = find_node_decl p root_node in
let rec aux st p scope eqs =
let st = VarMap.add (scope^"/init") (VBool true) st in
let add_subscopes =
List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs)
in
let add_eq st eq = match fst eq with
| AST_assign(_, e) -> add_subscopes st (subscopes p e)
| AST_assume _ | AST_guarantee _ -> st
| AST_automaton (aid, astates, ret) ->
let (initial, _) = List.find (fun (s, _) -> s.initial) astates in
let st = VarMap.add (scope^":"^aid^".state") (VState initial.name) st in
let add_astate st ((astate:Ast.state), _) =
aux st p (scope^":"^aid^"."^astate.name) astate.body
in
List.fold_left add_astate st astates
| AST_activate _ -> not_implemented "program_init_state activate"
in
List.fold_left add_eq st eqs
in
aux (program_consts p) p "" n.body
(* Program execution *)
(* build calc map *)
let rec build_prog_ccmap p scopes eqs st =
let scope = List.hd scopes in
let add_eq c eq = match fst eq with
| AST_assign(vars, e) ->
let calc st c =
let env = { p = p; c = c; scopes = scopes } in
let st, vals = eval_expr env st e in
List.fold_left2
(fun st (id,_) v -> VarMap.add (scope^"/"^id) v st)
st vars vals
in
let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in
let add_subscope c (ss_id, ss_eqs, ss_args) =
let c = VarMap.merge disjoint_union c
(build_prog_ccmap p [scope^"/"^ss_id] ss_eqs st)
in
let add_v c ((_, (id, _), _), eq) =
let calc st c =
let env = { p = p; c = c; scopes = scopes } in
let st, vals = eval_expr env st eq in
match vals with
| [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st
| _ -> type_error "invalid arity"
in
VarMap.add (scope^"/"^ss_id^"/"^id) (F calc) c
in
List.fold_left add_v c ss_args
in
List.fold_left add_subscope c (subscopes p e)
| AST_assume _ | AST_guarantee _ -> c
| AST_automaton _ -> not_implemented "build_prog_ccmap for automaton"
| AST_activate _ -> not_implemented "build_prog_ccmap for activate"
in
List.fold_left add_eq VarMap.empty eqs
let extract_next_state active env eqs st =
let csts = VarMap.filter
(fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/")
st
in
let rec aux active scopes eqs st nst =
let scope = List.hd env.scopes in
let r = VarMap.add (scope^"/init")
(if active then VBool false
else try VarMap.find (scope^"/init") st with Not_found -> assert false)
nst
in
let add_subscopes active =
List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) ->
aux active [scope^"/"^ss_id] ss_eqs st nst)
in
let add_eq (st, nst) eq = match fst eq with
| AST_assign(vars, e) ->
let st, nst = add_subscopes active (st, nst) (subscopes env.p e) in
List.fold_left (fun (st, nst) (pn, pe) ->
let st, v = if active then eval_expr { env with scopes = scopes } st pe
else st,
try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> []
with Not_found -> []
in
st, VarMap.add (scope^"/"^pn) (VPrevious v) nst)
(st, nst) (extract_pre e)
| AST_assume _ | AST_guarantee _ -> st, nst
| AST_automaton _ -> not_implemented "extract_next_state automaton"
| AST_activate _ -> not_implemented "extract_next_state activate"
in
List.fold_left add_eq (st, r) eqs
in aux active env.scopes eqs st csts
let program_step p st inputs root_node =
let (n, _) = find_node_decl p root_node in
let st = List.fold_left
(fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in
let ccmap = build_prog_ccmap p [""] n.body st in
let st = List.fold_left
(fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st)
st n.ret in
let outputs = List.map
(fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v))
n.ret in
let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in
st, outputs, next_st