(** Time-stamp: <modified the 20/11/2008 (at 14:32) by Erwan Jahier> *)
open Lxm
open Eff
(********************************************************************************)
(* stuff to create fresh var names. *)
let var_cpt = ref 0
let new_var node_env type_eff clock_eff =
incr var_cpt;
let id = Ident.of_string ("_v" ^ (string_of_int !var_cpt)) in
let var =
{
var_name_eff = id;
var_nature_eff = SyntaxTreeCore.VarLocal;
var_number_eff = -1; (* this field is used only for i/o.
Should i rather put something sensible there ? *)
var_type_eff = type_eff;
var_clock_eff = clock_eff;
}
in
Hashtbl.add node_env.lenv_vars id var;
var
let init_var () =
var_cpt := 0
(********************************************************************************)
(* functions that deal with tuple breaking *)
let rec (get_vel_from_tuple : val_exp -> val_exp list) =
function
| CallByPosEff({it=Eff.TUPLE }, OperEff vel) ->
List.flatten (List.map get_vel_from_tuple vel)
| ve -> [ve]
let to_be_broken = function
(* We are only interested in operators that can deal with tuples! *)
| CallByPosEff({ it = Eff.ARROW }, _) -> true
| CallByPosEff({ it = Eff.FBY }, _) -> true
| CallByPosEff({ it = Eff.PRE }, _) -> true
| CallByPosEff({ it = Eff.CURRENT }, _) -> true
| CallByPosEff({ it = Eff.TUPLE }, _) -> true
| CallByPosEff({ it = Eff.WHEN _ }, _) -> true
| CallByPosEff({ it = Eff.Predef(Predef.IF_n, []) }, _) -> true
| _ -> false
let (break_it : val_exp -> val_exp list) =
function
| CallByPosEff({it=Eff.Predef(Predef.IF_n,[]);src=lxm}, OperEff [c;ve1;ve2]) ->
let vel1 = get_vel_from_tuple ve1
and vel2 = get_vel_from_tuple ve2
in
List.map2
(fun ve1 ve2 ->
CallByPosEff({it=Eff.Predef(Predef.IF_n,[]);src=lxm},
OperEff [c;ve1;ve2])
)
vel1
vel2
| CallByPosEff({it=WHEN clk; src=lxm}, OperEff vel) ->
let vel = List.flatten (List.map get_vel_from_tuple vel) in
List.map
(fun ve -> CallByPosEff({it=WHEN clk ; src=lxm }, OperEff [ve]))
vel
| CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff vel) ->
let vel = List.flatten (List.map get_vel_from_tuple vel) in
List.map
(fun ve -> CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff [ve]))
vel
| CallByPosEff({it=op ; src=lxm }, OperEff [ve]) ->
let vel = get_vel_from_tuple ve in
List.map (fun ve -> CallByPosEff({it=op ; src=lxm }, OperEff [ve])) vel
| CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]) ->
let vel1 = get_vel_from_tuple ve1
and vel2 = get_vel_from_tuple ve2
in
List.map2
(fun ve1 ve2 ->
CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2])
)
vel1
vel2
| _ -> assert false
let (split_tuples:Eff.eq_info Lxm.srcflagged list -> Eff.eq_info Lxm.srcflagged list) =
fun eql ->
let split_one_eq eq =
let { src = lxm_eq ; it = (lhs, n_rhs) } = eq in
if List.length lhs > 1 && (to_be_broken n_rhs) then
let vel = break_it n_rhs in
let eqs =
try List.map2 (fun lhs ve -> [lhs], ve) lhs vel
with _ ->
assert false
in
let eqs = List.map (fun eq -> Lxm.flagit eq lxm_eq) eqs in
eqs
else
[eq]
in
List.flatten (List.map split_one_eq eql)
(********************************************************************************)
(* The functions below accumulate
(1) the new equations
(2) the fresh variables.
*)
type split_acc = (Eff.eq_info srcflagged) list * Eff.var_info list
let rec (split_eq :
Eff.local_env -> split_acc -> Eff.eq_info srcflagged -> split_acc) =
fun node_env (eqs, locs) eq ->
let (neqs, nlocs) = split_eq_do node_env eq in
(split_tuples (eqs@neqs), locs@nlocs)
and (split_eq_do : Eff.local_env -> Eff.eq_info Lxm.srcflagged -> split_acc) =
fun node_env { src = lxm_eq ; it = (lhs, rhs) } ->
let n_rhs, (neqs, nlocs) = split_val_exp true node_env rhs in
{ src = lxm_eq ; it = (lhs, n_rhs) }::neqs, nlocs
and (split_val_exp : bool -> Eff.local_env -> Eff.val_exp -> Eff.val_exp * split_acc) =
fun top_level node_env ve ->
match ve with
| CallByPosEff({it=Eff.IDENT _}, _)
| CallByPosEff({it=Eff.CONST _}, _)
| CallByPosEff({it=Eff.Predef(Predef.TRUE_n,_)}, _)
| CallByPosEff({it=Eff.Predef(Predef.FALSE_n,_)}, _)
| CallByPosEff({it=Eff.Predef(Predef.ICONST_n _,_)}, _)
| CallByPosEff({it=Eff.Predef(Predef.RCONST_n _,_)}, _)
(* We do not create an intermediary variable for those *)
-> ve, ([],[])
| CallByNameEff (by_name_op_eff, fl) ->
let lxm = by_name_op_eff.src in
let fl, eql, vl =
List.fold_left
(fun (fl_acc, eql_acc, vl_acc) (fn, fv) ->
let fv, (eql, vl) = split_val_exp false node_env fv in
((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc)
)
([],[],[])
fl
in
let rhs = CallByNameEff (by_name_op_eff, List.rev fl) in
if top_level then
rhs, (eql, vl)
else
(* create the var for the current call *)
let clk_l = EvalClock.get_val_exp_eff ve in
let typ_l = EvalType.val_exp_eff ve in
let nv_l = List.map2 (new_var node_env) typ_l clk_l in
let nve = match nv_l with
| [nv] -> CallByPosEff(
Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm,
OperEff []
)
| _ -> assert false
in
let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in
let eq = Lxm.flagit (lpl, rhs) lxm in
nve, (eql@[eq], vl@nv_l)
| CallByPosEff(by_pos_op_eff, OperEff vel) ->
(* recursively split the arguments *)
let lxm = by_pos_op_eff.src in
let (rhs, (eql,vl)) =
match by_pos_op_eff.it with
(* for WITH and HAT, a particular treatment is done because
the val_exp is attached to them *)
| Eff.WITH(ve) ->
let ve, (eql, vl) = split_val_exp false node_env ve in
let by_pos_op_eff = Lxm.flagit (Eff.WITH(ve)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
rhs, (eql, vl)
| Eff.HAT(i,ve) ->
let ve, (eql, vl) = split_val_exp false node_env ve in
let by_pos_op_eff = Lxm.flagit (Eff.HAT(i, ve)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
rhs, (eql, vl)
| Eff.WHEN ve -> (* should we create a var for the clock ? *)
let vel,(eql, vl) = split_val_exp_list false node_env vel in
let by_pos_op_eff = Lxm.flagit (Eff.WHEN(ve)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
rhs, (eql, vl)
| _ ->
let vel, (eql, vl) = split_val_exp_list false node_env vel in
let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
rhs, (eql, vl)
in
if top_level || by_pos_op_eff.it = TUPLE then
rhs, (eql, vl)
else
(* create the var for the current call *)
let clk_l = EvalClock.get_val_exp_eff ve in
let typ_l = EvalType.val_exp_eff ve in
let nv_l = List.map2 (new_var node_env) typ_l clk_l in
let nve = match nv_l with
| [nv] -> CallByPosEff(
Lxm.flagit (Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm,
OperEff []
)
| _ -> CallByPosEff(
Lxm.flagit Eff.TUPLE lxm,
OperEff
(List.map (
fun nv ->
CallByPosEff
(Lxm.flagit
(Eff.IDENT (Ident.to_idref nv.var_name_eff)) lxm,
OperEff []
))
nv_l
)
)
in
let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in
let eq = Lxm.flagit (lpl, rhs) lxm in
nve, (eql@[eq], vl@nv_l)
and (split_val_exp_list :
bool -> Eff.local_env -> Eff.val_exp list -> Eff.val_exp list * split_acc) =
fun top_level node_env vel ->
let vel, accl = List.split (List.map (split_val_exp top_level node_env) vel) in
let eqll,vll = List.split accl in
let eql, vl = List.flatten eqll, List.flatten vll in
(vel,(eql,vl))
(* exported *)
let (node : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
fun n_env n ->
match n.def_eff with
| ExternEff
| AbstractEff -> n
| BodyEff b ->
init_var ();
let loc = match n.loclist_eff with None -> [] | Some l -> l in
let (neqs, nv) = List.fold_left (split_eq n_env) ([], loc) b.eqs_eff in
let asserts = List.map (fun x -> x.it) b.asserts_eff in
let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in
let nasserts,(neqs_asserts,nv_asserts) =
split_val_exp_list true n_env asserts
in
let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in
let (neqs, nv) = (neqs@neqs_asserts, nv@nv_asserts) in
let nb = { eqs_eff = neqs ; asserts_eff = nasserts } in
let res =
{ n with
loclist_eff = Some nv;
def_eff = BodyEff nb
}
in
res