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
.