Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by Lélio Brun 7 months ago

reformatting

View differences:

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
(* compile-command:"make -C ../../.." *)
386 432
(* End: *)

Also available in: Unified diff