functorial abstraction over term blobs

[helm.git] / helm / software / components / ng_paramodulation / terms.mli

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index c49eaff832727d06f200df5bffce38aacb2f5bf4..3013ed7d0fb700b7bea4998b89f04571f66e40d2 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -50,3 +50,19 @@ module M : Map.S with type key = int
 
 type 'a bag = 'a unit_clause M.t
 
+module type Blob =
+  sig
+    type t
+    val eq : t -> t -> bool
+    val compare : t -> t -> int
+    val pp : t -> string
+  end
+
+module Utils (B : Blob) :
+  sig
+    val eq_literal : B.t literal -> B.t literal -> bool
+    val compare_literal : B.t literal -> B.t literal -> int
+
+    val eq_unit_clause : B.t unit_clause -> B.t unit_clause -> bool
+    val compare_unit_clause : B.t unit_clause -> B.t unit_clause -> int
+  end