Revision 642e116d
Added by Pierre-Loïc Garoche over 6 years ago
| 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
Ongoing work on salsa: introduce slicing of expr