From ecfb5a11167880d9ca00503effce5f52ca204cec Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 2 Feb 2021 04:36:21 -0800
Subject: [PATCH] [sledge] Improve Context tracing

Reviewed By: jvillard

Differential Revision: D25883710

fbshipit-source-id: 4e83cc485
---
 sledge/nonstdlib/map.ml      |  8 +++++---
 sledge/nonstdlib/map_intf.ml |  5 ++++-
 sledge/src/fol/context.ml    | 19 ++++++++-----------
 3 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 0ff64b2f5..61d5ab666 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -228,7 +228,10 @@ end) : S with type key = Key.t = struct
            Format.fprintf fs "@[%a@ @<2>↦ %a@]" pp_k k pp_v v ))
       (Iter.to_list (to_iter m))
 
-  let pp_diff pp_key pp_val pp_diff_val ~eq fs (x, y) =
+  let pp_diff ?(pre = ("[@[<hv>" : (unit, unit) fmt))
+      ?(suf = ("@]];@ " : (unit, unit) fmt))
+      ?(sep = (";@ " : (unit, unit) fmt)) pp_key pp_val pp_diff_val ~eq fs
+      (x, y) =
     let pp_diff_elt fs = function
       | k, `Left v ->
           Format.fprintf fs "-- [@[%a@ @<2>↦ %a@]]" pp_key k pp_val v
@@ -238,6 +241,5 @@ end) : S with type key = Key.t = struct
           Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv
     in
     let sd = Iter.to_list (symmetric_diff ~eq x y) in
-    if not (List.is_empty sd) then
-      Format.fprintf fs "[@[<hv>%a@]];@ " (List.pp ";@ " pp_diff_elt) sd
+    List.pp ~pre ~suf sep pp_diff_elt fs sd
 end
diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml
index fc146c73e..534afd082 100644
--- a/sledge/nonstdlib/map_intf.ml
+++ b/sledge/nonstdlib/map_intf.ml
@@ -146,7 +146,10 @@ module type S = sig
   val pp : key pp -> 'a pp -> 'a t pp
 
   val pp_diff :
-       key pp
+       ?pre:(unit, unit) fmt
+    -> ?suf:(unit, unit) fmt
+    -> ?sep:(unit, unit) fmt
+    -> key pp
     -> 'a pp
     -> ('a * 'a) pp
     -> eq:('a -> 'a -> bool)
diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 9d3d87ebf..483a3f5dc 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -254,8 +254,7 @@ let pp_raw fs {sat; rep; cls; pnd} =
   let pp_trm_v fs (k, v) = if not (Trm.equal k v) then Trm.pp fs v in
   let pp_cls_v fs (_, cls) = Cls.pp_raw fs cls in
   let pp_pnd fs pnd =
-    if not (List.is_empty pnd) then
-      Format.fprintf fs ";@ pnd= @[%a@]" (List.pp ";@ " pp_eq) pnd
+    List.pp ~pre:";@ pnd= [@[" ";@ " ~suf:"@]]" pp_eq fs pnd
   in
   Format.fprintf fs "@[{@[<hv>sat= %b;@ rep= %a;@ cls= %a%a@]}@]" sat
     (pp_alist Trm.pp pp_trm_v)
@@ -269,20 +268,18 @@ let pp_diff fs (r, s) =
       Format.fprintf fs "sat= @[-- %b@ ++ %b@];@ " r.sat s.sat
   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)
+    Trm.Map.pp_diff ~eq:Trm.equal ~pre:"rep= @[" ~sep:";@ " ~suf:"@]" Trm.pp
+      Trm.pp Trm.pp_diff fs (r.rep, s.rep)
   in
   let pp_cls fs =
-    if not (Trm.Map.equal Cls.equal r.cls s.cls) then
-      Format.fprintf fs "cls= %a;@ "
-        (Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp_raw Cls.pp_diff)
-        (r.cls, s.cls)
+    Trm.Map.pp_diff ~eq:Cls.equal ~pre:";@ cls= @[" ~sep:";@ " ~suf:"@]"
+      Trm.pp Cls.pp_raw Cls.pp_diff fs (r.cls, s.cls)
   in
   let pp_pnd fs =
-    List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ~pre:"pnd= @[" ~suf:"@]"
-      ";@ " pp_eq fs (r.pnd, s.pnd)
+    List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ~pre:";@ pnd= [@[" ";@ "
+      ~suf:"@]]" pp_eq fs (r.pnd, s.pnd)
   in
-  Format.fprintf fs "@[{@[<hv>%t%t%t%t@]}@]" pp_sat pp_rep pp_cls pp_pnd
+  Format.fprintf fs "@[{ @[<hv>%t%t%t%t@] }@]" pp_sat pp_rep pp_cls pp_pnd
 
 let ppx_classes x fs clss =
   List.pp "@ @<2>∧ "