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 tag 
module type Id_Datatype = sig .. end
Type of the keys of the map.
module Shape: 
functor (Key : Id_Datatype) -> sig .. end
This functor exports the shape of the maps indexed by keys Key.
module Make: 
functor (Key : Id_Datatype) ->
functor (V : Datatype.S) ->
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 -> V.t -> bool
Value for a leaf
val compose : bool -> bool -> bool
Composition of the values of two subtrees
val default : bool
end) ->
functor (Initial_Values : sig
val v : (Key.t * 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) -> sig .. end
module Comp_unused: sig .. end
Default implementation for the Compositional_bool argument of the functor Hptmap.Make.