Frama-C API - Make_with_compositional_bool
This functor builds the complete module of maps indexed by keys Key
to values V
, with an additional boolean information maintained for each tree.
Parameters
module Key : Id_Datatype
module V : Datatype.S
Signature
type key = Key.t
type of the keys
type v = V.t
type of the values
type prefix = prefix
include Hptmap_sig.Shape with type key := key with type 'v map = 'v Shape(Key).map
type 'v map = 'v Shape(Key).map
Type of the maps from type key
to type 'v
.
val id : 'v map -> int
Bijective function. The ids are positive.
val is_empty : 'v map -> bool
is_empty m
returns true
if and only if the map m
defines no bindings at all.
is_singleton m
returns Some (k, d)
if m
is a singleton map that maps k
to d
. Otherwise, it returns None
.
on_singleton f m
returns f k d
if m
is a singleton map that maps k
to d
. Otherwise, it returns false.
val cardinal : 'v map -> int
cardinal m
returns m
's cardinal, that is, the number of keys it binds, or, in other words, its domain's cardinal.
Both find key m
and find_check_missing key m
return the value bound to key
in m
, or raise Not_found
is key
is unbound. find
is optimised for the case where key
is bound in m
, whereas find_check_missing
is more efficient for the cases where m
is big and key
is missing.
This function is useful where there are multiple distinct keys that are equal for Key.equal
.
Iterators
for_all p m
returns true if all the bindings of the map m
satisfy the predicate p
.
for_all p m
returns true if at least one binding of the map m
satisfies the predicate p
.
fold f m seed
invokes f k d accu
, in turn, for each binding from key k
to datum d
in the map m
. Keys are presented to f
in increasing order according to the map's ordering. The initial value of accu
is seed
; then, at each new call, its value is the value returned by the previous invocation of f
. The value returned by fold
is the final value of accu
.
fold_rev
performs exactly the same job as fold
, but presents keys to f
in the opposite order.
to_seq m
builds a sequence of each pair (key, datum) in the map m
. Keys are presented in the sequence in increasing order according to the map's ordering.
val fold2_join_heterogeneous : cache:Hptmap_sig.cache_type -> empty_left:('b map -> 'c) -> empty_right:('a map -> 'c) -> both:(key -> 'a -> 'b -> 'c) -> join:('c -> 'c -> 'c) -> empty:'c -> 'a map -> 'b map -> 'c
fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty m1 m2
iterates simultaneously on m1
and m2
. If a subtree t
is present in m1
but not in m2
(resp. in m2
but not in m1
), empty_right t
(resp. empty_left t
) is called. If a key k
is present in both trees, and bound to v1
and v2
respectively, both k v1 v2
is called. If both trees are empty, empty
is returned. The values of type 'b
returned by the auxiliary functions are merged using join
, which is called in an unspecified order. The results of the function may be cached, depending on cache
.
Binary predicates
Existential (||
) or universal (&&
) predicates.
Does the given predicate hold or not. PUnknown
indicates that the result is uncertain, and that the more aggressive analysis should be used.
val binary_predicate : Hptmap_sig.cache_type -> predicate_type -> decide_fast:('a map -> 'b map -> predicate_result) -> decide_fst:(key -> 'a -> bool) -> decide_snd:(key -> 'b -> bool) -> decide_both:(key -> 'a -> 'b -> bool) -> 'a map -> 'b map -> bool
binary_predicate
decides whether some relation holds between two maps, according to the functions:
decide_fst
anddecide_snd
, called on keys present only in the first or second map respectively;decide_both
, called on keys present in both trees;decide_fast
, called on entire maps as an optimization. As its name implies, it must be fast. If can prevent the analysis of some maps by directly returningPTrue
orPFalse
when possible. Otherwise, it returnsPUnknown
and the maps are analyzed by calling the functions above on each binding.
If the predicate is existential, then the function returns true
as soon as one of the call to the functions above returns true
. If the predicate is universal, the function returns true
if all calls to the functions above return true
.
The computation of this relation can be cached, according to cache_type
.
val symmetric_binary_predicate : Hptmap_sig.cache_type -> predicate_type -> decide_fast:('v map -> 'v map -> predicate_result) -> decide_one:(key -> 'v -> bool) -> decide_both:(key -> 'v -> 'v -> bool) -> 'v map -> 'v map -> bool
Same as binary_predicate
, but for a symmetric relation. decide_fst
and decide_snd
are thus merged into decide_one
.
val decide_fast_inclusion : 'v map -> 'v map -> predicate_result
Function suitable for the decide_fast
argument of binary_predicate
, when testing for inclusion of the first map into the second. If the two arguments are equal, or the first one is empty, the relation holds.
val decide_fast_intersection : 'v map -> 'v map -> predicate_result
Function suitable for the decide_fast
argument of symmetric_binary_predicate
when testing for a non-empty intersection between two maps. If one map is empty, the intersection is empty. Otherwise, if the two maps are equal, the intersection is non-empty.
Misc
include Datatype.S_with_collections with type t = v map
include Datatype.S with type t = v map
include Datatype.S_no_copy with type t = v map
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
val hash : t -> int
Hash function: same spec than Hashtbl.hash
.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
mem_project f x
must return true
iff there is a value p
of type Project.t
in x
such that f p
returns true
.
module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
val self : State.t
val empty : t
the empty map
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.
replace f k m
returns a map whose bindings are all bindings in m
, except for the key k
which is:
- removed from the map if
f o
= None - bound to v' if
f o
= Some v' whereo
is (Some v) ifk
is bound tov
inm
, or None ifk
is not bound inm
.
Filters and maps
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))$.
Same as map
, except if f k v
returns None
. In this case, k
is not bound in the resulting map.
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
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):
- Neutral returns the subtree
t
unchanged; - Absorbing returns the empty tree;
- (Traversing f) applies the function
f
to each binding of the remaining subtreet
(seemap'
).
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.
partition_with_shape s m
returns two maps inter, diff
such that:
inter
contains the elements ofm
bound in the shapes
;diff
contains the elements ofm
not bound in the shapes
.
Misc
Build an entire map from another map indexed by the same keys. More efficient than just performing successive 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
val hash_subtree : subtree -> int