From 53a1160bdb0b0f1656cf481d7fece947aad1073e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 4 Sep 2020 13:36:56 -0700
Subject: [PATCH] [sledge] Refactor: Reorder Context definitions

Summary: To reduce upcoming diffs.

Reviewed By: ngorogiannis

Differential Revision: D23459516

fbshipit-source-id: 1cddde9ff
---
 sledge/src/fol.ml  | 39 ++++++++++++++++++++++-----------------
 sledge/src/fol.mli |  8 ++++----
 2 files changed, 26 insertions(+), 21 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 2a634f1ae..557d18923 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1452,21 +1452,13 @@ module Context = struct
   type t = Ses.Equality.t [@@deriving sexp]
 
   let invariant = Ses.Equality.invariant
-  let empty = Ses.Equality.true_
-
-  let add vs f x =
-    let vs', x' = Ses.Equality.and_term (vs_to_ses vs) (f_to_ses f) x in
-    (vs_of_ses vs', x')
 
-  let union vs x y =
-    let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
-    (vs_of_ses vs', z)
+  (* Query *)
 
-  let interN vs xs =
-    let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
-    (vs_of_ses vs', z)
+  let fold_vars ~init x ~f =
+    Ses.Equality.fold_vars x ~init ~f:(fun s v -> f s (v_of_ses v))
 
-  let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
+  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
   let is_empty x = Ses.Equality.is_true x
   let is_unsat x = Ses.Equality.is_false x
   let implies x b = Ses.Equality.implies x (f_to_ses b)
@@ -1476,11 +1468,6 @@ module Context = struct
 
   let normalize x e = ses_map (Ses.Equality.normalize x) e
 
-  let fold_vars ~init x ~f =
-    Ses.Equality.fold_vars x ~init ~f:(fun s v -> f s (v_of_ses v))
-
-  let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
-
   (* Classes *)
 
   let class_of x e = List.map ~f:of_ses (Ses.Equality.class_of x (to_ses e))
@@ -1534,6 +1521,24 @@ module Context = struct
       fs fml ~suf:"@]" ;
     first && List.is_empty fml
 
+  (* Construct *)
+
+  let empty = Ses.Equality.true_
+
+  let add vs f x =
+    let vs', x' = Ses.Equality.and_term (vs_to_ses vs) (f_to_ses f) x in
+    (vs_of_ses vs', x')
+
+  let union vs x y =
+    let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
+    (vs_of_ses vs', z)
+
+  let interN vs xs =
+    let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
+    (vs_of_ses vs', z)
+
+  let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
+
   (* Substs *)
 
   module Subst = struct
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index bc94ceb33..d7982c8b6 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -227,15 +227,15 @@ module Context : sig
   (** Holds only if a formula is inconsistent with a context of assumptions,
       that is, conjoining the formula to the assumptions is unsatisfiable. *)
 
-  val class_of : t -> Term.t -> Term.t list
-  (** Equivalence class of [e]: all the terms [f] in the context such that
-      [e = f] is implied by the assumptions. *)
-
   val normalize : t -> Term.t -> Term.t
   (** Normalize a term [e] to [e'] such that [e = e'] is implied by the
       assumptions, where [e'] and its subterms are expressed in terms of the
       canonical representatives of each equivalence class. *)
 
+  val class_of : t -> Term.t -> Term.t list
+  (** Equivalence class of [e]: all the terms [f] in the context such that
+      [e = f] is implied by the assumptions. *)
+
   val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
   (** Enumerate the variables occurring in the terms of the context. *)