Frama-C API - 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.
module type Id_Datatype = sig ... end
Type of the keys of 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 Info = sig ... end
Required information for the correctness of the hptmaps.
module Make (Key : Id_Datatype) (V : Datatype.S) (_ : Info with type key := Key.t and type v := V.t) : 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 type Compositional_bool = sig ... end
An additional boolean information is computed for each tree, by composing the boolean on the subtrees and the value information on each leaf.
module Make_with_compositional_bool (Key : Id_Datatype) (V : Datatype.S) (_ : Compositional_bool with type key := Key.t and type v := V.t) (_ : Info with type key := Key.t and type v := V.t) : 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
, with an additional boolean information maintained for each tree.