[sledge] Refactor: Revise external Context printing API

Summary:
The default printer is `pp_classes`, while `pp` is for debugging the
internal representation manipulation, so it is renamed to `pp_raw`.

Reviewed By: jvillard

Differential Revision: D22571135

fbshipit-source-id: 2d624e279

sledge/src/fol.ml

@@ -1253,7 +1253,6 @@ let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
 module Context = struct
   type t = Ses.Equality.t [@@deriving sexp]
 
-  let pp = Ses.Equality.pp
   let invariant = Ses.Equality.invariant
   let empty = Ses.Equality.true_
 
@@ -1306,6 +1305,9 @@ module Context = struct
         | [] -> None
         | cls -> Some cls )
 
+  (* Pretty printing *)
+
+  let pp_raw = Ses.Equality.pp
   let ppx_cls x = List.pp "@ = " (Term.ppx x)
 
   let ppx_classes x fs clss =
@@ -1315,7 +1317,7 @@ module Context = struct
           (List.sort ~compare:Term.compare cls) )
       fs (Term.Map.to_alist clss)
 
-  let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r)
+  let pp fs r = ppx_classes (fun _ -> None) fs (classes r)
 
   let ppx_diff var_strength fs parent_ctx fml ctx =
     let clss = diff_classes ctx parent_ctx in

sledge/src/fol.mli

@@ -189,7 +189,6 @@ module Context : sig
   type t [@@deriving sexp]
 
   val pp : t pp
-  val pp_classes : t pp
 
   val ppx_diff :
     Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
@@ -280,6 +279,8 @@ module Context : sig
 
   (**/**)
 
+  val pp_raw : t pp
+
   val replay : string -> unit
   (** Replay debugging *)
 end

sledge/src/fol_test.ml

@@ -20,8 +20,8 @@ let%test_module _ =
      * [@@@warning "-32"] *)
 
     let printf pp = Format.printf "@\n%a@." pp
-    let pp = printf pp
+    let pp_raw = printf pp_raw
-    let pp_classes = Format.printf "@\n@[<hv>  %a@]@." pp_classes
+    let pp = Format.printf "@\n@[<hv>  %a@]@." pp
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
     let ( - ) = Term.sub
@@ -75,8 +75,8 @@ let%test_module _ =
     let r9 = of_eqs [(x, z - !16)]
 
     let%expect_test _ =
-      pp_classes r9 ;
       pp r9 ;
+      pp_raw r9 ;
       [%expect
         {|
         (-16 + %z_5) = %x_3
@@ -89,8 +89,8 @@ let%test_module _ =
     let r10 = of_eqs [(!16, z - x)]
 
     let%expect_test _ =
-      pp_classes r10 ;
       pp r10 ;
+      pp_raw r10 ;
       Format.printf "@.%a@." Term.pp (z - (x + !8)) ;
       Format.printf "@.%a@." Term.pp (normalize r10 (z - (x + !8))) ;
       Format.printf "@.%a@." Term.pp (x + !8 - z) ;

sledge/src/sh.ml

@@ -682,8 +682,7 @@ let rec freshen_nested_xs q =
     invariant q']
 
 let rec propagate_context_ ancestor_vs ancestor_ctx q =
-  [%Trace.call fun {pf} ->
+  [%Trace.call fun {pf} -> pf "(%a)@ %a" Context.pp ancestor_ctx pp q]
-    pf "(%a)@ %a" Context.pp_classes ancestor_ctx pp q]
   ;
   (* extend vocabulary with variables in scope above *)
   let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in
@@ -714,8 +713,7 @@ let rec propagate_context_ ancestor_vs ancestor_ctx q =
     invariant q']
 
 let propagate_context ancestor_vs ancestor_ctx q =
-  [%Trace.call fun {pf} ->
+  [%Trace.call fun {pf} -> pf "(%a)@ %a" Context.pp ancestor_ctx pp q]
-    pf "(%a)@ %a" Context.pp_classes ancestor_ctx pp q]
   ;
   propagate_context_ ancestor_vs ancestor_ctx q
   |>