From 5132a46c69b9da291f297a9c077d6d24c9e4e8c1 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 15 Jan 2020 13:17:37 -0800
Subject: [PATCH] [sledge] Add Map.pp and use it for Var. and Equality.Subst.pp

Summary: Just a dedup refactoring.

Reviewed By: ngorogiannis

Differential Revision: D19282642

fbshipit-source-id: d050af84b
---
 sledge/src/import/import.ml     | 6 ++++++
 sledge/src/import/import.mli    | 2 ++
 sledge/src/llair/term.ml        | 7 +------
 sledge/src/symbheap/equality.ml | 6 +-----
 4 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml
index b14977615..5cfef1a1b 100644
--- a/sledge/src/import/import.ml
+++ b/sledge/src/import/import.ml
@@ -239,6 +239,12 @@ end
 module Map = struct
   include Base.Map
 
+  let pp pp_k pp_v fs m =
+    Format.fprintf fs "@[<1>[%a]@]"
+      (List.pp ",@ " (fun fs (k, v) ->
+           Format.fprintf fs "@[%a @<2>↦ %a@]" pp_k k pp_v v ))
+      (to_alist m)
+
   let equal_m__t (module Elt : Compare_m) equal_v = equal equal_v
 
   let find_and_remove m k =
diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli
index 284035966..27bee829f 100644
--- a/sledge/src/import/import.mli
+++ b/sledge/src/import/import.mli
@@ -180,6 +180,8 @@ end
 module Map : sig
   include module type of Base.Map
 
+  val pp : 'k pp -> 'v pp -> ('k, 'v, 'c) t pp
+
   val equal_m__t :
        (module Compare_m)
     -> ('v -> 'v -> bool)
diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 67bb4f433..1fd5aa493 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -361,12 +361,7 @@ module Var = struct
       in
       assert (Set.disjoint domain range)
 
-    let pp fs s =
-      Format.fprintf fs "@[<1>[%a]@]"
-        (List.pp ",@ " (fun fs (k, v) ->
-             Format.fprintf fs "@[%a ↦ %a@]" pp_t k pp_t v ))
-        (Map.to_alist s)
-
+    let pp = Map.pp pp_t pp_t
     let empty = Map.empty
     let is_empty = Map.is_empty
 
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 6f72cab36..c86255e31 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -41,11 +41,7 @@ module Subst : sig
 end = struct
   type t = Term.t Term.Map.t [@@deriving compare, equal, sexp]
 
-  let pp fs s =
-    Format.fprintf fs "@[<1>[%a]@]"
-      (List.pp ",@ " (fun fs (k, v) ->
-           Format.fprintf fs "@[%a ↦ %a@]" Term.pp k Term.pp v ))
-      (Map.to_alist s)
+  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