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

Feldspar.Lattice

Contents

Description

General operations on sets

Synopsis

# Documentation

class Eq a => Lattice a where Source

Lattice types

Methods

bot :: a Source

top :: a Source

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

Join

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

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

empty :: Lattice a => a Source

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

Accumulated join

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

Accumulated meet

# Computing fixed points

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

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

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

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 Source

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