Module Frama_c_kernel.Hptmap

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 (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 type Compositional_bool = sig ... end

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

module type Initial_values = sig ... end
module type Datatype_deps = sig ... end
module Make (Key : Id_Datatype) (V : V) (_ : Compositional_bool with type key := Key.t and type v := V.t) (_ : Initial_values with type key := Key.t and type v := V.t) (_ : Datatype_deps) : 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 Make. To be used when no interesting compositional bit can be computed.