CristalCaveGem » LustreC

(* Optimize a given expression. It returns another expression and a computed range. *)

  let rec opt_expr ranges formalEnv e =

    match e.LT.value_desc with

    | LT.Cst cst ->

    (* Convert formalEnv *)

    (* 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), _ = 

      Salsa.Rewrite.substVars 

	e_salsa

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

    in

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

    let abstractEnv = Hashtbl.fold 

      (fun id value accu -> (id,value)::accu) 

       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

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

	MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa));

      if !debug then Format.eprintf "Some free vars, not optimizing@.";

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

      new_e, None

    )

    else (

	if !debug then

	    (Utils.fprintf_list ~sep:",@ "(fun fmt (l,r) -> Format.fprintf fmt "%s -> %a" l FloatIntSalsa.pp r)) abstractEnv

	;

	let new_e_salsa, e_val = 

	in

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

	if !debug then Format.eprintf "@  @[<v>old: %a@ new: %a@ range: %a@]" MC.pp_val e MC.pp_val new_e RangesInt.pp_val e_val;

	new_e, Some e_val

      | Salsa.Epeg_types.EPEGError _ -> (

	Format.eprintf "BECAUSE OF AN ERROR, Expression %a was not optimized@ " MC.pp_val e;

	e, None

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

   definition of it according to formalEnv, and driven by the ranges. *)

  (* We print thhe expression in the order of definition *)

  let ordered_vars = 

      try

	(* Obtaining unfold expression of v in formalEnv *)

	let v_def = FormalEnv.get_def formalEnv v  in

	let instr_desc = 

	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then

	    LT.MLocalAssign(v, e)

(* Main recursive function: modify the instructions list while preserving the

   order of assigns for state variables. Returns a quintuple: (new_instrs,

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

  Format.eprintf "Rewrite intrs :%a@." Machine_code.pp_instrs instrs;

  match instrs with

  | [] -> 

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

	    (* LocalAssign are injected into formalEnv *)

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

	    if !debug then Format.eprintf "%a@ " MC.pp_instr hd_instr;

	    [],                        (* no instr generated *)

	    ranges,                    (* no new range computed *)

	    formalEnv',

	     Format.eprintf "%a@]@ " MC.pp_instr hd_instr;

	     Format.eprintf "Selected var %a: producing expression@ " Printers.pp_var vd;

	   );

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

	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  

	    in

	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)

	    Vars.remove vd vars_to_print     (* removed vd from variables 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

	     Format.eprintf "%a@]@ " MC.pp_instr hd_instr;

	     Format.eprintf "State assign %a: producing expression@ " Printers.pp_var vd;

	   );

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

	      assign_vars printed_vars ranges formalEnv' (Vars.singleton vd)  

	    in

	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)

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

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

	     well its dependencies *)

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

									 already

									 produced

	    let prefix_instr, ranges = 

	      assign_vars printed_vars ranges formalEnv required_vars in

	    let new_instr = 

	      match Corelang.get_instr_desc hd_instr with

	      | LT.MLocalAssign _ -> Corelang.update_instr_desc hd_instr (LT.MLocalAssign(vd,vt'))

	    let vtl', vtl_ranges = List.fold_right2 (

				       fun e typ_e (exprl, range_l)-> 

				       if Types.is_real_type typ_e then

					 e'::exprl, r'::range_l

				       else 

					 e::exprl, None::range_l

	    let printed_vars = Vars.union printed_vars required_vars in

	    let read_vars_tl = get_read_vars tl_instrs in

	    if !debug then Format.eprintf "@[<v 2>Dealing with branches@ ";

						       data, we copy it for

						       each branch *)

							     let b_instrs', b_ranges, b_formalEnv, b_printed, b_vars = 

							     in

							     (* b_vars should be empty *)

							     let _ = if b_vars != [] then assert false in

       let tl_instrs, ranges, formalEnv, printed_vars, vars_to_print = 

	 rewrite_instrs 

	   nodename

	   constEnv 	  

	   vars_env

	   m 

	    assert false 

	in

	let minv, maxv = get_cst minv, get_cst maxv in

	RangesInt.enlarge ranges v (Salsa.Float.Domain.nnew minv maxv)

      )

      | _ -> 

  let new_instrs, _, _, printed_vars, _ = 

    rewrite_instrs

      m.MC.mname.LT.node_id

      constEnv 

      vars_env

      m

  Hashtbl.iter (fun k v -> Format.fprintf fmt "%t%s@ " (f k v) sep) r;

  Format.fprintf fmt "]@]";

module Ranges = 

  functor (Value: sig type t val union: t -> t -> t val pp: Format.formatter -> t -> unit end)  ->

      ST.(I(min x1 x1', max x2 x2'), J(min y1 y1', max y2 y2'))

    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 

*)

    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather

				  compute the error associated to the float *)

					forget about errors and provide the

					mean/middle value of the interval

				     *)

      (* let new_float =  *)

      (* 	if f1 = f2 then *)

      (* 	  f1 *)

  | ST.Cst _ -> Vars.empty

  | _ -> assert false

(* Local Variables: *)

(* compile-command:"make -C ../../.." *)

(* End: *)