CristalCaveGem » LustreC

(* We try to avoid opening modules here *)

module SDT = SalsaDatatypes

module LT = LustreSpec

module MC = Machine_code

    | LT.Access _

    | LT.Power _ -> assert false  

  and opt_num_expr ranges formalEnv e = 

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

    (* Convert expression *)

    (* List.iter (fun (l,c) -> Format.eprintf "%s -> %a@ " l Printers.pp_const c) constEnv; *)

    (* Format.eprintf "apres deplaige constantes ok%a @." MC.pp_val (salsa_expr2value_t vars_env [](\* constEnv *\) e_salsa) ;  *)

    (* Convert formalEnv *)

    let formalEnv_salsa = 

      FormalEnv.fold (fun id expr accu ->

	(id, value_t2salsa_expr constEnv expr)::accu

		     ) formalEnv []  in

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

      Salsa.Rewrite.substVars 

	e_salsa

	formalEnv_salsa

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

    in

    let abstractEnv = Hashtbl.fold 

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

      ranges

       valEnv2ExprEnv remplce les paires id, abstractVal par id, Cst itv - on

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

       - on garde *)

    (*  Format.eprintf "avant evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);  *)

    let e_salsa =  

	e_salsa

    in

     (* Format.eprintf "apres evalpart: %a@." MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa);  *)

    (* Checking if we have all necessary information *)

    if Vars.cardinal free_vars > 0 then (

	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)

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

      new_e, None

    )

    else (

      try

	  Format.eprintf "Analyzing expression %a with env: @[<v>%a@ @]@ "

	    MC.pp_val (salsa_expr2value_t vars_env constEnv e_salsa)

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

	;

	let new_e_salsa, e_val = 

	  Salsa.MainEPEG.transformExpression fresh_id 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

      with Not_found -> assert false

      | Salsa.Epeg_types.EPEGError _ -> (

  in

    Format.eprintf "@[<v 2>Optimizing expression %a in environment %a and ranges %a@ "

      MC.pp_val e

      FormalEnv.pp formalEnv

      (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

(* 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) *)

  let assign_vars = assign_vars nodename constEnv vars_env in

  (*   Format.eprintf "------------@ "; *)

  (*   Format.eprintf "Current printed_vars: [%a]@ " Vars.pp printed_vars; *)

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

  | [] -> 

     (* 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 

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

	    (* LocalAssign are injected into formalEnv *)

	    let formalEnv' = FormalEnv.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 *)

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

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

	 | LT.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 *)

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

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

	   );

	    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 = get_expr_real_vars vt in

									 variables *)

	    let prefix_instr, ranges = 

	      assign_vars printed_vars ranges formalEnv required_vars in

	    let vt', _ = optimize_expr nodename constEnv (Vars.union required_vars printed_vars) vars_env ranges formalEnv vt in

	    let new_instr = 

	      match Corelang.get_instr_desc hd_instr with

	    Vars.diff vars_to_print written_vars (* removed vd + dependencies from

						  variables to print *)

	    (* 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 = List.fold_right2 (

				       fun e typ_e (exprl, range_l)-> 

				       if Types.is_real_type typ_e then

					 e::exprl, None::range_l

				     ) vtl tin ([], []) 

	    in 

	    let required_vars = 

	      List.fold_left2 

		(fun accu e typ_e -> 

 		Vars.empty 

		vtl' tin

	    in

					 Vars.pp required_vars 

					 Vars.pp printed_vars

					 Vars.pp (Vars.diff required_vars printed_vars)

	      Vars.union written_vars printed_vars,        (* adding vdl to new printed vars *)

	      Vars.diff vars_to_print written_vars

	    (* 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 vt', _ = optimize_expr nodename constEnv printed_vars vars_env ranges formalEnv vt in

	    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 (LT.MBranch(vt', branches'))],

	    merged_ranges, (* Only step functions call within branches

			    may have produced new ranges. We merge this data by

	 | LT.MReset(_) | LT.MNoReset _ | LT.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, 

	let get_cst e = match e.LT.expr_desc with 

	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 

	    (* calculer la valeur c * 10^e *) 

	  | _ -> 

	    Format.eprintf 

	      "Invalid scala range: %a. It should be a pair of constant floats.@." 

	    assert false 

	in

	let minv, maxv = get_cst minv, get_cst maxv in

      )

      | _ -> 

	Format.eprintf 

      )

  in 

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

  let new_instrs, _, _, printed_vars, _ = 

    rewrite_instrs

      m.MC.mname.LT.node_id

  { s with MC.step_instrs = new_instrs; MC.step_locals = locals } (* we have also to modify local variables to declare new vars *)

  try

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

    { mt with MC.mstep = new_step } 

module LT = LustreSpec

module MC = Machine_code

module Float = Salsa.Float

let pp_hash ~sep f fmt r = 

  Format.fprintf fmt "[@[<v>";

struct

  type t = ST.abstractValue

    | ST.I(a,b), ST.J(c,d) ->

    | ST.I(a,b), ST.JInfty ->  Format.fprintf fmt "[%f, %f] + oo" a b 

    | ST.Empty, _ -> Format.fprintf fmt "???"

    | _ -> assert false

    |(ST.I(x1, x2), ST.J(y1, y2)), (ST.I(x1', x2'), ST.J(y1', y2')) ->

      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 

  let inject cst = match cst with

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

				  compute the error associated to the float *)

    | _ -> assert false

end

    MC.mk_val (LT.Fun (op, [x;y])) t

  in

  match e with

					forget about errors and provide the

					mean/middle value of the interval

				     *)

      let cst =  

	let s = 

	  if new_float = 0. then "0." else

  let name = "salsa"

  let options = [

  let activate () = salsa_enabled := true