diff --git a/src/ast.ml b/src/ast.ml index c2fb0da..039a0cf 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -55,7 +55,7 @@ and t_equation = t_varlist * t_expression and t_eqlist = t_equation list -and t_state = | State of ident * t_eqlist * t_expression * ident +and t_state = | State of ident * t_eqlist * (t_expression list) * (ident list) and t_automaton = t_state * t_state list diff --git a/src/lustre_pp.ml b/src/lustre_pp.ml index 01d5b0c..9bd300c 100644 --- a/src/lustre_pp.ml +++ b/src/lustre_pp.ml @@ -153,14 +153,21 @@ let rec pp_automata fmt: t_automaton list -> unit = function pp_translist trans pp_automata tail +and pp_nexts fmt: t_expression list * string list -> unit = function + | [], [] -> () + | e::exprs, n::nexts -> + Format.fprintf fmt "if %a then %s else %a" + pp_expression e + n + pp_nexts (exprs, nexts) + and pp_translist fmt: t_state list -> unit = function | [] -> () | State(name, eqs, cond, next)::q -> - Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \t\t\tthen %s\n%a" + Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \n%a" name pp_equations eqs - pp_expression cond - next + pp_nexts (cond, next) pp_translist q let pp_node fmt node = diff --git a/src/parser.mly b/src/parser.mly index e2e0853..0890add 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -436,9 +436,10 @@ ident_comma_list: transition: | CASE IDENT BO_arrow DO equations DONE { - State($2, $5, EConst([TBool], CBool(true)), $2) } - | CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT { - State($2, $5, $7, $9)} + State($2, $5, [EConst([TBool], CBool(true))], [$2]) } + | CASE IDENT BO_arrow DO equations UNTIL next_list { + let (exprs, outs) = $7 in + State($2, $5, exprs, outs)} ; transition_list: @@ -446,3 +447,8 @@ transition_list: | transition transition_list { $1 :: $2 } | /* empty */ {raise(MyParsingError("Empty automaton", current_location()))} ; + +next_list: + | expr THEN IDENT { [$1], [$3] } + | next_list ELSE IF expr THEN IDENT { let (exprs, outs) = $1 in $4::exprs, $6::outs } +; diff --git a/src/passes.ml b/src/passes.ml index 1329ca6..5e9a3ef 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -852,14 +852,19 @@ let automaton_translation debug automaton = in List.map aux eqlist in + let rec next_construct exprs nexts = match exprs, nexts with + | [], [] -> EConst([TInt], CInt(1)) + | e::exprs, n::nexts -> ETriOp([TInt], TOp_if, e, EConst([TInt], CInt(find_state n)), next_construct exprs nexts) + | _, _ -> failwith "Automata translation: next construct: should not happen" + in let state_translation state = match state with | State( name, equations, expr, next ) -> - let b = create_branch_name name in - let eqs = translate_eqlist equations name in - let bool_expr = EComp([TBool], COp_eq, EVar([TInt], to_var automat_name TInt), EConst([TInt], CInt(find_state name))) in - let next_expr = EWhen([TInt], ETriOp([TInt], TOp_if, expr, EConst([TInt], CInt(find_state next)), EConst([TInt], CInt(1))), EVar([TBool], to_var (get_branch_bool name) TBool)) in - (([TBool], [to_var b TBool]), bool_expr)::(([TInt], [to_var (create_next_var name) TInt]), next_expr)::eqs + let b = create_branch_name name in + let eqs = translate_eqlist equations name in + let bool_expr = EComp([TBool], COp_eq, EVar([TInt], to_var automat_name TInt), EConst([TInt], CInt(find_state name))) in + let next_expr = EWhen([TInt], next_construct expr next, EVar([TBool], to_var (get_branch_bool name) TBool)) in + (([TBool], [to_var b TBool]), bool_expr)::(([TInt], [to_var (create_next_var name) TInt]), next_expr)::eqs in let rec iter_states states = match states with @@ -900,6 +905,7 @@ let automaton_translation debug automaton = |RVar(_)::q -> TReal::build_type q |[] -> [] in + let init, states = automaton in init_state_translation states 1; let transition_eq = (([TInt], [IVar(automat_name)]), EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, merge_state states))) in diff --git a/tests/automaton.node b/tests/automaton.node index e35065b..4070f34 100644 --- a/tests/automaton.node +++ b/tests/automaton.node @@ -15,7 +15,8 @@ node auto (i: int) returns (o : int); var x, y:int; let automaton - | Incr -> do (o,x) = (0 fby o + 1, 2); done - | Decr -> do (o,x) = diagonal_int(0 fby o); done + | Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done + | Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr + | Done -> do o = pre o; done tel