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/basic_library.ml
146 146
let is_stateless_fun x =
147 147
  List.mem x internal_funs
148 148

  
149
let pp_c i pp_val fmt vl =
150
  match i, vl with
151
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
152
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
153
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
154
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
155
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
156
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
157
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
158
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
159
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
160
    | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
161

  
162
let pp_java i pp_val fmt vl =
163
  match i, vl with
164
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
165
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
166
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
167
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
168
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
169
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
170
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
171
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
172
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
173
    | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false)
174

  
175
let pp_horn i pp_val fmt vl =
176
  match i, vl with
177
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
178

  
179
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
180
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
181
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
182
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
183
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
184
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
185
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
186
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
187
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
188
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
189
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
190
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
191
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
192
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
193

  
194
*)
149

  
150
(* let pp_java i pp_val fmt vl = *)
151
(*   match i, vl with *)
152
(*   (\*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *\) *)
153
(*     | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *)
154
(*     | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *)
155
(*     | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *)
156
(*     | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
157
(*     | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *)
158
(*     | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
159
(*     | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *)
160
(*     | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *)
161
(*     | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) *)
162

  
195 163

  
196 164
(* Local Variables: *)
197 165
(* compile-command:"make -C .." *)

Also available in: Unified diff