[sledge] Simplify Propositional interface

Reviewed By: ngorogiannis

Differential Revision: D26250535

fbshipit-source-id: ead7491cd

sledge/src/fol/propositional.ml

@@ -9,7 +9,10 @@
 
 include Propositional_intf
 
-module Make (Trm : TERM) = struct
+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

sledge/src/fol/propositional.mli

@@ -8,4 +8,10 @@
 (** Propositional formulas *)
 
 include module type of Propositional_intf
-module Make : MAKE
+
+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)
+end

sledge/src/fol/propositional_intf.ml

@@ -7,10 +7,6 @@
 
 (** Propositional formulas *)
 
-module type TERM = sig
-  type t [@@deriving compare, equal, sexp]
-end
-
 (** Formulas, built from literals with predicate symbols from various
     theories, and propositional constants and connectives. Denote sets of
     structures. *)
@@ -58,8 +54,3 @@ module type FORMULA_SET = sig
 
   val t_of_sexp : Sexp.t -> t
 end
-
-module type MAKE = functor (Trm : TERM) -> sig
-  module rec Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t)
-  and Fmls : (FORMULA_SET with type elt := Fml.t)
-end