diff options
Diffstat (limited to 'frontend')
| -rw-r--r-- | frontend/ast_printer.ml | 12 | ||||
| -rw-r--r-- | frontend/ast_util.ml | 75 | ||||
| -rw-r--r-- | frontend/rename.ml | 102 | ||||
| -rw-r--r-- | frontend/typing.ml | 178 |
4 files changed, 367 insertions, 0 deletions
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 3ac881e..7ddcb67 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -1,5 +1,6 @@ open Ast open Lexing +open Typing (* Locations *) @@ -252,3 +253,14 @@ let print_toplevel fmt = function let print_prog fmt p = List.iter (print_toplevel fmt) p + + +(* Typed variable *) + +let print_type fmt = function + | TInt -> Format.fprintf fmt "int" + | TReal -> Format.fprintf fmt "real" + | TEnum e -> Format.fprintf fmt "enum { %a }" (print_list print_id ", ") e + +let print_typed_var fmt (p, id, t) = + Format.fprintf fmt "%s%s: %a" (if p then "probe " else "") id print_type t diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml new file mode 100644 index 0000000..a7953ad --- /dev/null +++ b/frontend/ast_util.ml @@ -0,0 +1,75 @@ +open Ast +open Util + +(* 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) +let invalid_arity e = error ("Invalid arity (" ^ e ^ ")") + +(* Utility : find declaration of a const / a node *) + +let find_const_decl p id = + match List.find (function + | AST_const_decl (c, _) when c.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.n_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) + [] + + + +(* Utility : find instances declared in an expression *) + +(* extract_instances : + prog -> expr ext -> (id * id * eqs * (var_def * expr ext) list) list +*) +let rec extract_instances 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' -> extract_instances p e' + | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2) + | AST_arrow(e1, e2) -> + extract_instances p e1 @ extract_instances p e2 + | AST_if(e1, e2, e3) -> + extract_instances p e1 @ extract_instances p e2 @ extract_instances p e3 + | AST_instance((f, _), args, id) -> + let more = List.flatten (List.map (extract_instances 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 + (f, id, node.body, args_x)::more + +(* Utility : find pre declarations in an expression *) + +(* 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') + diff --git a/frontend/rename.ml b/frontend/rename.ml new file mode 100644 index 0000000..9c4cc31 --- /dev/null +++ b/frontend/rename.ml @@ -0,0 +1,102 @@ +(* Scope analyzer *) + +open Ast +open Util +open Ast_util +open Typing + +type renaming = (id * bool) VarMap.t (* bool: is const ? *) + +(* consts_renaming : prog -> renaming *) +let consts_renaming p = + let cdecl = extract_const_decls p in + List.fold_left + (fun rn (d,_) -> VarMap.add d.c_name (d.c_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 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.st_name^".") rn st.st_locals in + { st with + st_locals = List.map (rename_var_def rn) st.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.act_id^".") rn b.act_locals in + AST_activate_body{ b with + act_locals = List.map (rename_var_def rn) b.act_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 + diff --git a/frontend/typing.ml b/frontend/typing.ml new file mode 100644 index 0000000..07b3bcd --- /dev/null +++ b/frontend/typing.ml @@ -0,0 +1,178 @@ +(* + - Instanciate a program with a root node + - Enumerate all the variables, give them a type + - Give a type to expressions +*) + +open Ast +open Ast_util +open Util + +type typ = + | TInt + | TReal + | TEnum of string list + +let bool_true = "T" +let bool_false = "F" +let bool_type = TEnum [bool_true; bool_false] + +let t_of_ast_t = function + | AST_TINT -> TInt + | AST_TREAL -> TReal + | AST_TBOOL -> bool_type + + +(* probe? * variable full name * variable type *) +type var = bool * id * typ + +(* path to node * subscope prefix in node * equations in scope *) +type scope = id * id * eqn ext list + +type rooted_prog = { + p : prog; + root_node : node_decl; + root_scope : scope; + all_vars : var list; + const_vars : var list; +} + +(* Typing *) + +(* + type_expr_vl : prog -> var list -> string -> typ list +*) +let rec type_expr_vl p vl cvl node expr = + let sub = type_expr_vl p vl cvl node in + let err = loc_error (snd expr) type_error in + match fst expr with + (* Identifiers *) + | AST_identifier(id, _) -> + let _, _, t = List.find (fun (_, x, _) -> x = (node^"/"^id)) vl in [t] + | AST_idconst(id, _) -> + let _, _, t = List.find (fun (_, x, _) -> x = id) cvl in [t] + (* On numerical values *) + | AST_int_const _ -> [TInt] + | AST_real_const _ -> [TReal] + | AST_unary (_, se) -> + begin match sub se with + | [TInt] -> [TInt] + | [TReal] -> [TReal] + | _ -> err "Invalid argument for unary." + end + | AST_binary(_, a, b) -> + begin match sub a, sub b with + | [TInt], [TInt] -> [TInt] + | [TReal], [TReal] -> [TReal] + | [TInt], [TReal] | [TReal], [TInt] -> [TReal] + | _ -> err "Invalid argument for binary." + end + (* On boolean values *) + | AST_bool_const _ -> [bool_type] + | AST_binary_rel _ -> [bool_type] (* do not check subtypes... TODO? *) + | AST_binary_bool _ -> [bool_type] (* the same *) + | AST_not _ -> [bool_type] (* the same *) + (* Temporal primitives *) + | AST_pre(e, _) -> sub e + | AST_arrow(a, b) -> + let ta, tb = sub a, sub b in + if ta = tb then ta + else err "Arrow does not have same type on both sides." + (* other *) + | AST_if(c, a, b) -> + let ta, tb = sub a, sub b in + if ta = tb then ta + else err "If does not have same type on both branches." + | AST_instance((f, _), _, _) -> + (* do not check types of arguments... TODO? *) + let (n, _) = find_node_decl p f in + List.map (fun (_, _, t) -> t_of_ast_t t) n.ret + + +(* type_expr : tp -> string -> typ list *) +let type_expr tp = type_expr_vl tp.p tp.all_vars tp.const_vars + + +(* Program rooting *) + + +(* decls_of_node : node_decl -> var_decl list *) +let decls_of_node n = n.args @ n.ret @ n.var + +(* vars_in_node string -> var_decl list -> var list *) +let vars_in_node nid = + List.map (fun (p, id, t) -> p, nid^"/"^id, t_of_ast_t t) + +(* node_vars : prog -> id -> string -> var list *) +let node_vars p f nid = + let (n, _) = find_node_decl p f in + vars_in_node nid (decls_of_node n) + +(* + extract_all_vars : prog -> scope -> var list + + Extracts all variables with names given according to + naming convention used here and in transform.ml : + - pre variables are not prefixed by scope + - next values for variables are prefixed by capital N +*) +let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars = + let vars_of_expr e = + List.flatten + (List.map + (fun (f, id, eqs, args) -> + let nv = node_vars p f (node^"/"^id) in + nv @ extract_all_vars p (node^"/"^id, "", eqs) nv const_vars) + (extract_instances p e)) + @ + List.flatten + (List.map + (fun (id, expr) -> + let vd = + List.mapi + (fun i t -> false, id^"."^(string_of_int i), t) + (type_expr_vl p n_vars const_vars node expr) + in + vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd)) + (extract_pre e)) + in + let vars_of_eq e = match fst e with + | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e + | AST_activate (b, _) -> + let rec do_branch = function + | AST_activate_body b -> + let bvars = vars_in_node node b.act_locals in + bvars @ + extract_all_vars p + (node, b.act_id^".", b.body) + (bvars@n_vars) + const_vars + | AST_activate_if(c, a, b) -> + vars_of_expr c @ do_branch a @ do_branch b + in do_branch b + | AST_automaton _ -> not_implemented "extract_all vars automaton" + in + (false, node^"/"^prefix^"time", TInt):: + (false, "N"^node^"/"^prefix^"time", TInt):: + (List.flatten (List.map vars_of_eq eqs)) + + +(* + root_prog : prog -> id -> rooted_prog +*) +let root_prog p root = + let (n, _) = find_node_decl p root in + let root_scope = ("", "", n.body) in + + let const_vars = List.map + (fun (cd, _) -> (false, cd.c_name, t_of_ast_t cd.typ)) + (extract_const_decls p) + in + + let root_vars = vars_in_node "" (decls_of_node n) in + + { p; root_scope; root_node = n; + const_vars = const_vars; + all_vars = root_vars @ extract_all_vars p root_scope root_vars const_vars } + + |