X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fdiscrimination_tree.ml;h=faccadf654dfcf0ade39ab1b8b00945c01d19200;hb=fdd518320bc83f20e8cef9dd6638c9cf6dd6345d;hp=1609fba568bdcd872d69e28d48e89581530d0e41;hpb=cab8b6ddde6291eb2bccad550bbd4634c00986ae;p=helm.git

diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml
index 1609fba56..faccadf65 100644
--- 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