Merge remote-tracking branch 'origin/master' into wip
This commit is contained in:
commit
8d6349dd3f
@ -99,8 +99,8 @@ let pp_expression node_name =
|
||||
match expression with
|
||||
| EWhen (_, e1, e2) ->
|
||||
begin
|
||||
(* as don't use a variable assigned when the condition holds, can define it even if the condition doesn't hold *)
|
||||
Format.fprintf fmt "%a"
|
||||
Format.fprintf fmt "%a ? %a : 0"
|
||||
pp_expression_aux e2
|
||||
pp_expression_aux e1
|
||||
end
|
||||
| EReset (_, e1, e2) ->
|
||||
|
@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f =
|
||||
|
||||
let _ =
|
||||
(** 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 usage_msg =
|
||||
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
|
||||
@ -67,6 +67,8 @@ let _ =
|
||||
[
|
||||
("pre2vars", Passes.pre2vars);
|
||||
("chkvar_init_unicity", Passes.chkvar_init_unicity);
|
||||
("automata_translation", Passes.automata_translation_pass);
|
||||
("automata_validity", Passes.check_automata_validity);
|
||||
("linearization", Passes.pass_linearization);
|
||||
("equations_ordering", Passes.pass_eq_reordering);
|
||||
("check_typing", Passes.pass_typing);
|
||||
|
@ -199,7 +199,7 @@ node_content:
|
||||
n_local_vars = $10;
|
||||
n_equations = eqs;
|
||||
n_automata = aut; } in
|
||||
if List.length (snd $10) = 0 && node_name <> "main"
|
||||
if List.length t_in = 0
|
||||
then raise (MyParsingError
|
||||
(Format.asprintf "The node %s should have arguments."
|
||||
node_name,
|
||||
|
166
src/passes.ml
166
src/passes.ml
@ -155,6 +155,22 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option
|
||||
in
|
||||
node_pass aux
|
||||
|
||||
let rec tpl debug ((pat, exp): t_equation) =
|
||||
match exp with
|
||||
| ETuple (_, hexps :: texps) ->
|
||||
debug "An ETuple has been recognized, inlining...";
|
||||
let p1, p2 =
|
||||
list_select
|
||||
(List.length (type_exp hexps))
|
||||
(snd pat) in
|
||||
let t1 = List.flatten (List.map type_var p1) in
|
||||
let t2 = List.flatten (List.map type_var p2) in
|
||||
((t1, p1), hexps)
|
||||
:: (tpl debug ((t2, p2),
|
||||
ETuple (List.flatten (List.map type_exp texps), texps)))
|
||||
| ETuple (_, []) -> []
|
||||
| _ -> [(pat, exp)]
|
||||
|
||||
let pass_linearization verbose debug main_fn =
|
||||
let node_lin (node: t_node): t_node option =
|
||||
let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
|
||||
@ -251,7 +267,7 @@ let pass_linearization verbose debug main_fn =
|
||||
n_name = node.n_name;
|
||||
n_inputs = node.n_inputs;
|
||||
n_outputs = node.n_outputs;
|
||||
n_local_vars = new_locvars;
|
||||
n_local_vars = node.n_local_vars;
|
||||
n_equations = new_equations;
|
||||
n_automata = node.n_automata;
|
||||
}
|
||||
@ -362,3 +378,151 @@ let pass_typing verbose debug main_fn ast =
|
||||
else None
|
||||
in aux ast
|
||||
|
||||
let check_automata_validity verbos debug main_fn =
|
||||
let check_automaton_branch_vars automaton =
|
||||
let (init, states) = automaton in
|
||||
let left_side = Hashtbl.create 10 in
|
||||
|
||||
let rec init_left_side eqlist = match eqlist with
|
||||
| [] -> ()
|
||||
| (varlist, exp)::q ->
|
||||
begin
|
||||
Hashtbl.add left_side varlist true;
|
||||
init_left_side q;
|
||||
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
|
||||
let aux node =
|
||||
List.iter check_automaton_branch_vars node.n_automata;
|
||||
Some node
|
||||
in
|
||||
node_pass aux
|
||||
|
||||
let automaton_translation debug automaton =
|
||||
let gathered = Hashtbl.create 10 in
|
||||
let state_to_int = Hashtbl.create 10 in
|
||||
let add_to_table var exp state =
|
||||
if Hashtbl.mem gathered var then
|
||||
let res = Hashtbl.find gathered var in
|
||||
Hashtbl.replace gathered var ((state, exp)::res);
|
||||
else
|
||||
Hashtbl.replace gathered var ([(state, exp)])
|
||||
in
|
||||
let rec init_state_translation states c = match states with
|
||||
| [] -> ()
|
||||
| State(name, _, _, _)::q ->
|
||||
Hashtbl.replace state_to_int name c; (init_state_translation q (c+1))
|
||||
in
|
||||
|
||||
let rec find_state name =
|
||||
match Hashtbl.find_opt state_to_int name with
|
||||
| None -> failwith "Unknown state in automaton"
|
||||
| Some v -> v
|
||||
in
|
||||
|
||||
let rec equation_pass state : t_eqlist -> unit = function
|
||||
| [] -> ()
|
||||
| (vars, exp)::q -> begin
|
||||
add_to_table vars exp state;
|
||||
equation_pass state q
|
||||
end
|
||||
in
|
||||
|
||||
let flatten_state state = match state with
|
||||
| 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
|
||||
begin
|
||||
List.map
|
||||
(tpl debug)
|
||||
eq
|
||||
end in
|
||||
*)
|
||||
equation_pass name eq;
|
||||
State(name, eq, cond, next)
|
||||
in
|
||||
|
||||
let rec transition_eq states s =
|
||||
match states with
|
||||
| [] -> EVar([TInt], IVar(s))
|
||||
| State(name, eqs, cond, next)::q ->
|
||||
let name = find_state name
|
||||
and next = find_state next in
|
||||
ETriOp([TInt], TOp_if,
|
||||
EBinOp([TBool], BOp_and,
|
||||
EComp([TBool], COp_eq,
|
||||
EVar([TInt], IVar(s)),
|
||||
EConst([TInt], CInt(name))
|
||||
),
|
||||
cond
|
||||
),
|
||||
EConst([TInt], CInt(next)),
|
||||
transition_eq q s
|
||||
)
|
||||
in
|
||||
|
||||
let rec translate_var s v explist = match explist with
|
||||
| [] -> EConst([TInt], CInt(0)) (* TODO *)
|
||||
| (state, exp)::q ->
|
||||
ETriOp(Utils.type_exp exp, TOp_if,
|
||||
EComp([TBool], COp_eq,
|
||||
EVar([TInt], IVar(s)),
|
||||
EConst([TInt], CInt(Hashtbl.find state_to_int state))
|
||||
),
|
||||
exp,
|
||||
translate_var s v q
|
||||
)
|
||||
in
|
||||
|
||||
let flatten_automaton automaton =
|
||||
let (init, states) = automaton in
|
||||
(flatten_state init, List.map flatten_state states)
|
||||
in
|
||||
let (init, states) = flatten_automaton automaton in
|
||||
let s = create_automaton_name () in
|
||||
init_state_translation states 1;
|
||||
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
|
||||
Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist)::acc) gathered new_equations, IVar(s)
|
||||
|
||||
|
||||
let automata_trans_pass debug (node:t_node) : t_node option=
|
||||
|
||||
let rec aux automaton = match automaton with
|
||||
| [] -> [], [], []
|
||||
| a::q ->
|
||||
let eq, var = automaton_translation debug a
|
||||
and tail_eq, tail_var, tail_type = aux q in
|
||||
eq@tail_eq, var::tail_var, TInt::tail_type
|
||||
in
|
||||
|
||||
let eqs, vars, new_ty = aux node.n_automata in
|
||||
let ty, loc_vars = node.n_local_vars in
|
||||
Some
|
||||
{
|
||||
n_name = node.n_name;
|
||||
n_inputs = node.n_inputs;
|
||||
n_outputs = node.n_outputs;
|
||||
n_local_vars = (new_ty@ty, vars@loc_vars);
|
||||
n_equations = eqs@node.n_equations;
|
||||
n_automata = []; (* not needed anymore *)
|
||||
}
|
||||
|
||||
let automata_translation_pass verbose debug main_fn =
|
||||
node_pass (automata_trans_pass debug)
|
||||
|
||||
|
||||
|
@ -31,3 +31,8 @@ let expression_pass f: t_nodelist -> t_nodelist option =
|
||||
equation_pass aux
|
||||
|
||||
exception PassExn of string
|
||||
|
||||
let counter = ref 0
|
||||
let create_automaton_name : unit -> string = fun () ->
|
||||
counter := !counter + 1;
|
||||
Format.asprintf "_s%d" (!counter)
|
||||
|
@ -1,5 +1,4 @@
|
||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||
var i: int;
|
||||
let
|
||||
(o1, o2) = (i, i);
|
||||
tel
|
||||
@ -13,9 +12,10 @@ let
|
||||
tel
|
||||
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y:int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do o = (pre o) + 1; done
|
||||
| Decr -> do o = (pre o) - 1; done
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); done
|
||||
| Decr -> do (o,x) = diagonal_int(0 fby o); done
|
||||
tel
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user