Newer
Older
Erwan Jahier
committed
(* Time-stamp: <modified the 24/04/2013 (at 17:42) by Erwan Jahier> *)
let dbg = (Verbose.get_flag "en")
(* pack useful info into a single struct *)
type local_ctx = {
idgen : LicPrg.id_generator;
node : Lic.node_exp;
prg : LicPrg.t;
nodes : string list; (* nodes to repserve from expansion *)
(********************************************************************************)
(* stuff to create fresh var names.
XXX code dupl. with Split.new_var
*)
let new_var str lctx type_eff clock_eff =
let id = Ident.of_string (LicName.new_local_var str) in
var_nature_eff = AstCore.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
var
(********************************************************************************)
let get_locals node =
match node.loclist_eff with
| None -> []
| Some l -> l
let rec (get_node_body : local_ctx -> Lic.node_exp -> Lic.node_body option) =
fun lctx node ->
| ExternLic
| AbstractLic None -> None
| AbstractLic (Some node) -> assert false
| BodyLic node_body -> Some node_body
| MetaOpLic -> None
(********************************************************************************)
type subst = (Ident.t * var_info) list
Erwan Jahier
committed
let rec (substitute :
subst -> Lic.eq_info Lxm.srcflagged -> Lic.eq_info Lxm.srcflagged) =
fun s { it = (lhs,ve) ; src = lxm } ->
let lhs = List.map (subst_in_left s) lhs in
Erwan Jahier
committed
let newve = subst_in_val_exp s ve in
{ it = (lhs,newve) ; src = lxm }
and subst_in_left s left =
match left with
| LeftVarLic(v,lxm) -> (try LeftVarLic(List.assoc v.var_name_eff s,lxm) with Not_found -> left)
| LeftFieldLic(left,id,t) -> LeftFieldLic(subst_in_left s left,id,t)
| LeftArrayLic(left,i, t) -> LeftArrayLic(subst_in_left s left,i, t)
| LeftSliceLic(left,si,t) -> LeftSliceLic(subst_in_left s left,si,t)
and (subst_in_clock : subst -> clock -> clock) =
fun s clk ->
match clk with
| BaseLic -> BaseLic
| ClockVar i -> ClockVar i
| On ((cc,cv,ct),clk) ->
let cv = try (List.assoc cv s).var_name_eff with Not_found -> cv in
On ((cc,cv,ct), subst_in_clock s clk)
and (subst_in_val_exp : subst -> val_exp -> val_exp) =
fun s ve ->
let newve = {
ve with ve_core =
match ve.ve_core with
| CallByPosLic (by_pos_op, vel) ->
let lxm = by_pos_op.src in
let by_pos_op = by_pos_op.it in
let vel = List.map (subst_in_val_exp s) vel in
let by_pos_op = match by_pos_op with
| CONST_REF idl -> CONST_REF idl
| VAR_REF id ->
let id' =
try
let var = List.assoc id s in
var.var_name_eff
with Not_found -> id
in
VAR_REF id'
| WHEN(clk) -> WHEN(subst_in_clock s clk)
| PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT | TUPLE
| ARRAY | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _
CallByPosLic(Lxm.flagit by_pos_op lxm, vel)
| CallByNameLic(by_name_op, fl) ->
let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in
CallByNameLic(by_name_op, fl)
| Merge(ce,cl) ->
let cl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) cl in
Merge(ce, cl)
Erwan Jahier
committed
in
let mk_loc_subst l1 l2 = List.combine (List.map (fun v -> v.var_name_eff) l1) l2
(********************************************************************************)
(** The functions below accumulate
(1) the assertions
(2) the new equations
(3) the fresh variables
*)
type acc =
Lic.val_exp srcflagged list (* assertions *)
* (Lic.eq_info srcflagged) list (* equations *)
* Lic.var_info list (* new local vars *)
let (mk_fresh_loc : local_ctx -> var_info -> clock -> var_info) =
fun lctx v c ->
new_var (Ident.to_string v.var_name_eff) lctx v.var_type_eff (fst v.var_clock_eff, c)
(* When expanding a node call such as
x = toto(a when c);
when toto params are (for example) on the base clock, we need to
propagate the substitution between the toto base clock and "on(c)"
; for the toto arguments, it's been done during clock checking ;
but we need to remember this information to substitute the clock
of toto in its local variables.
*)
type clock_substs = (clock * clock) list
let (add_clock_subst: clock -> clock -> clock_substs -> clock_substs) =
fun c1 c2 cs ->
if List.mem_assoc c1 cs then cs else (c1,c2)::cs
let (mk_input_subst: local_ctx -> Lxm.t -> var_info list ->
Lic.val_exp list -> acc -> subst * acc * clock_substs) =
fun lctx lxm vl vel acc ->
assert(List.length vl = List.length vel);
(fun (s,(a_acc,e_acc,v_acc),cs) v ve ->
(* we create a new var for each node argument, which is a little
bit bourrin if ever ve is a simple ident... *)
let clk = match ve.ve_clk with
| [c] -> c
| _ -> assert false
in
let nv = mk_fresh_loc lctx v clk in
let neq = [LeftVarLic(nv,lxm)],ve in
let neq = flagit neq lxm in
let cs = add_clock_subst (snd v.var_clock_eff) clk cs in
(v.var_name_eff,nv)::s,(a_acc, neq::e_acc, nv::v_acc), cs
vl
vel
(* create fresh vars if necessary *)
let (mk_output_subst : local_ctx -> Lxm.t -> var_info list -> Lic.left list -> clock_substs ->
acc -> subst * acc * clock_substs) =
fun lctx lxm vl leftl cs acc ->
assert(List.length vl = List.length leftl);
(fun (s,acc,cs) v left ->
match left with
| LeftVarLic(v2,lxm) -> (v.var_name_eff,v2)::s, acc,cs
| _ ->
let clk = Lic.clock_of_left left in
let nv = mk_fresh_loc lctx v clk in
let nv_id = nv.var_name_eff in
let nve = {
ve_core = CallByPosLic({it=VAR_REF nv_id;src = lxm },[]);
ve_typ = [nv.var_type_eff];
ve_clk = [snd nv.var_clock_eff]
}
in
let neq = [left], nve in
let neq = flagit neq lxm in
(* for equations of the form
x.field = n(...);
we create
- a fresh var "_v"
- define the equation "x.field = _v;"
- create the substition n_output_par/_v
*)
let (aa,ae,av) = acc in
let cs = add_clock_subst (snd v.var_clock_eff) clk cs in
(v.var_name_eff,nv)::s, (aa, neq::ae, nv::av), cs
let rec (expand_eq : local_ctx -> acc -> Lic.eq_info Lxm.srcflagged -> acc) =
fun lctx (asserts, eqs, locs) { src = lxm_eq ; it = eq } ->
match expand_eq_aux lctx eq with
| None -> asserts, { src = lxm_eq ; it = eq }::eqs, locs
| Some(nasserts, neqs, nlocs) ->
List.rev_append nasserts asserts,
List.rev_append neqs eqs,
List.rev_append nlocs locs
and (expand_eq_aux: local_ctx -> Lic.eq_info -> acc option)=
fun lctx (lhs,ve) ->
| CallByPosLic( { it = Lic.CALL node_key ; src = lxm }, vel) ->
let node =
match LicPrg.find_node lctx.prg node_key.it with
| Some n -> n
| None ->
prerr_string (
Erwan Jahier
committed
"*** "^ (LicDump.string_of_node_key_rec false node_key.it) ^" not defined.\n" ^
"*** Defined nodes are:"^
(String.concat ",\n"
Erwan Jahier
committed
(List.map (fun (nk,_) -> "\""^LicDump.string_of_node_key_rec false nk^"\"")
(LicPrg.list_nodes lctx.prg)))
);
flush stderr;
assert false
in
let node = flagit node lxm in
let node = match node.it.def_eff with
| AbstractLic (Some n) -> { it = n ; src = lxm }
| _ -> node
in
if
let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in
(List.mem nname lctx.nodes)
then
None
else
(match get_node_body lctx node.it with
| None -> None
| Some node_body ->
let node_eqs = node_body.eqs_eff
and asserts = node_body.asserts_eff in
let node = node.it in
let node_locs = get_locals node in
let acc = [],[],[] in
let is,acc,cs = mk_input_subst lctx lxm node.inlist_eff vel acc in
let os,acc,cs = mk_output_subst lctx lxm node.outlist_eff lhs cs acc in
let rec (substitute_clock : clock -> clock) =
fun c ->
try List.assoc c cs
with Not_found ->
match c with
| BaseLic
| ClockVar _ -> c (* XXX should/can it happen? *)
| On(v,clk) -> On(v, substitute_clock clk)
in
let clks = List.map (fun v -> substitute_clock (snd v.var_clock_eff)) node_locs in
let fresh_locs = List.map2 (mk_fresh_loc lctx) node_locs clks in
let ls = mk_loc_subst node_locs fresh_locs in
let s = List.rev_append is (List.rev_append os ls) in
let fresh_locs = (* substitute the new vars in clocks *)
List.map (fun v ->
let id,clk = v.var_clock_eff in
{ v with var_clock_eff = id, subst_in_clock s clk })
fresh_locs
in
let acc = match acc with (a,b,c) -> (a,b,c@fresh_locs) in
let node_eqs = List.map (substitute s) node_eqs in
let subst_assert x = Lxm.flagit (subst_in_val_exp s x.it) x.src in
let asserts = List.map subst_assert asserts in
let acc = List.fold_left (expand_eq lctx) acc node_eqs in
let acc = List.fold_left (expand_assert lctx) acc asserts in
Some acc
)
and (expand_assert : local_ctx -> acc -> val_exp srcflagged -> acc) =
fun lctx (a_acc,e_acc,v_acc) ve ->
let clk = Ident.of_string "dummy_expand_assert", BaseLic in
let assert_var = new_var "assert" lctx Bool_type_eff clk in
let assert_eq = Lxm.flagit ([LeftVarLic(assert_var,lxm)], ve) lxm in
let assert_op = Lic.VAR_REF(assert_var.var_name_eff) in
let nve = {
ve_core = CallByPosLic((Lxm.flagit assert_op lxm, []));
ve_typ = [Bool_type_eff];
}
in
expand_eq lctx ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq
let (node : local_ctx -> Lic.node_exp -> Lic.node_exp) =
fun lctx n ->
| ExternLic
| AbstractLic _ -> n
| BodyLic b ->
let acc = List.fold_left (expand_eq lctx) ([],[],locs) b.eqs_eff in
let acc = List.fold_left (expand_assert lctx) acc b.asserts_eff in
let (asserts,neqs, nv) = acc in
let nb = {
eqs_eff = neqs ;
asserts_eff = asserts
}
in
let res =
{ n with
loclist_eff = Some nv;
let (doit : string list -> LicPrg.t -> LicPrg.t) =
fun nodes 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 (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) =
fun nk ne outprg ->
Verbose.exe ~flag:dbg (fun () ->
Printf.printf "#DBG: expand nodes of '%s'\n"
(Lic.string_of_node_key nk));
let lctx = {
idgen = LicPrg.fresh_var_id_generator inprg ne;
node = ne;
prg = inprg;
}
in
let ne = node lctx ne in
LicPrg.add_node nk ne outprg
in
let outprg = LicPrg.fold_nodes do_node inprg outprg in
outprg