Module Map_Lattice.Make_without_cardinal.M

module M: Hptmap.Make(K)(V)(Comp)(sig
val v : (K.t * V.t) list list
end)(sig
val l : State.t list
end)

type key = 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

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

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

Same as 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

Merge of two trees, parameterized by a merge function. If 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

Same as 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

Intersection of two trees, parameterized by a function which must verify 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.

Binary predicates

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`

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

Same functionality as 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

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

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

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.t -> 'a -> Hptmap.V.t) -> 'a Shape(Key).t -> t

Build an entire map from another map indexed by the same keys. More efficient than just performing successive add the elements of the other map

val shape : t -> Hptmap.V.t Shape(Key).t

Export the map as a value suitable for functions 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.