Functor Hptmap.Make

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 '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.

Parameters:
Key : Id_Datatype
V : V
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 *) end
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
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

type key 

type of the keys

type v 

type of the values

type prefix 
include Hptmap_sig.Shape
include Datatype.S_with_collections
val self : State.t
val empty : t

the empty map

val singleton : key -> v -> t

singleton k d returns a map whose only binding is from k to d.

val add : key -> v -> t -> t

add k d m returns a map whose bindings are all bindings in m, plus a binding of the key k to the datum d. If a binding already exists for k, it is overridden.

val remove : key -> t -> t

remove k m returns the map m deprived from any binding involving k.

val replace : (v option -> v option) ->
key -> t -> t

replace f k m returns a map whose bindings are all bindings in m, except for the key k which is:

Filters and maps

val filter : (key -> bool) -> t -> t

filter f t keep only the bindings of m whose key verify f.

val map : (v -> v) -> t -> t

map f m returns the map obtained by composing the map m with the function f; that is, the map $k\mapsto f(m(k))$.

val map' : (key -> v -> v option) -> t -> t

Same as map, except if f k v returns None. In this case, k is not bound in the resulting map.

val cached_map : cache:string * int ->
temporary:bool ->
f:(key -> v -> v) -> t -> t
val replace_key : decide:(key ->
v -> v -> v) ->
key map -> t -> bool * t

replace_key ~decide shape map substitute keys in map according to shape: it returns the map in which all bindings from key to v such that key is bound to key' in shape are replaced by a binding from key' to v. If the new key key' was already bound in the map, or if two keys are replaced by a same key key', the decide function is used to compute the final value bound to key'. The returned boolean indicates whether the map has been modified: it is false if the intersection between shape and map is empty.

Merge of two maps

type empty_action = 
| Neutral
| Absorbing
| Traversing of (key -> v -> v option)
val merge : cache:Hptmap_sig.cache_type ->
symmetric:bool ->
idempotent:bool ->
decide_both:(key ->
v -> v -> v option) ->
decide_left:empty_action ->
decide_right:empty_action -> t -> t -> t

Merge of two trees, parameterized by a merge function. If symmetric holds, the function must verify merge x y = merge y x. If idempotent holds, the function must verify merge x x = x. For each key k present in both trees, and bound to v1 and v2 in the left and the right tree respectively, decide_both k v1 v2 is called. If the decide function returns None, the key will not be in the resulting map; otherwise, the new value computed will be bound to k. The decide_left action is performed to the left subtree t when a right subtree is empty (and conversely for the decide_right action when a left subtree is empty):

The results of the function may be cached, depending on cache. If a cache is used, then the merge functions must be pure.

val generic_join : cache:Hptmap_sig.cache_type ->
symmetric:bool ->
idempotent:bool ->
decide:(key ->
v option -> v option -> v) ->
t -> t -> t

Merge of two trees, parameterized by the decide function. If symmetric holds, the function must verify decide key v1 v2 = decide key v2 v1. If idempotent holds, the function must verify decide k (Some x) (Some x) = x.

val join : cache:Hptmap_sig.cache_type ->
symmetric:bool ->
idempotent:bool ->
decide:(key ->
v -> v -> v) ->
t -> t -> t

Same as generic_merge, but we assume that decide key None (Some v) = decide key (Some v) None = v holds.

val inter : cache:Hptmap_sig.cache_type ->
symmetric:bool ->
idempotent:bool ->
decide:(key ->
v -> v -> v option) ->
t -> t -> t

Intersection of two trees, parameterized by the decide function. If the decide function returns None, the key will not be in the resulting map. Keys present in only one map are similarly unmapped in the result.

val inter_with_shape : 'a map -> t -> t

inter_with_shape s m keeps only the elements of m that are also bound in the map s. No caching is used, but this function is more efficient than successive calls to Hptmap_sig.S.remove or Hptmap_sig.S.add to build the resulting map.

val diff_with_shape : 'a map -> t -> t

diff_with_shape s m keeps only the elements of m that are not bound in the map s. No caching is used, but this function is more efficient than successive calls to Hptmap_sig.S.remove or Hptmap_sig.S.add to build the resulting map.

val partition_with_shape : 'a map -> t -> t * t

partition_with_shape s m returns two maps inter, diff such that:

Misc

val from_shape : (key -> 'a -> v) -> 'a map -> t

Build an entire map from another map indexed by the same keys. More efficient than just performing successive Hptmap_sig.S.add the elements of the other map

val compositional_bool : t -> bool

Value of the compositional boolean associated to the tree, as computed by the Compositional_bool argument of the functor.

val pretty_debug : Stdlib.Format.formatter -> t -> unit

Verbose pretty printer for debug purposes.

Prefixes and subtree; Undocumented

type subtree 
exception Found_prefix of prefix * subtree * subtree
val comp_prefixes : t -> t -> unit
val pretty_prefix : prefix -> Stdlib.Format.formatter -> t -> unit
val find_prefix : t -> prefix -> subtree option
val hash_subtree : subtree -> int
val equal_subtree : subtree -> subtree -> bool