summaryrefslogtreecommitdiff
path: root/frontend/typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'frontend/typing.ml')
-rw-r--r--frontend/typing.ml27
1 files changed, 10 insertions, 17 deletions
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 2859230..d814bbe 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -129,15 +129,12 @@ let clock_vars rp (node, prefix, _) =
let v =
if not (rp.no_time_scope (node^"/"^prefix))
then
- [
- false, node^"/"^prefix^"time", TInt;
- false, "N"^node^"/"^prefix^"time", TInt]
+ [false, node^"/"^prefix^"time", TInt]
else [] in
let v =
if rp.init_scope (node^"/"^prefix)
then
- (false, node^"/"^prefix^"init", bool_type)::
- (false, "N"^node^"/"^prefix^"init", bool_type)::v
+ (false, node^"/"^prefix^"init", bool_type)::v
else v in
v
@@ -145,9 +142,7 @@ let clock_vars rp (node, prefix, _) =
extract_all_vars : rooted_prog -> scope -> var list
Extracts all variables with names given according to
- naming convention used here and in transform.ml :
- - pre variables are not prefixed by scope
- - next values for variables are prefixed by capital N
+ naming convention used here and in transform.ml
*)
let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let vars_of_expr e =
@@ -162,12 +157,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
(List.map
(fun (id, expr) ->
let id = node^"/"^id in
- let vd =
- List.mapi
- (fun i t -> false, id^"."^(string_of_int i), t)
- (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))
+ List.mapi
+ (fun i t -> false, id^"."^(string_of_int i), t)
+ (type_expr_vl rp.p n_vars rp.const_vars node expr))
(extract_pre e))
in
let vars_of_eq e = match fst e with
@@ -206,14 +198,14 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars =
let st_scope = (node, aid^"."^st.st_name^".", st.body) in
let svars = vars_in_node node st.st_locals in
(if st.i_rst || st.o_rst then
- [false, node^"/"^aid^"."^st.st_name^".next_reset", bool_type]
+ [false, node^"/"^aid^"."^st.st_name^".must_reset", bool_type]
else [])
@ svars @ tvars @ clock_vars rp st_scope @
extract_all_vars rp st_scope (tvars@n_vars)
in
let st_ids = List.map (fun (st, _) -> st.st_name) states in
(false, node^"/"^aid^".state", TEnum st_ids)::
- (false, "N"^node^"/"^aid^".state", TEnum st_ids)::
+ (false, node^"/"^aid^".next_state", TEnum st_ids)::
(List.flatten (List.map do_state states))
in
let v = List.flatten (List.map vars_of_eq eqs) in
@@ -247,6 +239,7 @@ let root_prog p root no_time_scope init_scope =
let root_vars = vars_in_node "" (decls_of_node root_node) in
let root_clock_vars = clock_vars rp root_scope in
- { rp with all_vars = root_clock_vars @ root_vars @ extract_all_vars rp root_scope root_vars }
+ { rp with all_vars = root_clock_vars @
+ root_vars @ extract_all_vars rp root_scope root_vars }