(** Time-stamp: <modified the 24/11/2016 (at 16:26) by Erwan Jahier> *)
open Lxm
open Lic
open AstPredef
let dbg = (Lv6Verbose.get_flag "nwn")
(********************************************************************************)
(** The functions below accumulate
(1) the new assertions
(2) the new equations
(3) the fresh variables
(4) the table mapping boolean clock var to its (created) negation
**)
type clock_tbl = (Lv6Id.t, Lic.var_info) Hashtbl.t (* use 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 new_var label cv type_eff sclk clk_tbl =
try Hashtbl.find clk_tbl cv, true
with Not_found ->
let id = Lv6Id.of_string (FreshName.local_var cv) in
Lv6Verbose.exe
~flag:dbg
(fun() -> Printf.printf
"#NWN: negation of '%s' not found; create %s(%s) [%s]\n"
cv id (Lic.string_of_clock sclk) label);
let var = {
var_name_eff = id;
var_nature_eff = AstCore.VarLocal;
var_number_eff = -1;
var_type_eff = type_eff;
var_clock_eff = id, sclk;
}
in
Hashtbl.add clk_tbl cv var;
var,false
(********************************************************************************)
(* The one that performs the real work, namely:
- if it hasn't been created yet
- invent a fresh var name NV,
- generate the equation defining NV (NV= not v);)
*)
let (gen_ident : string -> Lxm.t -> Lv6Id.t -> type_ -> Lic.clock -> acc ->
var_info * acc ) =
fun label lxm cv ct clk (vl,eql,al,tbl) ->
let nv, already_done = new_var label cv ct clk tbl in
if already_done then
nv, (vl,eql,al,tbl)
else
let ve = {
ve_typ = [ct];
ve_clk = [clk];
ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[]);
ve_src = lxm
}
in
let not_ve = {
ve_typ = [Bool_type_eff];
ve_clk = [clk];
ve_core =
CallByPosLic({it=Lic.PREDEF_CALL({it=(("Lustre","not"),[]);src=lxm});src=lxm},
[ve]);
ve_src = lxm
}
in
let new_eq = (* NV= not v *) {src=lxm;it=[LeftVarLic (nv, lxm)], not_ve} in
nv, (nv::vl,new_eq::eql,al,tbl)
(********************************************************************************)
let rec update_clock : Lxm.t -> acc -> clock -> clock * acc =
fun lxm acc clk ->
match clk with
| BaseLic -> clk, acc
| ClockVar _ -> clk, acc
(* XXXX assert false *)
| On((cc,cv,ct),sclk) ->
let sclk, acc = update_clock lxm acc sclk in
if cc <> ("Lustre","false") then
On((cc,cv,ct),sclk), acc
else
let nv, acc =
let (_,_,_,clk_tbl) = acc in
try Hashtbl.find clk_tbl cv, acc
with Not_found -> gen_ident "ici" lxm cv ct sclk acc
in
Lv6Verbose.exe
~flag:dbg
(fun() -> Printf.printf
"#NWN: not(%s) -> %s\n" cv nv.var_name_eff);
On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc
let rec update_clock_list : Lxm.t -> clock list * acc -> clock -> clock list * acc =
fun lxm (res,acc) clk ->
let clk, acc = update_clock lxm acc clk in
clk::res, acc
let update_var_info : Lxm.t -> acc -> var_info -> var_info * acc =
fun lxm acc vi ->
let (id, clk) = vi.var_clock_eff in
let nclk, acc = update_clock lxm acc clk in
Lv6Verbose.exe
~flag:dbg
(fun() ->
if clk <> nclk then (
Printf.printf
"#NWN: update_var_info of %s (%s->%s\n"
vi.var_name_eff
(Lic.string_of_clock clk) (Lic.string_of_clock nclk)
));
{ vi with var_clock_eff = id, nclk }, acc
let update_var_info_list : Lxm.t -> var_info list * acc -> var_info ->
var_info list * acc =
fun lxm (res,acc) vi ->
let vi, acc = update_var_info lxm acc vi in
vi::res, acc
let rec update_left : acc -> left -> left * acc =
fun acc l ->
match l with
| LeftVarLic(vi,lxm) ->
let vi, acc = update_var_info lxm acc vi in
LeftVarLic(vi,lxm), acc
| LeftFieldLic(l,id,t) ->
let l, acc = update_left acc l in
LeftFieldLic(l,id,t),acc
| LeftArrayLic(l,i,t) ->
let l, acc = update_left acc l in
LeftArrayLic(l,i,t), acc
| LeftSliceLic(l,si,t) ->
let l, acc = update_left acc l in
LeftSliceLic(l,si,t), acc
let rec update_left_list : left list * acc -> left -> left list * acc =
fun (ll,acc) l ->
let l, acc = update_left acc l in
l::ll, acc
(********************************************************************************)
(* 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,acc = List.fold_left update_left_list ([],acc) left_list in
let left_list = List.rev 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((("Lustre","false"),cv,Bool_type_eff),clk)) ->
let clk, acc = update_clock op.src acc clk in
let nv, acc =
let (_,_,_,clk_tbl) = acc in
try Hashtbl.find clk_tbl cv, acc
with Not_found -> gen_ident "la" op.src cv Bool_type_eff clk acc
in
let true_cc = "Lustre","true" in
let new_op = WHEN (On((true_cc, nv.var_name_eff, Bool_type_eff),clk)) in
let op = Lxm.flagit new_op op.src in
CallByPosLic(op, vel), acc
| WHEN (On((cc,cv,Bool_type_eff),clk)) ->
let clk, acc = update_clock op.src acc clk in
let new_op = WHEN (On((cc, cv, Bool_type_eff),clk)) in
let op = Lxm.flagit new_op op.src in
CallByPosLic(op, vel), acc
| _ ->
CallByPosLic(op, vel), acc
)
in
let lxm = lxm_of_val_exp ve in
let ve_clk, acc = List.fold_left (update_clock_list lxm) ([],acc) ve.ve_clk in
{ ve with ve_core = ve_core;
ve_clk = List.rev ve_clk;
},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 acc =
match n.def_eff with
| ExternLic | MetaOpLic | AbstractLic _ -> n,acc
| BodyLic b ->
let acc = List.fold_left
(fun acc eq -> do_eq licprg eq acc)
acc
(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 uvi = update_var_info_list n.lxm in
let inlist_eff,acc = List.fold_left uvi ([],acc) n.inlist_eff in
let outlist_eff,acc = List.fold_left uvi ([],acc) n.outlist_eff in
let locs = match n.loclist_eff with Some x -> x | None -> [] in
let loclist_eff,acc = List.fold_left uvi ([],acc) locs in
let (nv,neqs,nass,tbl) = acc in
let nlocs = List.rev_append nv loclist_eff in
{ n with
def_eff = BodyLic { eqs_eff = neqs; asserts_eff = nass };
inlist_eff = List.rev inlist_eff;
outlist_eff = List.rev outlist_eff;
loclist_eff = Some (List.rev nlocs)
},acc
in
let n,acc = aux licprg n ([],[],[],tbl) in
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 "#NWN: '%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