package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

type 'v map

Type of the maps from type key to type 'v.

val id : 'v map -> int

Bijective function. The ids are positive.

val hash : 'v map -> int
val equal : 'v map -> 'v map -> bool
val compare : ('v -> 'v -> int) -> 'v map -> 'v map -> int
val is_empty : 'v map -> bool

is_empty m returns true if and only if the map m defines no bindings at all.

val is_singleton : 'v map -> (key * 'v) option

is_singleton m returns Some (k, d) if m is a singleton map that maps k to d. Otherwise, it returns None.

val on_singleton : (key -> 'v -> bool) -> 'v map -> bool

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.

val find : key -> 'v map -> 'v
val find_check_missing : key -> 'v map -> 'v

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.

val find_key : key -> 'v map -> key

This function is useful where there are multiple distinct keys that are equal for Key.equal.

val mem : key -> 'v map -> bool

mem k m returns true if k is bound in m, and false otherwise.

val min_binding : 'v map -> key * 'v
val max_binding : 'v map -> key * 'v

Iterators

val iter : (key -> 'v -> unit) -> 'v map -> unit

iter f m applies f to all bindings of the map m.

val for_all : (key -> 'v -> bool) -> 'v map -> bool

for_all p m returns true if all the bindings of the map m satisfy the predicate p.

val exists : (key -> 'v -> bool) -> 'v map -> bool

for_all p m returns true if at least one binding of the map m satisfies the predicate p.

val fold : (key -> 'v -> 'b -> 'b) -> 'v map -> 'b -> 'b

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.

val fold_rev : (key -> 'v -> 'b -> 'b) -> 'v map -> 'b -> 'b

fold_rev performs exactly the same job as fold, but presents keys to f in the opposite order.

val to_seq : 'v map -> (key * 'v) Stdlib.Seq.t

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 cached_fold : cache_name:string -> temporary:bool -> f:(key -> 'v -> 'b) -> joiner:('b -> 'b -> 'b) -> empty:'b -> 'v map -> 'b
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

type predicate_type =
  1. | ExistentialPredicate
  2. | UniversalPredicate

Existential (||) or universal (&&) predicates.

type predicate_result =
  1. | PTrue
  2. | PFalse
  3. | PUnknown

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

val clear_caches : unit -> unit

Clear all the persistent caches used internally by the functions of this module. Those caches are not project-aware, so this function must be called at least each time a project switch occurs.

type 'a t = 'a map
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct