module LayeredIndex:Indexes with undoable modifications.sig
..end
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:
Index.Index
.