[sledge] Simplify Var.strength type

Summary: It can be made non-parametric

Reviewed By: ngorogiannis

Differential Revision: D24532339

fbshipit-source-id: 9a9312736

sledge/src/arithmetic_intf.ml

@@ -7,14 +7,12 @@
 
 (** Arithmetic terms *)
 
-module Var = Ses.Var
-
 module type S = sig
   type var
   type trm
   type t [@@deriving compare, equal, sexp]
 
-  val ppx : var Var.strength -> t pp
+  val ppx : var Ses.Var_intf.strength -> t pp
 
   (** Construct and Destruct atomic terms *)
 
@@ -89,7 +87,7 @@ module type INDETERMINATE = sig
   type trm [@@deriving compare, equal, sexp]
   type var
 
-  val ppx : var Var.strength -> trm pp
+  val ppx : var Ses.Var_intf.strength -> trm pp
   val pp : trm pp
   val vars : trm -> var iter
 end

sledge/src/fml.mli

@@ -33,7 +33,7 @@ module Set : sig
   val t_of_sexp : Sexp.t -> t
 end
 
-val ppx : Var.t Var.strength -> t pp
+val ppx : Var.strength -> t pp
 val pp : t pp
 
 (** Construct *)

sledge/src/fol.mli

@@ -10,7 +10,7 @@ module rec Term : sig
   type t [@@deriving compare, equal, sexp]
 
   (* pretty-printing *)
-  val ppx : Var.t Var.strength -> t pp
+  val ppx : Var.strength -> t pp
   val pp : t pp
 
   module Map : Map.S with type key := t
@@ -88,7 +88,7 @@ and Formula : sig
   val project : Term.t -> t option
 
   (* pretty-printing *)
-  val ppx : Var.t Var.strength -> t pp
+  val ppx : Var.strength -> t pp
   val pp : t pp
 
   (** Construct *)
@@ -147,7 +147,7 @@ module Context : sig
   val pp : t pp
 
   val ppx_diff :
-    Var.t Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
+    Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
 
   include Invariant.S with type t := t
 

sledge/src/ses/equality.mli

@@ -22,7 +22,7 @@ val classes : t -> classes
 
 val pp : t pp
 val pp_classes : t pp
-val ppx_classes : Var.t Var.strength -> classes pp
+val ppx_classes : Var.strength -> classes pp
 
 include Invariant.S with type t := t
 

sledge/src/ses/term.mli

@@ -106,7 +106,7 @@ module Map : sig
   val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
 end
 
-val ppx : Var.t Var.strength -> t pp
+val ppx : Var.strength -> t pp
 val pp : t pp
 val pp_diff : (t * t) pp
 val invariant : t -> unit

sledge/src/ses/var0.ml

@@ -11,7 +11,7 @@ open Var_intf
 module Make (T : REPR) = struct
   include T
 
-  type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
+  type nonrec strength = t strength
 
   let ppx strength ppf v =
     let id = id v in

sledge/src/ses/var_intf.ml

@@ -13,11 +13,13 @@ module type REPR = sig
   val name : t -> string
 end
 
+type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
+
 module type VAR = sig
   type t [@@deriving compare, equal, sexp]
-  type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
+  type nonrec strength = t strength
 
-  val ppx : t strength -> t pp
+  val ppx : strength -> t pp
   val pp : t pp
 
   module Map : sig
@@ -27,13 +29,11 @@ module type VAR = sig
   end
 
   module Set : sig
-    type var := t
-
     include NS.Set.S with type elt := t
 
     val sexp_of_t : t -> Sexp.t
     val t_of_sexp : Sexp.t -> t
-    val ppx : var strength -> t pp
+    val ppx : strength -> t pp
     val pp : t pp
     val pp_xs : t pp
   end

sledge/src/trm.ml

@@ -89,7 +89,7 @@ and Trm : sig
     | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
 
-  val ppx : Var.t Var.strength -> t pp
+  val ppx : Var.strength -> t pp
   val pp : t pp
   val _Var : int -> string -> t
   val _Z : Z.t -> t

sledge/src/trm.mli

@@ -41,7 +41,7 @@ end
 module Arith :
   Arithmetic.S with type var := Var.t with type trm := t with type t = arith
 
-val ppx : Var.t Var.strength -> t pp
+val ppx : Var.strength -> t pp
 
 (** Construct *)