doSplit.ml

(*
Source 2 source transformation :

1 opérateur par équation

Réutilise ~ texto le Split d'R1

CONDITION :
- après DoNoPoly (et DoAliasType ?)
*)

open Lxm
open Eff

let dbg=Some (Verbose.get_flag "split")

(********************************************************************************)
let new_var getid type_eff clock_eff = 
  let id = getid "v" 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  = id,clock_eff;
    } in
    var

(********************************************************************************)
(* functions that deal with tuple breaking *)
let rec (get_vel_from_tuple : val_exp -> val_exp list) =
  function
    | { ve_core = CallByPosEff({it=Eff.TUPLE }, OperEff vel) } -> 
        List.flatten (List.map get_vel_from_tuple vel)
    | ve -> [ve]

let to_be_broken = function
    (* We are only interested in operators that can deal with tuples! *)
  | CallByPosEff({ it = Eff.ARROW }, _) -> true
  | CallByPosEff({ it = Eff.FBY }, _) -> true
  | CallByPosEff({ it = Eff.PRE }, _) -> true
  | CallByPosEff({ it = Eff.CURRENT }, _) -> true
  | CallByPosEff({ it = Eff.TUPLE }, _) -> true
  | CallByPosEff({ it = Eff.WHEN _ }, _) -> true
  | CallByPosEff({ it = Eff.PREDEF_CALL(Predef.IF_n, []) }, _) -> true
  | _ -> false


let (break_it : val_exp -> val_exp list) =
  fun ve -> 
    let nvel = 
      match ve.ve_core with
	| CallByPosEff({it=Eff.PREDEF_CALL(Predef.IF_n,[]);src=lxm}, OperEff [c;ve1;ve2]) ->
            let vel1 = get_vel_from_tuple ve1
            and vel2 = get_vel_from_tuple ve2 
            in
              List.map2
		(fun ve1 ve2 -> 
		   { ve_core = 
                       CallByPosEff({it=Eff.PREDEF_CALL(Predef.IF_n,[]);src=lxm}, 
                                    OperEff [c;ve1;ve2]);
                     ve_typ = ve1.ve_typ;
                     ve_clk = ve1.ve_clk;
                   }
		)
		vel1
		vel2

	| CallByPosEff({it=WHEN clk; src=lxm}, OperEff vel) ->
            let vel = List.flatten (List.map get_vel_from_tuple vel) in
              List.map 
		(fun ve -> 
                   { ve with 
                       ve_core=CallByPosEff({it=WHEN clk ; src=lxm }, OperEff [ve])}) 
		vel

	| CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff vel) ->
            let vel = List.flatten (List.map get_vel_from_tuple vel) in
              List.map 
		(fun ve -> 
                   { ve with 
                       ve_core=CallByPosEff({it=Eff.TUPLE ; src=lxm }, OperEff [ve])}) 
		vel

	| CallByPosEff({it=op ; src=lxm }, OperEff [ve]) ->
            let vel = get_vel_from_tuple ve in
              List.map 
                (fun ve -> { ve with ve_core=CallByPosEff({it=op;src=lxm}, OperEff [ve])})
                vel

	| CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]) ->
            let vel1 = get_vel_from_tuple ve1
            and vel2 = get_vel_from_tuple ve2 
            in
              List.map2
		(fun ve1 ve2 -> 
		   { ve_core = CallByPosEff({it=op ; src=lxm }, OperEff [ve1;ve2]);
                     ve_typ = ve1.ve_typ;
                     ve_clk = ve1.ve_clk }
		)
		vel1
		vel2
		
	| _ -> assert false (* dead code since it is guarded by to_be_broken... *)
    in
    let tl = ve.ve_typ
    and cl = ve.ve_clk in
    let nvel = List.map2 (fun nve t -> { nve with ve_typ = [t]; ve_clk=cl } ) nvel ve.ve_typ in
      assert(ve.ve_typ = tl);
      nvel

let (split_tuples:Eff.eq_info Lxm.srcflagged list -> Eff.eq_info Lxm.srcflagged list) =
  fun eql -> 
    let split_one_eq eq = 
      let { src = lxm_eq ; it = (lhs, n_rhs) } = eq in
        if List.length lhs > 1 && (to_be_broken n_rhs.ve_core) then
          let vel = break_it n_rhs in
          let eqs = 
            try List.map2 (fun lhs ve -> [lhs], ve) lhs vel 
            with _ -> 
              assert false
          in
          let eqs = List.map (fun eq -> Lxm.flagit eq lxm_eq) eqs in
            eqs
        else
          [eq]

    in
      List.flatten (List.map split_one_eq eql)

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

