Project

General

Profile

« Previous | Next » 

Revision ea8f51ae

Added by Pierre-Loïc Garoche about 6 years ago

Basic library printers moved into backend specific printer files

View differences:

src/backends/Horn/horn_backend_printers.ml
112 112
  |_ -> assert false
113 113

  
114 114

  
115
let pp_basic_lib_fun i pp_val fmt vl =
116
  match i, vl with
117
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
118

  
119
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
120
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
121
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
122
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
123
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
124
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
125
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
126
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
127
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
128
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
129
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
130
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
131
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
132
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
133

  
134
*)
135

  
136

  
115 137
(* Prints a value expression [v], with internal function calls only.
116 138
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
117 139
   but an offset suffix may be added for array variables
......
159 181
     if Types.is_array_type v.var_type
160 182
     then assert false
161 183
     else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
162
  | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
184
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val self pp_var)) vl
163 185

  
164 186
(* Prints a [value] indexed by the suffix list [loop_vars] *)
165 187
let rec pp_value_suffix self pp_value fmt value =
166 188
 match value.value_desc with
167 189
 | Fun (n, vl)  ->
168
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
190
   pp_basic_lib_fun n (pp_value_suffix self pp_value) fmt vl
169 191
 |  _            ->
170 192
   pp_horn_val self pp_value fmt value
171 193

  

Also available in: Unified diff