l2lExpandNodes.ml

(* Time-stamp: <modified the 13/08/2014 (at 16:25) by Erwan Jahier> *)


open Lxm
open Lic
open AstPredef
    
let dbg = (Verbose.get_flag "en")

(* pack useful info into a single struct *)
type local_ctx = { 
  init_prg : LicPrg.t; (* nodes before expansion *)
  curr_prg : LicPrg.t; (* nodes that have already been expanded *)
  nodes : string list; (* nodes to preserve from expansion *)
}

(********************************************************************************)
        
(* stuff to create fresh var names. 
   XXX code dupl. with Split.new_var 
*)
let new_var str lctx type_eff clock_eff = 
  let id = Ident.of_string (LicName.new_local_var str) in
  let var =
    { 
      var_name_eff   = id;
      var_nature_eff = AstCore.VarLocal;
      var_number_eff = -1; (* this field is used only for i/o. 
                              Should i rather put something sensible there ? *)
      var_type_eff   = type_eff;
      var_clock_eff  = clock_eff;
    }
  in
(*   let clk_str = string_of_clock (snd clock_eff) in *)
(*   print_string (" ===> creating "^id^ " from " ^ str^ " with clock " ^clk_str ^ "\n");flush stdout; *)
  var

(********************************************************************************)
let get_locals node =
  match node.loclist_eff with
    | None -> []
    | Some l -> l

let rec (get_node_body : local_ctx -> Lic.node_exp -> Lic.node_body option) =
  fun lctx node ->
    match node.def_eff with
      | ExternLic
      | AbstractLic None -> None
      | AbstractLic (Some node) -> assert false
      | BodyLic node_body -> Some node_body
      | MetaOpLic -> None

(********************************************************************************)
type subst = (Ident.t * var_info) list 
let rec (substitute : 
           subst -> Lic.eq_info Lxm.srcflagged -> Lic.eq_info Lxm.srcflagged) =
  fun s { it = (lhs,ve) ; src = lxm } -> 
    let lhs = List.map (subst_in_left s) lhs in
    let newve = subst_in_val_exp s ve in
    { it = (lhs,newve) ; src = lxm }

and subst_in_left s left =
  match left with
    | LeftVarLic(v,lxm) -> (try LeftVarLic(List.assoc v.var_name_eff s,lxm) with Not_found -> left)
    | LeftFieldLic(left,id,t) -> LeftFieldLic(subst_in_left s left,id,t)
    | LeftArrayLic(left,i, t) -> LeftArrayLic(subst_in_left s left,i, t)
    | LeftSliceLic(left,si,t) -> LeftSliceLic(subst_in_left s left,si,t)

and (subst_in_clock : subst -> clock -> clock) =
  fun s clk -> 
    match clk with
      | BaseLic -> BaseLic
      | ClockVar i -> ClockVar i
      | On ((cc,cv,ct),clk) -> 
        let cv = try (List.assoc cv s).var_name_eff with Not_found -> cv in 
        On ((cc,cv,ct), subst_in_clock s clk) 

and (subst_in_val_exp : subst -> val_exp -> val_exp) =
  fun s ve -> 
    let newve = {
      ve with ve_core =
        match ve.ve_core with
	       | CallByPosLic (by_pos_op, vel) -> 
            let lxm = by_pos_op.src in
            let by_pos_op = by_pos_op.it in
            let vel = List.map (subst_in_val_exp s) vel in
            let by_pos_op = match by_pos_op with
		        | CONST_REF idl -> CONST_REF idl 
              | VAR_REF id -> 
                let id' =
                  try
                    let var = List.assoc id s in
                    var.var_name_eff
                  with Not_found -> id
                in
                VAR_REF id'
              | WHEN(clk) -> WHEN(subst_in_clock s clk)
              | HAT(i) -> HAT(i)
              | PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT _ | TUPLE
              | ARRAY | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _ 
              | CONST _ 
                -> by_pos_op
            in
            CallByPosLic(Lxm.flagit by_pos_op lxm, vel)
		        
	       | CallByNameLic(by_name_op, fl) ->
            let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in
            CallByNameLic(by_name_op, fl) 
          | Merge(ce,cl) ->
            let cl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) cl in
            Merge(ce, cl)
    }
    in
    newve

let mk_loc_subst l1 l2 = List.combine (List.map (fun v -> v.var_name_eff) l1) l2

(********************************************************************************)
(** The functions below accumulate 
   (1) the assertions
   (2) the new equations 
   (3) the fresh variables

The fix-point is performed on nodes.
*)

type acc = 
    Lic.val_exp srcflagged list      (* assertions *)
    * (Lic.eq_info srcflagged) list  (* equations *)
    * Lic.var_info list              (* new local vars *)

