l2lNoWhenNot.ml

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

open Lxm
open Lic
 
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 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 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 (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 "#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