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

Safe HaskellSafe-Inferred

Feldspar.Lattice

Contents

Description

General operations on sets

Synopsis

Documentation

class Eq a => Lattice a whereSource

Lattice types

Methods

bot :: aSource

top :: aSource

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

Join

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

Meet

Instances

Lattice () 
Lattice AnySize 
BoundedInt a => Lattice (Range a) 
(Lattice a, Lattice b) => Lattice (a, b)

Lattice product

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

Three-way product

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

Four-way product

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

Five-way product

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

Six-way product

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

Accumulated join

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

Accumulated meet

Computing fixed points

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

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

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

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

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)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 :: Lattice a => Int -> Widening aSource

A widening operator which defaults to top 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)Source

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