X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=47846f999b155e6d24415fd77687afbde4022bb0;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=fdecba91fb350cba8e5a0ecb396fb6b853bba8cc;hpb=ddd751449e73a22af523ce78ce1d8f0bb211e941;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index fdecba91f..47846f999 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -11,21 +11,34 @@
 
 (* $Id$ *)
 
-module type Comparable =
+module Index (B : Orderings.Blob) : 
   sig
-    type t
-    val is_eq : t -> t -> bool
-  end
+    module ClauseSet : Set.S with 
+      type elt = Terms.direction * B.t Terms.unit_clause
+
+    module FotermIndexable : Discrimination_tree.Indexable with 
+      type constant_name = B.t and
+      type input = B.t Terms.foterm 
+
+    module DT : Discrimination_tree.DiscriminationTree with 
+      type constant_name = B.t and 
+      type input = B.t Terms.foterm and 
+      type data = ClauseSet.elt and 
+      type dataset = ClauseSet.t
+    
+    val index_unit_clause : 
+      DT.t -> B.t Terms.unit_clause -> DT.t 
 
-module C : Comparable 
+    val remove_unit_clause :
+      DT.t -> B.t Terms.unit_clause -> DT.t 
 
-module FotermIndexable : Discrimination_tree.Indexable
-with type constant_name = C.t and
-     type input = C.t Terms.foterm 
+    val fold : 
+      DT.t ->
+      (B.t Discrimination_tree.path -> ClauseSet.t -> 'a -> 'a) 
+      -> 'a -> 'a
 
-module ClauseSet : Set.S with type elt = Terms.direction * C.t Terms.unit_clause
+    val elems : DT.t -> ClauseSet.t
 
-module DiscriminationTree : Discrimination_tree.DiscriminationTree 
-with type constant_name = C.t
-and type input = C.t Terms.foterm
-and type data = ClauseSet.elt and type dataset = ClauseSet.t
+    type active_set = B.t Terms.unit_clause list * DT.t
+
+  end