diff options
Diffstat (limited to 'frontend')
| -rw-r--r-- | frontend/ast.ml | 4 | ||||
| -rw-r--r-- | frontend/lexer.mll | 6 | ||||
| -rw-r--r-- | frontend/parser.mly | 1 | ||||
| -rw-r--r-- | frontend/typing.ml | 38 |
4 files changed, 19 insertions, 30 deletions
diff --git a/frontend/ast.ml b/frontend/ast.ml index c561cef..d55626d 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -69,10 +69,6 @@ and state = { st_locals : var_def list; body : eqn ext list; until : transition list; - (* these two rst info are determined after parsing, in typing.ml when - the variable list is extracted *) - mutable i_rst : bool; (* resettable by S -> S transition *) - mutable o_rst : bool; (* resettable by S' -> S transition *) } and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *) diff --git a/frontend/lexer.mll b/frontend/lexer.mll index ef40aa7..837ee75 100644 --- a/frontend/lexer.mll +++ b/frontend/lexer.mll @@ -88,6 +88,7 @@ rule token = parse | const_real as c { REALVAL c } (* spaces, comments *) | "(*" { comment lexbuf; token lexbuf } + | "/*" { cppcomment lexbuf; token lexbuf } | "--" [^ '\n' '\r']* { token lexbuf } | newline { new_line lexbuf; token lexbuf } | space { token lexbuf } @@ -98,3 +99,8 @@ and comment = parse | "*)" { () } | [^ '\n' '\r'] { comment lexbuf } | newline { new_line lexbuf; comment lexbuf } + +and cppcomment = parse + | "*/" { () } + | [^ '\n' '\r'] { cppcomment lexbuf } + | newline { new_line lexbuf; cppcomment lexbuf } diff --git a/frontend/parser.mly b/frontend/parser.mly index 672bb9a..e8a6ecf 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -126,7 +126,6 @@ state: st_locals = v; body = b; until = until; - i_rst = false; o_rst = false; (* calculated later *) } } trans(TT): diff --git a/frontend/typing.ml b/frontend/typing.ml index 2859230..883e8e0 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 @@ -186,17 +178,12 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = vars_of_expr c @ do_branch a @ do_branch b in do_branch b | AST_automaton (aid, states, ret) -> - (* Determine which states can be reset *) - let rst_trans = List.flatten + let rst_states = List.flatten (List.map (fun (st, _) -> - List.map (fun (_, (id, _), _) -> (st.st_name, id)) + List.map (fun (_, (id, _), _) -> id) (List.filter (fun (_, _, rst) -> rst) st.until)) states) in - List.iter (fun (st, _) -> - st.i_rst <- List.mem (st.st_name, st.st_name) rst_trans; - st.o_rst <- List.exists (fun (a, b) -> b = st.st_name && a <> b) rst_trans) - states; let do_state (st, _) = let tvars = @@ -205,15 +192,15 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = in 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] + (if List.mem st.st_name rst_states then + [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 +234,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 } |