l2lWhenOnId.ml

(** 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