From 8725d5fe81ab676ad8e2156a3d4fd9ca6717d47d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jul 2020 07:44:43 -0700
Subject: [PATCH] [sledge] Refactor: pretty-printing of classes out of Ses to
 Fol

Reviewed By: jvillard

Differential Revision: D22381644

fbshipit-source-id: c5b487769
---
 sledge/src/fol.ml         | 18 +++++++-----------
 sledge/src/sh_test.ml     | 10 ++++++----
 sledge/src/solver_test.ml | 12 ++++++------
 3 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 69e990db6..ef013ccd3 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1183,23 +1183,19 @@ module Context = struct
         let cls' = List.map ~f:of_ses cls in
         Term.Map.set ~key:rep' ~data:cls' clss )
 
-  let classes_to_ses clss =
-    Term.Map.fold clss ~init:Ses.Term.Map.empty
-      ~f:(fun ~key:rep ~data:cls clss ->
-        let rep' = to_ses rep in
-        let cls' = List.map ~f:to_ses cls in
-        Ses.Term.Map.set ~key:rep' ~data:cls' clss )
-
   let classes x = classes_of_ses (Ses.Equality.classes x)
   let diff_classes x y = classes_of_ses (Ses.Equality.diff_classes x y)
   let pp = Ses.Equality.pp
-  let pp_classes = Ses.Equality.pp_classes
+  let ppx_cls x = List.pp "@ = " (Term.ppx x)
 
   let ppx_classes x fs clss =
-    Ses.Equality.ppx_classes
-      (fun v -> x (v_of_ses v))
-      fs (classes_to_ses clss)
+    List.pp "@ @<2>∧ "
+      (fun fs (rep, cls) ->
+        Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep (ppx_cls x)
+          (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 invariant = Ses.Equality.invariant
   let true_ = Ses.Equality.true_
 
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index c6d71dea3..bc8576f07 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -147,11 +147,13 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   %x_6 = %x_6^ ∧ (%y_7 + -1) = %y_7^ ∧ emp
+        ∃ %x_6 .   %x_6 = %x_6^ ∧ ((-1 × 1) + (1 × %y_7)) = %y_7^ ∧ emp
     
-          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = ((-1 × 1) + (1 × %y_7))) ∧ emp
-    
-          (%y_7 + -1) = %y_7^ ∧ emp |}]
+          ((-1 × 1) + (1 × %y_7)) = %y_7^
+        ∧ (%y_7^ = ((-1 × 1) + (1 × %y_7)))
+        ∧ emp
+
+          ((-1 × 1) + (1 × %y_7)) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
       let q =
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index 5c5d63748..9c36ca6d2 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -158,7 +158,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
         ) infer_frame:
-            %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ emp |}]
+            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -174,7 +174,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
         ) infer_frame:
-            %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ emp |}]
+            %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -194,8 +194,8 @@ let%test_module _ =
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
             %a_2 = %a0_10
-          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
+          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
@@ -216,8 +216,8 @@ let%test_module _ =
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
             %a_2 = %a0_10
-          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
+          ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
@@ -249,14 +249,14 @@ let%test_module _ =
                ∧ 16 = %m_8
                ∧ ((16 × 1) + (1 × %l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  %a_3 = _
-               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 1 = %n_9
                ∧ 16 = %m_8
+               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ emp)
             ∨ (  %a_3 = _
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ 0 = %n_9
                ∧ 16 = %m_8
+               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ emp)
             ) |}]