# Frama-C API - `Shape`

This functor builds `Hptmap_sig.Shape`

for maps indexed by keys `Key`

, which contains all functions on hptmap that do not create or modify maps.

## Parameters

`module Key : Id_Datatype`

## Signature

`include Hptmap_sig.Shape with type key = Key.t`

`type key = Key.t`

Type of the keys.

`val id : 'v map -> int`

Bijective function. The ids are positive.

`val hash : 'v map -> int`

`val pretty : 'v Pretty_utils.formatter -> 'v map Pretty_utils.formatter`

`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`

and`decide_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 returning`PTrue`

or`PFalse`

when possible. Otherwise, it returns`PUnknown`

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

`type 'a t = 'a map`