Project

General

Profile

Revision 949b2e1e src/printers.ml

View differences:

src/printers.ml
274 274
(*   ) *)
275 275

  
276 276

  
277

  
278
let pp_quantifiers fmt (q, vars) =
279
  match q with
280
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
281
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
282

  
283
let pp_eexpr fmt e =
284
  fprintf fmt "%a%t %a"
285
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
286
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
287
    pp_expr e.eexpr_qfexpr
288

  
277 289
let pp_spec fmt spec =
278 290
  fprintf fmt "@[<hov 2>(*@@ ";
279 291
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;

Also available in: Unified diff