(* exported *)
let rec (eq : LicPrg.id_generator -> Eff.eq_info Lxm.srcflagged -> split_acc) =
  fun getid { src = lxm_eq ; it = (lhs, rhs) } ->
    let n_rhs, (neqs, nlocs) = split_val_exp false true getid rhs in
      { src = lxm_eq ; it = (lhs, n_rhs) }::neqs, nlocs

and (split_eq_acc : 
       LicPrg.id_generator -> split_acc -> Eff.eq_info srcflagged -> split_acc) =
  fun getid (eqs, locs) equation -> 
    let (neqs, nlocs) = eq getid equation in 
      (split_tuples (eqs@neqs), locs@nlocs)
        
and (split_val_exp : bool -> bool -> LicPrg.id_generator -> Eff.val_exp -> 
      Eff.val_exp * split_acc) =
  fun when_flag top_level getid ve -> 
    (* [when_flag] is true is the call is made from a "when" statement.
       We need this flag in order to know if it is necessary to add
       a when on constants. Indeed, in Lustre V6, it is not necessary
       to write " 1 when clk + x " if x in on clk (it's more sweet). 
       So we need to add it  (because if we split "1+1+x", then it
       is hard to know the "1" are on the clock of x ; moreover, lustre
       v4 (and the other backends) cannot infer such clock).

       But is is not forbidden either! so we need to make sure that there
       is no "when"...
    *)
    match ve.ve_core with
      | CallByPosEff({it=Eff.VAR_REF _}, _) -> ve, ([],[])
      | CallByPosEff({it=Eff.CONST_REF _}, _) -> ve, ([],[])

      | CallByPosEff({src=lxm;it=Eff.PREDEF_CALL(Predef.TRUE_n,_)}, _) 
      | CallByPosEff({src=lxm;it=Eff.PREDEF_CALL(Predef.FALSE_n,_)}, _) 
      | CallByPosEff({src=lxm;it=Eff.PREDEF_CALL(Predef.ICONST_n _,_)}, _) 
      | CallByPosEff({src=lxm;it=Eff.PREDEF_CALL(Predef.RCONST_n _,_)}, _) 
          (* We do not create an intermediary variable for those, 
             but 
          *)
        -> if not when_flag then
          let clk = ve.ve_clk in
            match (List.hd clk) with
              | On(clock,_) -> 
                  let clk_exp = SyntaxTreeCore.NamedClock (Lxm.flagit clock lxm) in
                    { ve with ve_core = 
                        CallByPosEff({src=lxm;it=Eff.WHEN clk_exp},OperEff [ve])},
                  ([],[])
                    
              | (ClockVar _) (* should not occur *)
              | BaseEff  -> ve, ([],[])
        else
          ve, ([],[])

      | CallByNameEff (by_name_op_eff, fl) ->
          let lxm = by_name_op_eff.src in 
          let fl, eql, vl = 
            List.fold_left
              (fun (fl_acc, eql_acc, vl_acc) (fn, fv) ->
                 let fv, (eql, vl) = split_val_exp false false getid fv in
                   ((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc)
              )
              ([],[],[])
              fl
          in
          let rhs = { ve with ve_core = CallByNameEff (by_name_op_eff, List.rev fl) } in
	    if top_level then
              rhs, (eql, vl)
            else
              (* create the var for the current call *)
              let clk_l = ve.ve_clk in 
              let typ_l = ve.ve_typ in  
              let nv_l = List.map2 (new_var getid) typ_l clk_l  in
              let nve = match nv_l with
                | [nv] -> { ve with ve_core = 
                      CallByPosEff(
                        Lxm.flagit (Eff.VAR_REF (nv.var_name_eff)) lxm,
                        OperEff [] 
                      )}
                | _ -> assert false
              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)

                  
      | CallByPosEff(by_pos_op_eff, OperEff vel) -> (
          (* recursively split the arguments *) 
          let lxm = by_pos_op_eff.src in
          let (rhs, (eql,vl)) =
            match by_pos_op_eff.it with 
                (* for WITH and HAT, a particular treatment is done because
                   the val_exp is attached to them *)
              | Eff.WITH(ve) ->
                  let ve, (eql, vl) = split_val_exp false false getid ve in
                  let by_pos_op_eff = Lxm.flagit (Eff.WITH(ve)) lxm in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
                    rhs, (eql, vl)

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

              | Eff.WHEN ve -> (* should we create a var for the clock? *)
                  let vel,(eql, vl) = split_val_exp_list true false getid vel in
                  let by_pos_op_eff = Lxm.flagit (Eff.WHEN(ve)) lxm in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
                    rhs, (eql, vl)
                      
              | Eff.ARRAY vel ->
                  let vel, (eql, vl) = split_val_exp_list false false getid vel in
                  let by_pos_op_eff = Lxm.flagit (Eff.ARRAY(vel)) lxm in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
                    rhs, (eql, vl)
                      
              | _ -> 
                  let vel, (eql, vl) = split_val_exp_list false false getid vel in
                  let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
                    rhs, (eql, vl)
          in
          let rhs = { ve with ve_core = rhs } in
	    if top_level || by_pos_op_eff.it = TUPLE then 
              rhs, (eql, vl) 
            else
              (* create the var for the current call *)
              let clk_l = ve.ve_clk in 
              let typ_l = ve.ve_typ in
              let nv_l = List.map2 (new_var getid) typ_l clk_l  in

              let nve = 
                match nv_l with
                  | [nv] -> {
                      ve_typ = [nv.var_type_eff];
                      ve_clk = clk_l; 
                      ve_core = CallByPosEff(
                        Lxm.flagit (Eff.VAR_REF (nv.var_name_eff)) lxm,
                        OperEff [])		
	            }
                  | _ -> {
                      ve_typ = List.map (fun v -> v.var_type_eff) nv_l;
                      ve_clk = clk_l;
		      ve_core = CallByPosEff(
                        Lxm.flagit Eff.TUPLE lxm, 
                        OperEff
			  (List.map (
                             fun nv -> 
                               let nnv = {
                                 ve_core = CallByPosEff 
                                   (Lxm.flagit 
                                      (Eff.VAR_REF (nv.var_name_eff)) lxm,
				    OperEff []);
                                 ve_typ = [nv.var_type_eff];
                                 ve_clk = [snd nv.var_clock_eff]
                               }
			       in
			         nnv
			   )
                             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 -> 
      bool -> LicPrg.id_generator -> Eff.val_exp list -> Eff.val_exp list * split_acc) =
  fun when_flag top_level getid vel ->
    let vel, accl = 
      List.split (List.map (split_val_exp when_flag top_level getid) vel) 
    in
    let eqll,vll = List.split accl in
    let eql, vl = List.flatten eqll, List.flatten vll in
      (vel,(eql,vl))

(* exported *)
and split_node (getid: LicPrg.id_generator) (n: Eff.node_exp) : Eff.node_exp =
   Verbose.printf ~flag:dbg "*** Splitting node  %s\n"
      (LicDump.string_of_node_key_iter n.node_key_eff);
   let res = match n.def_eff with
   | ExternEff 
   | BuiltInEff _
   | AbstractEff None -> n
   | AbstractEff (Some pn) -> 
      { n with def_eff = AbstractEff (Some (split_node getid pn)) }
   | BodyEff b -> 
      let loc = match n.loclist_eff with None -> [] | Some l -> l in
      let (neqs, nv) = List.fold_left (split_eq_acc getid) ([], 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 false true getid 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
              { n with loclist_eff = Some nv; def_eff = BodyEff nb }
   in
   res

let rec doit (inprg : LicPrg.t) : LicPrg.t =
   (* n.b. on fait un minumum d'effet de bord pour
      pas avoir trop d'acummulateur ... *)
   let res = ref LicPrg.empty in

   (** TRAITE LES TYPES *)
   let do_type k (te:Eff.type_) =
      res := LicPrg.add_type k te !res
   in
   LicPrg.iter_types do_type inprg;

   (** TRAITE LES CONSTANTES *)
   let do_const k (ec: Eff.const) =
      res := LicPrg.add_const k ec !res
   in 
   LicPrg.iter_consts do_const inprg ;

   (** TRAITE LES NOEUDS : *)
   let rec do_node k (ne:Eff.node_exp) =
      (* On passe en parametre un constructeur de nouvelle variable locale *)
      let getid = LicPrg.fresh_var_id_generator inprg ne in
      let ne' = split_node getid ne in
      res := LicPrg.add_node k ne' !res
   in
   (*LET's GO *)
   LicPrg.iter_nodes do_node inprg;
   !res