abstractlattice.jl

abstract type AbstractLattice; end

function widen; end

"""
    struct JLTypeLattice

A singleton type representing the lattice of Julia types, without any inference
extensions.
"""
struct JLTypeLattice <: AbstractLattice; end
widen(::JLTypeLattice) = error("Type lattice is the least-precise lattice available")

"""
    struct ConstsLattice

A lattice extending `JLTypeLattice` and adjoining `Const` and `PartialTypeVar`.
"""
struct ConstsLattice <: AbstractLattice; end
widen(::ConstsLattice) = JLTypeLattice()

"""
    struct PartialsLattice{L}

A lattice extending lattice `L` and adjoining `PartialStruct` and `PartialOpaque`.
"""
struct PartialsLattice{L <: AbstractLattice} <: AbstractLattice
    parent::L
end
widen(L::PartialsLattice) = L.parent

"""
    struct PartialsLattice{L}

A lattice extending lattice `L` and adjoining `Conditional`.
"""
struct ConditionalsLattice{L <: AbstractLattice} <: AbstractLattice
    parent::L
end
widen(L::ConditionalsLattice) = L.parent

"""
    struct OptimizerLattice

The lattice used by the optimizer. Equivalent to
`ConditionalsLattice{PartialsLattice{ConstsLattice}}`, but wrapped in a struct.
"""
struct OptimizerLattice; end
widen(L::ConditionalsLattice) = ConditionalsLattice{PartialsLattice{ConstsLattice}}()

"""
    struct InferenceLattice

The full lattice used for abstract interpration during inference. This takes the
`OptimizerLattice` and adjoints `LimitedAccuracy` and `MaybeUndef`.
"""
struct InferenceLattice; end

"""
    tmeet(lattice, a, b)

Compute the lattice meet of lattice elements `a` and `b` over the lattice
`lattice`. If `lattice` is `JLTypeLattice`, this is equiavalent to type
intersection.
"""
function tmeet; end

"""
    tmerge(lattice, a, b)

Compute a lattice join of elements `a` and `b` over the lattice `lattice`.
Note that the computed element need not be the least upper bound of `a` and
`b`, but rather, we impose some heuristic limits on the complexity of the
joined element, ideally without losing too much precision in common cases and
remaining mostly associative and commutative.
"""
function tmerge; end

"""
    ⊑(lattice, a, b)

Compute the lattice ordering (i.e. less-than-or-equal) relationship between
lattice elements `a` and `b` over the lattice `lattice`. If `lattice` is
`JLTypeLattice`, this is equiavalent to subtyping.
"""
function ⊑; end

⊑(::JLTypeLattice, @nospecialize(a::Type), @nospecialize(b::Type)) = a <: b


"""
    ⊏(lattice, a, b) -> Bool

The strict partial order over the type inference lattice.
This is defined as the irreflexive kernel of `⊑`.
"""
⊏(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) = ⊑(lattice, a, b) && !⊑(lattice, b, a)

"""
    ⋤(lattice, a, b) -> Bool

This order could be used as a slightly more efficient version of the strict order `⊏`,
where we can safely assume `a ⊑ b` holds.
"""
⋤(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b)) = !⊑(lattice, b, a)

"""
    is_lattice_equal(a, b) -> Bool

Check if two lattice elements are partial order equivalent.
This is basically `a ⊑ b && b ⊑ a` but (optionally) with extra performance optimizations.
"""
function is_lattice_equal(lattice::AbstractLattice, @nospecialize(a), @nospecialize(b))
    a === b && return true
    ⊑(lattice, a, b) && ⊑(lattice, b, a)
end

a quantum of abstract solace ∞