Revision ca7ff3f7
Added by Lélio Brun 7 months ago
src/plugins/salsa/salsaDatatypes.ml  

5  5  
6  6 
let debug = ref false 
7  7  
8 
let _ = Salsa.Prelude.sliceSize := 5


9 


10 
let pp_hash ~sep f fmt r =


8 
let _ = Salsa.Prelude.sliceSize := 5 

9  
10 
let pp_hash ~sep f fmt r = 

11  11 
Format.fprintf fmt "[@[<v>"; 
12  12 
Hashtbl.iter (fun k v > Format.fprintf fmt "%t%s@ " (f k v) sep) r; 
13 
Format.fprintf fmt "]@]"; 

14  
13 
Format.fprintf fmt "]@]" 

15  14  
16 
module type VALUE = 

17 
sig 

15 
module type VALUE = sig 

18  16 
type t 
19 
val union: t > t > t 

20 
val pp: Format.formatter > t > unit 

21 
val leq: t > t > bool 

22 
end 

23 


24 
module Ranges = 

25 
functor (Value: VALUE) > 

26 
struct 

27 
module Value = Value 

28 
type t = Value.t 

29 
type r_t = (LT.ident, Value.t) Hashtbl.t 

30  
31 
let empty: r_t = Hashtbl.create 13 

32  
33 
(* Look for def of node i with inputs living in vtl_ranges, reinforce ranges 

34 
to bound vdl: each output of node i *) 

35 
let add_call ranges vdl id vtl_ranges = ranges (* TODO assert false. On est 

36 
pas obligé de faire 

37 
qqchose. On peut supposer 

38 
que les ranges sont donnés 

39 
pour chaque noeud *) 

40  
41  
42 
let pp fmt r = 

43 
if Hashtbl.length r = 0 then 

44 
Format.fprintf fmt "empty" 

45 
else 

46 
pp_hash ~sep:";" (fun k v fmt > Format.fprintf fmt "%s > %a" k Value.pp v) fmt r 

47 
let pp_val = Value.pp 

48  
49 
let add_def ranges name r = 

50 
(* Format.eprintf "%s: declare %a@." *) 

51 
(* x.LT.var_id *) 

52 
(* Value.pp r ; *) 

53 


54 
let fresh = Hashtbl.copy ranges in 

55 
Hashtbl.add fresh name r; fresh 

56  
57 
let enlarge ranges name r = 

58 
let fresh = Hashtbl.copy ranges in 

59 
if Hashtbl.mem fresh name then 

60 
Hashtbl.replace fresh name (Value.union r (Hashtbl.find fresh name)) 

61 
else 

62 
Hashtbl.add fresh name r; 

63 
fresh 

64 


65  
66 
(* Compute a join per variable *) 

67 
let merge ranges1 ranges2 = 

68 
(* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp ranges2; *) 

69 
let ranges = Hashtbl.copy ranges1 in 

70 
Hashtbl.iter (fun k v > 

71 
if Hashtbl.mem ranges k then ( 

72 
(* Format.eprintf "%s: %a union %a = %a@." *) 

73 
(* k *) 

74 
(* Value.pp v *) 

75 
(* Value.pp (Hashtbl.find ranges k) *) 

76 
(* Value.pp (Value.union v (Hashtbl.find ranges k)); *) 

77 
Hashtbl.replace ranges k (Value.union v (Hashtbl.find ranges k)) 

78 
) 

79 
else 

80 
Hashtbl.add ranges k v 

81 
) ranges2; 

82 
(* Format.eprintf "Merge result %a@." pp ranges; *) 

83 
ranges 

84  17  
18 
val union : t > t > t 

85  19  
86 
let to_abstract_env ranges = 

87 
Hashtbl.fold 

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

89 
ranges 

90 
[] 

20 
val pp : Format.formatter > t > unit 

21  
22 
val leq : t > t > bool 

91  23 
end 
92  24  
93 
module FloatIntSalsa = 

94 
struct 

95 
type t = ST.abstractValue 

25 
module Ranges = 

26 
functor 

27 
(Value : VALUE) 

28 
> 

29 
struct 

30 
module Value = Value 

96  31  
97 
let pp fmt ((f,r):t) = 

98 
let fs, rs = (Salsa.Float.Domain.print (f,r)) in 

