Project

General

Profile

Revision 642e116d src/plugins/salsa/salsaDatatypes.ml

View differences:

src/plugins/salsa/salsaDatatypes.ml
10 10
  Hashtbl.iter (fun k v -> Format.fprintf fmt "%t%s@ " (f k v) sep) r;
11 11
  Format.fprintf fmt "]@]";
12 12

  
13
module FormalEnv =
14
struct
15
  type fe_t = (LT.ident, (int * LT.value_t)) Hashtbl.t
16
  let cpt = ref 0
17

  
18
  exception NoDefinition of LT.var_decl
19
  (* Returns the expression associated to v in env *)
20
  let get_def (env: fe_t) v = 
21
    try 
22
      snd (Hashtbl.find env v.LT.var_id) 
23
    with Not_found -> raise (NoDefinition v)
24

  
25
  let def (env: fe_t) d expr = 
26
    incr cpt;
27
    let fresh = Hashtbl.copy env in
28
    Hashtbl.add fresh d.LT.var_id (!cpt, expr); fresh
29

  
30
  let empty (): fe_t = Hashtbl.create 13
31

  
32
  let pp fmt env = pp_hash ~sep:";" (fun k (_,v) fmt -> Format.fprintf fmt "%s -> %a" k MC.pp_val v) fmt env
33

  
34
  let fold f = Hashtbl.fold (fun k (_,v) accu -> f k v accu)
35

  
36
  let get_sort_fun env =
37
    let order = Hashtbl.fold (fun k (cpt, _) accu -> (k,cpt)::accu) env [] in
38
    fun v1 v2 -> 
39
      if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order then
40
	if (List.assoc v1.LT.var_id order) <= (List.assoc v2.LT.var_id order) then 
41
	  -1
42
	else 
43
	  1
44
      else
45
	assert false
46
    
47
end
48 13

  
49 14
module Ranges = 
50 15
  functor (Value: sig type t val union: t -> t -> t val pp: Format.formatter -> t -> unit end)  ->
......
125 90
      ST.(I(min x1 x1', max x2 x2'), J(min y1 y1', max y2 y2'))
126 91
    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 
127 92
*)
128
  let inject cst = match cst with
129
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (ST.R(Num.num_of_int i, []), ST.R(Num.num_of_int i, []))
93
  let inject cst = match cst with (* ATTENTION ATTENTION !!!!! Remettre les Num !!!! *) 
94
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (ST.R(float_of_int i (*Num.num_of_int i*), []), ST.R(float_of_int i (*Num.num_of_int i*), []))
130 95
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
131 96
				  compute the error associated to the float *)
132 97
       
......
269 234
					forget about errors and provide the
270 235
					mean/middle value of the interval
271 236
				     *)
272
      let  new_float = Num.float_of_num c in
237
      let  new_float = Salsa.NumMartel.float_of_num c in
273 238
      (* let new_float =  *)
274 239
      (* 	if f1 = f2 then *)
275 240
      (* 	  f1 *)
......
341 306
  | ST.Cst _ -> Vars.empty
342 307
  | _ -> assert false
343 308

  
309

  
310
module FormalEnv =
311
struct
312
  type fe_t = (LT.ident, (int * LT.value_t)) Hashtbl.t
313
  let cpt = ref 0
314

  
315
  exception NoDefinition of LT.var_decl
316
  (* Returns the expression associated to v in env *)
317
  let get_def (env: fe_t) v = 
318
    try 
319
      snd (Hashtbl.find env v.LT.var_id) 
320
    with Not_found -> raise (NoDefinition v)
321

  
322
  let fold f = Hashtbl.fold (fun k (_,v) accu -> f k v accu)
323
      
324
  let to_salsa constEnv formalEnv = 
325
    fold (fun id expr accu ->
326
      (id, value_t2salsa_expr constEnv expr)::accu
327
    ) formalEnv [] 
328

  
329
  let def constEnv vars_env (env: fe_t) d expr = 
330
    incr cpt;
331
    let fresh = Hashtbl.copy env in
332
    let expr_salsa = value_t2salsa_expr constEnv expr in
333
    let salsa_env = to_salsa constEnv env in
334
    let expr_salsa, _ = Salsa.Rewrite.substVars expr_salsa salsa_env 0 in
335
    let expr_salsa = Salsa.Analyzer.evalPartExpr expr_salsa salsa_env ([] (* no blacklisted vars *)) ([] (*no arrays *)) in
336
    let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in
337
    Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec); fresh
338

  
339
  let empty (): fe_t = Hashtbl.create 13
340

  
341
  let pp fmt env = pp_hash ~sep:";" (fun k (_,v) fmt -> Format.fprintf fmt "%s -> %a" k MC.pp_val v) fmt env
342

  
343

  
344
  let get_sort_fun env =
345
    let order = Hashtbl.fold (fun k (cpt, _) accu -> (k,cpt)::accu) env [] in
346
    fun v1 v2 -> 
347
      if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order then
348
	if (List.assoc v1.LT.var_id order) <= (List.assoc v2.LT.var_id order) then 
349
	  -1
350
	else 
351
	  1
352
      else
353
	assert false
354
end
355

  
356
     
344 357
(* Local Variables: *)
345 358
(* compile-command:"make -C ../../.." *)
346 359
(* End: *)

Also available in: Unified diff