Project

General

Profile

Revision 4f3cc9f3 src/horn_backend.ml

View differences:

src/horn_backend.ml
28 28
let pp_var fmt id = Format.pp_print_string fmt id.var_id
29 29

  
30 30

  
31
let prefix prefix x = if prefix = "" then x else prefix ^ "." ^ x 
32
let rename_machine p = rename (fun n -> prefix p n)
31
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
32
let rename f = (fun v -> {v with var_id = f v.var_id } )
33
let rename_machine p = rename (fun n -> concat p n)
33 34
let rename_machine_list p = List.map (rename_machine p)
34 35
    
35
let rename f = (fun v -> {v with var_id = f v.var_id } )
36 36
let rename_current =  rename (fun n -> n ^ "_c")
37 37
let rename_current_list = List.map rename_current
38 38
let rename_next = rename (fun n -> n ^ "_x")
......
43 43
  List.find (fun m  -> m.mname.node_id = node_name) machines 
44 44

  
45 45
let full_memory_vars machines machine =
46
  let rec aux fst prefix_s m =
47
    (rename_machine_list (if fst then prefix else prefix ^ "." ^ m.mname.node_id) m.mmemory) @
46
  let rec aux fst prefix m =
47
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
48 48
      List.fold_left (fun accu (id, (n, _)) -> 
49 49
	let name = node_name n in 
50 50
	if name = "_arrow" then accu else
51 51
	  let machine_n = get_machine machines name in
52
	( aux false (prefix_s ^ "." ^ id) machine_n ) @ accu
52
	( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
53 53
      ) [] (m.minstances) 
54 54
  in
55 55
  aux true machine.mname.node_id machine
......
85 85

  
86 86
(* Used to print boolean constants *)
87 87
let pp_horn_tag fmt t =
88
  pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
88
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
89 89

  
90 90
(* Prints a constant value *)
91 91
let rec pp_horn_const fmt c =
......
110 110
    | StateVar v    ->
111 111
      if Types.is_array_type v.var_type
112 112
      then assert false 
113
      else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
113
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
114 114
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
115 115

  
116 116
(* Prints a [value] indexed by the suffix list [loop_vars] *)
......
161 161
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
162 162
	    (Utils.pp_final_char_if_non_empty " " outputs)
163 163
	    (Utils.fprintf_list ~sep:" " pp_var) (
164
  	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
164
  	      rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine)) 
165 165
	     )
166 166
	  else
167 167
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
......
172 172
	      (Utils.pp_final_char_if_non_empty " " outputs)
173 173
	      (Utils.fprintf_list ~sep:" " pp_var) (
174 174

  
175
	      (rename_current_list m.mname.node_id (full_memory_vars machines i target_machine)) @ 
176
	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
175
	      (rename_machine_list (concat m.mname.node_id i) (rename_current_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) @ 
176
		(rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) 
177 177
	       )
178 178
	    
179 179
	     end
......
280 280
    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;
281 281
    (* We print the types of the main node "memory tree" TODO: add the output *)
282 282
    let main_memory_next = 
283
      (rename_next_list machine.mname.node_id (full_memory_vars machines "" machine)) 
283
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) 
284 284
    in
285 285
    let main_memory_current = 
286
      (rename_current_list machine.mname.node_id (full_memory_vars machines "" machine)) 
286
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) 
287 287
    in
288 288
    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
289 289
      (Utils.fprintf_list ~sep:" " pp_type) 

Also available in: Unified diff