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. SeeComp_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
val default :bool
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, hencev
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
) ->
sig
..end
Parameters: |
|
typekey =
Key.t
type
t
include Datatype.S_with_collections
val self : State.t
val empty : t
val hash : t -> int
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 -> Hptmap.V.t -> 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 find : key -> t -> Hptmap.V.t
val find_check_missing : key -> t -> Hptmap.V.t
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
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
val iter : (Key.t -> Hptmap.V.t -> unit) -> t -> unit
val map : (Hptmap.V.t -> Hptmap.V.t) -> 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.t -> Hptmap.V.t -> Hptmap.V.t option) -> t -> t
map
, except if f k v
returns None
. In this case, k
is not
bound in the resulting map.val fold : (Key.t -> Hptmap.V.t -> '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.t -> Hptmap.V.t -> '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.t -> Hptmap.V.t -> bool) -> t -> bool
val exists : (Key.t -> Hptmap.V.t -> bool) -> t -> bool
val generic_merge : cache:string * bool ->
decide:(Key.t -> Hptmap.V.t option -> Hptmap.V.t option -> Hptmap.V.t) ->
idempotent:bool ->
empty_neutral:bool -> t -> t -> t
idempotent
holds, the function must verify merge k (Some x) (Some x) = x
. If
empty_neutral
holds, the function must verify merge None (Some v) = v
and merge (Some v) None = v
. If snd cache
is true
, an internal
cache is used; thus the merge function must be pure.val symmetric_merge : cache:string * 'a ->
empty_neutral:bool ->
decide_none:(Key.t -> Hptmap.V.t -> Hptmap.V.t) ->
decide_some:(Hptmap.V.t -> Hptmap.V.t -> Hptmap.V.t) ->
t -> t -> t
generic_merge
, but we also assume that merge x y = merge y x
holds.val symmetric_inter : cache:string * 'a ->
decide_some:(Key.t -> Hptmap.V.t -> Hptmap.V.t -> Hptmap.V.t option) ->
t -> t -> t
inter x y == inter y x
and inter x Empty == Empty
. If the intersection
function returns None
, the key will not be in the resulting map.
decide_some
must be pure, as an internal cache is used).val inter_with_shape : 'a Shape(Key).t -> 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 remove
or add
to build the
resulting map.type
decide_fast =
| |
Done |
|||
| |
Unknown |
(* |
Shortcut for functions that decide whether a predicate holds on a tree.
Done means that the function returns its default value, which is
usually unit . Unknown means that the evaluation must continue in the
subtrees. | *) |
val generic_predicate : exn ->
cache:string * 'a ->
decide_fast:(t -> t -> decide_fast) ->
decide_fst:(Key.t -> Hptmap.V.t -> unit) ->
decide_snd:(Key.t -> Hptmap.V.t -> unit) ->
decide_both:(Hptmap.V.t -> Hptmap.V.t -> 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 |
||
) or universal (&&
) predicates.type
predicate_result =
| |
PTrue |
| |
PFalse |
| |
PUnknown |
PUnknown
indicates that the result
is uncertain, and that the more aggressive analysis should be used.val binary_predicate : Hptmap.cache_type ->
predicate_type ->
decide_fast:(t -> t -> predicate_result) ->
decide_fst:(Key.t -> Hptmap.V.t -> bool) ->
decide_snd:(Key.t -> Hptmap.V.t -> bool) ->
decide_both:(Key.t -> Hptmap.V.t -> Hptmap.V.t -> bool) ->
t -> t -> bool
generic_predicate
but with a different signature.
All decisin 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.t -> Hptmap.V.t -> unit) ->
decide_both:(Hptmap.V.t -> Hptmap.V.t -> unit) ->
t -> t -> unit
generic_predicate
, but for a symmetric relation. decide_fst
and decide_snd
are thus merged into decide_one
.val symmetric_binary_predicate : Hptmap.cache_type ->
predicate_type ->
decide_fast:(t -> t -> predicate_result) ->
decide_one:(Key.t -> Hptmap.V.t -> bool) ->
decide_both:(Key.t -> Hptmap.V.t -> Hptmap.V.t -> bool) ->
t -> t -> bool
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
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
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 -> Hptmap.V.t -> 'b) ->
joiner:('b -> 'b -> 'b) -> empty:'b -> t -> 'b
val cached_map : cache:string * int ->
temporary:bool ->
f:(key -> Hptmap.V.t -> Hptmap.V.t) ->
t -> t
val singleton : key -> Hptmap.V.t -> t
singleton k d
returns a map whose only binding is from k
to d
.val is_singleton : t -> (key * Hptmap.V.t) option
is_singleton m
returns Some (k, d)
if m
is a singleton map
that maps k
to d
. Otherwise, it returns None
.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 * Hptmap.V.t
val max_binding : t -> key * Hptmap.V.t
val split : key ->
t -> t * Hptmap.V.t option * t
val compositional_bool : t -> bool
Compositional_bool
argument of the functor.val clear_caches : unit -> unit
val from_shape : (Key.t -> 'a -> Hptmap.V.t) -> 'a Shape(Key).t -> t
add
the elements
of the other mapval shape : t -> Hptmap.V.t Shape(Key).t
inter_with_shape
and from_shape
val fold2_join_heterogeneous : cache:Hptmap.cache_type ->
empty_left:('a Shape(Key).t -> 'b) ->
empty_right:(t -> 'b) ->
both:(Key.t -> Hptmap.V.t -> 'a -> 'b) ->
join:('b -> 'b -> 'b) -> empty:'b -> t -> 'a Shape(Key).t -> '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 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
.