{-# 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 :: (a -> b) -> CounterExample a -> CounterExample b
fmapCounterExample = (Op (Set a) -> Op (Set b)) -> CounterExample a -> CounterExample b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Op (Set a) -> Op (Set b))
 -> CounterExample a -> CounterExample b)
-> ((a -> b) -> Op (Set a) -> Op (Set b))
-> (a -> b)
-> CounterExample a
-> CounterExample b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set a -> Set b) -> Op (Set a) -> Op (Set b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Set a -> Set b) -> Op (Set a) -> Op (Set b))
-> ((a -> b) -> Set a -> Set b)
-> (a -> b)
-> Op (Set a)
-> Op (Set b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Set a -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map

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

-- |
-- A homomorphism of /Heyting algebras/.
--
toBool :: CounterExample e -> Bool
toBool :: CounterExample e -> Bool
toBool (Lifted.Lift (Op Set e
s)) | Set e -> Bool
forall a. Set a -> Bool
Set.null Set e
s
                            = Bool
True
toBool CounterExample e
_                    = Bool
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 :: (e -> m) -> CounterExample e -> Levitated m
foldMapCounterExample e -> m
f (Lifted.Lift (Op Set e
s)) | Set e -> Bool
forall a. Set a -> Bool
Set.null Set e
s = Levitated m
forall a. Levitated a
Levitated.Top
                                             | Bool
otherwise  = m -> Levitated m
forall a. a -> Levitated a
Levitated.Levitate ((e -> m) -> Set e -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap e -> m
f Set e
s)
foldMapCounterExample e -> m
_ CounterExample e
Lifted.Bottom        = Levitated m
forall a. Levitated a
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 :: CounterExample a -> Levitated String
fromCounterExample CounterExample a
Lifted.Bottom        = Levitated String
forall a. Levitated a
Levitated.Bottom
fromCounterExample (Lifted.Lift (Op Set a
s)) | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
s
                                        = Levitated String
forall a. Levitated a
Levitated.Top
                                        | Bool
otherwise
                                        = String -> Levitated String
forall a. a -> Levitated a
Levitated.Levitate ((String -> a -> String) -> String -> Set a -> String
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' String -> a -> String
forall a. Show a => String -> a -> String
go String
"" Set a
s)
  where
    go :: String -> a -> String
go String
"" a
b = a -> String
forall a. Show a => a -> String
show a
b
    go !String
a a
b = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s, %s" String
a (a -> String
forall a. Show a => a -> String
show a
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' :: CounterExample a -> Maybe String
fromCounterExample' CounterExample a
ce = case CounterExample a -> Levitated String
forall a. Show a => CounterExample a -> Levitated String
fromCounterExample CounterExample a
ce of
  Levitated String
Levitated.Top        -> Maybe String
forall a. Maybe a
Nothing
  Levitated.Levitate String
s -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
  Levitated String
Levitated.Bottom     -> String -> Maybe String
forall a. a -> Maybe a
Just String
""

-- | 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 -> CounterExample e -> CounterExample e
annotate e
e CounterExample e
Lifted.Bottom = e -> CounterExample e
forall e. e -> CounterExample e
counterExample e
e
annotate e
_ CounterExample e
es            = CounterExample e
es

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

infixr 4 ===