Module type LayeredIndex.LayeredIndex

module type LayeredIndex = sig .. end

type entry

type index

val make_index : unit -> index

The index is created with a single initial layer.

val clear : index -> unit

Undefined if the index contains more than the single initial layer.

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

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

Undefined if the index contains more than the single initial layer.

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

type state

val obtain_state : index -> state

val install_state : state -> unit

val add_layer : state -> state

val new_layer : index -> state