Up  

Functor Map_lattice.Make_Map_Lattice.With_Cardinality

module With_Cardinality: 
functor (K : sig
val is_summary : Key.t -> bool
end) -> 
functor (Value : Lattice_type.Full_AI_Lattice_with_cardinality  with type t := Value.t) -> Map_lattice.Map_Lattice_with_cardinality  with type t := t
                                      and type key := key
                                      and type v := v

Adds cardinality functions for maps, according to a notion of cardinality on the values. It also requires a function is_summary on keys, indicating whether a key represents a summary of possibly multiple keys; a binding to such a key has never a cardinality of one.

Parameters:
K : sig val is_summary: Key.t -> bool end
Value : Lattice_type.Full_AI_Lattice_with_cardinality with type t := Value.t 
include Map_lattice.Lattice_with_cardinality
type key 
type v 
val find_lonely_key : t ->
       key *
       v

If t is a singleton map binding k to v and t is not a summary key, then returns the pair (k,v).

val find_lonely_binding : t ->
       key *
       v

If t is a singleton map binding k to v, if t is not a summary key, and if cardinal_zero_or_one v holds, returns the pair (k,v).