| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Feldspar.Lattice
Contents
Description
General operations on sets
- class Eq a => Lattice a where
- empty :: Lattice a => a
- universal :: Lattice a => a
- unions :: Lattice a => [a] -> a
- intersections :: Lattice a => [a] -> a
- lensedFixedPoint :: Lattice lat => Lens a lat -> Lens b lat -> (a -> b) -> a -> b
- lensedIndexedFixedPoint :: Lattice lat => Lens a lat -> Lens b lat -> (Int -> a -> b) -> a -> (b, Int)
- fixedPoint :: Lattice a => (a -> a) -> a -> a
- indexedFixedPoint :: Lattice a => (Int -> a -> a) -> a -> (a, Int)
- type Widening a = (Int -> a -> a) -> Int -> a -> a
- cutOffAt :: Lattice a => Int -> Widening a
- boundedLensedFixedPoint :: Lattice lat => Int -> Lens a lat -> Lens b lat -> (a -> b) -> a -> (b, Int)
Documentation
class Eq a => Lattice a where Source
Lattice types
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 |
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).