Module LayeredIndex


module LayeredIndex: sig .. end
Indexes with undoable modifications.


Extends Index with support for undoable modifications. The interface for undoable modifications can be explained with the help of considering a possible implementation:

An index is a store that is destructively modified. A layered index is a reference to a list of indexes. The list is not modified destructively. Read access on a layered index is performed on all the list elements. Write access on the first element. A state is represented by a list/reference pair. obtain_state returns such a state for a given layered index. install_state sets the reference value to the list. add_layer returns a new pair with the same reference and a list that is the cons of a fresh index with the input list.

Note that a program may perform modifications on a layered index that shares a part of its list with a state that has been extracted previously with obtain_state. When this state is installed later, the modifications in the shared indexes remain in effect. This property is no longer used, see tableau.ml.

module type LayeredIndex = sig .. end
module Make: 
functor (LayerType : Index.Index) -> LayeredIndex with type entry = LayerType.entry
Functor for building a layered index implementation based on an implementation of Index.Index.