[sledge] Rename Arithmetic.INDETERMINATE.trm to t

Reviewed By: ngorogiannis

Differential Revision: D26250519

fbshipit-source-id: 0a906c83c

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
+    include Multiset.Make (Int) (Trm)
-              (Int)
-              (struct
-                type t = Trm.trm [@@deriving compare, equal, sexp]
-              end)
 
-    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
+  module Poly = Sum
-    type t = Sum.t [@@deriving compare, equal, sexp]
-    type trm = Trm.trm
-  end
-
   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)

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

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 pp : t pp
-  val vars : trm -> var iter
+  val vars : t -> var iter
 end
 
 (** An embedding of arithmetic terms [t] into indeterminates [trm]. *)

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
+  Arithmetic.Representation (Var) (Trm)
-    (Var)
-    (struct
-      include Trm
-
-      type trm = t [@@deriving compare, equal, sexp]
-    end)
 
 and Arith : (Arithmetic.S with type trm := Trm.t with type t = Arith0.t) =
 struct