From 6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Fri, 20 Jun 2014 17:26:10 +0200
Subject: Not much. Still does not work very well.

---
 frontend/ast_printer.ml |  2 +-
 frontend/typing.ml      | 19 ++++++++-----------
 2 files changed, 9 insertions(+), 12 deletions(-)

(limited to 'frontend')

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 ->
@@ -182,10 +184,6 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
         (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
@@ -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
-- 
cgit v1.2.3