From dd7b7d30adddfa0258aa5b3819a0a58d6b5d8705 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 19 Jun 2014 18:48:54 +0200 Subject: Everything proved !! --- frontend/typing.ml | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'frontend') diff --git a/frontend/typing.ml b/frontend/typing.ml index a4abfe0..564d91e 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -158,7 +158,22 @@ let rec extract_all_vars rp (node, prefix, eqs) n_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" + | AST_automaton (aid, states, ret) -> + let do_state (st, _) = + let tvars = + List.flatten + (List.map (fun (e, _, _) -> vars_of_expr e) st.until) + in + let svars = vars_in_node node st.st_locals in + svars @ tvars @ + extract_all_vars rp + (node, aid^"."^st.st_name^".", st.body) + (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):: + (List.flatten (List.map do_state states)) in let v = List.flatten (List.map vars_of_eq eqs) in let v = -- cgit v1.2.3