From c815ccf6480a12b39b5b4655fed0b774de84e7d5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 18 Jan 2019 20:24:39 -0600 Subject: [PATCH] refactor: use `pp` instead of `print` --- src/backend/Backend_intf.ml | 2 +- src/backend/Coq.ml | 2 +- src/backend/Dedukti.ml | 6 +++--- src/backend/Dedukti.mli | 2 +- src/backend/Dot.ml | 2 +- src/core/Expr_intf.ml | 4 ++-- src/core/Formula_intf.ml | 2 +- src/core/Solver_types.ml | 21 +++++++-------------- src/main/main.ml | 2 +- src/sat/Expr_sat.ml | 2 +- src/tseitin/Msat_tseitin.ml | 18 +++++++++--------- src/tseitin/Tseitin_intf.ml | 4 ++-- 12 files changed, 30 insertions(+), 37 deletions(-) diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml index 9cfff729..29900a0c 100644 --- a/src/backend/Backend_intf.ml +++ b/src/backend/Backend_intf.ml @@ -20,7 +20,7 @@ module type S = sig type t (** The type of proofs. *) - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> t -> unit (** A function for printing proofs in the desired format. *) end diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index bba56ac7..7f536d67 100644 --- a/src/backend/Coq.ml +++ b/src/backend/Coq.ml @@ -149,7 +149,7 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause (* Here the main idea is to always try and have exactly one goal to prove, i.e False. So each *) - let print fmt p = + let pp fmt p = let h = count_uses p in let aux () node = Format.fprintf fmt "%a" (prove_node h) node diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml index 76c9db7f..46aa96a3 100644 --- a/src/backend/Dedukti.ml +++ b/src/backend/Dedukti.ml @@ -13,7 +13,7 @@ module type Arg = sig type lemma type formula - val print : Format.formatter -> formula -> unit + val pp : Format.formatter -> formula -> unit val prove : Format.formatter -> lemma -> unit val context : Format.formatter -> proof -> unit end @@ -38,7 +38,7 @@ module Make(S : Res.S)(A : Arg with type formula := S.formula S.Atom.lit (S.Atom.neg a), false in fprintf fmt "%s _b %a ->@ %a" - (if pos then "_pos" else "_neg") A.print f aux r + (if pos then "_pos" else "_neg") A.pp f aux r in fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c) @@ -53,7 +53,7 @@ module Make(S : Res.S)(A : Arg with type formula := S.formula fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b."; A.context fmt p - let print fmt p = + let pp fmt p = fprintf fmt "#NAME Proof."; fprintf fmt "(; Dedukti file automatically generated by mSAT ;)"; context fmt p; diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli index 826c8031..bb15697c 100644 --- a/src/backend/Dedukti.mli +++ b/src/backend/Dedukti.mli @@ -19,7 +19,7 @@ module type Arg = sig type proof type formula - val print : Format.formatter -> formula -> unit + val pp : Format.formatter -> formula -> unit val prove : Format.formatter -> lemma -> unit val context : Format.formatter -> proof -> unit end diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index d25f1a09..5a33f054 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -140,7 +140,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom print_contents fmt n; print_edges fmt n - let print fmt p = + let pp fmt p = Format.fprintf fmt "digraph proof {@\n"; S.fold (fun () -> print_node fmt) () p; Format.fprintf fmt "}@." diff --git a/src/core/Expr_intf.ml b/src/core/Expr_intf.ml index 4536d36c..15f9fe99 100644 --- a/src/core/Expr_intf.ml +++ b/src/core/Expr_intf.ml @@ -34,7 +34,7 @@ module type S = sig (** Hashing function for terms. Should be such that two terms equal according to {!val:Expr_intf.S.equal} have the same hash. *) - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> t -> unit (** Printing function used among other for debugging. *) end @@ -52,7 +52,7 @@ module type S = sig (** Hashing function for formulas. Should be such that two formulas equal according to {!val:Expr_intf.S.equal} have the same hash. *) - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> t -> unit (** Printing function used among other thing for debugging. *) val neg : t -> t diff --git a/src/core/Formula_intf.ml b/src/core/Formula_intf.ml index edf8b3ff..26226c91 100644 --- a/src/core/Formula_intf.ml +++ b/src/core/Formula_intf.ml @@ -32,7 +32,7 @@ module type S = sig (** Hashing function for formulas. Should be such that two formulas equal according to {!val:Expr_intf.S.equal} have the same hash. *) - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> t -> unit (** Printing function used among other thing for debugging. *) val neg : t -> t diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index dc73d889..d585f5dd 100644 --- a/src/core/Solver_types.ml +++ b/src/core/Solver_types.ml @@ -151,12 +151,12 @@ module McMake (E : Expr_intf.S) = struct | None -> Format.fprintf fmt "" | Some t -> - Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level E.Term.print t + Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level E.Term.pp t - let pp out v = E.Term.print out v.term + let pp out v = E.Term.pp out v.term let debug out v = Format.fprintf out "%d[%a][lit:@[%a@]]" - (v.lid+1) debug_assign v E.Term.print v.term + (v.lid+1) debug_assign v E.Term.pp v.term end let seen_pos = 0b1 @@ -251,7 +251,7 @@ module McMake (E : Expr_intf.S) = struct | Formula_intf.Negated -> var.na | Formula_intf.Same_sign -> var.pa - let pp fmt a = E.Formula.print fmt a.lit + let pp fmt a = E.Formula.pp fmt a.lit let pp_a fmt v = if Array.length v = 0 then ( @@ -293,7 +293,7 @@ module McMake (E : Expr_intf.S) = struct let debug out a = Format.fprintf out "%s%d[%a][atom:@[%a@]]" - (sign a) (a.var.vid+1) debug_value a E.Formula.print a.lit + (sign a) (a.var.vid+1) debug_value a E.Formula.pp a.lit let debug_a out vec = Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec @@ -400,15 +400,8 @@ module McMake (E : Expr_intf.S) = struct Format.fprintf fmt "%a0" aux atoms end - module Term = struct - include E.Term - let pp = print - end - - module Formula = struct - include E.Formula - let pp = print - end + module Term = E.Term + module Formula = E.Formula end[@@inline] diff --git a/src/main/main.ml b/src/main/main.ml index 28400e72..177b5b32 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -52,7 +52,7 @@ module Process = struct S.Proof.check p; if !p_dot_proof <> "" then begin let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in - D.print fmt p + D.pp fmt p end end; let t' = Sys.time () -. t in diff --git a/src/sat/Expr_sat.ml b/src/sat/Expr_sat.ml index 86fc6242..f41ba5d5 100644 --- a/src/sat/Expr_sat.ml +++ b/src/sat/Expr_sat.ml @@ -60,7 +60,7 @@ let iter: (t -> unit) -> unit = fun f -> done *) -let print fmt a = +let pp fmt a = Format.fprintf fmt "%s%s%d" (if a < 0 then "~" else "") (if a mod 2 = 0 then "v" else "f") diff --git a/src/tseitin/Msat_tseitin.ml b/src/tseitin/Msat_tseitin.ml index e1901aa1..3f162c8d 100644 --- a/src/tseitin/Msat_tseitin.ml +++ b/src/tseitin/Msat_tseitin.ml @@ -25,21 +25,21 @@ module Make (F : Tseitin_intf.Arg) = struct | Lit of atom | Comb of combinator * t list - let rec print fmt phi = + let rec pp fmt phi = match phi with | True -> Format.fprintf fmt "true" - | Lit a -> F.print fmt a + | Lit a -> F.pp fmt a | Comb (Not, [f]) -> - Format.fprintf fmt "not (%a)" print f - | Comb (And, l) -> Format.fprintf fmt "(%a)" (print_list "and") l - | Comb (Or, l) -> Format.fprintf fmt "(%a)" (print_list "or") l + Format.fprintf fmt "not (%a)" pp f + | Comb (And, l) -> Format.fprintf fmt "(%a)" (pp_list "and") l + | Comb (Or, l) -> Format.fprintf fmt "(%a)" (pp_list "or") l | Comb (Imp, [f1; f2]) -> - Format.fprintf fmt "(%a => %a)" print f1 print f2 + Format.fprintf fmt "(%a => %a)" pp f1 pp f2 | _ -> assert false - and print_list sep fmt = function + and pp_list sep fmt = function | [] -> () - | [f] -> print fmt f - | f::l -> Format.fprintf fmt "%a %s %a" print f sep (print_list sep) l + | [f] -> pp fmt f + | f::l -> Format.fprintf fmt "%a %s %a" pp f sep (pp_list sep) l let make comb l = Comb (comb, l) diff --git a/src/tseitin/Tseitin_intf.ml b/src/tseitin/Tseitin_intf.ml index abdfcf63..6ead857f 100644 --- a/src/tseitin/Tseitin_intf.ml +++ b/src/tseitin/Tseitin_intf.ml @@ -28,7 +28,7 @@ module type Arg = sig val fresh : unit -> t (** Generate fresh formulas (that are different from any other). *) - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> t -> unit (** Print the given formula. *) end @@ -80,7 +80,7 @@ module type S = sig list (which is a conjunction) of lists (which are disjunctions) of atomic formulas. *) - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> t -> unit (** [print fmt f] prints the formula on the formatter [fmt].*) end