jon.recoil.org

Module type Solver_intf.Lattices

A collection of lattices, indexed by obj;

type 'a obj

Lattice identifers, indexed by 'a the carrier type of that lattice

type 'a elt

An element in a lattice whose carrier type is 'a.

val min : 'a obj -> 'a elt
val max : 'a obj -> 'a elt
val le : 'a obj -> 'a elt -> 'a elt -> bool
val equal : 'a obj -> 'a elt -> 'a elt -> bool
val join : 'a obj -> 'a elt -> 'a elt -> 'a elt
val meet : 'a obj -> 'a elt -> 'a elt -> 'a elt
val print : 'a obj -> Fmt.formatter -> 'a elt -> unit
val compare_obj : 'a obj -> 'b obj -> int

Total ordering on objects, used for internal map keys. This is not a lattice ordering or semantic equality check. If this returns 0, then equal_obj must return Misc.Is_eq.

val equal_obj : 'a obj -> 'b obj -> ('a, 'b) Misc.is_eq

Equality on objects recognized by the solver. This is the only object comparison that carries type equality evidence.

val print_obj : Fmt.formatter -> 'a obj -> unit