Previous  Up  Next

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 type V = sig .. end
Values stored in the map 
module Shape: 
functor (Key : Id_Datatype) -> sig .. end
This functor exports the shape of the maps indexed by keys Key. 
type cache_type =
| NoCache (*
The results of the function will not be cached.
*)
| PersistentCache of string (*
The results of the function will be cached, and the function that uses the cache is a permanent closure (at the toplevel of an OCaml module).
*)
| TemporaryCache of string (*
The results of the function will be cached, but the function itself is a local function which is garbage-collectable.
*)
Some functions of this module may optionally use internal caches. It is the responsibility of the use to choose whether or not to use a cache, and whether this cache will be garbage-collectable by OCaml.
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





val default : bool
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) -> sig .. end
module Comp_unused: sig .. end
Default implementation for the Compositional_bool argument of the functor Hptmap.Make.