// Copyright (c) .NET Foundation and contributors. All rights reserved.
// Licensed under the MIT license. See LICENSE file in the project root for full license information.

using System;

// This is needed due to NativeAOT which doesn't enable nullable globally yet
#nullable enable

namespace ILLink.Shared.DataFlow
{
    // ILattice represents a lattice (technically a semilattice) of values.
    // A semilattice is a set of values along with a meet operation (or greatest lower bound).
    // The meet operation imposes a partial order on the values: a <= b iff Meet(a, b) == a.

    // In a dataflow analysis, the Meet operation is used to combine the tracked facts when
    // there are multiple control flow paths that reach the same program point (or in a backwards
    // analysis, to combine the tracked facts from multiple control flow paths out of a program point).

    // The interface constraint on TValue ensures that trying to instantiate
    // ILattice over a nullable type will produce a warning or error.

    // The lattice might be better represented as an interface describing individual lattice values
    // (as opposed to describing the lattice structure as ILattice does), with Top being a static
    // virtual interface method. This would avoid the need to pass around multiple generic arguments
    // (TValue and TLattice). However, we can't use static virtual interface methods in the analyzer
    // so the lattice instance provides the Top value.
    public interface ILattice<TValue> where TValue : IEquatable<TValue>
    {
        // We require that the lattice has a "Top" or maximum element.
        // Top is >= a for every element a of the lattice.
        // Top is an identity for Meet: Meet(a, Top) = a.

        // The typical use in a dataflow analysis is for Top to represent the "unknown" initial state
        // with the least possible information about the analysis.
        public TValue Top { get; }

        // The Meet operation is associative, commutative, and idempotent.
        // This is used in dataflow analysis to iteratively Meet the tracked facts from different control
        // flow paths until the analysis converges to the most specific set of tracked facts.
        public TValue Meet(TValue left, TValue right);
    }
}