[sledge] Parameterize Var.strength over type of variables

Summary: Hopefully only transitional until Fol.Var and Ses.Var are conflated.

Reviewed By: jvillard

Differential Revision: D24306039

fbshipit-source-id: 5c3be8d4d

sledge/src/fol.mli

@@ -31,7 +31,7 @@ module rec Term : sig
   type t [@@deriving compare, equal, sexp]
 
   (* pretty-printing *)
-  val ppx : Var.strength -> t pp
+  val ppx : Var.t Var.strength -> t pp
   val pp : t pp
 
   module Map : Map.S with type key := t
@@ -104,7 +104,7 @@ and Formula : sig
   val project : Term.t -> t option
 
   (* pretty-printing *)
-  val ppx : Var.strength -> t pp
+  val ppx : Var.t Var.strength -> t pp
   val pp : t pp
 
   (** Construct *)
@@ -170,7 +170,7 @@ module Context : sig
   val pp : t pp
 
   val ppx_diff :
-    Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
+    Var.t 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.strength -> classes pp
+val ppx_classes : Var.t 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.strength -> t pp
+val ppx : Var.t 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 strength = t -> [`Universal | `Existential | `Anonymous] option
+  type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
 
   let ppx strength ppf v =
     let id = id v in

sledge/src/ses/var_intf.ml

@@ -15,9 +15,9 @@ end
 
 module type VAR = sig
   type t [@@deriving compare, equal, sexp]
-  type strength = t -> [`Universal | `Existential | `Anonymous] option
+  type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
 
-  val ppx : strength -> t pp
+  val ppx : t strength -> t pp
   val pp : t pp
 
   module Map : sig
@@ -27,11 +27,13 @@ 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 : strength -> t pp
+    val ppx : var strength -> t pp
     val pp : t pp
     val pp_xs : t pp
   end