Module Map_lattice

module Map_lattice: sig .. end
Maps equipped with a lattice structure.

module type Value = sig .. end
module type Lattice = sig .. end
Complete semi-bounded lattice with over- and under-approximation, intersection and difference.
module type Lattice_with_cardinality = sig .. end
Complete lattice as above, plus a notion of cardinality on the values.
module type Map_Lattice = sig .. end
A map with a complete lattice structure.
module type Map_Lattice_with_cardinality = sig .. end
A notion of cardinality for maps with a complete lattice structure.
module type MapSet_Lattice = sig .. end
A lattice structure on top of maps from keys to values and sets of keys.
module type MapSet_Lattice_with_cardinality = sig .. end
A notion of cardinality for mapset lattice.
module Make_Map_Lattice: 
functor (Key : Hptmap.Id_Datatype) ->
functor (Value : Lattice_type.Full_Lattice) ->
functor (KVMap : Hptmap_sig.S with type key = Key.t and type v = Value.t) -> sig .. end
Equips an Hptmap with a lattice structure, provided that the values have a lattice structure.
module Make_MapSet_Lattice: 
functor (Key : Hptmap.Id_Datatype) ->
functor (KSet : Lattice_type.Lattice_Set with type O.elt = Key.t) ->
functor (Value : Value) ->
functor (KVMap : Map_Lattice with type key = Key.t and type v = Value.t) -> sig .. end
Builds a lattice mixing maps and sets, provided that each one has a lattice structure.