Feldspar.Set

General operations on sets

Documentation

class Eq a => Set a where

A Set is an *over-approximation* of a set of values. The class does not care about how the set is interpreted, but it only makes sense to use interpretations for which the operations are sound.

Methods

empty :: a

universal :: a

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

Union

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

Intersection

Instances

Set ()

Approximates all sets as (), which is the universal set.

BoundedInt a => Set (Range a)

(Set a, Set b) => Set (a, b)

Set product

(Set a, Set b) => Set (:> a b)

Type a => Set (EdgeSize role a)

(Set a, Set b, Set c) => Set (a, b, c)

Three-way product

(Set a, Set b, Set c, Set d) => Set (a, b, c, d)

Four-way product

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

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

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

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

indexedFixedPoint :: Set 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 :: Set a => Int -> Widening a

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