let (mk_fresh_loc : local_ctx -> var_info -> clock -> var_info) =
  fun lctx v c ->
    new_var (Ident.to_string v.var_name_eff) lctx v.var_type_eff (fst v.var_clock_eff, c)
      
(* When expanding a node call such as 

    x = toto(a when c);

   when toto params are (for example) on the base clock, we need to
   propagate the substitution between the toto base clock and "on(c)"
   ; for the toto arguments, it's been done during clock checking ;
   but we need to remember this information to substitute the clock
   of toto in its local variables.
*)
type clock_substs = (clock * clock) list
    
let (add_clock_subst: clock -> clock -> clock_substs -> clock_substs) =
  fun c1 c2 cs -> 
    if List.mem_assoc c1 cs then cs else (c1,c2)::cs

let (mk_input_subst: local_ctx -> Lxm.t -> var_info list -> 
     Lic.val_exp list -> acc -> subst * acc * clock_substs) = 
  fun lctx lxm vl vel acc -> 
    assert(List.length vl = List.length vel);
    List.fold_left2
      (fun (s,(a_acc,e_acc,v_acc),cs) v ve ->
        (* we create a new var for each node argument, which is a little
           bit  bourrin  if ever ve is a simple ident... *)
        let clk = match ve.ve_clk with
          | [c] ->  c
          | _ -> assert false
        in
        let nv = mk_fresh_loc lctx v clk in
        let neq = [LeftVarLic(nv,lxm)],ve in
        let neq = flagit neq lxm in
        let cs = add_clock_subst (snd v.var_clock_eff) clk cs in 
        (v.var_name_eff,nv)::s,(a_acc, neq::e_acc, nv::v_acc), cs
      )
      ([],acc,[])
      vl
      vel

(* create fresh vars if necessary *)
let (mk_output_subst : local_ctx -> Lxm.t -> var_info list -> Lic.left list -> clock_substs -> 
     acc -> subst * acc * clock_substs) = 
  fun lctx lxm vl leftl cs acc ->
    assert(List.length vl = List.length leftl);
    List.fold_left2
      (fun (s,acc,cs) v left -> 
        match left with
          | LeftVarLic(v2,lxm) -> (v.var_name_eff,v2)::s, acc,cs
          | _ -> 
            let clk = Lic.clock_of_left left in
            let nv = mk_fresh_loc lctx v clk in
            let nv_id = nv.var_name_eff in
	         let nve = {
              ve_core = CallByPosLic({it=VAR_REF nv_id;src = lxm },[]);
              ve_typ = [nv.var_type_eff];
              ve_clk = [snd nv.var_clock_eff]
            }
            in
            let neq = [left], nve in
            let neq = flagit neq lxm in
            (* for equations of the form 
               x.field = n(...);
               we create 
               - a fresh var "_v" 
               - define the equation "x.field = _v;"
               - create the substition n_output_par/_v
            *)
            let (aa,ae,av) = acc in
            let cs = add_clock_subst (snd v.var_clock_eff) clk cs in 
            (v.var_name_eff,nv)::s, (aa, neq::ae, nv::av), cs
      )
      ([],acc,cs)
      vl 
      leftl

let rec (expand_eq : local_ctx * acc -> Lic.eq_info Lxm.srcflagged -> local_ctx * acc) =
  fun (lctx, (asserts, eqs, locs)) { src = lxm_eq ; it = eq } ->
    match expand_eq_aux lctx eq with
      | lctx, None -> lctx, (asserts, { src = lxm_eq ; it = eq }::eqs, locs)
      | lctx, Some(nasserts, neqs, nlocs) -> 
        (lctx,
         (List.rev_append nasserts asserts, 
          List.rev_append neqs eqs, 
          List.rev_append nlocs locs))

