summaryrefslogtreecommitdiff
path: root/frontend
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-19 17:53:33 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-19 17:53:33 +0200
commit3c3b96e877dcb121d17da282dc4ca0caadda72b2 (patch)
treee6cd5c3f6ca686c0d106f89c308e9feb0f67d8b2 /frontend
parentf4200a0aa90e2641ce1b0b1c54d00d9d4dd3b73e (diff)
downloadscade-analyzer-3c3b96e877dcb121d17da282dc4ca0caadda72b2.tar.gz
scade-analyzer-3c3b96e877dcb121d17da282dc4ca0caadda72b2.zip
Very buggy disjunction domain !
Diffstat (limited to 'frontend')
-rw-r--r--frontend/ast_util.ml1
-rw-r--r--frontend/typing.ml71
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 }