Module type Index.Index

module type Index = sig .. end

Signature of an index.

type index

The type of an index.

type entry

The type of the index entries.

val make_index : unit -> index

make_index () returns a newly created index.

val clear : index -> unit

clear index removes all elements from index.

val insert : index -> Term.term -> entry -> unit

insert index term entry inserts a new value, entry, into index, associated with key term.

val remove_variant : index -> Term.term -> unit

remove_variant index term context deletes a single entry which has a variant of term as key from the index. It has no effect, if the index does not contain such an entry.

val iter_all : (entry -> unit) -> index -> unit

iter_all f index applies f to all entries in the index.

val iter_all_and_throw_away : (entry -> unit) -> index -> unit

iter_all_and_throw_away f index is similar to

iter_all f
       index

, except, that the implementation is allowed to remove entries as they are iterated over from the index. The index must be reinitialized with clear if it is to be used afterwards.

(Note: A kind of iteration, that allows to remove the current entry would be more desirable. See Java hashtables.)

val iter_instance_candidates : (entry -> unit) ->
       index -> Term.term -> Term.context -> unit

iter_instance_candidates f index term context applies f to all those entries in the index, whose keys are variants or proper instances of term in context , and maybe to more entries in the index.

context may be Term.null_context.

val iter_generalization_candidates : (entry -> unit) ->
       index -> Term.term -> Term.context -> unit

iter_generalization_candidates f index term context applies f to all those entries in the index, whose keys are variants or more general than term in context, and maybe to more entries in the index.

context may be Term.null_context.

val iter_unification_candidates : (entry -> unit) ->
       index -> Term.term -> Term.context -> unit

iter_unification_candidates f index term applies f to all those entries in the index, whose keys are unifiable with of term in context, and maybe to more entries in the index.

context may be Term.null_context.

val size : index -> int