-- | Representation of @'Set' 'Bool'@ as a 4-element enum type.
--
-- All operations in constant time and space.
--
-- Mimics the interface of 'Data.Set'.
--
-- Import as:
-- @
--    import qualified Agda.Utils.BoolSet as BoolSet
--    import Agda.Utils.BoolSet (BoolSet)
-- @

module Agda.Utils.BoolSet
  ( BoolSet
  , (\\)
  , complement
  , delete
  , difference
  , elems
  , empty
  , fromList, fromAscList, fromDistinctAscList
  , insert
  , intersection
  , isSubsetOf
  , lookupMin
  , member
  , notMember
  , null
  , singleton
  , size
  , toList, toAscList
  , toSingleton
  , total
  , union
  ) where

import Prelude hiding (null)

import Agda.Utils.Impossible

-- | Isomorphic to @'Set' 'Bool'@.
data BoolSet = SetEmpty | SetTrue | SetFalse | SetBoth
  deriving (Eq, Ord, Show, Enum, Bounded)

-- * Query

null :: BoolSet -> Bool
null = (SetEmpty ==)

size :: BoolSet -> Int
size = \case
  SetEmpty -> 0
  SetTrue  -> 1
  SetFalse -> 1
  SetBoth  -> 2

member :: Bool -> BoolSet -> Bool
member b = \case
  SetEmpty -> False
  SetBoth  -> True
  SetTrue  -> b
  SetFalse -> not b

-- | @not . member b@.
notMember :: Bool -> BoolSet -> Bool
notMember b = not . member b

isSubsetOf ::  BoolSet -> BoolSet -> Bool
isSubsetOf = curry $ \case
  (SetEmpty , _        ) -> True
  (_        , SetBoth  ) -> True
  (SetTrue  , SetTrue  ) -> True
  (SetFalse , SetFalse ) -> True
  _                      -> False

lookupMin :: BoolSet -> Maybe Bool
lookupMin = \case
  SetEmpty -> Nothing
  SetTrue  -> Just True
  _        -> Just False

-- | @toSingleton s == Just b@ iff @s == singleton b@.
toSingleton :: BoolSet -> Maybe Bool
toSingleton  = \case
  SetTrue  -> Just True
  SetFalse -> Just False
  _        -> Nothing

-- * Construction

-- | The empty set.
empty :: BoolSet
empty = SetEmpty

-- | The full set.
total :: BoolSet
total = SetBoth

-- | A singleton set.
singleton :: Bool -> BoolSet
singleton = \case
  True  -> SetTrue
  False -> SetFalse

insert :: Bool -> BoolSet -> BoolSet
insert b = \case
  SetBoth  -> SetBoth
  SetEmpty -> singleton b
  SetTrue  -> if b then SetTrue else SetBoth
  SetFalse -> if b then SetBoth else SetFalse

delete :: Bool -> BoolSet -> BoolSet
delete b = \case
  SetEmpty -> SetEmpty
  SetTrue  -> if b then SetEmpty else SetTrue
  SetFalse -> if b then SetFalse else SetEmpty
  SetBoth  -> if b then SetFalse else SetTrue

-- * Combine

complement :: BoolSet -> BoolSet
complement = \case
  SetEmpty -> SetBoth
  SetBoth  -> SetEmpty
  SetTrue  -> SetFalse
  SetFalse -> SetTrue

difference, (\\) :: BoolSet -> BoolSet -> BoolSet
difference = curry $ \case
  (SetEmpty , _        ) -> SetEmpty
  (_        , SetBoth  ) -> SetEmpty
  (s        , SetEmpty ) -> s
  (SetBoth  , SetTrue  ) -> SetFalse
  (SetBoth  , SetFalse ) -> SetTrue
  (SetTrue  , SetTrue  ) -> SetEmpty
  (SetTrue  , SetFalse ) -> SetTrue
  (SetFalse , SetTrue  ) -> SetFalse
  (SetFalse , SetFalse ) -> SetEmpty
(\\)       = difference

intersection ::  BoolSet -> BoolSet -> BoolSet
intersection = curry $ \case
  (SetEmpty , _        ) -> SetEmpty
  (_        , SetEmpty ) -> SetEmpty
  (SetBoth  , s        ) -> s
  (s        , SetBoth  ) -> s
  (SetTrue  , SetTrue  ) -> SetTrue
  (SetFalse , SetTrue  ) -> SetEmpty
  (SetTrue  , SetFalse ) -> SetEmpty
  (SetFalse , SetFalse ) -> SetFalse

union ::  BoolSet -> BoolSet -> BoolSet
union = curry $ \case
  (SetBoth  , _        ) -> SetBoth
  (_        , SetBoth  ) -> SetBoth
  (SetEmpty , s        ) -> s
  (s        , SetEmpty ) -> s
  (SetTrue  , SetTrue  ) -> SetTrue
  (SetFalse , SetTrue  ) -> SetBoth
  (SetTrue  , SetFalse ) -> SetBoth
  (SetFalse , SetFalse ) -> SetFalse

-- * Conversion

elems, toList, toAscList :: BoolSet -> [Bool]
elems     = \case
  SetEmpty -> []
  SetTrue  -> [True]
  SetFalse -> [False]
  SetBoth  -> [False, True]
toList    = elems
toAscList = elems

fromList, fromAscList, fromDistinctAscList :: [Bool] -> BoolSet
fromList            = foldr insert SetEmpty
fromAscList         = fromList
fromDistinctAscList = \case
  []            -> SetEmpty
  [False]       -> SetFalse
  [True]        -> SetTrue
  [False, True] -> SetBoth
  _             -> __IMPOSSIBLE__