more functors

[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 3013ed7d0fb700b7bea4998b89f04571f66e40d2..f5aaa619f2dc01dfac4c13d661f7cc29b65597bd 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -52,14 +52,24 @@ type 'a bag = 'a unit_clause M.t
 
 module type Blob =
   sig
+    (* Blob is the type for opaque leaves: 
+     * - checking equlity should be efficient
+     * - atoms have to be equipped with a total order relation
+     *)
     type t
     val eq : t -> t -> bool
     val compare : t -> t -> int
-    val pp : t -> string
+    (* TODO: consider taking in input an imperative buffer for Format 
+     *  val pp : Format.formatter -> t -> unit
+     * *)
+    val pp : t -> string 
   end
 
 module Utils (B : Blob) :
   sig
+    val eq_foterm : B.t foterm -> B.t foterm -> bool
+    val compare_foterm : B.t foterm -> B.t foterm -> int
+
     val eq_literal : B.t literal -> B.t literal -> bool
     val compare_literal : B.t literal -> B.t literal -> int