let rec pp_print_term' db ppf t = match Term.T.node_of_t t with (* Delegate printing of free variables to function in input module *) | Term.T.FreeVar v -> Var.pp_print_var ppf v (* Print bound variable with its de Bruijn index *) | Term.T.BoundVar dbv -> Format.fprintf ppf "X%i" (db - dbv + 1) (* Delegate printing of leaf to function in input module *) | Term.T.Leaf s -> pp_print_symbol ?arity:(Some 0) ppf s (* Print array store *) | Term.T.Node (s, [a; i; v]) when s == Symbol.s_store -> Format.fprintf ppf "@[<hv 1>(%a@ %a (%a)@ %a)@]" (pp_print_symbol ?arity:(Some 3)) s (pp_print_term' db) a (pp_print_term' db) i (pp_print_term' db) v (* Print a function application as S-expression *) | Term.T.Node (s, a) -> Format.fprintf ppf "@[<hv 1>(%a@ %a)@]" (pp_print_symbol ?arity:(Some (List.length a))) s (pp_print_list (pp_print_term' db) "@ ") a (* Print a let binding *) | Term.T.Let (l, b) -> let Term.T.L (x, t) = Term.T.node_of_lambda l in Format.fprintf ppf "@[<hv 1>(let@ @[<hv 1>(%a)@]@ %a)@]" (pp_print_let_bindings 0 db) (b, x) (pp_print_term' (db + List.length b)) t (* Print a universal quantification *) | (Term.T.Forall l | Term.T.Exists l) as nt -> let Term.T.L (x, t) = Term.T.node_of_lambda l in let quant = match nt with | Term.T.Forall _ -> "forall" | Term.T.Exists _ -> "exists" | _ -> assert false in Format.fprintf ppf "@[<hv 1>(%s@ @[<hv 1>(%a)@ %a@])@]" quant (pp_print_typed_var_list db) x (pp_print_term' (db + List.length x)) t | _ -> Term.T.pp_print_term_w pp_print_symbol Var.pp_print_var pp_print_sort ~db ppf t (* Pretty-print a list of variable term bindings *) and pp_print_let_bindings i db ppf = function (* Print nothing for the empty list *) | [], [] -> () (* Print the first binding *) | t :: tl, s :: sl -> (* Increment variable index *) let db' = succ db in (* Print as binding as (Xn t) *) Format.fprintf ppf "@[<hv 1>(X%i::%a@ %a)@]" db' pp_print_type s (pp_print_term' (db - i)) t; (* Add space and recurse if more bindings follow *) if not (tl = []) then (Format.pp_print_space ppf (); pp_print_let_bindings (succ i) db' ppf (tl, sl)) | _ -> assert false