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 type V =sig
..end
Values stored in the map
module Shape:
This functor exports the shape of the maps indexed by keys Key
.
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 'a shape = 'a Shape(Key).t and type prefix = prefix
module Comp_unused:sig
..end
Default implementation for the Compositional_bool
argument of the functor
Hptmap.Make
.