(* Time-stamp: <modified the 08/04/2013 (at 10:43) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
let finish_me lxm
= print_string ("\nsocPref.ml:"^(Lxm.details lxm)^" -> finish me!\n")
open Soc
(* Some aliases *)
let b = Soc.Bool
let i = Soc.Int
let r = Soc.Real
let aa t1 t2 = ["x", t1], ["z", t2]
let aaa t1 t2 t3 = ["x", t1; "y",t2], ["z", t3]
let aab t1 t2 = ["x", t1; "y",t2], ["z", Bool]
(* if/then/else *)
let baaa t = ["c", b; "xt", t; "xe", t], ["z", t]
let (soc_profile_of_types : Soc.var_type list -> var list * var list) =
function
| [t1; t2] -> aa t1 t2
| [t1;t2;t3] -> aaa t1 t2 t3
| [Bool;t1;t2;t3] -> baaa t1
| tl ->
print_string ("Unsupported case: "^ (
String.concat "," (List.map SocUtils.string_of_type_ref tl)));
flush stdout;
assert false
(* For diese and nor *)
let (soc_profile_of_types_nary : Soc.var_type list -> var list * var list) =
fun vl ->
["x", Array(Bool,List.length vl)], ["z",Bool]
let step11 = { (* a useful alias again *)
name = "step";
lxm = Lxm.dummy "predef soc";
idx_ins = [0];
idx_outs = [0];
impl = Predef;
}
let step21 impl = { (* a useful alias again *)
name = "step";
lxm = Lxm.dummy "predef soc";
idx_ins = [0;1];
idx_outs = [0];
impl = Predef;
}
(* used to build predef soc with no memory *)
let make_soc key profile steps = {
key = key;
profile = profile;
instances = [];
(* init = None; *)
precedences = [];
step = steps;
have_mem = None;
}
let first_instant = Var("first_instant", Bool)
let (get_mem_name : Soc.key -> var_type -> string) =
fun (k,tl,_) vt ->
match Str.split (Str.regexp "::") k with
| ["Lustre";op] -> (
match op.[0] with
| 'i' | 'b' | 'r' -> String.set op 0 '_'; ("mem"^op)
| _ -> "mem_"^op
)
| _ -> "mem_"^k
(* exported *)
let of_soc_key : Soc.key -> Soc.t =
fun sk ->
let (id, tl, _) = sk in
let sp = soc_profile_of_types in
let sp_nary = soc_profile_of_types_nary in
match id with
| "Lustre::mod" -> (make_soc sk (sp tl) [step11])
| "Lustre::uminus" -> (make_soc sk (sp tl) [step11])
| "Lustre::not" -> (make_soc sk (sp tl) [step11])
| "Lustre::real2int" -> (make_soc sk (sp tl) [step11])
| "Lustre::int2real" -> (make_soc sk (sp tl) [step11])
| "Lustre::plus" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::times" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::div" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::minus" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::lt" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::gt" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::lte" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::gte" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::and" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::eq" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::neq" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::or" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::xor" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::impl" -> (make_soc sk (sp tl) [step21 None])
(* Those have instances *)
| "Lustre::current" -> (
let _,tl,_ = sk in
let t = List.hd tl in
let pre_mem:var = (get_mem_name sk t, t) in
let prof = sp tl in
let v1,vout = match prof with ([v1],[vout]) -> v1,vout | _ -> assert false in
{
key = sk;
profile = (sp tl);
instances = [];
have_mem = Some (t, None); (* so that pre_mem exist *)
step = [
{
name = "get";
lxm = Lxm.dummy "predef soc";
idx_ins = [];
idx_outs = [0];
impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
};
{
name = "set";
lxm = Lxm.dummy "predef soc";
idx_ins = [0];
idx_outs = [];
impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]);
};
];
precedences = ["get", ["set"]];
}
)
| "Lustre::pre" ->
let _,tl,_ = sk in
let t = List.hd tl in
let pre_mem:var = (get_mem_name sk t, t) in
let prof = sp tl in
let v1,vout = match prof with ([v1],[vout]) -> v1,vout | _ -> assert false in
{
key = sk;
profile = (sp tl);
instances = [];
have_mem = Some (t, None); (* so that pre_mem exist *)
step = [
{
name = "get";
lxm = Lxm.dummy "predef soc";
idx_ins = [];
idx_outs = [0];
impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
};
{
name = "set";
lxm = Lxm.dummy "predef soc";
idx_ins = [0];
idx_outs = [];
impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]);
};
];
precedences = ["set", ["get"]];
}
| "Lustre::arrow" ->
let prof = sp tl in
{
key = sk;
profile = prof;
instances = [];
step = [
{
name = "step";
lxm = Lxm.dummy "predef soc";
idx_ins = [0;1];
idx_outs = [0];
impl = Predef;
}
];
precedences = [];
have_mem = None;
}
| "Lustre::fby" -> assert false
| "Lustre::if" -> {
key = sk;
profile = (sp tl);
instances = [];
(* init = None; *)
precedences = [];
have_mem = None;
step = [
{
name = "step";
lxm = Lxm.dummy "predef soc";
idx_ins = [0; 1; 2];
idx_outs = [0];
impl = Predef;
} ];
}
| "Lustre::nor" ->
let size = match sk with
| _,[Array(Bool,size);_],_ -> size
| _ -> assert false
in
{
Soc.key = sk;
Soc.profile = sp_nary tl;
Soc.instances = [] ;
Soc.step = [
{
name = "step";
lxm = Lxm.dummy "nor soc";
idx_ins = [0];
idx_outs = [0];
impl = Boolred(0,0, size);
}
];
Soc.have_mem = None;
Soc.precedences = [];
}
| "Lustre::diese" ->
let size = match sk with
| _,[Array(Bool,size);_],_ -> size
| _ -> assert false
in
{
Soc.key = sk;
Soc.profile = sp_nary tl;
Soc.instances = [] ;
Soc.step = [
{
name = "step";
lxm = Lxm.dummy "diese soc";
idx_ins = [0];
idx_outs = [0];
impl = Boolred(1,1, size);
}
];
Soc.have_mem = None;
Soc.precedences = [];
}
| _ ->
print_string ("*** The soc of "^id ^ " is not defined. FINISH ME! \n"); flush stdout;
assert false
(** Instancie un composant polymorphe avec un type concret. *)
let instanciate_soc: Soc.t -> Soc.var_type -> Soc.t =
fun c concrete_type ->
let rec instanciate_type vt =
match vt with
| Alpha _ -> concrete_type
| Struct(sn, fl) ->
Struct(sn, List.map (fun (id,vt) -> (id,instanciate_type vt)) fl)
| Array(vt,i) -> Array(instanciate_type vt,i)
| vt -> vt
in
let new_profile =
List.map (fun (vn,vt) -> vn, instanciate_type vt) (fst c.profile),
List.map (fun (vn,vt) -> vn, instanciate_type vt) (snd c.profile)
in
let instanciate_key (key1, key2, key3) =
(key1, List.map instanciate_type key2, key3)
in
let new_key = instanciate_key c.key in
let new_instances =
List.map (fun (id,sk) -> (id,instanciate_key sk)) c.instances
in
{
c with
key = new_key;
profile = new_profile;
instances = new_instances;
}
(*
XXX Faut-il definir une version g�n�rique des composants tranches ?
Je les ai d�fini directement via "make_slice_soc", ce qui
n'est pas homogene avec la facon dont sont trait�s les autres
composants g�n�riques style 'fby'.
Le truc, c'est que je ne sais pas trop quoi mettre dans la version
g�n�rique, et comme celle-ci est destin�e � �tre instanci�e... En
effet, le type de sortie des composants tranche depend de la
slice_info pass� en parametre lors de l'instanciation des composant
g�n�riques. Je pourrais mettre un type alpha, mais je trouve ca
idiot, alors je ne le fais pas...
Une autre solution pour rendre ce traitement homogene serait de ne
pas passer par une version g�n�rique pour les composants fby et
consort. A voir.
idem pour "x^n" (Hat_n).
*)
let make_slice_soc: Lic.slice_info -> Soc.var_type -> Soc.t =
fun si t ->
let (f,l,step) = (si.Lic.se_first, si.Lic.se_last,si.Lic.se_step) in
let sub_array_type =
match t with
| Soc.Array(t_elt,size) ->
let slice_size = 1+abs( (l - f) / step) in
Soc.Array(t_elt, slice_size)
| _ -> assert false
in
{
key = ("array_slice", [t], Some (f, l, step));
profile = (["t", t], ["st", sub_array_type ]);
instances = [];
step = [
{
name = "step";
lxm = Lxm.dummy "predef soc";
idx_ins = [0];
idx_outs = [0];
impl = Predef;
};
];
precedences = [];
have_mem = None;
(* init = None; *)
}
let (make_merge_soc: Soc.key -> Soc.t) =
fun sk ->
let (id, tl, _) = sk in
let in_tl, out_t = match List.rev tl with x::l -> List.rev l, x | [] -> assert false in
let profile_in = ("clk", List.hd in_tl)::
(List.mapi (fun i vt -> "x"^(string_of_int i), vt) in_tl)
in
let i = List.length in_tl in
{
Soc.key = sk;
Soc.profile = profile_in, ["z", out_t];
Soc.instances = [] ;
Soc.step = [
{
name = "step";
lxm = Lxm.dummy "merge soc";
idx_ins = SocUtils.gen_index_list (i+1);
idx_outs = [0];
impl = Predef;
}
];
Soc.have_mem = None;
Soc.precedences = [];
}
let make_array_soc: int -> Soc.var_type -> Soc.t =
fun i t ->
let iprof =
let res = ref [] in
for k=i downto 1 do
res:= ("x"^(string_of_int k),t) :: !res;
done;
!res
in
let array_type = Array(t,i) in
let key_prof = (List.map snd iprof) @ [array_type] in
{
key = ("Lustre::array", key_prof, None);
profile = (iprof, ["z", array_type]);
instances = [];
step = [
{
name = "step";
lxm = Lxm.dummy "predef array soc";
idx_ins = SocUtils.gen_index_list i;
idx_outs = [0];
impl = Predef;
};
];
precedences = [];
have_mem = None;
}
let make_array_concat_soc: int -> int -> Soc.var_type -> Soc.t =
fun s1 s2 t ->
let iprof = (["x", Array(t,s1); "y", Array(t,s2)], ["z", Array(t,s1+s2)])in
let key_prof = [Array(t,s1); Array(t,s2); Array(t,s1+s2)] in
{
key = ("Lustre::concat", key_prof, None);
profile = iprof;
instances = [];
step = [
{
name = "step";
lxm = Lxm.dummy "predef array concat soc";
idx_ins = [0;1];
idx_outs = [0];
impl = Predef;
};
];
precedences = [];
have_mem = None;
}
let make_hat_soc: int -> Soc.var_type -> Soc.t =
fun i t ->
let array_type =
match t with
| Soc.Alpha _ -> assert false
| t -> Soc.Array(t,i)
in
{
key = ("Lustre::hat", [t;array_type], None);
profile = ([("x", t)], ["z", array_type]);
instances = [];
step = [
{
name = "step";
lxm = Lxm.dummy "predef hat soc";
idx_ins = [0];
idx_outs = [0];
impl = Predef;
};
];
precedences = [];
have_mem = None;
}
let output_type_of_op op tl =
match op with
| "Lustre::eq"
| "Lustre::neq"
| "Lustre::lt"
| "Lustre::gt"
| "Lustre::lte"
| "Lustre::gte"
| "Lustre::nor"
| "Lustre::diese"
-> Bool
| "Lustre::real2int" -> Int
| "Lustre::int2real" -> Real
| "Lustre::if" -> List.hd (List.tl tl)
| _ -> List.hd tl
let (soc_interface_of_pos_op:
Lxm.t -> Lic.by_pos_op -> Soc.var_type list -> Soc.t) =
fun lxm op types ->
match (op, types) with
| Lic.PREDEF_CALL ({Lxm.it=("Lustre","if"),[]}), _ ->
let concrete_type = List.nth types 1 in
let soc = of_soc_key ("Lustre::if", types@[concrete_type], None) in
instanciate_soc soc concrete_type
| Lic.PREDEF_CALL {Lxm.it=(op,sargs)}, _ ->
assert (sargs=[]);
let soc_name = Ident.string_of_long op in
let out_type = output_type_of_op soc_name types in
let soc = of_soc_key (soc_name, types@[out_type], None) in
soc
| Lic.FBY, _ ->
let concrete_type = List.nth types 0 in
let soc = of_soc_key (("Lustre::fby"), types@[concrete_type], None) in
instanciate_soc soc concrete_type
| Lic.PRE, _ ->
let concrete_type = List.nth types 0 in
let soc = of_soc_key (("Lustre::pre"), types@[concrete_type], None) in
instanciate_soc soc concrete_type
| Lic.CURRENT, _ ->
let concrete_type = List.nth types 0 in
let soc = of_soc_key (("Lustre::current"), types@[concrete_type], None) in
instanciate_soc soc concrete_type
| Lic.ARROW, _ ->
let concrete_type = List.nth types 0 in
let soc = of_soc_key (("Lustre::arrow"), types@[concrete_type], None) in
let soc = instanciate_soc soc concrete_type in
soc
| Lic.HAT i,_ ->
let elt_type = List.nth types 0 in
(make_hat_soc i elt_type)
| Lic.ARRAY, _ ->
let elt_type = List.nth types 0 in
let i = (List.length types) in
(make_array_soc i elt_type)
| Lic.CONCAT , [Array (t1, s1); Array (t2, s2)]->
assert (t1=t2);
(make_array_concat_soc s1 s2 t1)
| Lic.CONCAT , _ -> assert false
| Lic.CALL _,_ -> assert false (* XXX todo *)
| Lic.CONST _ , _ -> assert false
(* Those are not soc *)
| Lic.ARRAY_SLICE sinfo,_ -> assert false
| Lic.VAR_REF _, _ -> assert false
| Lic.CONST_REF _, _ -> assert false
| Lic.STRUCT_ACCESS _, _ -> assert false
| Lic.WHEN _, _ -> assert false
| Lic.TUPLE, _ -> assert false
| Lic.ARRAY_ACCES _, _ -> assert false
(*
21/02/2013 : ai-je vraiment besoin de ca maintenant que les metaop ont �t� encapsul�
dans des noeuds ? bon, je garde quelque temps en commentaire au cas ou...
| Lic.Fill(node,size), _
| Lic.FillRed(node,size), _
| Lic.Red(node,size), _ ->
let soc = _key node with
| Undef name -> Undef name
(* Given
- a node n of type
tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l
- a integer c
the red expression has the profile:
tau * tau_1^c * ... * tau_n^c -> tau * teta_1^c * ... * teta_l^c
*)
| Some c ->
let arrayse l =
let exp (id,t) =
match t with
| Soc.Alpha _ -> assert false
| t -> id, Soc.Array(t,size)
in
match l with
| [] -> assert false
| (id,t)::tail ->(id, t):: (List.map exp tail)
in
Some {
(* XXX la clef devrait contenir le node et la taille ?
Les socosants iterateurs ne meritent ils pas un traitement
specifique ?
Ce que je veux, c'est
- y mettre toute l'information necessaire pour pouvoir generer
la boucle for qui va bien,
- garder une forme synthetique qui permette de faire des
analyses et de la v�rification
*)
key = ("fillred" ^ node ^ (string_of_int size), [], None);
profile =
(arrayse (fst c.profile), arrayse (snd c.profile));
instances = c.instances;
step = c.step;
(* XXX non ! le probleme, c'est que cette methode step
doit �tre fabriqu�e � partir de la methode step
du noeud it�r�, et que je n'ai rien pour exprimer
ce genre de truc pour l'instant.
*)
precedences = [];
init = c.init; (* XXX non ! *)
}
)
| Lic.Map(node,size), _ ->
let soc = _key node with
| Undef name -> Undef name
| Some c ->
(* Given
- a node n of type: tau_1 * ... * tau_n -> teta_1 * ... * teta_l
- an integer c
The profile of map is:
tau_1^c * ... * tau_n^c -> teta_1^c * ... * teta_l^c
*)
let arrayse l =
let exp (id,t) =
match t with
| Soc.Alpha _ -> assert false
| t -> id, Soc.Array(t,size)
in
(List.map exp l)
in
Some {
key = ("map" ^ node ^ (string_of_int size), [], None);
profile =
(arrayse (fst c.profile), arrayse (snd c.profile));
instances = c.instances;
step = c.step; (* XXX non ! *)
precedences = [];
init = c.init;
}
)
| Lic.BoolRed(i,j,k), _ -> Errors.finish_me lxm ; assert false
(* Cas particulier du boolred *)
| Lic.DIESE, _-> Errors.finish_me lxm ; assert false
| Lic.NOR ,_-> Errors.finish_me lxm ; assert false
*)