Safe Haskell | None |
---|

General operations on sets

- class Eq a => Lattice a where
- 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 whereSource

Lattice types

Union

Intersection

Lattice () | |

Lattice AnySize | |

(Eq (Range a), BoundedInt a) => Lattice (Range a) | |

(Eq (a, b), Lattice a, Lattice b) => Lattice (a, b) | Lattice product |

(Eq (:> a b), Lattice a, Lattice b) => Lattice (:> a b) | |

(Eq (a, b, c), Lattice a, Lattice b, Lattice c) => Lattice (a, b, c) | Three-way product |

(Eq (a, b, c, d), Lattice a, Lattice b, Lattice c, Lattice d) => Lattice (a, b, c, d) | Four-way product |

(Eq (a, b, c, d, e), Lattice a, Lattice b, Lattice c, Lattice d, Lattice e) => Lattice (a, b, c, d, e) | Five-way product |

(Eq (a, b, c, d, e, f), Lattice a, Lattice b, Lattice c, Lattice d, Lattice e, Lattice f) => Lattice (a, b, c, d, e, f) | Six-way product |

(Eq (a, b, c, d, e, f, g), 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] -> aSource

Accumulated intersection

# 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 `empty`

.

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 `universal`

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