l2lExpandArrays.ml

(** Time-stamp: <modified the 13/12/2012 (at 16:28) by Erwan Jahier> *)

(* Replace structures and arrays by as many variables as necessary.
   Since structures can be recursive, it migth be a lot of new variables...
   
   For instance, a variable
   v : Toto { f1 : int ; f2 : int ^ 3 ; f3 : t^2 }

   where
   type t = T { x:int ; y:int } 

   will be expanded into 

   _v_f1 : int;
   _v_f2_0 : int;
   _v_f2_1 : int;
   _v_f2_2 : int;
   _v_f3_1_x : int;
   _v_f3_1_y : int;
   _v_f3_2_x : int;
   _v_f3_3_y : int;

   nb : if 't' was a type that does not contain any struct type, we would just 
   have 3 variables.
  *)

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


(********************************************************************************)
        
        
(* 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 (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  = id, clock_eff;
    }
  in
    Hashtbl.add node_env.lenv_vars id var;
    var

(* returns a new var based on [vi] with type [type_eff]. *)
let clone_var node_env vi str type_eff = 
  let str = (Ident.to_string vi.var_name_eff) ^ str in
  let id = Ident.of_string (str) in
  let clk_id = Ident.of_string str in
  let type_eff = match type_eff with 
      TypeVar Any | TypeVar AnyNum -> 
        Errors.print_internal_error 
          "L2lExpandArrays.clone" "should not have been called for a any(num) var";
        assert false

    | _ -> type_eff
  in
  let var =
    { 
      var_name_eff   = id;
      var_nature_eff = vi.var_nature_eff;
      var_number_eff = vi.var_number_eff; (* this field is useless: to be removed. *)
      var_type_eff   = type_eff;
      var_clock_eff  = clk_id, snd vi.var_clock_eff;
    }
  in
    (*     Hashtbl.add node_env.lenv_vars id var; *)
  var


let rec (is_a_basic_type : Lic.type_ -> bool) =
  function
    | Array_type_eff _ | Struct_type_eff _ -> false
    | TypeVar Any | TypeVar AnyNum -> 
      Errors.print_internal_error 
        "L2lExpandArrays.is_a_basic_type" "should not have been called for a any(num) var";
      assert false
    | Abstract_type_eff(_, teff) -> is_a_basic_type teff 
    | External_type_eff(_) 
    | Enum_type_eff (_, _) 
    | Real_type_eff 
    | Int_type_eff 
    | Bool_type_eff  -> true

let soi = string_of_int


let (index_list_of_slice_info : Lic.slice_info -> int list) =
  fun si -> 
    let rec aux acc cpt =
      if ((si.se_step > 0 & cpt > si.se_last) || (si.se_step < 0 & cpt < si.se_last))
      then acc else aux (cpt::acc) (cpt + si.se_step)
    in
      List.rev (aux [] si.se_first)


(** left expr expansion.

  The objective is to generate the set of vars defined by a left expr.

  First step: var_trees_of_left recursively traverse the left structure 
  to compute the left expr variable. E.g., in the left expr "X.f2[4]" we 
  want to find "X" (and its type). 
  
  Second step: Using the type of X, we compute the set of variables defined 
  by "X" (gen_var_trees). The set is actually structured into a tree-like
  data struture var_tree (to be able to deal with slices).
  
  Third step (var_trees_of_left again): cut off some branches of the tree using
  the left filter ("f2[4]") to keep only the  variable effectivily defined 
  by the left expr (exercise for the reader: try to do the same with a flat data 
  type ; it's just a nigthmare because of slices).
  
  In other words: 
  - when we find a left leave, we generate all the possible names
  corresponding to that var, in a data structure (a tree) that reflect
  the lustre data structure (w.r.t. array and struct)
  - Then, struct or array accesses remove some branches of that tree
  
*)
(* var_trees are used to represent  left var_tree, and val_exp var_tree *)
type 'a var_tree = 
    A of 'a var_tree list  (* should i use an array there? *)
  | S of (Ident.t * 'a var_tree) list (* A Map.t ? *)
  | L of 'a
(* Quite similar to L2lCheckOutputs.var_def_state, which is logic. *)

let rec (flatten_var_tree : 'a var_tree -> 'a list) =
  function       
    | A array -> List.flatten (List.map flatten_var_tree array)
    | S fl -> List.flatten (List.map (fun (id,vt) -> flatten_var_tree vt) fl)
    | L str -> [str] 

let rec (gen_var_trees :
	        (string -> Lic.type_ -> 'a) -> string -> Lic.type_ -> 'a var_tree) =
  fun make_leave prefix teff ->
    let loop = gen_var_trees make_leave in
    match teff with
      | TypeVar Any | TypeVar AnyNum -> 
        Errors.print_internal_error
          "L2lExpandArrays.gen_var_trees" "should not have been called for a any(num) var";
        assert false
      | Bool_type_eff | Int_type_eff | Real_type_eff 
      | Enum_type_eff(_) | External_type_eff(_)
        -> 
        L (make_leave prefix teff)

      | Abstract_type_eff(_,teff) ->  loop prefix teff

      | Array_type_eff(teff_elt,i) ->
        let rec unfold acc cpt =
	       if cpt < 0 then acc else
            let prefix = prefix ^ "_" ^ (soi cpt) in
            let vt = loop prefix teff_elt in
            unfold (vt::acc) (cpt-1)
        in
	     A (unfold [] (i-1))
	       
      | Struct_type_eff(_, fl) ->
        S (List.map 
             (fun (fn, (steff, _const_opt)) ->
               let prefix = prefix^"_"^(Ident.to_string fn) in
		         (fn, loop prefix steff )
             ) 
             fl)

let (expand_left : Lic.local_env -> left -> left list) = 
  fun nenv left -> 
    let rec (var_trees_of_left : left -> left var_tree) =
      fun left -> 
        match left with
          | LeftVarLic (vi,lxm)   -> 
	      let make_left nenv lxm vi prefix teff =
		LeftVarLic (clone_var nenv vi prefix teff, lxm)
	      in
		gen_var_trees (make_left nenv lxm vi) "" vi.var_type_eff
          | LeftFieldLic (l,id,t) -> 
              (match var_trees_of_left l with
                 | S fl -> List.assoc id fl 
                 | A _ | L _  -> assert false
              )
          | LeftArrayLic (l,i,t)  ->
              (match var_trees_of_left l with
                 | A array -> List.nth array i
                 | S _ | L _ -> assert false
              )
          | LeftSliceLic (l,si,t) ->
              (match var_trees_of_left l with
                 | A array -> 
                     let index_list = index_list_of_slice_info si in
                     let l = List.map (fun i -> List.nth array i) index_list in
                       A l
                 | S _ | L _ -> assert false
              )
    in
    let vt = try var_trees_of_left left 
    with _ -> assert false
      (* should not occur: just a defense against nth and assoc *)
    in
      flatten_var_tree vt


	  
(********************************************************************************)

(** build a new loc that will alias ve, and add its definition in the 
  set of equations (cf acc) *)
let rec (make_new_loc : Lic.local_env -> Lic.id_solver -> Lxm.t -> acc -> 
         Lic.val_exp -> acc * var_info) =
  fun nenv id_solver lxm acc ve -> 
    let teff = List.hd ve.ve_typ in
    let ceff = List.hd ve.ve_clk in
    let nv = new_var "v" nenv teff ceff in
    let neq = [LeftVarLic(nv,lxm)], ve in
    let neq = flagit neq lxm in
    let nvl, (asserts,eqs,locs) = expand_var_info nenv id_solver ([],acc) nv in
    let acc = (asserts,eqs, List.rev_append nvl locs) in
    expand_eq nenv id_solver acc neq, nv

and (var_trees_of_val_exp : Lic.local_env -> Lic.id_solver -> acc -> Lic.val_exp
     -> acc * Lic.val_exp var_tree) =
  fun nenv id_solver acc ve -> 

    let make_val_exp nenv lxm vi prefix teff =
      let prefix = (Ident.to_string vi.var_name_eff) ^ prefix in
      let id = prefix in 
	   {
        ve_core = CallByPosLic({src=lxm;it=(VAR_REF id)}, OperLic []);
        ve_typ  = [vi.var_type_eff] ;
        ve_clk = [snd vi.var_clock_eff]
      }
    in
    let loop = var_trees_of_val_exp nenv id_solver acc in
    match ve.ve_core with
      | CallByPosLic (by_pos_op, OperLic vel) -> (
        let lxm = by_pos_op.src in
        let by_pos_op = by_pos_op.it in
        match by_pos_op with
          | STRUCT_ACCESS (id) -> (
            let ve = try List.hd vel with _ -> assert false in
            match loop ve with
              | acc, S fl -> acc, List.assoc id fl 
              | _, (A _ | L _)  -> assert false
		    )
          | ARRAY_ACCES (i) -> (
            let ve = try List.hd vel with _ -> assert false in
            match loop ve with
              | acc, A array -> acc, List.nth array i
              | _, (S _ | L _)  -> assert false
		          
          )
          | ARRAY_SLICE (si) -> (
            let ve = try List.hd vel with _ -> assert false in
            match loop ve with
              | acc, A array -> 
                let index_list = index_list_of_slice_info si in
                let l = List.map (fun i -> List.nth array i) index_list in
                acc, A l			         
              | _, (S _ | L _)  -> assert false
		    )
          | VAR_REF id -> (
            try
              let vi = UglyStuff.var_info_of_ident id_solver id lxm in
              (acc, gen_var_trees (make_val_exp nenv lxm vi) "" vi.var_type_eff)
            with _ ->  
              let msg = 
                "\n*** during Array expansion: '"^
                  (id)^
			         "': Unknown variable.\n"^
                  "*** Current variables are: "^
			         (Hashtbl.fold
                     (fun i v acc -> acc^(Printf.sprintf "\n\t%s" (Lic.string_of_var_info v)))
			            nenv.lenv_vars "")
              in
			     raise (Errors.Compile_error(lxm, msg))
          )
          | CONST_REF idl -> (
            try
              let const = UglyStuff.const_eff_of_item_key id_solver idl lxm in
              let s, ve_const = 
                UnifyClock.const_to_val_eff lxm true UnifyClock.empty_subst const
              in
              let ve_const,acc =
                match ve_const.ve_core with
                  | CallByPosLic ({it=CONST_REF _},_) ->  
                    (* in order to avoid a potential infinite loop *)
                    (ve_const, acc)
                      
                  | _ -> expand_val_exp nenv id_solver acc ve_const 
              in (acc, L (ve_const))
            with _ ->  
              let msg = 
                "\n*** during Array expansion: '"^
                  (Ident.string_of_long idl)^
                  "': Unknown variable.\n"^
                  "*** Current variables are: "^
                  (Hashtbl.fold
                     (fun i v acc -> acc^(Printf.sprintf "\n\t%s" (Lic.string_of_var_info v)))
                     nenv.lenv_vars "")
              in
              raise (Errors.Compile_error(lxm, msg))
          ) 
          | WITH(_) | HAT(_) | CONCAT | ARRAY(_) 
          | PREDEF_CALL _ | CALL _  | MERGE _ 
          | PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE -> (
            (* Create a new loc var to alias such expressions *)
            let acc, nloc = make_new_loc nenv id_solver lxm acc ve in
            acc, gen_var_trees (make_val_exp nenv lxm nloc) "" nloc.var_type_eff
          )
      )
      | CallByNameLic(by_name_op, fl) ->
	     let lxm = by_name_op.src in
        let acc, nloc = make_new_loc nenv id_solver lxm acc ve in
        acc, gen_var_trees (make_val_exp nenv lxm nloc) "" nloc.var_type_eff
	       
and (break_tuple : Lxm.t -> left list -> val_exp -> Lic.eq_info srcflagged list) =
  fun lxm left_list ve ->
    if not !Global.ec then
      [{ src = lxm ; it = (left_list, ve) }] 
    else
      (* we only need to break tuples in this mode ...
	      Note that this work only if the node expansion has already been done!
	      (otherwise, we would not have the same number of items in the left and 
	      in the rigth part)
      *)
      let rec aux ve = (* flatten val exp*)
	     match ve.ve_core with 
	       | CallByPosLic ({it= TUPLE}, OperLic vel) -> List.flatten (List.map aux vel)
	       | CallByPosLic (unop, OperLic [ve1]) ->
	         let ve1l = aux ve1 in
		      List.map
		        (fun ve1 -> { ve1 with ve_core = CallByPosLic (unop, OperLic [ve1])} ) 
		        ve1l 
	       | CallByPosLic (binop, OperLic [ve1;ve2]) ->
	         let ve1l, ve2l = aux ve1, aux ve2 in
		      if (List.length ve1l <> List.length ve2l) then
		        let vel2str vel = 
		          (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel))
		        in
		        let msg =
                "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^ 
		            "\n cannot be broken \n" ^(vel2str ve1l) ^ 
		            " should have the same arity as\n"^(vel2str ve2l) ^ "\n"
		        in
		        raise (Errors.Compile_error(lxm, msg)) 
		      else
		        List.map2 
		          (fun ve1 ve2 -> 
                  { ve with ve_core = CallByPosLic (binop, OperLic [ve1;ve2])})
		          ve1l 
		          ve2l
		          
	       | CallByPosLic ({it= PREDEF_CALL(IF_n,[]); src=lxm}, OperLic [cond; ve1; ve2]) ->
            
	         let ve1l, ve2l = aux ve1, aux ve2 in
		      if (List.length ve1l <> List.length ve2l) then
		        let vel2str vel = 
		          (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel))
		        in
		        let msg = 
                "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^ 
		            "\n cannot be broken \n" ^(vel2str ve1l) ^ 
		            " should have the same arity as\n"^(vel2str ve2l) ^ "\n"
		        in
		        raise (Errors.Compile_error(lxm, msg)) 
		      else
		        List.map2 
		          (fun ve1 ve2 -> 
                  { ve with ve_core = 
                      CallByPosLic ({it= PREDEF_CALL(IF_n,[]); src=lxm}, 
                                    OperLic [cond;ve1;ve2])}
                ) 
		          ve1l 
		          ve2l

	       |  _ -> [ve]
      in
      let vel = aux ve in
	   if (List.length vel <> List.length left_list) then
	     (* migth occur for generic nodes, that needs to be compiled,
	        but that will not be dumped. *)
	     [{ src = lxm ; it = (left_list, ve) }] 
	   else
	     List.map2
	       (fun l ve -> 
            let clk = [snd (Lic.var_info_of_left l).var_clock_eff] in
	         { src = lxm ; 
              it = ([l], { ve with ve_typ = [Lic.type_of_left l] ; ve_clk = clk}) }
	       )
	       left_list
	       vel

and (expand_eq :
       Lic.local_env -> Lic.id_solver -> acc -> Lic.eq_info srcflagged -> acc) =
  fun nenv id_solver acc eqf -> 
    let { src = lxm_eq ; it = (left_list, ve) } = eqf in
    let left_list = List.flatten (List.map (expand_left nenv) left_list) in
    let ve,acc = expand_val_exp nenv id_solver acc ve in
    let eq_list = break_tuple lxm_eq left_list ve in    
    let (asserts, eqs, locs) = acc in
    (asserts,  eq_list@eqs, locs)

and expand_val_exp_list n_env id_solver acc vel = 
  List.fold_left 
    (fun (vel,acc) ve -> 
      let ve,acc = expand_val_exp n_env id_solver acc ve in
      ve::vel, acc
    ) 
    ([],acc) (List.rev vel)

and (expand_val_exp: Lic.local_env -> Lic.id_solver -> acc -> val_exp -> 
     val_exp * acc) =
  fun n_env id_solver acc ve ->
    match ve.ve_core with
      | CallByPosLic (by_pos_op, OperLic vel) -> 
        let lxm = by_pos_op.src in
        let by_pos_op = by_pos_op.it in
        let by_pos_op, acc, vel = 
	       match by_pos_op with
            | WITH(ve) -> 
              let ve, acc = expand_val_exp n_env id_solver acc ve in
              let vel,acc = expand_val_exp_list n_env id_solver acc vel in
              WITH(ve), acc, vel
            | HAT(i,ve) ->
              let ve, acc = expand_val_exp n_env id_solver acc ve in
              let rec unfold cpt =
                if cpt = 0 then [] else ve::(unfold (cpt-1))
              in
              TUPLE, acc, unfold i
            | ARRAY(vel) ->
              let vel,acc = expand_val_exp_list n_env id_solver acc vel in
              TUPLE, acc, vel
		          
            | CONCAT | PREDEF_CALL _ | CALL _  | MERGE _
            | PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE 
              -> 
              let vel,acc = expand_val_exp_list n_env id_solver acc vel in
              by_pos_op, acc, vel
		          
            | STRUCT_ACCESS (_)
            | ARRAY_ACCES (_)
            | ARRAY_SLICE (_) 
            | VAR_REF _ 
            | CONST_REF _ ->
		        let acc, vt = try var_trees_of_val_exp n_env id_solver acc ve 
		          with (Not_found | Failure _) -> 
                  assert false (* just a defense against nth and assoc *)
		        in
              TUPLE, acc, flatten_var_tree vt
                
	     in
	     let newve = CallByPosLic(Lxm.flagit by_pos_op lxm, OperLic vel) in
        let newve =  { ve with ve_core = newve } in
        (* 	    if newve.core <> ve.core then ( *)
        (*               EvalClock.copy newve ve *)
        (*             ); *)
        newve, acc
          
      | CallByNameLic(by_name_op, fl_val) ->
	     (* we want to print fields in the order of the type.
	        Moreover, we have to deal with default value.
	     *)
	     let teff = ve.ve_typ in 
	     match teff with 
	       | [Struct_type_eff(_,fl)] -> 
		      let lxm = by_name_op.src in
		      let vel,acc = 
		        List.fold_left
		          (fun (vel,acc) (id,(_,const_opt)) ->
			         try
			           let _,ve = List.find (fun (id2,_) -> id2.it = id) fl_val in
			           let ve,acc = expand_val_exp n_env id_solver acc ve in
			           ve::vel, acc
			         with Not_found -> 
			           match const_opt with
			             | None -> assert false
                      (* ougth to have been checked before *)
			             | Some const -> 
                        let s, ve_const =  (* XXX *)
                          UnifyClock.const_to_val_eff lxm true
                            UnifyClock.empty_subst const
                        in
                        let ve_const,acc=  
                          expand_val_exp n_env id_solver acc ve_const 
                        in
				            ve_const::vel,acc
		          )
		          ([],acc)
		          fl 
		      in
		      let newve = { 
              ve_typ = ve.ve_typ;
              ve_clk = ve.ve_clk;
              ve_core=CallByPosLic({ src=lxm ; it=TUPLE }, OperLic (List.rev vel)) 
            }
            in
            (* 	            if newve.core <> ve.core then ( *)
            (* 		      EvalClock.copy newve ve *)
            (*                     ); *)
		      newve, acc

	       | _ -> assert false

and (expand_val_exp_flag: Lic.local_env -> Lic.id_solver -> acc -> 
     val_exp srcflagged -> val_exp srcflagged * acc) =
  fun n_env id_solver acc { src = lxm ; it = ve } -> 
    let ve,acc = expand_val_exp n_env id_solver acc ve in
    { src = lxm ; it = ve }, acc

and (expand_assert: 
       Lic.local_env -> Lic.id_solver -> acc -> val_exp srcflagged -> acc) =
  fun n_env id_solver acc ve -> 
    let (ve, (asserts, eqs, locs)) = expand_val_exp_flag n_env id_solver acc ve in
    (ve::asserts, eqs, locs)

and (expand_var_info: Lic.local_env -> Lic.id_solver -> var_info list * acc ->
     var_info -> var_info list * acc) =
  fun nenv id_solver (vil, acc) vi -> 
    let rec aux teff =
      match teff with
        | Abstract_type_eff (_, teff) -> aux teff
        | TypeVar Any | TypeVar AnyNum -> 
          Errors.print_internal_error
            "L2lExpandArrays.expand_var_info" "should not have been called for a any(num) var";
          assert false
        | Struct_type_eff (name, fl) -> 
          List.fold_left
            (fun (vil,acc) (fn, (ft,_const_opt)) ->
              let new_var = clone_var nenv vi ("_" ^ Ident.to_string fn) ft in
              let new_vil, new_acc = expand_var_info nenv id_solver (vil,acc) new_var in
              if new_vil = new_var::vil then (
                (* [new_var] type is not made of structure *)
                assert (is_a_basic_type ft);
                Hashtbl.add nenv.lenv_vars new_var.var_name_eff new_var);
              new_vil, new_acc
            )
            (vil, acc)
            fl

        | Array_type_eff(at,size) ->
          let rec aux i (vil,acc) =
            if i=size then  (vil,acc) else
              let new_var = clone_var nenv vi ("_" ^ soi i) at in
              let new_vil, new_acc = expand_var_info nenv id_solver (vil,acc) new_var in
              if new_vil = new_var::vil then (
                (* [new_var] type is not made of structure *)
                assert (is_a_basic_type at);
                Hashtbl.add nenv.lenv_vars new_var.var_name_eff new_var);
              aux (i+1) (new_vil, new_acc)
          in
          aux 0 (vil,acc)

        | External_type_eff(_)
        | Enum_type_eff (_, _)
        | Real_type_eff
        | Int_type_eff
        | Bool_type_eff -> 
          vi::vil, acc
    in
    aux vi.var_type_eff

let rec (node : Lic.id_solver -> Lic.local_env -> Lic.node_exp -> Lic.node_exp) =
  fun is n_env n -> 

    let inlist = n.inlist_eff in
    let outlist = n.outlist_eff in            
    let acc = ([],[],[]) in
    let inlist, acc = List.fold_left (expand_var_info n_env is) ([],acc)  inlist in
    let outlist, acc = List.fold_left (expand_var_info n_env is) ([],acc) outlist in
    let n =
      match n.def_eff with
        | ExternLic 
        | MetaOpLic _
        | AbstractLic None -> n
        | AbstractLic (Some pn) -> 
            { n with def_eff = AbstractLic (Some (node is n_env pn)) }
        | BodyLic b ->
            let loclist = match n.loclist_eff with None -> [] | Some l -> l in
            let loclist, acc = List.fold_left (expand_var_info n_env is) ([],acc) loclist in
            let acc = List.fold_left (expand_eq n_env is) acc b.eqs_eff in
            let acc = List.fold_left (expand_assert n_env is) acc b.asserts_eff in
            let (asserts,neqs, nv) = acc in
            let nb = { 
              eqs_eff = neqs ; 
              asserts_eff = asserts
            } 
            in
              { n with 
                  loclist_eff = Some (List.rev_append loclist nv);
                  def_eff = BodyLic nb
              }
    in
      { n with 
          inlist_eff  = List.rev inlist;
          outlist_eff = List.rev outlist;
      }


(* exported *)
let rec (doit : Lic.id_solver -> Lic.local_env -> LicPrg.t -> LicPrg.t) =
  fun id_solver lenv 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 rec (do_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) = 
      fun nk ne outprg -> 
        let ne = node id_solver lenv ne in
        LicPrg.add_node nk ne outprg
    in
    let outprg = LicPrg.fold_nodes do_node inprg outprg in
    outprg