From 781280faf1fc5d4ed0a2f64b84f9e95d020fff25 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 9 Feb 2021 04:23:18 -0800
Subject: [PATCH] [sledge] Rename Arithmetic.INDETERMINATE.trm to t

Reviewed By: ngorogiannis

Differential Revision: D26250519

fbshipit-source-id: 0a906c83c
---
 sledge/src/fol/arithmetic.ml      | 20 ++++++--------------
 sledge/src/fol/arithmetic.mli     |  2 +-
 sledge/src/fol/arithmetic_intf.ml |  6 +++---
 sledge/src/fol/trm.ml             |  8 +-------
 4 files changed, 11 insertions(+), 25 deletions(-)

diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index d9d90c305..14701863b 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -15,13 +15,9 @@ module Representation
     (Trm : INDETERMINATE with type var := Var.t) =
 struct
   module Prod = struct
-    include Multiset.Make
-              (Int)
-              (struct
-                type t = Trm.trm [@@deriving compare, equal, sexp]
-              end)
+    include Multiset.Make (Int) (Trm)
 
-    let t_of_sexp = t_of_sexp Trm.trm_of_sexp
+    let t_of_sexp = t_of_sexp Trm.t_of_sexp
   end
 
   module Mono = struct
@@ -88,14 +84,10 @@ struct
     let t_of_sexp = t_of_sexp Mono.t_of_sexp
   end
 
-  module Poly = struct
-    type t = Sum.t [@@deriving compare, equal, sexp]
-    type trm = Trm.trm
-  end
-
+  module Poly = Sum
   include Poly
 
-  module Make (Embed : EMBEDDING with type trm := Trm.trm and type t := t) =
+  module Make (Embed : EMBEDDING with type trm := Trm.t and type t := t) =
   struct
     include Poly
 
@@ -167,7 +159,7 @@ struct
 
     (* projections and embeddings *)
 
-    type kind = Trm of trm | Const of Q.t | Interpreted | Uninterpreted
+    type kind = Trm of Trm.t | Const of Q.t | Interpreted | Uninterpreted
 
     let classify poly =
       match Sum.classify poly with
@@ -209,7 +201,7 @@ struct
       (** Monomials [Mono.t] have [trm] indeterminates, which include, via
           [get_arith], polynomials [t] over monomials themselves. To avoid
           redundant representations, singleton polynomials are flattened. *)
-      let of_trm : ?power:int -> trm -> t =
+      let of_trm : ?power:int -> Trm.t -> t =
        fun ?(power = 1) base ->
         [%trace]
           ~call:(fun {pf} -> pf "@ %a^%i" Trm.pp base power)
diff --git a/sledge/src/fol/arithmetic.mli b/sledge/src/fol/arithmetic.mli
index 58edc93e2..4c38d1c27 100644
--- a/sledge/src/fol/arithmetic.mli
+++ b/sledge/src/fol/arithmetic.mli
@@ -13,4 +13,4 @@ include module type of Arithmetic_intf
 module Representation
     (Var : VAR)
     (Indeterminate : INDETERMINATE with type var := Var.t) :
-  REPRESENTATION with type var := Var.t with type trm := Indeterminate.trm
+  REPRESENTATION with type var := Var.t with type trm := Indeterminate.t
diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index 108ddc353..753fa7861 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -83,11 +83,11 @@ end
 (** Indeterminate terms, treated as atomic / variables except when they can
     be flattened using [EMBEDDING.get_arith]. *)
 module type INDETERMINATE = sig
-  type trm [@@deriving compare, equal, sexp]
+  type t [@@deriving compare, equal, sexp]
   type var
 
-  val pp : trm pp
-  val vars : trm -> var iter
+  val pp : t pp
+  val vars : t -> var iter
 end
 
 (** An embedding of arithmetic terms [t] into indeterminates [trm]. *)
diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index 96003407a..4ae5918d6 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -40,13 +40,7 @@ end
 
 and Arith0 :
   (Arithmetic.REPRESENTATION with type var := Var.t with type trm := Trm.t) =
-  Arithmetic.Representation
-    (Var)
-    (struct
-      include Trm
-
-      type trm = t [@@deriving compare, equal, sexp]
-    end)
+  Arithmetic.Representation (Var) (Trm)
 
 and Arith : (Arithmetic.S with type trm := Trm.t with type t = Arith0.t) =
 struct