Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

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

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