First pretty printing functions

[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..02e3a8b6686b865f2975a44747ee4b19369399d5 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -18,7 +18,7 @@ type 'a foterm =
 
 type 'a substitution = (int * 'a foterm) list
 
-type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type direction = Left2Right | Right2Left | Nodir
@@ -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