sig
module TermHashIndex :
sig
type index
type entry = Term.term
val make_index : unit -> index
val clear : index -> unit
val insert : index -> Term.term -> entry -> unit
val remove_variant : index -> Term.term -> unit
val iter_all : (entry -> unit) -> index -> unit
val iter_all_and_throw_away : (entry -> unit) -> index -> unit
val iter_instance_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val iter_generalization_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val iter_unification_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val size : index -> int
end
module TermAlistIndex :
sig
type index
type entry = Term.term
val make_index : unit -> index
val clear : index -> unit
val insert : index -> Term.term -> entry -> unit
val remove_variant : index -> Term.term -> unit
val iter_all : (entry -> unit) -> index -> unit
val iter_all_and_throw_away : (entry -> unit) -> index -> unit
val iter_instance_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val iter_generalization_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val iter_unification_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val size : index -> int
end
type hkey
module type TableType =
sig
type key = DtIndex.hkey
type 'a t
val make_table : unit -> 'a DtIndex.TableType.t
val add : 'a DtIndex.TableType.t -> DtIndex.TableType.key -> 'a -> unit
val remove : 'a DtIndex.TableType.t -> DtIndex.TableType.key -> unit
val find : 'a DtIndex.TableType.t -> DtIndex.TableType.key -> 'a
val iter :
(DtIndex.TableType.key -> 'a -> unit) ->
'a DtIndex.TableType.t -> unit
val iter_and_throw_away :
(DtIndex.TableType.key -> 'a -> unit) ->
'a DtIndex.TableType.t -> unit
end
module Make :
functor (Entry : Index.EntryType) ->
functor (Table : TableType) ->
sig
type index
type entry = Entry.entry
val make_index : unit -> index
val clear : index -> unit
val insert : index -> Term.term -> entry -> unit
val remove_variant : index -> Term.term -> unit
val iter_all : (entry -> unit) -> index -> unit
val iter_all_and_throw_away : (entry -> unit) -> index -> unit
val iter_instance_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val iter_generalization_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val iter_unification_candidates :
(entry -> unit) -> index -> Term.term -> Term.context -> unit
val size : index -> int
end
module HashTableImplementation : TableType
module AlistTableImplementation : TableType
end