[passes] linearisation: correction (10 -> pre (20 -> 30)) works

This commit is contained in:
Arnaud DABY-SEESARAM 2022-12-16 09:44:22 +01:00
parent 7c2c43fe24
commit 3417d75620
3 changed files with 7 additions and 11 deletions

View File

@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f =
let _ = let _ =
(** Usage and argument parsing. *) (** Usage and argument parsing. *)
let default_passes = ["pre2vars"; "automata_validity" ;"automata_translation"; "linearization"; "equations_ordering"] in let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"] in
let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
let usage_msg = let usage_msg =
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \

View File

@ -188,9 +188,9 @@ let pass_linearization verbose debug main_fn =
| [TReal] -> RVar nvar | [TReal] -> RVar nvar
| _ -> failwith "Should not happened." in | _ -> failwith "Should not happened." in
let neq_patt: t_varlist = (t, [nvar]) in let neq_patt: t_varlist = (t, [nvar]) in
let neq_expr: t_expression = EMonOp (t, MOp_pre, e) in let neq_expr: t_expression = e in
let vars = varlist_concat (t, [nvar]) vars in let vars = varlist_concat (t, [nvar]) vars in
(neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar) (neq_patt, neq_expr) :: eqs, vars, EMonOp (t, MOp_pre, EVar (t, nvar))
| _ -> | _ ->
let eqs, vars, e = pre_aux_expression vars e in let eqs, vars, e = pre_aux_expression vars e in
eqs, vars, EMonOp (t, op, e) eqs, vars, EMonOp (t, op, e)
@ -228,8 +228,7 @@ let pass_linearization verbose debug main_fn =
let eqs, vars, e = pre_aux_expression vars e in let eqs, vars, e = pre_aux_expression vars e in
eqs, vars, EApp (t, n, e) eqs, vars, EApp (t, n, e)
in in
let rec pre_aux_equation (vars: t_varlist) (eq: t_equation) = let rec pre_aux_equation (vars: t_varlist) ((patt, expr): t_equation) =
let (patt, expr) = eq in
let eqs, vars, expr = pre_aux_expression vars expr in let eqs, vars, expr = pre_aux_expression vars expr in
(patt, expr)::eqs, vars (patt, expr)::eqs, vars
in in
@ -259,7 +258,7 @@ let pass_linearization verbose debug main_fn =
(fun (eqs, vars) eq -> (fun (eqs, vars) eq ->
let es, vs = pre_aux_equation vars eq in let es, vs = pre_aux_equation vars eq in
es @ eqs, ((fst vs) @ (fst vars), (snd vs) @ (snd vars))) es @ eqs, ((fst vs) @ (fst vars), (snd vs) @ (snd vars)))
(new_equations, node.n_local_vars) ([], node.n_local_vars)
new_equations new_equations
in in
Some Some

View File

@ -1,7 +1,4 @@
node diagonal_int (i: int) returns (o1, o2 : int); node main (i: int) returns (o1: int);
var y: int;
let let
o2 = y; o1 = 10 -> pre (20 -> 30);
y = i;
o1 = i;
tel tel