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 'a shape = 'a Shape(Key).t
and type prefix = prefix
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 'a
shape
type
prefix
include Datatype.S_with_collections
val id : t -> int
Bijective function. The ids are positive.
val self : State.t
val empty : t
the empty map
val is_empty : t -> bool
is_empty m
returns true
if and only if the map m
defines no
bindings at all.
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 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:
- removed from the map if
f o
= None
- bound to v' if
f o
= Some v'
where o
is (Some v) if k
is bound to v
in m
, or None if k
is not bound in m
.
val find : key -> t -> v
val find_check_missing : key -> t -> 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 -> t -> key
This function is useful where there are multiple distinct keys that
are equal for Key.equal
.
val remove : key -> t -> t
remove k m
returns the map m
deprived from any binding involving
k
.
val mem : key -> t -> bool
mem k m
returns true if k
is bound in m
, and false otherwise.
val iter : (key -> v -> unit) -> t -> unit
iter f m
applies f
to all bindings of the map m
.
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 filter : (key -> bool) -> t -> t
filter f t
keep only the bindings of m
whose key verify f
.
val fold : (key -> v -> 'b -> 'b) -> t -> '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) -> t -> 'b -> 'b
fold_rev
performs exactly the same job as fold
, but presents keys
to f
in the opposite order.
val for_all : (key -> v -> bool) -> t -> bool
for_all p m
returns true if all the bindings of the map m
satisfy
the predicate p
.
val exists : (key -> v -> bool) -> t -> bool
for_all p m
returns true if at least one binding of the map m
satisfies
the predicate p
.
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):
- Neutral returns the subtree
t
unchanged;
- Absorbing returns the empty tree;
- (Traversing f) applies the function
f
to each binding of the remaining
subtree t
(see map'
).
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 shape -> 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 shape -> 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.
Binary predicates
type
decide_fast =
val generic_predicate : exn ->
cache:string * 'a ->
decide_fast:(t -> t -> decide_fast) ->
decide_fst:(key -> v -> unit) ->
decide_snd:(key -> v -> unit) ->
decide_both:(v -> v -> unit) -> t -> t -> unit
generic_is_included e (cache_name, cache_size) ~decide_fast
~decide_fst ~decide_snd ~decide_both t1 t2
decides whether some
relation holds between
t1
and
t2
. All
decide
functions must raise
e
when the relation does not hold, and do nothing otherwise.
decide_fst
(resp. decide_snd
) is called when one key is present only
in t1
(resp. t2
).
decide_both
is called when a key is present in both trees.
decide_fast
is called on entire keys. As its name implies, it must be
fast; in doubt, returning Unknown
is always correct. Raising e
means
that the relation does not hold. Returning Done
means that the relation
holds.
The computation of this relation cached. cache_name
is used to identify
the cache when debugging. cache_size
is currently unused.
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:(t -> t -> predicate_result) ->
decide_fst:(key -> v -> bool) ->
decide_snd:(key -> v -> bool) ->
decide_both:(key -> v -> v -> bool) ->
t -> t -> bool
Same functionality as generic_predicate
but with a different signature.
All decision functions return a boolean that are combined differently
depending on whether the predicate is existential or universal.
val generic_symmetric_predicate : exn ->
decide_fast:(t -> t -> decide_fast) ->
decide_one:(key -> v -> unit) ->
decide_both:(v -> v -> unit) -> t -> t -> unit
Same as generic_predicate
, but for a symmetric relation. decide_fst
and decide_snd
are thus merged into decide_one
.
val symmetric_binary_predicate : Hptmap_sig.cache_type ->
predicate_type ->
decide_fast:(t -> t -> predicate_result) ->
decide_one:(key -> v -> bool) ->
decide_both:(key -> v -> v -> bool) ->
t -> t -> 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 : t -> t -> 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 : t -> t -> 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 cached_fold : cache_name:string ->
temporary:bool ->
f:(key -> v -> 'b) ->
joiner:('b -> 'b -> 'b) -> empty:'b -> t -> 'b
val cached_map : cache:string * int ->
temporary:bool ->
f:(key -> v -> v) -> t -> t
val singleton : key -> v -> t
singleton k d
returns a map whose only binding is from k
to d
.
val is_singleton : t -> (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) -> t -> 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 : t -> int
cardinal m
returns m
's cardinal, that is, the number of keys it
binds, or, in other words, its domain's cardinal.
val min_binding : t -> key * v
val max_binding : t -> key * v
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 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.
val from_shape : (key -> 'a -> v) -> 'a shape -> 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 from_shape_id : v shape -> t
Same as from_shape (fun _ v -> v)
.
val shape : t -> v shape
val fold2_join_heterogeneous : cache:Hptmap_sig.cache_type ->
empty_left:('a shape -> 'b) ->
empty_right:(t -> 'b) ->
both:(key -> v -> 'a -> 'b) ->
join:('b -> 'b -> 'b) -> empty:'b -> t -> 'a shape -> 'b
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
.