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
+