Project

General

Profile

Revision faa5e5c5 src/horn_backend.ml

View differences:

src/horn_backend.ml
27 27

  
28 28
let pp_var fmt id = Format.pp_print_string fmt id.var_id
29 29

  
30
let pp_instr machine_name fmt i =
31
  Format.fprintf fmt "(xxx)"
32 30

  
33 31
let rename f = (fun v -> {v with var_id = f v.var_id } )
34
let rename_current machine_name =  rename (fun n -> machine_name ^ "." ^ n ^ "_c")
35
let rename_current_list machine_name = List.map (rename_current machine_name)
36
let rename_next machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_x")
37
let rename_next_list machine_name = List.map (rename_next machine_name)
38
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n)
39
let rename_machine_list machine_name = List.map (rename_machine machine_name)
40

  
41
let full_memory_vars machine instance =
42
  (rename_current_list machine.mname.node_id machine.mmemory) @
43
    (rename_next_list machine.mname.node_id machine.mmemory)
44

  
45
let machine_vars m = 
32
let rename_current prefix =  rename (fun n -> prefix ^ "." ^ n ^ "_c")
33
let rename_current_list prefix = List.map (rename_current prefix)
34
let rename_next prefix = rename (fun n -> prefix ^ "." ^ n ^ "_x")
35
let rename_next_list prefix = List.map (rename_next prefix)
36
let rename_machine prefix = rename (fun n -> prefix ^ "." ^ n)
37
let rename_machine_list prefix = List.map (rename_machine prefix)
38

  
39
let get_machine machines node_name = 
40
  List.find (fun m  -> m.mname.node_id = node_name) machines 
41

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

  
55
let machine_vars machines m = 
56
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
57
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
58
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 
59
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
60

  
61
let step_vars machines m = 
62
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
63
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
64
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 
65
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
66

  
67
let init_vars machines m = 
46 68
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
47 69
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@
48
  full_memory_vars m ()
70
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 
49 71

  
50 72
  
51 73
(********************************************************************************************)
......
130 152
      | name, _, _ ->  
131 153
	begin
132 154
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
133
	  Format.fprintf fmt "(%s_%s %a%t%a%t%a)"
155
	  if init then
156
	  Format.fprintf fmt "(%s_init %a%t%a%t%a)"
134 157
	    (node_name n) 
135
	    (if init then "init" else "step")
136 158
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
137 159
	    (Utils.pp_final_char_if_non_empty " " inputs) 
138 160
	    (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
139
	       (Utils.pp_final_char_if_non_empty " " outputs)
140
	    (Utils.fprintf_list ~sep:" " pp_var) (full_memory_vars target_machine i)
161
	    (Utils.pp_final_char_if_non_empty " " outputs)
162
	    (Utils.fprintf_list ~sep:" " pp_var) (
163
  	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
164
	     )
165
	  else
166
	    Format.fprintf fmt "(%s_step %a%t%a%t%a)"
167
	    (node_name n) 
168
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
169
	      (Utils.pp_final_char_if_non_empty " " inputs) 
170
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs)
171
	      (Utils.pp_final_char_if_non_empty " " outputs)
172
	      (Utils.fprintf_list ~sep:" " pp_var) (
173

  
174
	      (rename_current_list m.mname.node_id (full_memory_vars machines i target_machine)) @ 
175
	      (rename_next_list m.mname.node_id (full_memory_vars machines i target_machine)) 
176
	       )
141 177
	    
142 178
	     end
143 179
    end
......
209 245
   Format.fprintf fmt "; %s@." m.mname.node_id;
210 246
   (* Printing variables *)
211 247
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
212
     ((machine_vars m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
248
     ((machine_vars machines m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
213 249
   Format.pp_print_newline fmt ();
214 250
   (* Declaring predicate *)
215 251
   Format.fprintf fmt "(declare-rel %a (%a))@."
216 252
     pp_machine_reset_name m.mname.node_id
217
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mmemory);
253
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));
218 254
   
219 255
   Format.fprintf fmt "(declare-rel %a (%a))@."
220 256
     pp_machine_step_name m.mname.node_id
221
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
257
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m));
222 258
   Format.pp_print_newline fmt ();
223 259

  
224 260
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
225 261
     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
226 262
     m.mname.node_id
227
     (Utils.fprintf_list ~sep:" " pp_var) (rename_next_list m.mname.node_id m.mmemory);
263
     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
264

  
228 265

  
229 266
   Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
230 267
     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
231 268
     m.mname.node_id
232
     (Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
269
     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
233 270
   
234 271
()
235 272
  )
236 273

  
237
let main_print fmt = ()
274
let main_print machines fmt = 
275
if !Options.main_node <> "" then 
276
  begin
277
    let node = !Options.main_node in
278
    let machine = get_machine machines node in
279
    Format.fprintf fmt "; Collecting semantics with main node %s@.@." node;
280
    (* We print the types of the main node "memory tree" TODO: add the output *)
281
    let main_memory_next = 
282
      (rename_next_list machine.mname.node_id (full_memory_vars machines "" machine)) 
283
    in
284
    let main_memory_current = 
285
      (rename_current_list machine.mname.node_id (full_memory_vars machines "" machine)) 
286
    in
287
    Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
288
      (Utils.fprintf_list ~sep:" " pp_type) 
289
      (List.map (fun v -> v.var_type) main_memory_next);
290
    
291
    Format.fprintf fmt "; Initial set@.";
292
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
293
    Format.fprintf fmt "(rule INIT_STATE)@.";
294
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
295
      node
296
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
297
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
298

  
299
    Format.fprintf fmt "; Inductive def@.";
300
    Format.fprintf fmt "(declare-var dummy Bool)@.";
301
    Format.fprintf fmt 
302
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
303
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
304
      node
305
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
306
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next;
307

  
308
    Format.fprintf fmt "; Property def@.";
309
    Format.fprintf fmt "(declare-rel ERR ())@.";
310
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (= top.OK true))@ (MAIN %a)@])@ ERR))@."
311
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current;
312
    Format.fprintf fmt "(query ERR)@.";
313

  
314
    ()
315
end
316

  
238 317

  
239 318
let translate fmt basename prog machines =
240 319
  List.iter (print_machine machines fmt) (List.rev machines);
241
  main_print fmt 
320
  main_print machines fmt 
242 321

  
243 322

  
244 323
(* Local Variables: *)

Also available in: Unified diff