Project

General

Profile

Revision c76f1d66 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)
33
let rename_machine_list p = List.map (rename_machine p)
34
    
31 35
let rename f = (fun v -> {v with var_id = f v.var_id } )
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)
36
let rename_current =  rename (fun n -> n ^ "_c")
37
let rename_current_list = List.map rename_current
38
let rename_next = rename (fun n -> n ^ "_x")
39
let rename_next_list = List.map rename_next
40

  
38 41

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

  
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) @
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 48
      List.fold_left (fun accu (id, (n, _)) -> 
47 49
	let name = node_name n in 
48 50
	if name = "_arrow" then accu else
49 51
	  let machine_n = get_machine machines name in
50
	( aux (pref id) machine_n ) @ accu
52
	( aux false (prefix_s ^ "." ^ id) machine_n ) @ accu
51 53
      ) [] (m.minstances) 
52 54
  in
53
  aux prefix machine
55
  aux true machine.mname.node_id machine
54 56

  
55 57
let machine_vars machines m = 
56 58
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
57 59
    (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
    (rename_current_list (full_memory_vars machines m)) @ 
61
    (rename_next_list (full_memory_vars machines m)) 
60 62

  
61 63
let step_vars machines m = 
62 64
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
63 65
    (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
    (rename_current_list (full_memory_vars machines m)) @ 
67
    (rename_next_list (full_memory_vars machines m)) 
66 68

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

  
72
    (rename_next_list (full_memory_vars machines m)) 
72 73
  
73 74
(********************************************************************************************)
74 75
(*                    Instruction Printing functions                                        *)
......
110 111
      if Types.is_array_type v.var_type
111 112
      then assert false 
112 113
      else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
113
    | Fun (n, vl)   -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
114
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
114 115

  
115 116
(* Prints a [value] indexed by the suffix list [loop_vars] *)
116 117
let rec pp_value_suffix self pp_value fmt value =

Also available in: Unified diff