l2lWhenOnId.ml

(** Time-stamp: <modified the 29/08/2019 (at 16:07) by Erwan Jahier> *)

open Lxm
open Lic
 
let dbg =  (Lv6Verbose.get_flag "woi")


(********************************************************************************)
(** The functions below accumulate 
   (1) the new assertions
   (2) the new equations 
   (3) the fresh variables
   (4) the table mapping enumerated clocks to new boolean clock
*)

type clock_tbl = ((Lv6Id.long * 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 (cc,cv) type_eff clock_eff clk_tbl = 
   try Hashtbl.find clk_tbl (cc,cv), true
   with Not_found ->
     let str = (snd cc) ^ "_" ^ cv in
     let str2 = (snd cc) ^ "(" ^ cv ^")" in
     let id = Lv6Id.of_string (FreshName.local_var (str)) in 
     Lv6Verbose.exe
       ~flag:dbg
       (fun() -> Printf.printf
                   "L2lWhenOnId: '%s' not found; create %s\n" str2 id);
     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,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=(Idle=st);)
*)
let (gen_ident : Lxm.t -> Lv6Id.long -> Lv6Id.t -> type_ -> Lic.clock -> acc -> 
                  var_info * acc ) =
   fun lxm cc cv ct clk (vl,eql,al,tbl) -> (* On(Idle, st, enum_t)  *)
   let nv, already_done = 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,[]);
       ve_src = lxm
     }
     in
     let ve2 = {
       ve_typ = [ct];
       ve_clk = [clk]; 
       ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[]);
       ve_src = 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]);
       ve_src = lxm
     }
     in
     if already_done then
       nv, (vl,eql,al,tbl)
     else
       let new_eq = (* NV=(Idle=st) *) {src=lxm;it=[LeftVarLic (nv, lxm)], 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 | ClockVar _ -> clk, acc
  | On((cc,cv,ct),sclk) ->
     let sclk, acc = update_clock lxm acc sclk in
     let (_,_,_,clk_tbl) = acc in
     try 
       let nv = Hashtbl.find clk_tbl (cc,cv) in
       On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc
     with Not_found ->
       if cc = ("Lustre","true") || cc = ("Lustre","false") then 
         On((cc,cv,ct),sclk), acc
       else
         let nv, acc = gen_ident lxm cc cv ct sclk acc in
         On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc

let 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 clk, acc = update_clock lxm acc clk in
  Lv6Verbose.exe
    ~flag:dbg
    (fun() -> Printf.printf
                "#DBG: L2lWhenOnId;  update_var_info %s\n" id);
  { vi with var_clock_eff = id, clk }, 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 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((cc,cv,Bool_type_eff),clk)) -> (* nothing to do in this case *)
             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
          | WHEN (On((cc,cv,ct),clk)) ->
             let clk, acc = update_clock op.src acc clk in              
             let nv, acc = gen_ident op.src cc cv ct 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
          | _ ->
             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 (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 (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