From b741bcd490ebc1e6847b264dac63d5ae5be09888 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jul 2020 08:17:46 -0700
Subject: [PATCH] [sledge] Refactor: Move diff_classes from Equality to Context

Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.

Reviewed By: jvillard

Differential Revision: D22455725

fbshipit-source-id: 6f0059873
---
 sledge/src/fol.ml           | 57 +++++++++++++++++++++++--------------
 sledge/src/ses/equality.ml  |  6 ----
 sledge/src/ses/equality.mli |  4 ---
 3 files changed, 36 insertions(+), 31 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 410a08964..0d14776e4 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1190,28 +1190,8 @@ let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
 
 module Context = struct
   type t = Ses.Equality.t [@@deriving sexp]
-  type classes = exp list Term.Map.t
 
-  let classes_of_ses clss =
-    Ses.Term.Map.fold clss ~init:Term.Map.empty
-      ~f:(fun ~key:rep ~data:cls clss ->
-        let rep' = of_ses rep in
-        let cls' = List.map ~f:of_ses cls in
-        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 ppx_cls x = List.pp "@ = " (Term.ppx x)
-
-  let ppx_classes x fs 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_
 
@@ -1232,7 +1212,6 @@ module Context = struct
   let is_true x = Ses.Equality.is_true x
   let is_false x = Ses.Equality.is_false x
   let entails_eq x e f = Ses.Equality.entails_eq x (to_ses e) (to_ses f)
-  let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e))
   let normalize x e = ses_map (Ses.Equality.normalize x) e
   let normalizef x e = f_ses_map (Ses.Equality.normalize x) e
   let difference x e f = Ses.Equality.difference x (to_ses e) (to_ses f)
@@ -1240,6 +1219,42 @@ module Context = struct
   let fold_terms ~init x ~f =
     Ses.Equality.fold_terms x ~init ~f:(fun s e -> f s (of_ses e))
 
+  (* Classes *)
+
+  let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e))
+
+  type classes = exp list Term.Map.t
+
+  let classes_of_ses clss =
+    Ses.Term.Map.fold clss ~init:Term.Map.empty
+      ~f:(fun ~key:rep ~data:cls clss ->
+        let rep' = of_ses rep in
+        let cls' = List.map ~f:of_ses cls in
+        Term.Map.set ~key:rep' ~data:cls' clss )
+
+  let classes x = classes_of_ses (Ses.Equality.classes x)
+
+  let diff_classes r s =
+    Term.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls ->
+        match
+          List.filter cls ~f:(fun exp -> not (entails_eq s rep exp))
+        with
+        | [] -> None
+        | cls -> Some cls )
+
+  let ppx_cls x = List.pp "@ = " (Term.ppx x)
+
+  let ppx_classes x fs 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)
+
+  (* Substs *)
+
   module Subst = struct
     type t = Ses.Equality.Subst.t [@@deriving sexp]
 
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index d47cfe2a1..afa8850cb 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -710,12 +710,6 @@ let fold_vars r ~init ~f =
 
 let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
 
-let diff_classes r s =
-  Term.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls ->
-      match List.filter cls ~f:(fun exp -> not (entails_eq s rep exp)) with
-      | [] -> None
-      | cls -> Some cls )
-
 (** Existential Witnessing and Elimination *)
 
 let subst_invariant us s0 s =
diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli
index b608a477c..6760c4e59 100644
--- a/sledge/src/ses/equality.mli
+++ b/sledge/src/ses/equality.mli
@@ -20,10 +20,6 @@ val classes : t -> classes
 (** [classes r] maps each equivalence class representative to the other
     terms [r] proves equal to it. *)
 
-val diff_classes : t -> t -> classes
-(** [diff_classes r s] is the equality classes of [r] omitting equalities in
-    [s]. *)
-
 val pp : t pp
 val pp_classes : t pp
 val ppx_classes : Var.strength -> classes pp