(** Time-stamp: <modified the 07/06/2016 (at 13:30) by Erwan Jahier> *)
open Lxm
open Lic
open AstPredef
let dbg = (Lv6Verbose.get_flag "woi")
(********************************************************************************)
(** The functions below accumulate
(1) the assertions
(2) the new equations
(3) the fresh variables
*)
type clock_tbl = ((Lv6Id.long * Lv6Id.t), Lic.var_info) Hashtbl.t (* Map.t ? *)
type acc =
Lic.var_info list (* new local vars *)
* Lic.eq_info srcflagged list (* equations *)
* Lic.val_exp srcflagged list (* assertions *)
* clock_tbl
let rec update_clock : clock_tbl -> clock -> clock =
fun clk_tbl clk ->
match clk with
| BaseLic | ClockVar _ -> clk
| On((cc,cv,ct),sclk) ->
let sclk = update_clock clk_tbl sclk in
try
let nv = Hashtbl.find clk_tbl (cc,cv) in
On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk)
with Not_found ->
On((cc,cv,ct),sclk)
let update_var_info : clock_tbl -> var_info -> var_info =
fun tbl vi ->
let (id, clk) = vi.var_clock_eff in
{ vi with var_clock_eff = id, update_clock tbl clk }
let rec update_left : clock_tbl -> left -> left =
fun tbl l ->
match l with
| LeftVarLic(vi,lxm) -> LeftVarLic(update_var_info tbl vi,lxm)
| LeftFieldLic(l,id,t) -> LeftFieldLic(update_left tbl l,id,t)
| LeftArrayLic(l,i,t) -> LeftArrayLic(update_left tbl l,i,t)
| LeftSliceLic(l,si,t) -> LeftSliceLic(update_left tbl l,si,t)
let new_var (cc,cv) type_eff clock_eff clk_tbl =
try Hashtbl.find clk_tbl (cc,cv)
with Not_found ->
let str = (snd cc) ^ "_" ^ cv in
let id = Lv6Id.of_string (FreshName.local_var str) in
let var =
{
var_name_eff = id;
var_nature_eff = AstCore.VarLocal;
var_number_eff = -1;
var_type_eff = type_eff;
var_clock_eff = id,clock_eff;
}
in
Hashtbl.add clk_tbl (cc,cv) var;
var
(********************************************************************************)
(* The one that perform the real work, namely:
- invent a fresh var name NV
- replace 'when Idle(st)' by 'when NV'
- generate the equation defining NV (NV=(Idle=st);)
*)
let (gen_ident : Lxm.t -> Lv6Id.long -> Lv6Id.t -> type_ -> Lic.clock -> acc ->
Lic.by_pos_op srcflagged * acc ) =
fun lxm cc cv ct clk (vl,eql,al,tbl) -> (* On(Idle, st, enum_t) *)
let nv = new_var (cc,cv) Bool_type_eff clk tbl in
let ve1 = {
ve_typ = [ct];
ve_clk = [clk];
ve_core = CallByPosLic(Lxm.flagit (Lic.CONST_REF cc) lxm,[])
}
in
let ve2 = {
ve_typ = [ct];
ve_clk = [clk];
ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[])
}
in
let ve = (* Idle=st *){
ve_typ = [Bool_type_eff];
ve_clk = [clk];
ve_core =
CallByPosLic({it=Lic.PREDEF_CALL({it=(("Lustre","eq"),[]);src=lxm});src=lxm},
[ve1;ve2])
}
in
let new_eq = (* NV=(Idle=st) *) {src=lxm;it=[LeftVarLic (nv, lxm)], ve} in
let true_cc = "Lustre","true" in
let op = WHEN (On((true_cc, nv.var_name_eff, Bool_type_eff),clk)) in
Lxm.flagit op lxm, (nv::vl,new_eq::eql,al,tbl)
(********************************************************************************)
(* All the remaining are admnistrative functions *)
let rec (do_eq : LicPrg.t -> Lic.eq_info srcflagged -> acc -> acc) =
fun licprg { src = lxm_eq ; it = (left_list, ve) } acc ->
let ve, (nv,neqs,nass,tbl) = do_val_exp licprg ve acc in
let left_list = List.map (update_left tbl) left_list in
nv, { src = lxm_eq ; it = (left_list, ve) }::neqs, nass,tbl
and (do_val_exp: LicPrg.t -> val_exp -> acc -> val_exp * acc) =
fun licprg ve acc ->
let ve_core, acc =
match ve.ve_core with
| Merge(ce,cl) -> (
let cl,acc =
List.fold_left
(fun (ncl,acc) (c, ve) ->
let ve, acc = do_val_exp licprg ve acc in
((c, ve)::ncl), acc)
([],acc)
cl
in
Merge(ce,cl),acc
)
| CallByNameLic(op, fl) -> (
let fl,acc = List.fold_left
(fun (nfl,acc) (id,ve) ->
let nf, acc = do_val_exp licprg ve acc in
((id,nf)::nfl), acc
)
([],acc)
fl
in
CallByNameLic(op, fl), acc
)
| CallByPosLic (op, vel) -> (
let vel, acc = List.fold_left
(fun (vel,acc) ve ->
let ve, acc = do_val_exp licprg ve acc in
(ve::vel), acc
)
([],acc)
(List.rev vel)
in
match op.it with
| WHEN (On((_,_,Bool_type_eff),_)) -> (* nothing to do in this case *)
CallByPosLic(op, vel), acc
| WHEN (On((cc,cv,ct),clk)) ->
let op, acc = gen_ident op.src cc cv ct clk acc in
CallByPosLic(op, vel), acc
| _ -> CallByPosLic(op, vel), acc
)
in
{ ve with ve_core = ve_core },acc
and (do_val_exp_flag: LicPrg.t -> val_exp srcflagged -> acc ->
val_exp srcflagged * acc) =
fun licprg ve_f acc ->
let ve, acc = do_val_exp licprg ve_f.it acc in
{ ve_f with it = ve }, acc
and (do_node : LicPrg.t -> Lic.node_exp -> Lic.node_exp) =
fun licprg n ->
let tbl = Hashtbl.create 0 in
let aux licprg n =
match n.def_eff with
| ExternLic | MetaOpLic | AbstractLic _ -> n
| BodyLic b ->
let acc = List.fold_left
(fun acc eq -> do_eq licprg eq acc)
([],[],[],tbl)
(List.rev b.eqs_eff)
in
let acc = List.fold_left
(fun acc ve ->
let ve,(nv,neq,nass,tbl) = do_val_exp_flag licprg ve acc in
(nv,neq,ve::nass,tbl)
)
acc
b.asserts_eff
in
let (nv,neqs,nass,tbl) = acc in
let nlocs = match n.loclist_eff with
| None -> nv (* SNO, but eats no bread *)
| Some v -> List.rev_append nv v
in
let update_var_info = update_var_info tbl in
{ n with
def_eff = BodyLic {
eqs_eff = neqs;
asserts_eff = nass;
};
inlist_eff = List.map update_var_info n.inlist_eff;
outlist_eff = List.map update_var_info n.outlist_eff;
loclist_eff = Some (List.map update_var_info nlocs);
}
in
let n = aux licprg n in
let n = aux licprg n in (* do it twice to make sure they are all substituted *)
n
(* exported *)
let rec (doit : LicPrg.t -> LicPrg.t) =
fun inprg ->
let outprg = LicPrg.empty in
(** types and constants do not change *)
let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in
let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
(** transform nodes *)
let rec (doit_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) =
fun nk ne outprg ->
Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf "#DBG: L2lWhenOnId '%s'\n"
(Lic.string_of_node_key nk));
let ne = do_node inprg ne in
LicPrg.add_node nk ne outprg
in
let outprg = LicPrg.fold_nodes doit_node inprg outprg in
outprg