l2lWhenOnId.ml

(** Time-stamp: <modified the 01/06/2016 (at 17:34) 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 acc = 
      Lic.var_info list           (* new local vars *)
    * Lic.eq_info srcflagged list (* equations *)
    * Lic.val_exp srcflagged list (* assertions *)

let new_var = FreshName.var_info
let new_var str type_eff clock_eff = 
  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
    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) -> (* On(Idle, st, enum_t)  *)
  
  let nv_base = (snd cc) ^ "_" ^ cv in
  let nv = new_var nv_base Bool_type_eff clk 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)

(********************************************************************************)
(* 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) = do_val_exp licprg ve acc in
    nv, { src = lxm_eq ; it = (left_list, ve) }::neqs, nass
      
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 -> 
    match n.def_eff with
      | ExternLic | MetaOpLic | AbstractLic _ -> n
      | BodyLic b ->
        let acc = List.fold_left 
          (fun acc eq -> do_eq licprg eq acc) 
          ([],[],[]) 
          (List.rev b.eqs_eff)
        in
        let acc = List.fold_left 
          (fun acc ve -> 
            let ve,(nv,neq,nass) = do_val_exp_flag licprg ve acc in
            (nv,neq,ve::nass)
          )
          acc
          b.asserts_eff 
        in
        let (nv,neqs,nass) = acc in
        let nlocs = match n.loclist_eff with
          | None -> nv (* SNO, but eats no bread *)
          | Some v -> List.rev_append nv v
        in
        { n with 
          def_eff = BodyLic  { 
            eqs_eff = neqs; 
            asserts_eff = nass;
          };
          loclist_eff = Some nlocs;
        }

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