Project

General

Profile

Revision 86ae18b7 src/backends/Horn/horn_backend_common.ml

View differences:

src/backends/Horn/horn_backend_common.ml
25 25
  | Types.Treal           -> fprintf fmt "Real"
26 26
  | Types.Tconst ty       -> pp_print_string fmt ty
27 27
  | Types.Tclock t        -> pp_type fmt t
28
  | Types.Tarray _
29
  | Types.Tstatic _
28
  | Types.Tarray(dim,ty)   -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
29
  | Types.Tstatic(d, ty)-> pp_type fmt ty
30 30
  | Types.Tarrow _
31 31
  | _                     -> eprintf "internal error: pp_type %a@."
32 32
    Types.print_ty t; assert false
......
69 69

  
70 70
let local_memory_vars machines machine =
71 71
  rename_machine_list machine.mname.node_id machine.mmemory
72
    
72

  
73 73
let instances_memory_vars ?(without_arrow=false) machines machine =
74 74
  let rec aux fst prefix m =
75 75
    (
......
81 81
      List.fold_left (fun accu (id, (n, _)) ->
82 82
	let name = node_name n in
83 83
	if without_arrow && name = "_arrow" then
84
	  accu 
84
	  accu
85 85
	else
86 86
	  let machine_n = get_machine machines name in
87
	  ( aux false (concat prefix 
87
	  ( aux false (concat prefix
88 88
			 (if fst then id else concat m.mname.node_id id))
89 89
	      machine_n ) @ accu
90 90
      ) [] (m.minstances)
......
101 101

  
102 102
let step_vars machines m =
103 103
  (inout_vars machines m)
104
  @ (rename_current_list (full_memory_vars machines m)) 
104
  @ (rename_current_list (full_memory_vars machines m))
105 105
  @ (rename_next_list (full_memory_vars machines m))
106 106

  
107 107
let step_vars_m_x machines m =
108 108
  (inout_vars machines m)
109
  @ (rename_mid_list (full_memory_vars machines m)) 
109
  @ (rename_mid_list (full_memory_vars machines m))
110 110
  @ (rename_next_list (full_memory_vars machines m))
111 111

  
112 112
let reset_vars machines m =
113
  (rename_current_list (full_memory_vars machines m)) 
113
  (rename_current_list (full_memory_vars machines m))
114 114
  @ (rename_mid_list (full_memory_vars machines m))
115 115

  
116 116

  

Also available in: Unified diff