nodesExpand.ml

(** Time-stamp: <modified the 11/03/2009 (at 16:41) by Erwan Jahier> *)

(** 
   nb : only user nodes are expanded.

   Expand nodes:
   ------------

   if n is a node defined as follows

     node n(x,y) returns(a,b);
     var v1,v2;
     let
       v1 = x+y;
       v2 = x*y;
       a = v1*x;
       b = v2*y;
     tel
   
   equations such as :

      o1,o2 = n(i1, i2);

   becomes
   
       h1 = i1+i2;
       h2 = i1*i2;
       o1 = h1*i1;
       o2 = h2*i2;
     
   where h1 and h2 are fresh local vars

   In other terms, we need to 
   - create a fresh local var for each local var of n
   - take all the equations of n, and substitute
      - the inputs parameters by intput args
      - the outputs parameters by lhs list
      - the local vars by the fresh local var names


  nb : to simplify, for equations like

      f.a = n(t[1], 3);
   
    we first create fresh vars for "f.a", "t[1]", and "3"

      _v1 = t[1];
      _v2 = 3;
      f.a = _v3;
      _v3 = n(_v1,_v2);
   
    and then we apply the transformation

   Expand assertions:
   -----------------

   In order to deal with assertions on nodes, i.e., of the form

     assert (n(i1,i2));

   we first transform it into
   
     assert_var = n(i1,i2);
     assert(assert_var);

   where assert_var is a fresh bool local var, and we apply the transformation
   on the first equation.
 *)

open Lxm
open Eff
open Predef
    
(********************************************************************************)
        
(* stuff to create fresh var names. 
   XXX code dupl. with Split.new_var 
*)
let new_var str node_env type_eff clock_eff = 
  let id = Ident.of_string (Name.new_local_var str) in
