From ae5ef09d9e6840bbd6f01bf63fb9637dc5228ae8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 21 Feb 2021 13:18:02 -0800
Subject: [PATCH] [sledge] Reorder Arithmetic interface

Summary: No functional change, just to make the interface easier to read

Reviewed By: jvillard

Differential Revision: D26250513

fbshipit-source-id: f3b07bccc
---
 sledge/src/fol/arithmetic_intf.ml | 54 +++++++++++++++----------------
 1 file changed, 26 insertions(+), 28 deletions(-)

diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index ec813d6bc..192322ab7 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -5,34 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Arithmetic terms *)
-
-(** An embedding of arithmetic terms [t] into indeterminates [trm]. *)
-module type EMBEDDING = sig
-  type t
-  type trm
-
-  val to_trm : t -> trm
-  (** Embedding from [t] to [trm]: [to_trm a] is arithmetic term [a]
-      embedded into an indeterminate term. *)
-
-  val get_arith : trm -> t option
-  (** Partial projection from [trm] to [t]: [get_arith x] is [Some a] iff
-      [x = to_trm a]. *)
-end
-
-(** Indeterminate terms, treated as atomic / variables except when they can
-    be flattened using {!EMBEDDING.get_arith}. *)
-module type TRM = sig
-  include Comparer.S
-
-  val pp : t pp
-
-  type var
-
-  val vars : t -> var iter
-end
-
 (** Arithmetic terms, e.g. polynomials [t] over indeterminate terms [trm] *)
 module type S0 = sig
   type trm
@@ -94,6 +66,32 @@ module type S0 = sig
       [j]. *)
 end
 
+(** An embedding of arithmetic terms [t] into indeterminates [trm]. *)
+module type EMBEDDING = sig
+  type t
+  type trm
+
+  val to_trm : t -> trm
+  (** Embedding from [t] to [trm]: [to_trm a] is arithmetic term [a]
+      embedded into an indeterminate term. *)
+
+  val get_arith : trm -> t option
+  (** Partial projection from [trm] to [t]: [get_arith x] is [Some a] iff
+      [x = to_trm a]. *)
+end
+
+(** Indeterminate terms, treated as atomic / variables except when they can
+    be flattened using {!EMBEDDING.get_arith}. *)
+module type TRM = sig
+  include Comparer.S
+
+  val pp : t pp
+
+  type var
+
+  val vars : t -> var iter
+end
+
 (** Arithmetic terms, where an embedding {!EMBEDDING.get_arith} into
     indeterminate terms is used to implicitly flatten arithmetic terms that
     are embedded into general terms to the underlying arithmetic term. *)