CristalCaveGem » LustreC

    | Access _

    | Power _ -> assert false  

  and opt_num_expr vars_env ranges formalEnv e = 

    (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e;  *)

    let fresh_id = "toto"  in (* TODO more meaningful name *)

    (* Convert expression *)

    (* if !debug then Format.eprintf "Formal env is [%a]@ " FormalEnv.pp formalEnv; *)

    (* if !debug then Format.eprintf "Formal env converted to salsa@ "; *)

    (* Substitute all occurences of variables by their definition in env *)

    let (e_salsa: Salsa.Types.expression), _ = 

	0 (* TODO: Nasrine, what is this integer value for ? *)

    in

    (* if !debug then Format.eprintf "Substituted def in expr@ "; *)

    let abstractEnv = RangesInt.to_abstract_env ranges in

       garde evalPartExpr remplace les variables e qui sont dans env par la cst

       - on garde *)

    (* if !debug then Format.eprintf "avant avant eval part@ "; *)

    let e_salsa =  

      Salsa.Analyzer.evalPartExpr 

	e_salsa

	([] (* no blacklisted variables *))

	([] (* no arrays *))

    in

    (* Checking if we have all necessary information *)

    let free_vars = get_salsa_free_vars vars_env constEnv abstractEnv e_salsa in

      Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Warning: unbounded free vars (%a) in expression %a. We do not optimize it.@ " 

	Vars.pp (Vars.fold (fun v accu -> let v' = {v with LT.var_id = nodename.LT.node_id ^ "." ^ v.LT.var_id } in Vars.add v' accu) free_vars Vars.empty)

	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));

      let new_e = try salsa_expr2value_t vars_env constEnv e_salsa   with Not_found -> assert false in

      new_e, None, []

      try 

	if !debug then

	    (C_backend_common.pp_c_val "" (C_backend_common.pp_c_var_read m)) (salsa_expr2value_t vars_env constEnv e_salsa)

	;

	(* Slicing it XXX C'est là !!! ploc *)

	let e_salsa, seq = Salsa.Rewrite.sliceExpr e_salsa 0 (Salsa.Types.Nop(Salsa.Types.Lab 0)) in

	let def_tmps = Salsa.Utils.flatten_seq seq [] in

	(* Registering tmp ids in vars_env *)

	let vars_env' = List.fold_left

	  vars_env

	  def_tmps

	in 

	(* Optimize def tmp, and build the associated instructions. Update the abstract Env with computed ranges *)

	let rev_def_tmp_instrs, ranges =

	  List.fold_left (fun (accu_instrs, ranges) (id, e_id) ->

	    let abstractEnv = RangesInt.to_abstract_env ranges in

	    let e_id', e_range = Salsa.MainEPEG.transformExpression id e_id abstractEnv in

	  ) ([], ranges) def_tmps

	in

	let abstractEnv = RangesInt.to_abstract_env ranges in

	let new_e_salsa, e_val = 

	(* let range_after = Float.evalExpr new_e_salsa abstractEnv in *)

    	let new_e = try salsa_expr2value_t vars_env' constEnv new_e_salsa   with Not_found -> assert false in

	new_e, Some e_val, List.rev rev_def_tmp_instrs

      with (* Not_found ->  *)

      | Salsa.Epeg_types.EPEGError _ -> (

	e, None, []

      )

    )

  in

(* Returns a list of assign, for each var in vars_to_print, that produce the

      (FormalEnv.get_sort_fun formalEnv) 

      (Vars.elements vars_to_print) 

  in

  List.fold_right (

    fun v (accu_instr, accu_ranges) -> 

      try

	(* Obtaining unfold expression of v in formalEnv *)

	let v_def = FormalEnv.get_def formalEnv v  in

   ranges, formalEnv, printed_vars, and remaining vars to be printed) *)

