(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-module Orderings (B : Terms.Blob) :
+module type Blob =
sig
+ include Terms.Blob
(* This order relation should be:
* - stable for instantiation
* - total on ground terms
*
- * The output can range only on Eq, Lt, Gt, Incomparable
*)
val compare_terms :
- B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
+ t Terms.foterm -> t Terms.foterm -> Terms.comparison
+
+ (* these could be outside the module, but to ease experimentation
+ * we allow them to be tied with the ordering *)
+ val compute_clause_weight : 't Terms.clause -> int
+
+ val name : string
end
+
+module NRKBO (B : Terms.Blob) : Blob
+with type t = B.t
+
+module KBO (B : Terms.Blob) : Blob
+with type t = B.t
+
+module LPO (B : Terms.Blob) : Blob
+with type t = B.t