Very buggy disjunction domain !

2 files changed, 49 insertions, 23 deletions

diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml
index b3393a7..d229f2f 100644
--- a/frontend/ast_util.ml
+++ b/frontend/ast_util.ml
@@ -6,7 +6,6 @@ open Util
 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 *)
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 }