refactor: use pp instead of print

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

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

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;

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

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 "}@."

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

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

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 "@[<hov>@@%d->@ %a@]" v.l_level E.Term.print t
+        Format.fprintf fmt "@[<hov>@@%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:@[<hov>%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:@[<hov>%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
+  module Term = E.Term
-    include E.Term
+  module Formula = E.Formula
-    let pp = print
-  end
-
-  module Formula = struct
-    include E.Formula
-    let pp = print
-  end
 end[@@inline]
 
 

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

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")

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
+      Format.fprintf fmt "not (%a)" pp f
-    | Comb (And, l) -> Format.fprintf fmt "(%a)" (print_list "and") l
+    | Comb (And, l) -> Format.fprintf fmt "(%a)" (pp_list "and") l
-    | Comb (Or, l) ->  Format.fprintf fmt "(%a)" (print_list "or") 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] -> pp fmt f
-    | f::l -> Format.fprintf fmt "%a %s %a" print f sep (print_list sep) l
+    | f::l -> Format.fprintf fmt "%a %s %a" pp f sep (pp_list sep) l
 
   let make comb l = Comb (comb, l)
 

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