diff options
Diffstat (limited to 'interpret')
| -rw-r--r-- | interpret/ast_util.ml | 35 | ||||
| -rw-r--r-- | interpret/data.ml | 12 | ||||
| -rw-r--r-- | interpret/interpret.ml | 43 | ||||
| -rw-r--r-- | interpret/sca.ml | 101 |
4 files changed, 151 insertions, 40 deletions
diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml new file mode 100644 index 0000000..db9a76f --- /dev/null +++ b/interpret/ast_util.ml @@ -0,0 +1,35 @@ +open Ast +open Util + +(* Utility : find declaration of a const / a node *) + +let find_const_decl p id = + match List.find (function + | AST_const_decl (c, _) when c.name = id -> true + | _ -> false) + p with + | AST_const_decl d -> d + | _ -> assert false + +let find_node_decl p id = + match List.find (function + | AST_node_decl (c, _) when c.name = id -> true + | _ -> false) + p with + | AST_node_decl d -> d + | _ -> assert false + +let extract_const_decls = + List.fold_left + (fun l d -> match d with + | AST_const_decl d -> d::l + | _ -> l) + [] + +(* Some errors *) + +let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v) +let no_variable e = error ("No such variable: " ^ e) +let type_error e = error ("Type error: " ^ e) +let not_implemented e = error ("Not implemented: " ^ e) + diff --git a/interpret/data.ml b/interpret/data.ml index 51afcc3..cf7d820 100644 --- a/interpret/data.ml +++ b/interpret/data.ml @@ -2,13 +2,7 @@ open Util open Ast - -exception Combinatorial_cycle of string -exception No_variable of string -exception Type_error of string -let type_error e = raise (Type_error e) -exception Not_implemented of string -let not_implemented e = raise (Not_implemented e) +open Ast_util type scope = string @@ -38,10 +32,10 @@ let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) = let r = f (VarMap.add id VBusy st) c in (* Format.printf "]%s " id; *) r - with Not_found -> raise (No_variable id) + with Not_found -> no_variable id in match VarMap.find id st with - | VBusy -> raise (Combinatorial_cycle id) + | VBusy -> combinatorial_cycle id | v -> st, v (* pretty-printing *) diff --git a/interpret/interpret.ml b/interpret/interpret.ml index 373ed5f..6ff125c 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -1,32 +1,17 @@ open Ast open Data open Util +open Ast_util -(* Utility : find declaration of a const / a node *) -let find_const_decl p id = - match List.find (function - | AST_const_decl (c, _) when c.name = id -> true - | _ -> false) - p with - | AST_const_decl d -> d - | _ -> assert false - -let find_node_decl p id = - match List.find (function - | AST_node_decl (c, _) when c.name = id -> true - | _ -> false) - p with - | AST_node_decl d -> d - | _ -> assert false - -(* Utility : build subscopes of equation ; extract pre declarations *) +(* 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_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> [] + | 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) -> @@ -41,7 +26,8 @@ let rec subscopes p e = match fst e with (* 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_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) -> @@ -69,13 +55,13 @@ 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_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 No_variable _ -> aux q + with _ -> aux q in aux env.scopes (* on numerical values *) | AST_int_const (i, _) -> st, [VInt (int_of_string i)] @@ -172,18 +158,13 @@ let rec calc_const p d st c = | _ -> type_error ("Cannot assign tuple to constant" ^ d.name) let program_consts p = - let cdecl = List.fold_left - (fun l d -> match d with - | AST_const_decl (d, _) -> d::l - | _ -> l) - [] p - in + 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) + (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) + (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.name) in st) VarMap.empty cdecl @@ -211,8 +192,8 @@ let program_init_state p root_node = in aux (program_consts p) p "" n.body -(* Program execution *) +(* Program execution *) (* build calc map *) let rec build_prog_ccmap p scopes eqs st = diff --git a/interpret/sca.ml b/interpret/sca.ml new file mode 100644 index 0000000..4a012ae --- /dev/null +++ b/interpret/sca.ml @@ -0,0 +1,101 @@ +(* Scope analyzer *) + +open Ast +open Util +open Ast_util + +type renaming = (id * bool) VarMap.t + +(* consts_renaming : prog -> renaming *) +let consts_renaming p = + let cdecl = extract_const_decls p in + List.fold_left + (fun rn (d,_) -> VarMap.add d.name (d.name, true) rn) + VarMap.empty + cdecl + +(* add_var_defs : string -> renaming -> var_def list -> renaming *) +let add_var_defs prefix = + List.fold_left + (fun rn (_,(n,_),_) -> VarMap.add n (prefix^n, false) rn) + +(* rename_expr : expr ext -> renaming -> expr ext *) +let rec rename_expr exp rn = + let sub e = rename_expr e rn in + let a = match fst exp with + | AST_identifier(id, l) -> + begin try let (nn, const) = VarMap.find id rn in + if const then AST_idconst(nn, l) else AST_identifier(nn, l) + with Not_found -> loc_error l no_variable id + end + | AST_idconst(id, l) -> assert false (* expression not already renamed *) + | AST_unary(op, e) -> AST_unary(op, sub e) + | AST_binary(op, a, b) -> AST_binary(op, sub a, sub b) + | AST_binary_rel(op, a, b) -> AST_binary_rel(op, sub a, sub b) + | AST_binary_bool(op, a, b) -> AST_binary_bool(op, sub a, sub b) + | AST_not(e) -> AST_not(sub e) + | AST_pre (e, x) -> AST_pre(sub e, x) + | AST_arrow(a, b) -> AST_arrow(sub a, sub b) + | AST_if(a, b, c) -> AST_if(sub a, sub b, sub c) + | AST_instance(i, l, s) -> AST_instance(i, List.map sub l, s) + | x -> x (* other cases : constant literals *) + in a, snd exp + +(* rename_var : renaming -> id -> id *) +let rename_var rn id = + try let (nn, const)= VarMap.find id rn in + if const then error ("Constant "^id^" cannot be defined in node."); + nn + with Not_found -> no_variable id + +let rename_var_ext rn (id, loc) = (rename_var rn id, loc) + +let rename_var_def rn (p, id, t) = (p, rename_var_ext rn id, t) + +(* rename_eqn : renaming -> eqn ext -> eqn ext *) +let rec rename_eqn rn e = + let a = match fst e with + | AST_assign(s, e) -> AST_assign (List.map (rename_var_ext rn) s, rename_expr e rn) + | AST_guarantee(g, e) -> AST_guarantee(g, rename_expr e rn) + | AST_assume(a, e) -> AST_assume(a, rename_expr e rn) + | AST_automaton(aid, states, ret) -> + let rename_state ((st:Ast.state),l) = + let rn = add_var_defs (aid^"."^st.name^".") rn st.locals in + { st with + locals = List.map (rename_var_def rn) st.locals; + body = List.map (rename_eqn rn) st.body; + until = List.map (fun (c, n, r) -> (rename_expr c rn, n, r)) st.until; + }, l + in + AST_automaton(aid, List.map rename_state states, List.map (rename_var rn) ret) + | AST_activate (c, ret) -> + let rec rename_activate_if = function + | AST_activate_if(c, a, b) -> + AST_activate_if(rename_expr c rn, rename_activate_if a, rename_activate_if b) + | AST_activate_body b -> + let rn = add_var_defs (b.id^".") rn b.locals in + AST_activate_body{ b with + locals = List.map (rename_var_def rn) b.locals; + body = List.map (rename_eqn rn) b.body; + } + in + AST_activate(rename_activate_if c, List.map (rename_var rn) ret) + in a, snd e + +(* rename_node : renaming -> node_decl -> node_decl *) +let rename_node const_rn node = + let rn = add_var_defs "" const_rn node.args in + let rn = add_var_defs "" rn node.ret in + let rn = add_var_defs "" rn node.var in + { node with + body = List.map (rename_eqn rn) node.body } + +(* rename_prog : prog -> prog *) +let rename_prog p = + let const_rn = consts_renaming p in + let rn_toplevel = function + | AST_node_decl (n, l) -> AST_node_decl (rename_node const_rn n, l) + | x -> x + in + List.map rn_toplevel p + |