From c0d106cb0acc8c33e5c578ee38458c52cab07323 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 21 Feb 2021 13:18:09 -0800
Subject: [PATCH] [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            |  3 ---
 sledge/src/fol/propositional.ml  | 41 +++++++++++++++++++-------------
 sledge/src/fol/propositional.mli |  4 ++--
 3 files changed, 26 insertions(+), 22 deletions(-)

diff --git a/sledge/src/fol/fml.ml b/sledge/src/fol/fml.ml
index c49dd2a1b..ab7106d14 100644
--- a/sledge/src/fol/fml.ml
+++ b/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 =
diff --git a/sledge/src/fol/propositional.ml b/sledge/src/fol/propositional.ml
index 5558c83a7..de3540f39 100644
--- a/sledge/src/fol/propositional.ml
+++ b/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 rec Fmls : (FORMULA_SET with type elt := Fml.t) = struct
-    module T = struct
-      type t = Fml.t [@@deriving compare, equal, sexp]
-    end
-
-    include Set.Make (T)
-    include Provide_of_sexp (T)
-  end
+  module Fml1 = struct
+    type compare [@@deriving compare, equal, sexp]
 
-  (** 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}
-      | Or of {pos: Fmls.t; neg: Fmls.t}
+      | And of {pos: set; neg: set}
+      | 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
diff --git a/sledge/src/fol/propositional.mli b/sledge/src/fol/propositional.mli
index f32528117..5168246a4 100644
--- a/sledge/src/fol/propositional.mli
+++ b/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)
-  and Fmls : (FORMULA_SET with type elt := Fml.t)
+  module Fml : FORMULA with type trm := Trm.t
+  module Fmls : FORMULA_SET with type elt := Fml.t with type t = Fml.set
 end