CounterExample.hs

{-# LANGUAGE BangPatterns #-}
module Algebra.Heyting.CounterExample where

import           Data.Set (Set)
import qualified Data.Set as Set
import           Text.Printf (printf)

import           Algebra.Lattice (top)
import           Algebra.Lattice.Lifted (Lifted)
import qualified Algebra.Lattice.Lifted as Lifted
import           Algebra.Lattice.Levitated (Levitated)
import qualified Algebra.Lattice.Levitated as Levitated
import           Algebra.Lattice.Op (Op (..))


-- | 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.
--
type CounterExample a = Lifted (Op (Set a))

fmapCounterExample
  :: (Ord a, Ord b)
  => (a -> b)
  -> CounterExample a
  -> CounterExample b
fmapCounterExample = fmap . fmap . Set.map

-- | A bijection from @e@ to atoms of the @'CounterExample' e@ lattice.
--
counterExample :: e -> CounterExample e
counterExample e = Lifted.Lift (Op (Set.singleton 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.
--
fromBool :: Ord e => e -> Bool -> CounterExample e
fromBool e False = counterExample e
fromBool _ True  = top

-- |
-- A homomorphism of /Heyting algebras/.
--
toBool :: CounterExample e -> Bool
toBool (Lifted.Lift (Op s)) | Set.null s
                            = True
toBool _                    = False

-- | 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@.
--
foldMapCounterExample
  :: (Ord e, Monoid m)
  => (e -> m)
  -> CounterExample e
  -> Levitated m
foldMapCounterExample f (Lifted.Lift (Op s)) | Set.null s = Levitated.Top
                                             | otherwise  = Levitated.Levitate (foldMap f s)
foldMapCounterExample _ Lifted.Bottom        = Levitated.Bottom

-- |
-- 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 -> Levitated String 
fromCounterExample Lifted.Bottom        = Levitated.Bottom
fromCounterExample (Lifted.Lift (Op s)) | Set.null s
                                        = Levitated.Top
                                        | otherwise
                                        = Levitated.Levitate (Set.foldl' go "" s)
  where
    go "" b = show b
    go !a b = printf "%s, %s" a (show b)

-- | Map `CounterExample` to a Maybe, representing @'Levitated.Top'@ as
-- @'Nothing'@ and mapping both @'Levitated.Levitate'@ and @'Levitate.Bottom'@ to
-- a @Just String@.
--
fromCounterExample' :: Show a => CounterExample a -> Maybe String
fromCounterExample' ce = case fromCounterExample ce of
  Levitated.Top        -> Nothing
  Levitated.Levitate s -> Just s
  Levitated.Bottom     -> Just ""

-- | 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 @\\/@.
--
annotate :: Ord e => e -> CounterExample e -> CounterExample e
annotate e Lifted.Bottom = counterExample e
annotate _ es            = es

(===) :: (Ord e, Eq a) => a -> a -> CounterExample e
a === b = if a == b then Lifted.Lift (Op Set.empty) else Lifted.Bottom

infixr 4 ===