Module Hptmap

module Hptmap: sig .. end

Efficient maps from hash-consed trees to values, implemented as Patricia trees.

This implementation of big-endian Patricia trees follows Chris Okasaki's paper at the 1998 ML Workshop in Baltimore. Maps are implemented on top of Patricia trees. A tree is big-endian if it expects the key's most significant bits to be tested first.

type prefix

Undocumented. Needed for advanced users only

module type Id_Datatype = sig .. end

Type of the keys of the map.

module type V = sig .. end

Values stored in the map

module Shape: functor (Key : Id_Datatype) -> sig .. end

This functor builds Hptmap_sig.Shape for maps indexed by keys Key, which contains all functions on hptmap that do not create or modify maps.

module Make: functor (Key : Id_Datatype) -> functor (V : V) -> functor (Compositional_bool : sig

A boolean information is maintained for each tree, by composing the boolean on the subtrees and the value information present on each leaf. See Comp_unused for a default implementation.

val e : bool

Value for the empty tree

val f : Key.t -> Hptmap.V.t -> bool

Value for a leaf

val compose : bool -> bool -> bool

Composition of the values of two subtrees

end) -> functor (Initial_Values : sig

val v : (Key.t * Hptmap.V.t) list list

List of the maps that must be shared between all instances of Frama-C (the maps being described by the list of their elements). Must include all maps that are exported at Caml link-time when the functor is applied. This usually includes at least the empty map, hence v nearly always contains [].

end) -> functor (Datatype_deps : sig

val l : State.t list

Dependencies of the hash-consing table. The table will be cleared whenever one of those dependencies is cleared.

end) -> Hptmap_sig.S  with type key = Key.t
                  and type v = V.t
                  and type 'v map = 'v Shape(Key).map
                  and type prefix = prefix

This functor builds the complete module of maps indexed by keys Key to values V.

module Comp_unused: sig .. end

Default implementation for the Compositional_bool argument of the functor Hptmap.Make.