and (expand_eq_aux: local_ctx -> Lic.eq_info -> local_ctx * acc option)=
  fun lctx (lhs,ve) -> 
    match ve.ve_core with
      | CallByPosLic( { it = Lic.CALL node_key ; src = lxm }, vel) ->
        let lctx, node = 
          match LicPrg.find_node lctx.curr_prg node_key.it with 
            | Some node -> lctx, node
            | None -> (* node has not been expanded yet: fix point! *)
              let raw_node =
                match LicPrg.find_node lctx.init_prg node_key.it with 
                  | Some n -> n
                  | None ->
                    prerr_string (
                      "*** "^ (LicDump.string_of_node_key_rec false node_key.it) ^" not defined.\n" ^
                        "*** Defined nodes are:"^ 
                        (String.concat ",\n"  
                           (List.map (fun (nk,_) -> "\""^LicDump.string_of_node_key_rec false nk^"\"")
                              (LicPrg.list_nodes lctx.init_prg)))
                    );
                    flush stderr;
                    assert false 
              in
              expand_node lctx raw_node 
        in
        let node = flagit node lxm in
        let node = match node.it.def_eff with
          | AbstractLic (Some n) ->  { it = n ; src = lxm }
          | _  -> node
        in            
        if 
          let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in
          (List.mem nname lctx.nodes)
        then
          lctx, None
        else
          (match get_node_body lctx node.it with
            | None -> lctx, None
            | Some node_body ->
              let node_eqs = node_body.eqs_eff
              and asserts = node_body.asserts_eff in
              let node = node.it in
              let node_locs = get_locals node in
              let acc = [],[],[] in
              let is,acc,cs = mk_input_subst lctx lxm node.inlist_eff vel acc in
              let os,acc,cs = mk_output_subst lctx lxm node.outlist_eff lhs cs acc in
              let rec (substitute_clock : clock -> clock) = 
                fun c -> 
                  try List.assoc c cs
                  with Not_found ->
                    match c with
                      | BaseLic
                      | ClockVar _ -> c (* XXX should/can it happen? *)
                      | On(v,clk) -> On(v, substitute_clock clk)
              in
              let clks = List.map (fun v -> substitute_clock (snd v.var_clock_eff)) node_locs in
              let fresh_locs = List.map2 (mk_fresh_loc lctx) node_locs clks in
              let ls = mk_loc_subst node_locs fresh_locs in
              let s = List.rev_append is (List.rev_append os ls) in
              let fresh_locs = (* substitute the new vars in clocks *)
                List.map (fun v -> 
                  let id,clk = v.var_clock_eff in
                  { v with var_clock_eff = id, subst_in_clock s clk }) 
                  fresh_locs
              in
              let node_eqs = List.map (substitute s) node_eqs in
              let subst_assert x = Lxm.flagit (subst_in_val_exp s x.it) x.src in
              let asserts = List.map subst_assert asserts in              
              let acc = match acc with (a,b,c) ->  (a@asserts,b@node_eqs,c@fresh_locs) in
              lctx, Some acc
          )
      | CallByPosLic (_, _)
      | Merge (_, _) 
      | CallByNameLic (_, _) -> lctx, None

and (expand_assert : local_ctx * acc -> val_exp srcflagged -> local_ctx * acc) =
  fun (lctx, (a_acc,e_acc,v_acc)) ve -> 
    let lxm = ve.src in
    let ve = ve.it in
    let clk = Ident.of_string "dummy_expand_assert", BaseLic in
    let assert_var = new_var "assert" lctx Bool_type_eff clk in
    let assert_eq = Lxm.flagit ([LeftVarLic(assert_var,lxm)], ve) lxm in
    let assert_op = Lic.VAR_REF(assert_var.var_name_eff) in
    let nve = { 
      ve_core = CallByPosLic((Lxm.flagit assert_op lxm, []));
      ve_typ = [Bool_type_eff];
      ve_clk = [BaseLic]
    }
    in
    expand_eq (lctx, ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc)) assert_eq

and (expand_node : local_ctx -> Lic.node_exp -> local_ctx * Lic.node_exp) =
  fun lctx n ->
    match LicPrg.find_node lctx.curr_prg n.node_key_eff with 
      | Some n -> lctx, n
      | None ->
        let lctx, exp_node =
          match n.def_eff with
            | ExternLic 
            | AbstractLic _ -> lctx, n
            | BodyLic b -> 
              let locs = get_locals n in
              let lctx,acc = List.fold_left expand_eq (lctx, ([],[],locs)) b.eqs_eff in
              let lctx,acc = List.fold_left expand_assert (lctx, acc) b.asserts_eff in
              let (asserts,neqs, nv) = acc in
              let nb = {
                eqs_eff = neqs ; 
                asserts_eff = asserts
              } 
              in
              let res =
                { n with 
                  loclist_eff = Some nv;
                  def_eff = BodyLic nb
                }
              in
              Verbose.exe ~flag:dbg (fun () ->
                Printf.printf "#DBG: expand nodes of '%s'\n" (Lic.string_of_node_key n.node_key_eff));
              lctx, res
            | MetaOpLic -> lctx, n
        in
        { lctx with curr_prg = LicPrg.add_node n.node_key_eff exp_node lctx.curr_prg },
        exp_node

(* exported *)
let (doit : string list -> LicPrg.t -> LicPrg.t) =
  fun nodes 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
    let lctx_init = {
      init_prg = inprg;
      curr_prg = outprg;
      nodes = nodes;
    }
    in
    (** transform nodes *)
    let rec (do_node : Lic.node_key -> Lic.node_exp -> local_ctx -> local_ctx) = 
      fun nk ne lctx -> 
        fst (expand_node lctx ne)
    in
    let lctx = LicPrg.fold_nodes do_node inprg lctx_init in
    lctx.curr_prg