more abstract discrimination tree

[helm.git] / helm / software / components / cic / discrimination_tree.ml

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 1609fba568bdcd872d69e28d48e89581530d0e41..faccadf654dfcf0ade39ab1b8b00945c01d19200 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.ml
+++ b/helm/software/components/cic/discrimination_tree.ml
@@ -105,9 +105,29 @@ let arity_of = function
   | _ -> 0 
 ;;
 
-module DiscriminationTreeIndexing =  
-  functor (I:Indexable) -> 
-  functor (A:Set.S) -> 
+module type DiscriminationTree =
+    sig
+
+      type input 
+      type data
+      type dataset
+      type constant_name
+      type t
+
+      val iter : t -> (constant_name path -> dataset -> unit) -> unit
+
+      val empty : t
+      val index : t -> input -> data -> t
+      val remove_index : t -> input -> data -> t
+      val in_index : t -> input -> (data -> bool) -> bool
+      val retrieve_generalizations : t -> input -> dataset
+      val retrieve_unifiables : t -> input -> dataset
+    end
+
+module Make (I:Indexable) (A:Set.S) : DiscriminationTree 
+with type constant_name = I.constant_name and type input = I.input
+and type data = A.elt and type dataset = A.t =
+
     struct
 
       module OrderedPathStringElement = struct
@@ -115,6 +135,11 @@ module DiscriminationTreeIndexing =
         let compare = I.compare
       end
 
+      type constant_name = I.constant_name
+      type data = A.elt
+      type dataset = A.t
+      type input = I.input
+
       module PSMap = Map.Make(OrderedPathStringElement);;
 
       type key = PSMap.key