[sledge] Simplify handling of Var.strength

Summary:
Instead of passing the Var.strength across interfaces, pass the Trm.pp
partially applied to the Var.strength. This hides the type of
Var.strength, and thereby removes the need for `Arithmetic.S.var`.

Reviewed By: jvillard

Differential Revision: D26250516

fbshipit-source-id: 64dbd3870

sledge/src/fol/arithmetic.ml

@@ -29,10 +29,10 @@ struct
 
     let num_den m = Prod.partition m ~f:(fun _ i -> i >= 0)
 
-    let ppx strength ppf power_product =
+    let ppx pp_trm ppf power_product =
       let pp_factor ppf (indet, exponent) =
-        if exponent = 1 then (Trm.ppx strength) ppf indet
+        if exponent = 1 then pp_trm ppf indet
-        else Format.fprintf ppf "%a^%i" (Trm.ppx strength) indet exponent
+        else Format.fprintf ppf "%a^%i" pp_trm indet exponent
       in
       let pp_num ppf num =
         if Prod.is_empty num then Trace.pp_styled `Magenta "1" ppf
@@ -49,7 +49,7 @@ struct
         Format.fprintf ppf "@[<2>%a@]" pp_num num
       else Format.fprintf ppf "@[<2>(%a%a)@]" pp_num num pp_den den
 
-    let pp = ppx (fun _ -> None)
+    let pp = ppx Trm.pp
 
     (** [one] is the empty product Πᵢ₌₁⁰ xᵢ^pᵢ *)
     let one = Prod.empty
@@ -99,14 +99,14 @@ struct
   struct
     include Poly
 
-    let ppx strength ppf poly =
+    let ppx pp_trm ppf poly =
       if Sum.is_empty poly then Trace.pp_styled `Magenta "0" ppf
       else
         let pp_coeff_mono ppf (m, c) =
           if Mono.equal_one m then Trace.pp_styled `Magenta "%a" ppf Q.pp c
           else if Q.equal Q.one c then
-            Format.fprintf ppf "%a" (Mono.ppx strength) m
+            Format.fprintf ppf "%a" (Mono.ppx pp_trm) m
-          else Format.fprintf ppf "%a@<1>×%a" Q.pp c (Mono.ppx strength) m
+          else Format.fprintf ppf "%a@<1>×%a" Q.pp c (Mono.ppx pp_trm) m
         in
         if Sum.is_singleton poly then
           Format.fprintf ppf "@[<2>%a@]" (Sum.pp "@ + " pp_coeff_mono) poly
@@ -115,7 +115,7 @@ struct
             (Sum.pp "@ + " pp_coeff_mono)
             poly
 
-    let pp = ppx (fun _ -> None)
+    let pp = ppx Trm.pp
 
     let mono_invariant mono =
       let@ () = Invariant.invariant [%here] mono [%sexp_of: Mono.t] in

sledge/src/fol/arithmetic_intf.ml

@@ -8,11 +8,10 @@
 (** Arithmetic terms *)
 
 module type S = sig
-  type var
   type trm
   type t [@@deriving compare, equal, sexp]
 
-  val ppx : var Var_intf.strength -> t pp
+  val ppx : trm pp -> t pp
 
   (** Construct and Destruct atomic terms *)
 
@@ -87,7 +86,6 @@ module type INDETERMINATE = sig
   type trm [@@deriving compare, equal, sexp]
   type var
 
-  val ppx : var Var_intf.strength -> trm pp
   val pp : trm pp
   val vars : trm -> var iter
 end
@@ -118,5 +116,5 @@ module type REPRESENTATION = sig
   type trm
 
   module Make (_ : EMBEDDING with type trm := trm and type t := t) :
-    S with type var := var with type trm := trm with type t := t
+    S with type trm := trm with type t := t
 end

sledge/src/fol/fml.ml

@@ -20,7 +20,7 @@ let pp_boxed fs fmt =
 
 let ppx strength fs fml =
   let pp_t = Trm.ppx strength in
-  let pp_a = Trm.Arith.ppx strength in
+  let pp_a = Trm.Arith.ppx pp_t in
   let rec pp fs fml =
     let pf fmt = pp_boxed fs fmt in
     let pp_binop x = pf "(%a@ @<2>%s %a)" x in

sledge/src/fol/trm.ml

@@ -48,11 +48,8 @@ and Arith0 :
       type trm = t [@@deriving compare, equal, sexp]
     end)
 
-and Arith :
+and Arith : (Arithmetic.S with type trm := Trm.t with type t = Arith0.t) =
-  (Arithmetic.S
+struct
-    with type var := Var.t
-    with type trm := Trm.t
-    with type t = Arith0.t) = struct
   include Arith0
 
   include Make (struct
@@ -161,7 +158,7 @@ end = struct
       | Var _ as v -> Var.ppx strength fs (Var.of_ v)
       | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
       | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
-      | Arith a -> Arith.ppx strength fs a
+      | Arith a -> Arith.ppx (ppx strength) fs a
       | Splat x -> pf "%a^" pp x
       | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
       | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len

sledge/src/fol/trm.mli

@@ -34,8 +34,7 @@ module Var : sig
   val of_trm : trm -> t option
 end
 
-module Arith :
+module Arith : Arithmetic.S with type trm := t with type t = arith
-  Arithmetic.S with type var := Var.t with type trm := t with type t = arith
 
 module Set : sig
   include Set.S with type elt := t

sledge/src/fol/var0.ml

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

sledge/src/fol/var_intf.ml

@@ -13,11 +13,9 @@ 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 nonrec strength = t strength
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
 
   val ppx : strength -> t pp
   val pp : t pp