feldspar-language- A functional embedded language for DSP and parallelism



General operations on sets



class Eq a => Set a whereSource

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.


empty :: aSource

universal :: aSource

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


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



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] -> aSource

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

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

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)Source

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 -> aSource

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 aSource

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