let rec rewrite_instrs nodename m constEnv  vars_env m instrs ranges formalEnv printed_vars vars_to_print =

  let formal_env_def = FormalEnv.def constEnv vars_env in

  let assign_vars = assign_vars nodename m constEnv vars_env in

  match instrs with

  | [] -> 

     (* End of instruction list: we produce the definition of each variable that

	appears in vars_to_print. Each of them should be defined in formalEnv *)

    let instrs, ranges' = assign_vars printed_vars ranges formalEnv vars_to_print in

    instrs,

    ranges',     

     (* We reformulate hd_instr, producing or not a fresh instruction, updating

	formalEnv, possibly ranges and vars_to_print *)

     begin

       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =

	 match Corelang.get_instr_desc hd_instr with 

	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 

	   (* LocalAssign are injected into formalEnv *)

	   (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)

	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)

	   [],                        (* no instr generated *)

	   ranges,                    (* no new range computed *)

	   vars_to_print              (* no more or less variables to print *)

	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->

           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)

           (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)

	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *)

	   let instrs', ranges' = (* printing vd = optimized vt *)

	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  

	   Vars.remove vd vars_to_print     (* removed vd from variables to print *)

	 | MT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 

	   (* StateAssign are produced since they are required by the function. We still

	      keep their definition in the formalEnv in case it can optimize later

	      outputs. vd is removed from remaining vars_to_print *)

	   (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)

	   let formalEnv' = formal_env_def formalEnv vd vt in (* formelEnv updated with vd = vt *) 

	   let instrs', ranges' = (* printing vd = optimized vt *)

	     assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  

	   Vars.remove vd vars_to_print     (* removed vd from variables to print *)

	 | (MT.MLocalAssign(vd,vt) | MT.MStateAssign(vd,vt))  ->

	   (* We have to produce the instruction. But we may have to produce as

	      well its dependencies *)

									  already

									  produced

									  variables *)

	   let required_vars = Vars.diff required_vars (Vars.of_list m.MT.mmemory) in

	   let prefix_instr, ranges = 

	     assign_vars printed_vars ranges formalEnv required_vars in

						   variables to print *)

	 | MT.MStep(vdl,id,vtl) ->

	   (* Call of an external function. Input expressions have to be

	      optimized, their free variables produced. A fresh range has to be

	      computed for each output variable in vdl. Output of the function

	     else

	       fun_types node

	   in

	   let vtl', vtl_ranges, il = List.fold_right2 (

	     fun e typ_e (exprl, range_l, il_l)-> 

	       if Types.is_real_type typ_e then

		 e::exprl, None::range_l, il_l

	   ) vtl tin ([], [], []) 

	   in 

	    (* Required variables to compute vt are introduced. 

	       Then each branch is refactored specifically 

	    *)

	   let required_vars = get_expr_real_vars vt in

	   let required_vars = Vars.diff required_vars printed_vars in (* remove

									  already

	   let read_vars_tl = get_read_vars tl_instrs in

	   let branches', written_vars, merged_ranges = List.fold_right (

	     fun (b_l, b_instrs) (new_branches, written_vars, merged_ranges) -> 

	       let b_write_vars = get_written_vars b_instrs in

	       RangesInt.merge merged_ranges b_ranges      

	   ) branches ([], required_vars, ranges) in

	   prefix_instr@[Corelang.update_instr_desc hd_instr (MT.MBranch(vt', branches'))],

	     merged_ranges, (* Only step functions call within branches

			       may have produced new ranges. We merge this data by

	 | MT.MReset(_) | MT.MNoReset _ | MT.MComment _ ->

	   (* Untouched instruction *)

	   [ hd_instr ],                    (* unmodified instr *)

	      vars_to_print                    (* no more or less variables to print *)

       in

       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 

	 rewrite_instrs 

	   nodename

	   printed_vars

	   vars_to_print

       in

       hd_instrs @ tl_instrs,

       ranges,

       formalEnv, 

	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))

	  | _ -> 

	    Format.eprintf 

	    assert false 

	in

	(* let minv = Salsa.Float.Domain.of_num (get_cst minv) and *)

      )

      | _ -> 

	Format.eprintf 

	  Printers.pp_expr value.LT.eexpr_qfexpr; 

	assert false

    ) ranges annots

  (* TODO: should be at least step output + may be memories *)

  let vars_env = compute_vars_env m in  

  let new_instrs, _, _, printed_vars, _ = 

    rewrite_instrs

      m.MT.mname

  let unused = (Vars.diff all_local_vars printed_vars) in

  let locals =

    if not (Vars.is_empty unused) then (

      List.filter (fun v -> not (Vars.mem v unused)) s.MT.step_locals

    )

    else

let machine_t2machine_t_optimized_by_salsa constEnv  mt =

  try

    let new_step = salsaStep constEnv  mt mt.MT.mstep in

    { mt with MT.mstep = new_step }