diff options
Diffstat (limited to 'frontend')
| -rw-r--r-- | frontend/ast_printer.ml | 2 | ||||
| -rw-r--r-- | frontend/typing.ml | 19 |
2 files changed, 9 insertions, 12 deletions
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index ac30fe9..b6c06fb 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -264,7 +264,7 @@ let print_prog fmt p = 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 + | TEnum e -> Format.fprintf fmt "enum @[<h>{ %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/typing.ml b/frontend/typing.ml index 564d91e..0417d27 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -33,7 +33,6 @@ type rooted_prog = { 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; @@ -146,7 +145,10 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = (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_assign(_, e) | AST_assume(_, e) -> vars_of_expr e + | AST_guarantee((id, _), e) -> + let gn = node^"/g_"^id in + (false, gn, bool_type)::vars_of_expr e | AST_activate (b, _) -> let rec do_branch = function | AST_activate_body b -> @@ -183,10 +185,6 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = (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):: @@ -196,9 +194,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = (* - root_prog : prog -> id -> rooted_prog + root_prog : prog -> id -> string list -> string list -> rooted_prog *) -let root_prog p root = +let root_prog p root no_time_scope init_scope = let (root_node, _) = find_node_decl p root in let root_scope = ("", "", root_node.body) in @@ -212,9 +210,8 @@ let root_prog p root = let rp = { p; root_scope; root_node; - no_time_scope = ["/"]; - act_scope = []; - init_scope = ["/"]; + no_time_scope; + init_scope; const_vars; all_vars = [] } in |