99 
Format.fprintf fmt "%s + %s" fs rs 

100 
(* match f, r with 

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

102 
Format.fprintf fmt "[%f, %f] + [%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d) 

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

104 
 ST.Empty, _ > Format.fprintf fmt "???" 

105  
106 
 _ > assert false 

107 
*) 

108 
let union v1 v2 = Salsa.Float.Domain.join v1 v2 

109 
(* match v1, v2 with 

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

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

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

113 
*) 

114 
let inject cst = match cst with 

115 
 LT.Const_int(i) > Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i) 

116 
 LT.Const_real r > (* TODO: this is incorrect. We should rather 

117 
compute the error associated to the float *) 

118 
(* let f = float_of_string s in *) 

119 
let n = Real.to_q r in 

120 
Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q n) 

121 


122 
(* let r = Salsa.Prelude.r_of_f_aux r in *) 

123 
(* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *) 

124 


125 
(* let r = float_of_string s in *) 

126 
(* if r = 0. then *) 

127 
(* Salsa.Builder.mk_cst (ST.R(. min_float, min_float),Float.ulp (ST.R(. min_float, min_float))) *) 

128 
(* else *) 

129 
(* Salsa.Builder.mk_cst (ST.I(r*.(1..epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *) 

130 
 _ > assert false 

32 
type t = Value.t 

131  33  
132 
let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq 

133 
end 

34 
type r_t = (LT.ident, Value.t) Hashtbl.t 

134  35  
135 
module RangesInt = Ranges (FloatIntSalsa)


36 
let empty : r_t = Hashtbl.create 13


136  37  
137 
module Vars =


138 
struct


139 
module VarSet = Set.Make (struct type t = LT.var_decl let compare x y = compare x.LT.var_id y.LT.var_id end)


140 
let real_vars vs = VarSet.filter (fun v > Types.is_real_type v.LT.var_type) vs


141 
let of_list = List.fold_left (fun s e > VarSet.add e s) VarSet.empty


38 
(* Look for def of node i with inputs living in vtl_ranges, reinforce ranges


39 
to bound vdl: each output of node i *)


40 
let add_call ranges vdl id vtl_ranges = ranges


41 
(* TODO assert false. On est pas obligé de faire qqchose. On peut supposer


42 
que les ranges sont donnés pour chaque noeud *)


142  43  
143 
include VarSet 

44 
let pp fmt r = 

45 
if Hashtbl.length r = 0 then Format.fprintf fmt "empty" 

46 
else 

47 
pp_hash ~sep:";" 

48 
(fun k v fmt > Format.fprintf fmt "%s > %a" k Value.pp v) 

49 
fmt r 

50  
51 
let pp_val = Value.pp 

52  
53 
let add_def ranges name r = 

54 
(* Format.eprintf "%s: declare %a@." *) 

55 
(* x.LT.var_id *) 

56 
(* Value.pp r ; *) 

57 
let fresh = Hashtbl.copy ranges in 

58 
Hashtbl.add fresh name r; 

59 
fresh 

60  
61 
let enlarge ranges name r = 

62 
let fresh = Hashtbl.copy ranges in 

63 
if Hashtbl.mem fresh name then 

64 
Hashtbl.replace fresh name (Value.union r (Hashtbl.find fresh name)) 

65 
else Hashtbl.add fresh name r; 

66 
fresh 

67  
68 
(* Compute a join per variable *) 

69 
let merge ranges1 ranges2 = 

70 
(* Format.eprintf "Mergeing rangesint %a with %a@." pp ranges1 pp ranges2; *) 

71 
let ranges = Hashtbl.copy ranges1 in 

72 
Hashtbl.iter 

73 
(fun k v > 

74 
if Hashtbl.mem ranges k then 

75 
(* Format.eprintf "%s: %a union %a = %a@." *) 

76 
(* k *) 

77 
(* Value.pp v *) 

78 
(* Value.pp (Hashtbl.find ranges k) *) 

79 
(* Value.pp (Value.union v (Hashtbl.find ranges k)); *) 

80 
Hashtbl.replace ranges k (Value.union v (Hashtbl.find ranges k)) 

81 
else Hashtbl.add ranges k v) 

82 
ranges2; 

83 
(* Format.eprintf "Merge result %a@." pp ranges; *) 

84 
ranges 

144  85  
145 
let remove_list (set:t) (v_list: elt list) : t = List.fold_right VarSet.remove v_list set


146 
let pp fmt vs = Utils.fprintf_list ~sep:", " Printers.pp_var fmt (VarSet.elements vs)


147 
end 

86 
let to_abstract_env ranges =


87 
Hashtbl.fold (fun id value accu > (id, value) :: accu) ranges []


88 
end


148  89  
90 
module FloatIntSalsa = struct 

91 
type t = ST.abstractValue 

149  92  
93 
let pp fmt ((f, r) : t) = 

94 
let fs, rs = Salsa.Float.Domain.print (f, r) in 

95 
Format.fprintf fmt "%s + %s" fs rs 

150  96  
97 
(* match f, r with  ST.I(a,b), ST.J(c,d) > Format.fprintf fmt "[%f, %f] + 

98 
[%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d)  ST.I(a,b), 

99 
ST.JInfty > Format.fprintf fmt "[%f, %f] + oo" a b  ST.Empty, _ > 

100 
Format.fprintf fmt "???" 

151  101  
102 
 _ > assert false *) 

103 
let union v1 v2 = Salsa.Float.Domain.join v1 v2 

152  104  
105 
(* match v1, v2 with (ST.I(x1, x2), ST.J(y1, y2)), (ST.I(x1', x2'), ST.J(y1', 

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

107 
Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false *) 

108 
let inject cst = 

109 
match cst with 

110 
 LT.Const_int i > 

111 
Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i) 

112 
 LT.Const_real r > 

113 
(* TODO: this is incorrect. We should rather compute the error associated 

114 
to the float *) 

115 
(* let f = float_of_string s in *) 

116 
let n = Real.to_q r in 

117 
Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q n) 

118 
(* let r = Salsa.Prelude.r_of_f_aux r in *) 

119 
(* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *) 

120  
121 
(* let r = float_of_string s in *) 

122 
(* if r = 0. then *) 

123 
(* Salsa.Builder.mk_cst (ST.R(. min_float, min_float),Float.ulp (ST.R(. 

124 
min_float, min_float))) *) 

125 
(* else *) 

126 
(* Salsa.Builder.mk_cst 

127 
(ST.I(r*.(1..epsilon_float),r*.(1.+.epsilon_float)),Float.ulp 

128 
(ST.I(r,r))) *) 

129 
 _ > 

130 
assert false 

131  
132 
let leq = 

133 
(* Salsa.Float.feSseq *) 

134 
Salsa.Float.Domain.leq 

135 
end 

153  136  
137 
module RangesInt = Ranges (FloatIntSalsa) 

154  138  
139 
module Vars = struct 

140 
module VarSet = Set.Make (struct 

141 
type t = LT.var_decl 

155  142  
143 
let compare x y = compare x.LT.var_id y.LT.var_id 

144 
end) 

156  145  
146 
let real_vars vs = 

147 
VarSet.filter (fun v > Types.is_real_type v.LT.var_type) vs 

148  
149 
let of_list = List.fold_left (fun s e > VarSet.add e s) VarSet.empty 

150  
151 
include VarSet 

152  
153 
let remove_list (set : t) (v_list : elt list) : t = 

154 
List.fold_right VarSet.remove v_list set 

155  
156 
let pp fmt vs = 

157 
Utils.fprintf_list ~sep:", " Printers.pp_var fmt (VarSet.elements vs) 

158 
end 

157  159  
158  160 
(*************************************************************************************) 
159 
(* Converting values back and forth *)


161 
(* Converting values back and forth *)


160  162 
(*************************************************************************************) 
161  163  
162 
let rec value_t2salsa_expr constEnv vt =


164 
let rec value_t2salsa_expr constEnv vt = 

163  165 
let value_t2salsa_expr = value_t2salsa_expr constEnv in 
164 
let res =


166 
let res = 

165  167 
match vt.MT.value_desc with 
166  168 
(*  LT.Cst(LT.Const_tag(t) as c) > *) 
167  169 
(* Format.eprintf "v2s: cst tag@."; *) 
...  ...  
171  173 
(* ) *) 
172  174 
(* else ( *) 
173  175 
(* Format.eprintf "Const tag %s unhandled@.@?" t ; *) 
174 
(* raise (Salsa.Prelude.Error ("Entschuldigung6, constant tag not yet implemented")) *) 

175 
(* ) *) 

176 
 MT.Cst(cst) > (* Format.eprintf "v2s: cst tag 2: %a@." Printers.pp_const cst; *)FloatIntSalsa.inject cst 

177 
 MT.Var(v) > (* Format.eprintf "v2s: var %s@." v.LT.var_id; *) 

178 
let sel_fun = (fun (vname, _) > v.LT.var_id = vname) in 

179 
if List.exists sel_fun constEnv then 

180 
let _, cst = List.find sel_fun constEnv in 

181 
FloatIntSalsa.inject cst 

176 
(* raise (Salsa.Prelude.Error ("Entschuldigung6, constant tag not yet 

177 
implemented")) *) 

178 
(* ) *) 

179 
 MT.Cst cst > 

180 
(* Format.eprintf "v2s: cst tag 2: %a@." Printers.pp_const cst; *) 

181 
FloatIntSalsa.inject cst 

182 
 MT.Var v > 

183 
(* Format.eprintf "v2s: var %s@." v.LT.var_id; *) 

184 
let sel_fun (vname, _) = v.LT.var_id = vname in 

185 
if List.exists sel_fun constEnv then 

186 
let _, cst = List.find sel_fun constEnv in 

187 
FloatIntSalsa.inject cst 

182  188 
else 
183 
let id = v.LT.var_id in 

184 
Salsa.Builder.mk_id id 

185 
 MT.Fun(binop, [x;y]) > let salsaX = value_t2salsa_expr x in 

186 
let salsaY = value_t2salsa_expr y in 

187 
let op = ( 

188 
let pred f x y = Salsa.Builder.mk_int_of_bool (f x y) in 

189 
match binop with 

190 
 "+" > Salsa.Builder.mk_plus 

191 
 "" > Salsa.Builder.mk_minus 

192 
 "*" > Salsa.Builder.mk_times 

193 
 "/" > Salsa.Builder.mk_div 

194 
 "=" > pred Salsa.Builder.mk_eq 

195 
 "<" > pred Salsa.Builder.mk_lt 

196 
 ">" > pred Salsa.Builder.mk_gt 

197 
 "<=" > pred Salsa.Builder.mk_lte 

198 
 ">=" > pred Salsa.Builder.mk_gte 

199 
 _ > assert false 

200 
) 

201 
in 

202 
op salsaX salsaY 

203 
 MT.Fun(unop, [x]) > let salsaX = value_t2salsa_expr x in 

204 
Salsa.Builder.mk_uminus salsaX 

205  
206 
 MT.Fun(f,_) > raise (Salsa.Prelude.Error 

207 
("Unhandled function "^f^" in conversion to salsa expression")) 

208 


209 
 MT.Array(_) 

210 
 MT.Access(_) 

211 
 MT.Power(_) > raise (Salsa.Prelude.Error ("Unhandled construct in conversion to salsa expression")) 

189 
let id = v.LT.var_id in 

190 
Salsa.Builder.mk_id id 

191 
 MT.Fun (binop, [ x; y ]) > 

192 
let salsaX = value_t2salsa_expr x in 

193 
let salsaY = value_t2salsa_expr y in 

194 
let op = 

195 
let pred f x y = Salsa.Builder.mk_int_of_bool (f x y) in 

196 
match binop with 

197 
 "+" > 

198 
Salsa.Builder.mk_plus 

199 
 "" > 

200 
Salsa.Builder.mk_minus 

201 
 "*" > 

202 
Salsa.Builder.mk_times 

203 
 "/" > 

204 
Salsa.Builder.mk_div 

205 
 "=" > 

206 
pred Salsa.Builder.mk_eq 

207 
 "<" > 

208 
pred Salsa.Builder.mk_lt 

209 
 ">" > 

210 
pred Salsa.Builder.mk_gt 

211 
 "<=" > 

212 
pred Salsa.Builder.mk_lte 

213 
 ">=" > 

214 
pred Salsa.Builder.mk_gte 

215 
 _ > 

216 
assert false 

217 
in 

218 
op salsaX salsaY 

219 
 MT.Fun (unop, [ x ]) > 

220 
let salsaX = value_t2salsa_expr x in 

221 
Salsa.Builder.mk_uminus salsaX 

222 
 MT.Fun (f, _) > 

223 
raise 

224 
(Salsa.Prelude.Error 

225 
("Unhandled function " ^ f ^ " in conversion to salsa expression")) 

226 
 MT.Array _  MT.Access _  MT.Power _ > 

227 
raise 

228 
(Salsa.Prelude.Error 

229 
"Unhandled construct in conversion to salsa expression") 

212  230 
in 
213  231 
(* if debug then *) 
214  232 
(* Format.eprintf "value_t2salsa_expr: %a > %a@ " *) 
215  233 
(* MC.pp_val vt *) 
216 
(* (fun fmt x > Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *)


234 
(* (fun fmt x > Format.fprintf fmt "%s" (Salsa.Print.printExpression x)) res; *) 

217  235 
res 
218  236  
219 
type var_decl = { vdecl: LT.var_decl; is_local: bool } 

220 
module VarEnv = Map.Make (struct type t = LT.ident let compare = compare end ) 

237 
type var_decl = { vdecl : LT.var_decl; is_local : bool } 

238  
239 
module VarEnv = Map.Make (struct 

240 
type t = LT.ident 

241  
242 
let compare = compare 

243 
end) 

221  244  
222  245 
(* let is_local_var vars_env v = *) 
223  246 
(* try *) 
224  247 
(* (VarEnv.find v vars_env).is_local *) 
225 
(* with Not_found > Format.eprintf "Impossible to find var %s@.@?" v; assert false *) 

248 
(* with Not_found > Format.eprintf "Impossible to find var %s@.@?" v; assert 

249 
false *) 

226  250  
227  251 
let get_var vars_env v = 
228 
try 

229 
VarEnv.find v vars_env 

230 
with Not_found > Format.eprintf "Impossible to find var %s in var env %a@ " v 

231 
(Utils.fprintf_list ~sep:", " (fun fmt (id, _) > Format.pp_print_string fmt id)) (VarEnv.bindings vars_env) 

232 
; assert false 

252 
try VarEnv.find v vars_env 

253 
with Not_found > 

254 
Format.eprintf "Impossible to find var %s in var env %a@ " v 

255 
(Utils.fprintf_list ~sep:", " (fun fmt (id, _) > 

256 
Format.pp_print_string fmt id)) 

257 
(VarEnv.bindings vars_env); 

258 
assert false 

233  259  
234  260 
let compute_vars_env m = 
235  261 
let env = VarEnv.empty in 
236 
let env =


237 
List.fold_left


238 
(fun accu v > VarEnv.add v.LT.var_id {vdecl = v; is_local = false; } accu)


239 
env


240 
m.MT.mmemory 

262 
let env = 

263 
List.fold_left 

264 
(fun accu v > 

265 
VarEnv.add v.LT.var_id { vdecl = v; is_local = false } accu)


266 
env m.MT.mmemory


241  267 
in 
242 
let env = 

243 
List.fold_left ( 

244 
fun accu v > VarEnv.add v.LT.var_id {vdecl = v; is_local = true; } accu 

245 
) 

268 
let env = 

269 
List.fold_left 

270 
(fun accu v > VarEnv.add v.LT.var_id { vdecl = v; is_local = true } accu) 

246  271 
env 
247 
MC.(m.MT.mstep.MT.step_inputs@m.MT.mstep.MT.step_outputs@m.MT.mstep.MT.step_locals) 

272 
MC.( 

273 
m.MT.mstep.MT.step_inputs @ m.MT.mstep.MT.step_outputs 

274 
@ m.MT.mstep.MT.step_locals) 

248  275 
in 
249 
env 

276 
env


250  277  
251 
let rec salsa_expr2value_t vars_env cst_env e =


252 
(* let e = Float.evalPartExpr e [] [] in *)


278 
let rec salsa_expr2value_t vars_env cst_env e =


279 
(* let e = Float.evalPartExpr e [] [] in *) 

253  280 
let salsa_expr2value_t = salsa_expr2value_t vars_env cst_env in 
254 
let binop op e1 e2 t =


281 
let binop op e1 e2 t = 

255  282 
let x = salsa_expr2value_t e1 in 
256 
let y = salsa_expr2value_t e2 in


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


283 
let y = salsa_expr2value_t e2 in 

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


258  285 
in 
259  286 
match e with 
260 
ST.Cst(abs_val,_) > (* We project ranges into constants. We 

261 
forget about errors and provide the 

262 
mean/middle value of the interval 

263 
*) 

287 
 ST.Cst (abs_val, _) > 

288 
(* We project ranges into constants. We forget about errors and provide the 

289 
mean/middle value of the interval *) 

264  290 
let new_float = Salsa.Float.Domain.to_float abs_val in 
265 
(* let new_float = Salsa.NumMartel.float_of_num c in *)


266 
(* let new_float = *)


267 
(* if f1 = f2 then *)


268 
(* f1 *)


269 
(* else *)


270 
(* (f1 +. f2) /. 2.0 *)


271 
(* in *)


272 
(* Log.report ~level:3 *)


273 
(* (fun fmt > Format.fprintf fmt "projecting [%.45f, %.45f] > %.45f@ " f1 f2 new_float); *)


274 
let cst =


275 
let s =


276 
if new_float = 0. then "0." else


277 
(* We have to convert it into our format: int * int * real *)


278 
(* string_of_float new_float *)


279 
let _ = Format.flush_str_formatter () in


280 
Format.fprintf Format.str_formatter "%.11f" new_float;


281 
Format.flush_str_formatter ()


282 
in


283 
Parser_lustre.signed_const Lexer_lustre.token (Lexing.from_string s)


291 
(* let new_float = Salsa.NumMartel.float_of_num c in *) 

292 
(* let new_float = *) 

293 
(* if f1 = f2 then *) 

294 
(* f1 *) 

295 
(* else *) 

296 
(* (f1 +. f2) /. 2.0 *) 

297 
(* in *) 

298 
(* Log.report ~level:3 *) 

299 
(* (fun fmt > Format.fprintf fmt "projecting [%.45f, %.45f] > %.45f@ " f1


300 
f2 new_float); *)


301 
let cst =


302 
let s =


303 
if new_float = 0. then "0."


304 
else


305 
(* We have to convert it into our format: int * int * real *)


306 
(* string_of_float new_float *)


307 
let _ = Format.flush_str_formatter () in


308 
Format.fprintf Format.str_formatter "%.11f" new_float;


309 
Format.flush_str_formatter ()


284  310 
in 
285 
MC.mk_val (MT.Cst(cst)) Type_predef.type_real 

286 
 ST.Id(id, _) > 

311 
Parser_lustre.signed_const Lexer_lustre.token (Lexing.from_string s) 

312 
in 

313 
MC.mk_val (MT.Cst cst) Type_predef.type_real 

314 
 ST.Id (id, _) > 

287  315 
(* Format.eprintf "Looking for id=%s@.@?" id; *) 
288 
if List.mem_assoc id cst_env then (


289 
let cst = List.assoc id cst_env in


316 
if List.mem_assoc id cst_env then


317 
let cst = List.assoc id cst_env in 

290  318 
(* Format.eprintf "Found cst = %a@.@?" Printers.pp_const cst; *) 
291 
MC.mk_val (MT.Cst cst) Type_predef.type_real 

292 
) 

293 
else 

319 
MC.mk_val (MT.Cst cst) Type_predef.type_real 

320 
else 

294  321 
(* if is_const salsa_label then *) 
295  322 
(* MC.Cst(LT.Const_tag(get_const salsa_label)) *) 
296 
(* else *) 

297 
let var_id = try get_var vars_env id with Not_found > assert false in 

298 
MC.mk_val (MT.Var(var_id.vdecl)) var_id.vdecl.LT.var_type 

299 
 ST.Plus(x, y, _) > binop "+" x y Type_predef.type_real 

300 
 ST.Minus(x, y, _) > binop "" x y Type_predef.type_real 

301 
 ST.Times(x, y, _) > binop "*" x y Type_predef.type_real 

302 
 ST.Div(x, y, _) > binop "/" x y Type_predef.type_real 

303 
 ST.Uminus(x,_) > let x = salsa_expr2value_t x in 

304 
MC.mk_val (MT.Fun("uminus",[x])) Type_predef.type_real 

305 
 ST.IntOfBool(ST.Eq(x, y, _),_) > binop "=" x y Type_predef.type_bool 

306 
 ST.IntOfBool(ST.Lt(x,y,_),_) > binop "<" x y Type_predef.type_bool 

307 
 ST.IntOfBool(ST.Gt(x,y,_),_) > binop ">" x y Type_predef.type_bool 

308 
 ST.IntOfBool(ST.Lte(x,y,_),_) > binop "<=" x y Type_predef.type_bool 

309 
 ST.IntOfBool(ST.Gte(x,y,_),_) > binop ">=" x y Type_predef.type_bool 

310 
 _ > raise (Salsa.Prelude.Error "Entschuldigung, salsaExpr2value_t case not yet implemented") 

311  
312  
323 
(* else *) 

324 
let var_id = try get_var vars_env id with Not_found > assert false in 

325 
MC.mk_val (MT.Var var_id.vdecl) var_id.vdecl.LT.var_type 

326 
 ST.Plus (x, y, _) > 

327 
binop "+" x y Type_predef.type_real 

328 
 ST.Minus (x, y, _) > 

329 
binop "" x y Type_predef.type_real 

330 
 ST.Times (x, y, _) > 

331 
binop "*" x y Type_predef.type_real 

332 
 ST.Div (x, y, _) > 

333 
binop "/" x y Type_predef.type_real 

334 
 ST.Uminus (x, _) > 

335 
let x = salsa_expr2value_t x in 

336 
MC.mk_val (MT.Fun ("uminus", [ x ])) Type_predef.type_real 

337 
 ST.IntOfBool (ST.Eq (x, y, _), _) > 

338 
binop "=" x y Type_predef.type_bool 

339 
 ST.IntOfBool (ST.Lt (x, y, _), _) > 

340 
binop "<" x y Type_predef.type_bool 

341 
 ST.IntOfBool (ST.Gt (x, y, _), _) > 

342 
binop ">" x y Type_predef.type_bool 

343 
 ST.IntOfBool (ST.Lte (x, y, _), _) > 

344 
binop "<=" x y Type_predef.type_bool 

345 
 ST.IntOfBool (ST.Gte (x, y, _), _) > 

346 
binop ">=" x y Type_predef.type_bool 

347 
 _ > 

348 
raise 

349 
(Salsa.Prelude.Error 

350 
"Entschuldigung, salsaExpr2value_t case not yet implemented") 

313  351  
314  352 
let rec get_salsa_free_vars vars_env constEnv absenv e = 
315  353 
let f = get_salsa_free_vars vars_env constEnv absenv in 
316  354 
match e with 
317 
 ST.Id (id, _) > 

318 
if not (List.mem_assoc id absenv) && not (List.mem_assoc id constEnv) then 

319 
Vars.singleton ((try VarEnv.find id vars_env with Not_found > assert false).vdecl) 

320 
else 

321 
Vars.empty 

322 
 ST.Plus(x, y, _) 

323 
 ST.Minus(x, y, _) 

324 
 ST.Times(x, y, _) 

325 
 ST.Div(x, y, _) 

326 
 ST.IntOfBool(ST.Eq(x, y, _),_) 

327 
 ST.IntOfBool(ST.Lt(x,y,_),_) 

328 
 ST.IntOfBool(ST.Gt(x,y,_),_) 

329 
 ST.IntOfBool(ST.Lte(x,y,_),_) 

330 
 ST.IntOfBool(ST.Gte(x,y,_),_) 

331 
> Vars.union (f x) (f y) 

332 
 ST.Uminus(x,_) > f x 

333 
 ST.Cst _ > Vars.empty 

334 
 _ > assert false 

335  
336  
337 
module FormalEnv = 

338 
struct 

339 
type fe_t = (LT.ident, (int * MT.value_t)) Hashtbl.t 

355 
 ST.Id (id, _) > 

356 
if (not (List.mem_assoc id absenv)) && not (List.mem_assoc id constEnv) then 

357 
Vars.singleton 

358 
(try VarEnv.find id vars_env with Not_found > assert false).vdecl 

359 
else Vars.empty 

360 
 ST.Plus (x, y, _) 

361 
 ST.Minus (x, y, _) 

362 
 ST.Times (x, y, _) 

363 
 ST.Div (x, y, _) 

364 
 ST.IntOfBool (ST.Eq (x, y, _), _) 

365 
 ST.IntOfBool (ST.Lt (x, y, _), _) 

366 
 ST.IntOfBool (ST.Gt (x, y, _), _) 

367 
 ST.IntOfBool (ST.Lte (x, y, _), _) 

368 
 ST.IntOfBool (ST.Gte (x, y, _), _) > 

369 
Vars.union (f x) (f y) 

370 
 ST.Uminus (x, _) > 

371 
f x 

372 
 ST.Cst _ > 

373 
Vars.empty 

374 
 _ > 

375 
assert false 

376  
377 
module FormalEnv = struct 

378 
type fe_t = (LT.ident, int * MT.value_t) Hashtbl.t 

379  
340  380 
let cpt = ref 0 
341  381  
342  382 
exception NoDefinition of LT.var_decl 
383  
343  384 
(* Returns the expression associated to v in env *) 
344 
let get_def (env: fe_t) v = 

345 
try 

346 
snd (Hashtbl.find env v.LT.var_id) 

385 
let get_def (env : fe_t) v = 

386 
try snd (Hashtbl.find env v.LT.var_id) 

347  387 
with Not_found > raise (NoDefinition v) 
348  388  
349 
let fold f = Hashtbl.fold (fun k (_,v) accu > f k v accu) 

350 


351 
let to_salsa constEnv formalEnv =


352 
fold (fun id expr accu >


353 
(id, value_t2salsa_expr constEnv expr)::accu


354 
) formalEnv []


389 
let fold f = Hashtbl.fold (fun k (_, v) accu > f k v accu)


390  
391 
let to_salsa constEnv formalEnv = 

392 
fold 

393 
(fun id expr accu > (id, value_t2salsa_expr constEnv expr) :: accu)


394 
formalEnv []


355  395  
356 
let def constEnv vars_env (env: fe_t) d expr =


396 
let def constEnv vars_env (env : fe_t) d expr =


357  397 
incr cpt; 
358  398 
let fresh = Hashtbl.copy env in 
359  399 
let expr_salsa = value_t2salsa_expr constEnv expr in 
360  400 
let salsa_env = to_salsa constEnv env in 
361  401 
let expr_salsa, _ = Salsa.Rewrite.substVars expr_salsa salsa_env 0 in 
362 
let expr_salsa = Salsa.Analyzer.evalPartExpr expr_salsa salsa_env ([] (* no blacklisted vars *)) ([] (*no arrays *)) in 

402 
let expr_salsa = 

403 
Salsa.Analyzer.evalPartExpr expr_salsa salsa_env [] 

404 
(* no blacklisted vars *) 

405 
[] 

406 
(*no arrays *) 

407 
in 

363  408 
let expr_lustrec = salsa_expr2value_t vars_env [] expr_salsa in 
364 
Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec); fresh 

365  
366 
let empty (): fe_t = Hashtbl.create 13 

409 
Hashtbl.add fresh d.LT.var_id (!cpt, expr_lustrec); 

410 
fresh 

367  411  
368 
let pp m fmt env = pp_hash ~sep:";@ " (fun k (_,v) fmt > Format.fprintf fmt "%s > %a" k (MC.pp_val m) v) fmt env


412 
let empty () : fe_t = Hashtbl.create 13


369  413  
414 
let pp m fmt env = 

415 
pp_hash ~sep:";@ " 

416 
(fun k (_, v) fmt > Format.fprintf fmt "%s > %a" k (MC.pp_val m) v) 

417 
fmt env 

370  418  
371  419 
let get_sort_fun env = 
372 
let order = Hashtbl.fold (fun k (cpt, _) accu > (k,cpt)::accu) env [] in 

373 
fun v1 v2 > 

374 
if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order then 

375 
if (List.assoc v1.LT.var_id order) <= (List.assoc v2.LT.var_id order) then 

376 
1 

377 
else 

378 
1 

379 
else 

380 
assert false 

420 
let order = Hashtbl.fold (fun k (cpt, _) accu > (k, cpt) :: accu) env [] in 

421 
fun v1 v2 > 

422 
if List.mem_assoc v1.LT.var_id order && List.mem_assoc v2.LT.var_id order 

423 
then 

424 
if List.assoc v1.LT.var_id order <= List.assoc v2.LT.var_id order then 

425 
1 

426 
else 1 

427 
else assert false 

381  428 
end 
382  429  
383 


384  430 
(* Local Variables: *) 
385  431 
(* compilecommand:"make C ../../.." *) 
386  432 
(* End: *) 
Also available in: Unified diff
reformatting