General operations on sets
- class Eq a => Set a where
- unions :: Set a => [a] -> a
- intersections :: Set a => [a] -> a
- fixedPoint :: Set a => (a -> a) -> a -> a
- indexedFixedPoint :: Set a => (Int -> a -> a) -> a -> (a, Int)
- type Widening a = (Int -> a -> a) -> Int -> a -> a
- cutOffAt :: Set a => Int -> Widening a
Set is an *over-approximation* of a set of values. The class does not
care about how the set is interpreted, but it only makes sense to use
interpretations for which the operations are sound.
Approximates all sets as
|BoundedInt a => Set (Range a)|
|(Set a, Set b) => Set (a, b)|
|(Set a, Set b) => Set (:> a b)|
|Type a => Set (EdgeSize role a)|
|(Set a, Set b, Set c) => Set (a, b, c)|
|(Set a, Set b, Set c, Set d) => Set (a, b, c, d)|
Take the fixed point of a monotonic function. The second argument is
an initial element. A sensible default for the initial element is
fixedPoint but keeps track of the number of iterations
in the fixed point iteration. Useful for defining widening operators.
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.