[sledge] Rework propositional formula definition to avoid recursive modules

Summary:
Similarly to terms, use the Comparar interface of Sets to defined
formulas using recursive types instead of recursive modules.

Reviewed By: jvillard

Differential Revision: D26250512

fbshipit-source-id: 84f0ae8c0

sledge/src/fol/fml.ml

@@ -9,9 +9,6 @@
 
 module Prop = Propositional.Make (Trm)
 module Set = Prop.Fmls
-
-type set = Set.t
-
 include Prop.Fml
 
 let pp_boxed fs fmt =

sledge/src/fol/propositional.ml

@@ -13,33 +13,40 @@ module Make (Trm : sig
   type t [@@deriving compare, equal, sexp]
 end) =
 struct
-  (** Sets of formulas *)
+  module Fml1 = struct
-  module rec Fmls : (FORMULA_SET with type elt := Fml.t) = struct
+    type compare [@@deriving compare, equal, sexp]
-    module T = struct
-      type t = Fml.t [@@deriving compare, equal, sexp]
-    end
-
-    include Set.Make (T)
-    include Provide_of_sexp (T)
-  end
 
-  (** Formulas, built from literals with predicate symbols from various
-      theories, and propositional constants and connectives. Denote sets of
-      structures. *)
-  and Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t) =
-  struct
     type t =
       | Tt
       | Eq of Trm.t * Trm.t
       | Eq0 of Trm.t
       | Pos of Trm.t
       | Not of t
-      | And of {pos: Fmls.t; neg: Fmls.t}
+      | And of {pos: set; neg: set}
-      | Or of {pos: Fmls.t; neg: Fmls.t}
+      | Or of {pos: set; neg: set}
       | Iff of t * t
       | Cond of {cnd: t; pos: t; neg: t}
       | Lit of Predsym.t * Trm.t array
-    [@@deriving compare, equal, sexp]
+
+    and set = (t, compare) Set.t [@@deriving compare, equal, sexp]
+  end
+
+  module Fml2 = struct
+    include Comparer.Counterfeit (Fml1)
+    include Fml1
+  end
+
+  (** Sets of formulas *)
+  module Fmls = struct
+    include Set.Make_from_Comparer (Fml2)
+    include Provide_of_sexp (Fml2)
+  end
+
+  (** Formulas, built from literals with predicate symbols from various
+      theories, and propositional constants and connectives. Denote sets of
+      structures. *)
+  module Fml = struct
+    include Fml2
 
     let invariant f =
       let@ () = Invariant.invariant [%here] f [%sexp_of: t] in

sledge/src/fol/propositional.mli

@@ -12,6 +12,6 @@ include module type of Propositional_intf
 module Make (Trm : sig
   type t [@@deriving compare, equal, sexp]
 end) : sig
-  module rec Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t)
+  module Fml : FORMULA with type trm := Trm.t
-  and Fmls : (FORMULA_SET with type elt := Fml.t)
+  module Fmls : FORMULA_SET with type elt := Fml.t with type t = Fml.set
 end