diff options
Diffstat (limited to 'frontend/ast_util.ml')
-rw-r--r-- | frontend/ast_util.ml | 75 |
1 files changed, 75 insertions, 0 deletions
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') + |