diff options
Diffstat (limited to 'interpret')
| -rw-r--r-- | interpret/interpret.ml | 171 |
1 files changed, 101 insertions, 70 deletions
diff --git a/interpret/interpret.ml b/interpret/interpret.ml index d141bc6..373ed5f 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -20,18 +20,63 @@ let find_node_decl p id = | AST_node_decl d -> d | _ -> assert false +(* Utility : build 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_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_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 : prog -> calc_map -> state -> string -> expr ext -> (state * value) + eval_expr : eval_env -> string -> expr ext -> (state * value) *) -let rec eval_expr p c scope st exp = - let sub_eval = eval_expr p c scope in +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, _) -> - begin try let st, v = get_var st c (scope^"/"^id) in st, [v] - with No_variable _ -> let st, v = get_var st c ("cst/"^id) in st, [v] - end + 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 No_variable _ -> 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)] @@ -111,16 +156,18 @@ let rec eval_expr p c scope st exp = | _ -> type_error "Invalid condition in if." end | AST_instance((f, _), args, nid) -> - let (n, _) = find_node_decl p f in + let (n, _) = find_node_decl env.p f in List.fold_left - (fun (st, vs) (_, (id,_), _) -> let st, v = get_var st c (scope^"/"^nid^"/"^id) in + (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 = - match eval_expr p c "cst" st d.value with + 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) @@ -140,46 +187,41 @@ let program_consts p = VarMap.empty cdecl -(* Program execution *) - -(* subscopes : - prog -> expr ext -> (id * eqs * (id * expr ext) list) list -*) -let rec subscopes p e = match fst e with - | 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 +(* 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 -(* extract_pre : expr ext -> (id * expr ext) list *) -let rec extract_pre e = match fst e with - | AST_identifier _ | 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') +(* Program execution *) (* build calc map *) -let rec build_prog_ccmap p scope eqs st = +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 st, vals = eval_expr p c scope st e in + 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 @@ -187,15 +229,13 @@ let rec build_prog_ccmap p scope eqs st = 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 (fun _ a b -> match a, b with - | Some x, None -> Some x - | None, Some y -> Some y - | _ -> assert false) c - (build_prog_ccmap p (scope^"/"^ss_id) ss_eqs st) + 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 st, vals = eval_expr p c scope st eq in + 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" @@ -207,15 +247,18 @@ let rec build_prog_ccmap p scope eqs st = 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 p scope eqs st ccmap = +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 scope eqs st nst = + 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) @@ -223,13 +266,13 @@ let extract_next_state active p scope eqs st ccmap = in let add_subscopes active = List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) -> - aux active (scope^"/"^ss_id) ss_eqs st nst) + 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 p e) in + 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 p ccmap scope st 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 -> [] @@ -238,24 +281,11 @@ let extract_next_state active p scope eqs st ccmap = (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 scope eqs st csts + in aux active env.scopes eqs st csts -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 - List.fold_left (fun st eq -> match fst eq with - | AST_assign(_, e) -> add_subscopes st (subscopes p e) - | AST_assume _ | AST_guarantee _ -> st - | AST_automaton _ -> not_implemented "prog_init_state aux automaton") - st eqs - in - aux (program_consts p) p "" n.body let program_step p st inputs root_node = @@ -263,7 +293,7 @@ let program_step p st inputs root_node = 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 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) @@ -271,7 +301,8 @@ let program_step p st inputs root_node = 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 "" n.body st ccmap in + + let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in st, outputs, next_st |