module Hptshape:Hptmap_sig.Shape
with type key = t and type 'v map = 'v Hptmap.Shape(Base).t
type
key
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 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.
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
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 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
iterates simultaneously on
~join ~empty m1 m2m1
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
.
type
predicate_type =
| |
ExistentialPredicate |
| |
UniversalPredicate |
Existential (||
) or universal (&&
) predicates.
type
predicate_result =
| |
PTrue |
| |
PFalse |
| |
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.
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.