[sledge] Refactor pp_diff from Equality to Map and List

Summary: In preparation for more uses.

Reviewed By: ngorogiannis

Differential Revision: D19282643

fbshipit-source-id: f3f78f59c

sledge/src/import/import.ml

@@ -234,6 +234,14 @@ module List = struct
       | [], ys -> map ~f:Either.second ys
     in
     symmetric_diff_ (sort ~compare xs) (sort ~compare ys)
+
+  let pp_diff ~compare sep pp_elt fs (xs, ys) =
+    let pp_diff_elt fs elt =
+      match (elt : _ Either.t) with
+      | First x -> Format.fprintf fs "-- %a" pp_elt x
+      | Second y -> Format.fprintf fs "++ %a" pp_elt y
+    in
+    pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
 end
 
 module Map = struct
@@ -245,6 +253,19 @@ module Map = struct
            Format.fprintf fs "@[%a @<2>↦ %a@]" pp_k k pp_v v ))
       (to_alist m)
 
+  let pp_diff ~data_equal pp_key pp_val pp_diff_val fs (x, y) =
+    let pp_diff_elt fs = function
+      | k, `Left v ->
+          Format.fprintf fs "-- [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
+      | k, `Right v ->
+          Format.fprintf fs "++ [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
+      | k, `Unequal vv ->
+          Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv
+    in
+    let sd = Sequence.to_list (symmetric_diff ~data_equal x y) in
+    if not (List.is_empty sd) then
+      Format.fprintf fs "[@[<hv>%a@]];@ " (List.pp ";@ " pp_diff_elt) sd
+
   let equal_m__t (module Elt : Compare_m) equal_v = equal equal_v
 
   let find_and_remove m k =

sledge/src/import/import.mli

@@ -148,6 +148,12 @@ module List : sig
     -> 'a list pp
   (** Pretty-print a list. *)
 
+  val pp_diff :
+       compare:('a -> 'a -> int)
+    -> (unit, unit) fmt
+    -> 'a pp
+    -> ('a list * 'a list) pp
+
   val pop_exn : 'a list -> 'a * 'a list
 
   val find_map_remove :
@@ -182,6 +188,13 @@ module Map : sig
 
   val pp : 'k pp -> 'v pp -> ('k, 'v, 'c) t pp
 
+  val pp_diff :
+       data_equal:('v -> 'v -> bool)
+    -> 'k pp
+    -> 'v pp
+    -> ('v * 'v) pp
+    -> (('k, 'v, 'c) t * ('k, 'v, 'c) t) pp
+
   val equal_m__t :
        (module Compare_m)
     -> ('v -> 'v -> bool)

sledge/src/llair/term.ml

@@ -227,6 +227,7 @@ and pp_record strength fs elts =
 
 let pp = ppx (fun _ -> None)
 let pp_t = pp
+let pp_diff fs (x, y) = Format.fprintf fs "-- %a ++ %a" pp x pp y
 
 (** Invariant *)
 

sledge/src/llair/term.mli

@@ -155,6 +155,7 @@ end
 val comparator : (t, comparator_witness) Comparator.t
 val ppx : Var.strength -> t pp
 val pp : t pp
+val pp_diff : (t * t) pp
 val invariant : t -> unit
 
 (** Construct *)

sledge/src/symbheap/equality.ml

@@ -24,8 +24,9 @@ module Subst : sig
   type t [@@deriving compare, equal, sexp]
 
   val pp : t pp
-  val pp_sdiff : ?pre:string -> Format.formatter -> t -> t -> unit
+  val pp_diff : (t * t) pp
   val empty : t
+  val is_empty : t -> bool
   val length : t -> int
   val mem : t -> Term.t -> bool
   val fold : t -> init:'a -> f:(key:Term.t -> data:Term.t -> 'a -> 'a) -> 'a
@@ -43,30 +44,11 @@ end = struct
 
   let pp = Map.pp Term.pp Term.pp
 
-  let pp_sdiff ?(pre = "") =
-    let pp_sdiff_elt pp_key pp_val pp_sdiff_val fs = function
-      | k, `Left v ->
-          Format.fprintf fs "-- [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
-      | k, `Right v ->
-          Format.fprintf fs "++ [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
-      | k, `Unequal vv ->
-          Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_sdiff_val vv
-    in
-    let pp_sdiff_map pp_elt_diff equal fs x y =
-      let sd =
-        Sequence.to_list (Map.symmetric_diff ~data_equal:equal x y)
-      in
-      if not (List.is_empty sd) then
-        Format.fprintf fs "%s[@[<hv>%a@]];@ " pre
-          (List.pp ";@ " pp_elt_diff)
-          sd
-    in
-    let pp_sdiff_term fs (u, v) =
-      Format.fprintf fs "-- %a ++ %a" Term.pp u Term.pp v
-    in
-    pp_sdiff_map (pp_sdiff_elt Term.pp Term.pp pp_sdiff_term) Term.equal
+  let pp_diff =
+    Map.pp_diff ~data_equal:Term.equal Term.pp Term.pp Term.pp_diff
 
   let empty = Term.Map.empty
+  let is_empty = Map.is_empty
   let length = Map.length
   let mem = Map.mem
   let fold = Map.fold
@@ -222,7 +204,10 @@ let pp_diff fs (r, s) =
     if not (Bool.equal r.sat s.sat) then
       Format.fprintf fs "sat= @[-- %b@ ++ %b@];@ " r.sat s.sat
   in
-  let pp_rep fs = Subst.pp_sdiff ~pre:"rep= " fs r.rep s.rep in
+  let pp_rep fs =
+    if not (Subst.is_empty r.rep) then
+      Format.fprintf fs "rep= %a" Subst.pp_diff (r.rep, s.rep)
+  in
   Format.fprintf fs "@[{@[<hv>%t%t@]}@]" pp_sat pp_rep
 
 (** Invariant *)