Project

General

Profile

Revision ca88e660 src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
42 42
let rec pp_horn_const fmt c =
43 43
  match c with
44 44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real r   -> pp_print_string fmt r
46
    | Const_float r  -> pp_print_float fmt r
45
    | Const_real (c,e,s)   -> assert false (* TODO rational pp_print_string fmt r *)
46
    (* | Const_float r  -> pp_print_float fmt r *)
47 47
    | Const_tag t    -> pp_horn_tag fmt t
48 48
    | _              -> assert false
49 49

  
......
52 52
   but an offset suffix may be added for array variables
53 53
*)
54 54
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
55
  match v with
55
  match v.value_desc with
56 56
    | Cst c         -> pp_horn_const fmt c
57 57
    | Array _
58 58
    | Access _ -> assert false (* no arrays *)
......
66 66

  
67 67
(* Prints a [value] indexed by the suffix list [loop_vars] *)
68 68
let rec pp_value_suffix self pp_value fmt value =
69
 match value with
69
 match value.value_desc with
70 70
 | Fun (n, vl)  ->
71 71
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
72 72
 |  _            ->
......
157 157
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
158 158
	fprintf fmt "@[<v 5>(and ";
159 159
	fprintf fmt "(= %a (ite %a %a %a))"
160
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
160
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
161 161
	  (pp_horn_var m) mem_m 
162 162
	  (pp_horn_val self (pp_horn_var m)) i1
163 163
	  (pp_horn_val self (pp_horn_var m)) i2
......
173 173
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
174 174
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
175 175
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
176
	  (List.map (fun v -> LocalVar v) outputs)
176
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
177 177
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
178 178
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
179 179
	
......
187 187
      inputs
188 188
      (Utils.pp_final_char_if_non_empty "@ " inputs)
189 189
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
190
      (List.map (fun v -> LocalVar v) outputs)
190
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
191 191
  )
192 192
    
193 193
    
......
203 203
  | MLocalAssign (i,v) ->
204 204
    pp_assign
205 205
      m (pp_horn_var m) fmt
206
      i.var_type (LocalVar i) v;
206
      i.var_type (mk_val (LocalVar i) i.var_type) v;
207 207
    reset_instances
208 208
  | MStateAssign (i,v) ->
209 209
    pp_assign
210 210
      m (pp_horn_var m) fmt
211
      i.var_type (StateVar i) v;
211
      i.var_type (mk_val (StateVar i) i.var_type) v;
212 212
    reset_instances
213
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
213
  | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
214 214
    assert false (* This should not happen anymore *)
215 215
  | MStep (il, i, vl) ->
216 216
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =

Also available in: Unified diff