split.ml

(** Time-stamp: <modified the 25/08/2008 (at 10:18) by Erwan Jahier> *)


open Lxm
open CompiledData

(********************************************************************************)
(* stuff to create fresh var names. *)
let var_cpt = ref 0
let new_var type_eff clock_eff = 
  incr var_cpt; 
  { 
    var_name_eff   = Ident.of_string ("_v" ^ (string_of_int !var_cpt));
    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;
  }
    
let init_var () = 
  var_cpt := 0


(********************************************************************************)
(* The functions below accumulate 
   (1) the new equations 
   (2) the fresh variables. 
*)
type split_acc = (eq_info_eff srcflagged) list * var_info_eff list

let rec (split_eq : split_acc -> eq_info_eff srcflagged -> split_acc) =
  fun (eqs, locs) eq -> 
    let (neqs, nlocs) = split_eq_do eq in 
      (eqs@neqs, locs@nlocs)

and (split_eq_do : eq_info_eff Lxm.srcflagged -> split_acc) =
  fun { src = lxm ; it = (lhs, rhs) } -> 
    let n_rhs, (neqs, nlocs) = split_val_exp true rhs in
      { src = lxm ; it = (lhs, n_rhs) }::neqs, nlocs

and (split_val_exp : bool -> val_exp_eff -> val_exp_eff * split_acc) =
  fun top_level ve -> 
    match ve with
      | CallByPosEff({it= IDENT_eff _}, _) 
      | CallByPosEff({it=CONST_eff _}, _) 
      | CallByPosEff({it=Predef_eff(Predef.TRUE_n,_)}, _) 
      | CallByPosEff({it=Predef_eff(Predef.FALSE_n,_)}, _) 
      | CallByPosEff({it=Predef_eff(Predef.ICONST_n _,_)}, _) 
      | CallByPosEff({it=Predef_eff(Predef.RCONST_n _,_)}, _) 
          (* We do not create an intermediary variable for those *)
        -> ve, ([],[])

      | CallByNameEff (_by_name_op_eff, _fl) ->  
          ve, ([],[]) (* but what about that one ??? *)

      | CallByPosEff(by_pos_op_eff, OperEff vel) ->
          (* recursively split the arguments *) 
          let lxm = by_pos_op_eff.src in
          let (rhs, vel, (eql,vl)) =
            match by_pos_op_eff.it with 
              | WITH_eff(ve) -> 
                  let ve, (eql, vl) = split_val_exp false ve in
                  let by_pos_op_eff = Lxm.flagit (WITH_eff(ve)) lxm in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
                    rhs, [ve], (eql, vl)

              | HAT_eff (i,ve) ->
                  let ve, (eql, vl) = split_val_exp false ve in
                  let by_pos_op_eff = Lxm.flagit (HAT_eff(i, ve)) lxm in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
                    rhs, [ve], (eql, vl)

              | _ -> 
                  let vel, (eql, vl) = split_val_exp_list false vel in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
                    rhs, vel, (eql, vl)
          in
            if top_level then 
              CallByPosEff(by_pos_op_eff, OperEff vel), (eql, vl) 
            else
              (* create the var for the current call *)
              let clk_l = EvalClock.val_exp_eff ve in
              let typ_l = EvalType.val_exp_eff ve in 
              let nv_l = List.map2 new_var typ_l clk_l in

              let nve = match nv_l with
                | [nv] -> CallByPosEff(
                    Lxm.flagit (IDENT_eff (Ident.to_idref nv.var_name_eff)) lxm,
                    OperEff []
                  )
                | _ -> CallByPosEff(
                    Lxm.flagit TUPLE_eff lxm, 
                    OperEff
                      (List.map (
                         fun nv -> 
                           CallByPosEff 
                             (Lxm.flagit 
                                (IDENT_eff (Ident.to_idref nv.var_name_eff)) lxm, 
                              OperEff []
                             ))
                         nv_l
                      )
                  )
              in
              let lpl = List.map (fun nv -> LeftVarEff(nv, lxm)) nv_l in

              let eq = Lxm.flagit (lpl, rhs) lxm in
                nve, (eql@[eq], vl@nv_l)
                  

and (split_val_exp_list : bool -> val_exp_eff list -> val_exp_eff list * split_acc) =
  fun top_level vel ->     
    let vel, accl = List.split (List.map (split_val_exp top_level) vel) in
    let eqll,vll = List.split accl in
    let eql, vl = List.flatten eqll, List.flatten vll in
      (vel,(eql,vl))

(* exported *)
let (node : CompiledData.node_exp_eff -> CompiledData.node_exp_eff) =
  fun n ->
    match n.def_eff with
      | ExternEff 
      | AbstractEff -> n
      | BodyEff b -> 
          init_var ();
          let loc = match n.loclist_eff with None -> [] | Some l -> l in
          let (neqs, nv) = List.fold_left split_eq ([], loc) b.eqs_eff in
          let asserts = List.map (fun x -> x.it) b.asserts_eff in
          let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in
          let nasserts,(neqs_asserts,nv_asserts) = split_val_exp_list true asserts in
          let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in
          let (neqs, nv) =  (neqs@neqs_asserts, nv@nv_asserts) in
          let nb = { eqs_eff = neqs ; asserts_eff = nasserts } in
          let res =
            { n with 
                loclist_eff = Some nv;
                def_eff = BodyEff nb
            }
          in
            res