diff options
Diffstat (limited to 'frontend/typing.ml')
| -rw-r--r-- | frontend/typing.ml | 71 |
1 files changed, 49 insertions, 22 deletions
diff --git a/frontend/typing.ml b/frontend/typing.ml index 1545a38..a4abfe0 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -30,11 +30,16 @@ type var = bool * id * typ 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; + p : prog; + + no_time_scope : id list; (* scopes in which not to introduce time variable *) + act_scope : id list; (* scopes in which to introduce act variable *) + init_scope : id list; (* scopes in which to introduce init variable *) + + root_node : node_decl; + root_scope : scope; + all_vars : var list; + const_vars : var list; } (* Typing *) @@ -120,14 +125,14 @@ let node_vars p f nid = - 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 rec extract_all_vars rp (node, prefix, eqs) n_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)) + let nv = node_vars rp.p f (node^"/"^id) in + nv @ extract_all_vars rp (node^"/"^id, "", eqs) nv) + (extract_instances rp.p e)) @ List.flatten (List.map @@ -135,7 +140,7 @@ let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars = let vd = List.mapi (fun i t -> false, id^"."^(string_of_int i), t) - (type_expr_vl p n_vars const_vars node expr) + (type_expr_vl rp.p n_vars rp.const_vars node expr) in vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd)) (extract_pre e)) @@ -147,36 +152,58 @@ let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars = | AST_activate_body b -> let bvars = vars_in_node node b.act_locals in bvars @ - extract_all_vars p + extract_all_vars rp (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)) + let v = List.flatten (List.map vars_of_eq eqs) in + let v = + if not (List.mem (node^"/") rp.no_time_scope) + then + (false, node^"/"^prefix^"time", TInt):: + (false, "N"^node^"/"^prefix^"time", TInt)::v + else v in + let v = + if List.mem (node^"/") rp.act_scope + then (false, node^"/"^prefix^"act", bool_type)::v + else v in + let v = + if List.mem (node^"/") rp.init_scope + then + (false, node^"/"^prefix^"init", bool_type):: + (false, "N"^node^"/"^prefix^"init", bool_type)::v + else v in + v (* 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 (root_node, _) = find_node_decl p root in + let root_scope = ("", "", root_node.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 } + let root_vars = vars_in_node "" (decls_of_node root_node) in + + let rp = { + p; root_scope; root_node; + + no_time_scope = ["/"]; + act_scope = []; + init_scope = ["/"]; + + const_vars; + all_vars = [] } in + + { rp with all_vars = root_vars @ extract_all_vars rp root_scope root_vars } |