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.