more abstract discrimination tree

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

diff --git a/helm/software/components/cic/discrimination_tree.mli b/helm/software/components/cic/discrimination_tree.mli
index ae6fe0347ccf9068f37003534d599e1edcaaf9dd..a311293068247737d0c0232e7c5dae0722e6ce8b 100644 (file)
--- a/helm/software/components/cic/discrimination_tree.mli
+++ b/helm/software/components/cic/discrimination_tree.mli
@@ -48,20 +48,27 @@ end
 module CicIndexable : Indexable 
 with type input = Cic.term and type constant_name = UriManager.uri
 
-module DiscriminationTreeIndexing :
- functor (I: Indexable) ->
-  functor (A : Set.S) ->
+module type DiscriminationTree  =
     sig
 
-      type t 
-      val iter : t -> (I.constant_name path -> A.t -> unit) -> unit
+      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 -> I.input -> A.elt -> t
-      val remove_index : t -> I.input -> A.elt -> t
-      val in_index : t -> I.input -> (A.elt -> bool) -> bool
-      val retrieve_generalizations : t -> I.input -> A.t
-      val retrieve_unifiables : t -> I.input -> A.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
+

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml
index d3a334a591db27453e13a2bd678a00ae63f83495..bd64cfe5d5a036b2ad0e69e0356c52a2718384af 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.ml
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml
@@ -24,10 +24,22 @@
  *)
 
 (* $Id$ *)
-(*
-module NCicIndexable : Discrimination_tree.Indexable
+
+open Discrimination_tree
+
+module TermOT : Set.OrderedType with type t = NCic.term = struct 
+  type t = NCic.term 
+  let compare = Pervasives.compare 
+end
+
+module TermSet = Set.Make(TermOT)
+
+module NCicIndexable : Indexable
 with type input = NCic.term and type constant_name = NUri.uri = struct
 
+type input = NCic.term
+type constant_name = NUri.uri
+
 let ppelem = function
   | Constant (uri,arity) -> 
       "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
@@ -71,6 +83,4 @@ let string_of_path l = String.concat "." (List.map ppelem l) ;;
 
 end
 
-module DiscriminationTree = 
-  Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable)
-  *)
+module DiscriminationTree = Make(NCicIndexable)(TermSet)

diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli
index 29fdbb68eb4b5c2462206060d1fda7628e2e60fd..b008277167caf2973879b91618d91b64118711ae 100644 (file)
--- a/helm/software/components/ng_refiner/nDiscriminationTree.mli
+++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli
@@ -23,10 +23,12 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*
 module NCicIndexable : Discrimination_tree.Indexable
 with type input = NCic.term and type constant_name = NUri.uri
 
-module DiscriminationTree : 
-        Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable)
-*)
+module TermSet : Set.S with type elt = NCic.term
+
+module DiscriminationTree : Discrimination_tree.DiscriminationTree 
+with type constant_name = NCicIndexable.constant_name 
+and type input = NCicIndexable.input
+and type data = TermSet.elt and type dataset = TermSet.t

diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.ml b/helm/software/components/tactics/paramodulation/equality_indexing.ml
index 390fa1c984acc2f7f83546c0c77741a541c4e7d7..458433abac541016f6b32add22e84f59f481f8fa 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality_indexing.ml
+++ b/helm/software/components/tactics/paramodulation/equality_indexing.ml
@@ -28,8 +28,7 @@
 module type EqualityIndex =
   sig
     module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
-    type t =
-            Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t
+    type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
     val empty : t
     val retrieve_generalizations : t -> Cic.term -> PosEqSet.t
     val retrieve_unifiables : t -> Cic.term -> PosEqSet.t
@@ -51,8 +50,7 @@ struct
 
     module PosEqSet = Set.Make(OrderedPosEquality);;
     
-    include
-    Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet)
+    include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet)
     
 
     (* DISCRIMINATION TREES *)
@@ -97,8 +95,7 @@ module PT =
 
     module PosEqSet = Set.Make(OrderedPosEquality);;
     
-    include
-    Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet)
+    include Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet)
     
 
     (* DISCRIMINATION TREES *)

diff --git a/helm/software/components/tactics/paramodulation/equality_indexing.mli b/helm/software/components/tactics/paramodulation/equality_indexing.mli
index 4ac6d54ecb2257b4a195bd0db89cfa8be4a8c7fa..c4b9df0ea4d94b9e4c016a863b9caf72caf1ba87 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality_indexing.mli
+++ b/helm/software/components/tactics/paramodulation/equality_indexing.mli
@@ -26,7 +26,7 @@
 module type EqualityIndex =
   sig
     module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
-    type t = Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t
+    type t = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
     val empty : t
     val retrieve_generalizations : t -> Cic.term -> PosEqSet.t
     val retrieve_unifiables : t -> Cic.term -> PosEqSet.t

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 9e7ba76f701d943c6a78039812c5e478e713dcf9..52afad8c2d05d9e9cbca70856a3818cd34432689 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -31,7 +31,7 @@ module Index :
       with type elt = Utils.pos * Equality.equality
       and type t = Equality_indexing.DT.PosEqSet.t
     type t =
-            Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t
+            Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
   end
 
 val index : Index.t -> Equality.equality -> Index.t

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index b914fab069881143d37a71a50ed31208c74e9c91..a7418461e060603ca6546dc817f9ced288b4a998 100644 (file)
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -28,7 +28,7 @@ module Codomain = struct
   let compare = Pervasives.compare 
 end
 module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(S)
+module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S)
 type universe = TI.t
 
 let empty = TI.empty