[sledge] Improve consistency of naming Equality pp functions

Summary:
Match the `x` suffix naming convention of Term pp functions that take
a classification function.

Reviewed By: ngorogiannis

Differential Revision: D19282639

fbshipit-source-id: fc340e4bc

sledge/src/symbheap/equality.ml

@@ -430,7 +430,7 @@ let fold_vars r ~init ~f =
 
 let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
 
-let pp_classes x fs r =
+let ppx_classes x fs r =
   List.pp "@ @<2>∧ "
     (fun fs (key, data) ->
       Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) key
@@ -439,7 +439,9 @@ let pp_classes x fs r =
     fs
     (Map.to_alist (classes r))
 
-let pp_classes_diff x fs (r, s) =
+let pp_classes fs r = ppx_classes (fun _ -> None) fs r
+
+let ppx_classes_diff x fs (r, s) =
   let clss = classes s in
   let clss =
     Map.filter_mapi clss ~f:(fun ~key:rep ~data:cls ->

sledge/src/symbheap/equality.mli

@@ -11,8 +11,9 @@
 type t [@@deriving compare, equal, sexp]
 
 val pp : t pp
-val pp_classes : Var.strength -> t pp
+val pp_classes : t pp
-val pp_classes_diff : Var.strength -> (t * t) pp
+val ppx_classes : Var.strength -> t pp
+val ppx_classes_diff : Var.strength -> (t * t) pp
 
 include Invariant.S with type t := t
 

sledge/src/symbheap/equality_test.ml

@@ -14,10 +14,7 @@ let%test_module _ =
     (* let () = Trace.init ~margin:160 ~config:all () *)
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
-
+    let pp_classes = Format.printf "@\n@[<hv>  %a@]@." pp_classes
-    let pp_classes =
-      Format.printf "@\n@[<hv>  %a@]@." (pp_classes (fun _ -> None))
-
     let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add

sledge/src/symbheap/sh.ml

@@ -150,7 +150,7 @@ let rec pp_ ?var_strength vs parent_cong fs {us; xs; cong; pure; heap; djns}
     Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
   let first = Equality.entails parent_cong cong in
   if not first then Format.fprintf fs "  " ;
-  Equality.pp_classes_diff x fs (parent_cong, cong) ;
+  Equality.ppx_classes_diff x fs (parent_cong, cong) ;
   let pure =
     List.filter_map pure ~f:(fun e ->
         let e' = Equality.normalize cong e in