Feldspar.Lattice

General operations on sets

Documentation

class Eq a => Lattice a where

Lattice types

Methods

empty :: a

universal :: a

(\/) :: a -> a -> a

Union

(/\) :: a -> a -> a

Intersection

Instances

Lattice ()

Lattice AnySize

(Eq (Range a), BoundedInt a) => Lattice (Range a)

(Eq (a, b), Lattice a, Lattice b) => Lattice (a, b)

Lattice product

(Eq (:> a b), Lattice a, Lattice b) => Lattice (:> a b)

(Eq (a, b, c), Lattice a, Lattice b, Lattice c) => Lattice (a, b, c)

Three-way product

(Eq (a, b, c, d), Lattice a, Lattice b, Lattice c, Lattice d) => Lattice (a, b, c, d)

Four-way product

(Eq (a, b, c, d, e), Lattice a, Lattice b, Lattice c, Lattice d, Lattice e) => Lattice (a, b, c, d, e)

Five-way product

(Eq (a, b, c, d, e, f), Lattice a, Lattice b, Lattice c, Lattice d, Lattice e, Lattice f) => Lattice (a, b, c, d, e, f)

Six-way product

(Eq (a, b, c, d, e, f, g), Lattice a, Lattice b, Lattice c, Lattice d, Lattice e, Lattice f, Lattice g) => Lattice (a, b, c, d, e, f, g)

Seven-way product

unions :: Lattice a => [a] -> a

Accumulated union

intersections :: Lattice a => [a] -> a

Accumulated intersection

Computing fixed points

lensedFixedPoint :: Lattice lat => Lens a lat -> Lens b lat -> (a -> b) -> a -> b

Generalization of fixedPoint to functions whose argument and result contain (i.e has a lens to) a common lattice

lensedIndexedFixedPoint :: Lattice lat => Lens a lat -> Lens b lat -> (Int -> a -> b) -> a -> (b, Int)

Generalization of indexedFixedPoint to functions whose argument and result contain (i.e has a lens to) a common lattice

fixedPoint :: Lattice a => (a -> a) -> a -> a

Take the fixed point of a function. The second argument is an initial element. A sensible default for the initial element is empty.

The function is not required to be monotonic. It is made monotonic internally by always taking the union of the result and the previous value.

indexedFixedPoint :: Lattice a => (Int -> a -> a) -> a -> (a, Int)

Much like fixedPoint but keeps track of the number of iterations in the fixed point iteration. Useful for defining widening operators.

type Widening a = (Int -> a -> a) -> Int -> a -> a

The type of widening operators. A widening operator modifies a function that is subject to fixed point analysis. A widening operator introduces approximations in order to guarantee (fast) termination of the fixed point analysis.

cutOffAt :: Lattice a => Int -> Widening a

A widening operator which defaults to universal when the number of iterations goes over the specified value.

boundedLensedFixedPoint :: Lattice lat => Int -> Lens a lat -> Lens b lat -> (a -> b) -> a -> (b, Int)

A bounded version of lensedFixedPoint. It will always do at least one iteration regardless of the provided bound (in order to return something of the right type).