Algebra.Heyting.CounterExample

Documentation

type CounterExample a = Lifted (Op (Set a))

A counter example type is a Heyting algebra; it useful for tests and properties. It records all failures. The truth value is represented by an empty set. Since CounterExample e is a Heyting algebra, it is useful in expressing properties that require assumptions.

fmapCounterExample :: (Ord a, Ord b) => (a -> b) -> CounterExample a -> CounterExample b

counterExample :: e -> CounterExample e

A bijection from e to atoms of the CounterExample e lattice.

fromBool :: Ord e => e -> Bool -> CounterExample e

A lattice homomorphism from Bool to CounterExample, which lifts False to an atom of CounterExample (uniquely determined by e) and which preserves the top element.

toBool :: CounterExample e -> Bool

A homomorphism of Heyting algebras.

foldMapCounterExample :: (Ord e, Monoid m) => (e -> m) -> CounterExample e -> Levitated m

Note that this map is not a lattice homomorphism (it does not preserve meet nor join). It is also not a poset map in general. Nevertheless, it preserves top and bottom.

fromCounterExample :: Show a => CounterExample a -> Levitated String

Map a CounterExample to Levitated String. Each set of counter example is concatenated into a single comma separated string. This is useful for printing counter examples in tests. See fromCounterExample'.

fromCounterExample' :: Show a => CounterExample a -> Maybe String

Map CounterExample to a Maybe, representing Top as Nothing and mapping both Levitate and Bottom to a Just String.

annotate :: Ord e => e -> CounterExample e -> CounterExample e

Add a counter example. This is simply lifts the bottom to an atom given by e, otherwise it preserves the CounterExample e.

Note that take join of e es = counterExample e \/ es will return top if e if e is not in the set es; thus this map is not defined with using \/.

(===) :: (Ord e, Eq a) => a -> a -> CounterExample e infixr 4