diff options
Diffstat (limited to 'frontend')
| -rw-r--r-- | frontend/typing.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/frontend/typing.ml b/frontend/typing.ml index 0417d27..aca8d15 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -32,8 +32,8 @@ type scope = id * id * eqn ext list type rooted_prog = { p : prog; - no_time_scope : id list; (* scopes in which not to introduce time variable *) - init_scope : id list; (* scopes in which to introduce init variable *) + no_time_scope : id -> bool; (* scopes in which not to introduce time variable *) + init_scope : id -> bool; (* scopes in which to introduce init variable *) root_node : node_decl; root_scope : scope; @@ -179,13 +179,13 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = in let v = List.flatten (List.map vars_of_eq eqs) in let v = - if not (List.mem (node^"/") rp.no_time_scope) + if not (rp.no_time_scope (node^"/")) then (false, node^"/"^prefix^"time", TInt):: (false, "N"^node^"/"^prefix^"time", TInt)::v else v in let v = - if List.mem (node^"/") rp.init_scope + if rp.init_scope (node^"/") then (false, node^"/"^prefix^"init", bool_type):: (false, "N"^node^"/"^prefix^"init", bool_type)::v @@ -197,7 +197,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = root_prog : prog -> id -> string list -> string list -> rooted_prog *) let root_prog p root no_time_scope init_scope = - let (root_node, _) = find_node_decl p root in + let (root_node, _) = + try find_node_decl p root + with Not_found -> error ("No such root node: " ^ root) in let root_scope = ("", "", root_node.body) in let const_vars = List.map |