(*   let id = Ident.of_string (Name.new_local_var "h") in *)
  let var =
    { 
      var_name_eff   = id;
      var_nature_eff = SyntaxTreeCore.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
    Hashtbl.add node_env.lenv_vars id var;
    var

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

let (get_node_body : Eff.local_env -> Eff.node_exp -> Eff.node_body option) =
  fun node_env node ->
    match node.def_eff with
      | ExternEff
      | AbstractEff -> None
      | BodyEff node_body -> Some node_body
          

(********************************************************************************)
type subst = (var_info * var_info) list 
let rec (substitute : 
           subst -> Eff.eq_info Lxm.srcflagged -> Eff.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
      EvalClock.copy newve ve;
      { it = (lhs,newve) ; src = lxm }

and subst_in_left s left =
  match left with
    | LeftVarEff(v,lxm) -> (try LeftVarEff(List.assoc v s,lxm) with Not_found -> left)
    | LeftFieldEff(left,id,t) -> LeftFieldEff(subst_in_left s left,id,t)
    | LeftArrayEff(left,i, t) -> LeftArrayEff(subst_in_left s left,i, t)
    | LeftSliceEff(left,si,t) -> LeftSliceEff(subst_in_left s left,si,t)

and (subst_in_val_exp : subst -> val_exp -> val_exp) =
  fun s ve -> 
    let newve = {
      ve with core =
        match ve.core with
	  | CallByPosEff (by_pos_op, OperEff 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
		  
                | IDENT idref -> 
                    let idref =
                      try
                        let id = Ident.of_idref idref in
                        let var = snd(List.find (fun (v,_) -> v.var_name_eff = id) s) in
                        let idref = Ident.to_idref var.var_name_eff in
			  idref
                      with Not_found -> idref
                    in
                      IDENT idref
                        
                | WITH(ve) -> WITH(subst_in_val_exp s ve)
                | HAT(i,ve) -> HAT(i, subst_in_val_exp s ve)
                | ARRAY(vel) -> ARRAY(List.map (subst_in_val_exp s) vel)
                | WHEN(SyntaxTreeCore.Base) ->  WHEN(SyntaxTreeCore.Base)
                | WHEN(SyntaxTreeCore.NamedClock {src=lxm;it=(cc,cv)}) -> 
                    let var = snd(List.find (fun (v,_) -> v.var_name_eff = cv) s) in
                    let cv = var.var_name_eff in
                      WHEN(SyntaxTreeCore.NamedClock  {src=lxm;it=(cc,cv)})
                | Predef _| CALL _ | PRE | ARROW | FBY | CURRENT  | TUPLE
                | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _  | MERGE _ 
                      (*               | CONST _ *)
                    -> by_pos_op
              in
                CallByPosEff(Lxm.flagit by_pos_op lxm, OperEff vel)
		  
	  | CallByNameEff(by_name_op, fl) ->
              let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in
                CallByNameEff(by_name_op, fl) 
    }
    in
      EvalClock.copy newve ve;
      newve

let mk_loc_subst = List.combine

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

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

let (mk_fresh_loc : Eff.local_env -> var_info -> var_info) =
  fun node_env v -> 
    new_var (Ident.to_string v.var_name_eff) node_env v.var_type_eff v.var_clock_eff  
      
let (mk_input_subst: Eff.local_env -> Lxm.t -> var_info list -> 
      Eff.val_exp list -> acc -> subst * acc) = 
  fun node_env lxm vl vel acc -> 
    List.fold_left2
      (fun (s,(a_acc,e_acc,v_acc)) 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 nv = mk_fresh_loc node_env v in
         let neq = [LeftVarEff(nv,lxm)],ve in
         let neq = flagit neq lxm in
           (v,nv)::s,(a_acc, neq::e_acc, nv::v_acc)
      )
      ([],acc)
      vl
      vel

(* create fresh vars if necessary *)
let (mk_output_subst : Eff.local_env -> Lxm.t -> var_info list -> Eff.left list -> 
      acc -> subst * acc) = 
  fun node_env lxm vl leftl acc ->
    List.fold_left2
      (fun (s,acc) v left -> 
         match left with
           | LeftVarEff(v2,lxm) -> (v,v2)::s, acc
           | _ -> 
               let nv = mk_fresh_loc node_env v in
               let nv_idref = Ident.to_idref nv.var_name_eff in
	       let nve = {
                 core = CallByPosEff({it=IDENT nv_idref;src = lxm },OperEff []);
                 typ = [nv.var_type_eff]
               }
               in
               let neq = 
		 EvalClock.add nve [nv.var_clock_eff];		 
                 [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
                 (v,nv)::s, (aa, neq::ae, nv::av)
      )
      ([],acc)
      vl 
      leftl

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

and (expand_eq_aux: Eff.local_env -> Eff.eq_info -> acc option)=
  fun node_env (lhs,ve) -> 
    match ve.core with
      | CallByPosEff( { it = Eff.CALL node ; src = lxm }, OperEff vel) ->
          if 
            let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in
            (List.mem nname !Global.dont_expand_nodes)
          then
            None
          else
            (match get_node_body node_env node.it with
               | None -> 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 fresh_locs = List.map (mk_fresh_loc node_env) node_locs in
                   let acc = [],[],fresh_locs in
                   let is,acc = mk_input_subst node_env lxm node.inlist_eff vel acc in
                   let os,acc = mk_output_subst node_env lxm node.outlist_eff lhs acc in
                   let ls = mk_loc_subst node_locs fresh_locs in
                   let s = List.rev_append is (List.rev_append os ls) 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 = List.fold_left (expand_eq node_env) acc node_eqs in
                   let acc = List.fold_left (expand_assert node_env) acc asserts in
                     Some acc
            )
      | CallByPosEff (_, _)
      | CallByNameEff (_, _) -> None


and (expand_assert : Eff.local_env -> acc -> val_exp srcflagged -> acc) =
  fun n_env (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", BaseEff in
    let assert_var = new_var "assert" n_env Bool_type_eff clk in
    let assert_eq = Lxm.flagit ([LeftVarEff(assert_var,lxm)], ve) lxm in
    let assert_op = Eff.IDENT(Ident.to_idref assert_var.var_name_eff) in
    let nve = { 
      core = CallByPosEff((Lxm.flagit assert_op lxm, OperEff []));
      typ = [Bool_type_eff]
    }
    in
      EvalClock.copy nve ve;
      expand_eq n_env ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc) assert_eq


(* exported *)
let (f : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
  fun n_env n ->
    match n.def_eff with
      | ExternEff 
      | AbstractEff -> n
      | BodyEff b -> 
          let locs = get_locals n in
          let acc = List.fold_left (expand_eq n_env) ([],[],locs) b.eqs_eff in
          let acc = List.fold_left (expand_assert n_env) 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 = BodyEff nb
            }
          in
            res