Compare commits

...

2 Commits

3 changed files with 47 additions and 28 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"; "linearization"; "equations_ordering"] in let default_passes = ["pre2vars"; "automata_validity" ;"automata_translation"; "linearization"; "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] \
@ -67,6 +67,8 @@ let _ =
[ [
("pre2vars", Passes.pre2vars); ("pre2vars", Passes.pre2vars);
("chkvar_init_unicity", Passes.chkvar_init_unicity); ("chkvar_init_unicity", Passes.chkvar_init_unicity);
("automata_translation", Passes.automata_translation_pass);
("automata_validity", Passes.check_automata_validity);
("linearization", Passes.pass_linearization); ("linearization", Passes.pass_linearization);
("equations_ordering", Passes.pass_eq_reordering); ("equations_ordering", Passes.pass_eq_reordering);
("check_typing", Passes.pass_typing); ("check_typing", Passes.pass_typing);

View File

@ -295,28 +295,35 @@ let pass_typing verbose debug main_fn ast =
else None else None
in aux ast in aux ast
let check_automaton_branch_vars automaton = let check_automata_validity verbos debug main_fn =
let (init, states) = automaton in let check_automaton_branch_vars automaton =
let left_side = Hashtbl.create 10 in let (init, states) = automaton in
let left_side = Hashtbl.create 10 in
let rec init_left_side eqlist = match eqlist with let rec init_left_side eqlist = match eqlist with
| [] -> () | [] -> ()
| (varlist, exp)::q -> | (varlist, exp)::q ->
begin begin
Hashtbl.add left_side varlist true; Hashtbl.add left_side varlist true;
init_left_side q; init_left_side q;
end end
in
let check_state s = match s with
| State(name, eqs, cond, next) ->
List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs
in
begin
match init with | State(name, eqs, cond, next) -> init_left_side eqs;
let validity = List.for_all (fun s -> (check_state s)) states in
if not validity then
failwith "Automaton branch has different variables assignment in different branches"
end
in in
let check_state s = match s with let aux node =
| State(name, eqs, cond, next) -> List.iter check_automaton_branch_vars node.n_automata;
List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs Some node
in in
begin node_pass aux
match init with | State(name, eqs, cond, next) -> init_left_side eqs;
let validity = List.for_all (fun s -> (check_state s)) states in
if not validity then
failwith "Automaton branch has different variables assignment in different branches"
end
let automaton_translation debug automaton = let automaton_translation debug automaton =
let gathered = Hashtbl.create 10 in let gathered = Hashtbl.create 10 in
@ -331,7 +338,7 @@ let automaton_translation debug automaton =
let rec init_state_translation states c = match states with let rec init_state_translation states c = match states with
| [] -> () | [] -> ()
| State(name, _, _, _)::q -> | State(name, _, _, _)::q ->
Hashtbl.replace state_to_int name c; (init_state_translation q c) Hashtbl.replace state_to_int name c; (init_state_translation q (c+1))
in in
let rec find_state name = let rec find_state name =
@ -350,14 +357,20 @@ let automaton_translation debug automaton =
let flatten_state state = match state with let flatten_state state = match state with
| State(name, eq, cond, next) -> | State(name, eq, cond, next) ->
(* Flattening is not possible
for example a branch where x,y = 1, 2 will be unpacked
when in another branch x, y = f(z) will not be unpacked
*)
(*
let new_equations = List.flatten let new_equations = List.flatten
begin begin
List.map List.map
(tpl debug) (tpl debug)
eq eq
end in end in
equation_pass name new_equations; *)
State(name, new_equations, cond, next) equation_pass name eq;
State(name, eq, cond, next)
in in
let rec transition_eq states s = let rec transition_eq states s =
@ -399,7 +412,7 @@ let automaton_translation debug automaton =
let (init, states) = flatten_automaton automaton in let (init, states) = flatten_automaton automaton in
let s = create_automaton_name () in let s = create_automaton_name () in
init_state_translation states 1; init_state_translation states 1;
let exp_transition = transition_eq states s in let exp_transition = EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, transition_eq states s)) in
let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in
Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist)::acc) gathered new_equations, IVar(s) Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist)::acc) gathered new_equations, IVar(s)
@ -423,6 +436,10 @@ let automata_trans_pass debug (node:t_node) : t_node option=
n_outputs = node.n_outputs; n_outputs = node.n_outputs;
n_local_vars = (new_ty@ty, vars@loc_vars); n_local_vars = (new_ty@ty, vars@loc_vars);
n_equations = eqs@node.n_equations; n_equations = eqs@node.n_equations;
n_automata = node.n_automata; n_automata = []; (* not needed anymore *)
} }
let automata_translation_pass verbose debug main_fn =
node_pass (automata_trans_pass debug)

View File

@ -1,5 +1,4 @@
node diagonal_int (i: int) returns (o1, o2 : int); node diagonal_int (i: int) returns (o1, o2 : int);
var i: int;
let let
(o1, o2) = (i, i); (o1, o2) = (i, i);
tel tel
@ -13,9 +12,10 @@ let
tel tel
node auto (i: int) returns (o : int); node auto (i: int) returns (o : int);
var x, y:int;
let let
automaton automaton
| Incr -> do o = (pre o) + 1; done | Incr -> do (o,x) = (0 fby o + 1, 2); done
| Decr -> do o = (pre o) - 1; done | Decr -> do (o,x) = diagonal_int(0 fby o); done
tel tel