-- | 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 (BoolSet -> BoolSet -> Bool
(BoolSet -> BoolSet -> Bool)
-> (BoolSet -> BoolSet -> Bool) -> Eq BoolSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BoolSet -> BoolSet -> Bool
== :: BoolSet -> BoolSet -> Bool
$c/= :: BoolSet -> BoolSet -> Bool
/= :: BoolSet -> BoolSet -> Bool
Eq, Eq BoolSet
Eq BoolSet
-> (BoolSet -> BoolSet -> Ordering)
-> (BoolSet -> BoolSet -> Bool)
-> (BoolSet -> BoolSet -> Bool)
-> (BoolSet -> BoolSet -> Bool)
-> (BoolSet -> BoolSet -> Bool)
-> (BoolSet -> BoolSet -> BoolSet)
-> (BoolSet -> BoolSet -> BoolSet)
-> Ord BoolSet
BoolSet -> BoolSet -> Bool
BoolSet -> BoolSet -> Ordering
BoolSet -> BoolSet -> BoolSet
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BoolSet -> BoolSet -> Ordering
compare :: BoolSet -> BoolSet -> Ordering
$c< :: BoolSet -> BoolSet -> Bool
< :: BoolSet -> BoolSet -> Bool
$c<= :: BoolSet -> BoolSet -> Bool
<= :: BoolSet -> BoolSet -> Bool
$c> :: BoolSet -> BoolSet -> Bool
> :: BoolSet -> BoolSet -> Bool
$c>= :: BoolSet -> BoolSet -> Bool
>= :: BoolSet -> BoolSet -> Bool
$cmax :: BoolSet -> BoolSet -> BoolSet
max :: BoolSet -> BoolSet -> BoolSet
$cmin :: BoolSet -> BoolSet -> BoolSet
min :: BoolSet -> BoolSet -> BoolSet
Ord, Int -> BoolSet -> ShowS
[BoolSet] -> ShowS
BoolSet -> String
(Int -> BoolSet -> ShowS)
-> (BoolSet -> String) -> ([BoolSet] -> ShowS) -> Show BoolSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BoolSet -> ShowS
showsPrec :: Int -> BoolSet -> ShowS
$cshow :: BoolSet -> String
show :: BoolSet -> String
$cshowList :: [BoolSet] -> ShowS
showList :: [BoolSet] -> ShowS
Show, Int -> BoolSet
BoolSet -> Int
BoolSet -> [BoolSet]
BoolSet -> BoolSet
BoolSet -> BoolSet -> [BoolSet]
BoolSet -> BoolSet -> BoolSet -> [BoolSet]
(BoolSet -> BoolSet)
-> (BoolSet -> BoolSet)
-> (Int -> BoolSet)
-> (BoolSet -> Int)
-> (BoolSet -> [BoolSet])
-> (BoolSet -> BoolSet -> [BoolSet])
-> (BoolSet -> BoolSet -> [BoolSet])
-> (BoolSet -> BoolSet -> BoolSet -> [BoolSet])
-> Enum BoolSet
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BoolSet -> BoolSet
succ :: BoolSet -> BoolSet
$cpred :: BoolSet -> BoolSet
pred :: BoolSet -> BoolSet
$ctoEnum :: Int -> BoolSet
toEnum :: Int -> BoolSet
$cfromEnum :: BoolSet -> Int
fromEnum :: BoolSet -> Int
$cenumFrom :: BoolSet -> [BoolSet]
enumFrom :: BoolSet -> [BoolSet]
$cenumFromThen :: BoolSet -> BoolSet -> [BoolSet]
enumFromThen :: BoolSet -> BoolSet -> [BoolSet]
$cenumFromTo :: BoolSet -> BoolSet -> [BoolSet]
enumFromTo :: BoolSet -> BoolSet -> [BoolSet]
$cenumFromThenTo :: BoolSet -> BoolSet -> BoolSet -> [BoolSet]
enumFromThenTo :: BoolSet -> BoolSet -> BoolSet -> [BoolSet]
Enum, BoolSet
BoolSet -> BoolSet -> Bounded BoolSet
forall a. a -> a -> Bounded a
$cminBound :: BoolSet
minBound :: BoolSet
$cmaxBound :: BoolSet
maxBound :: BoolSet
Bounded)

-- * Query

null :: BoolSet -> Bool
null :: BoolSet -> Bool
null = (BoolSet
SetEmpty BoolSet -> BoolSet -> Bool
forall a. Eq a => a -> a -> Bool
==)

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

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

-- | @not . member b@.
notMember :: Bool -> BoolSet -> Bool
notMember :: Bool -> BoolSet -> Bool
notMember Bool
b = Bool -> Bool
not (Bool -> Bool) -> (BoolSet -> Bool) -> BoolSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> BoolSet -> Bool
member Bool
b

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

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

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

-- * Construction

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

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

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

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

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

-- * Combine

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

difference, (\\) :: BoolSet -> BoolSet -> BoolSet
difference :: BoolSet -> BoolSet -> BoolSet
difference = ((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet)
-> ((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet
forall a b. (a -> b) -> a -> b
$ \case
  (BoolSet
SetEmpty , BoolSet
_        ) -> BoolSet
SetEmpty
  (BoolSet
_        , BoolSet
SetBoth  ) -> BoolSet
SetEmpty
  (BoolSet
s        , BoolSet
SetEmpty ) -> BoolSet
s
  (BoolSet
SetBoth  , BoolSet
SetTrue  ) -> BoolSet
SetFalse
  (BoolSet
SetBoth  , BoolSet
SetFalse ) -> BoolSet
SetTrue
  (BoolSet
SetTrue  , BoolSet
SetTrue  ) -> BoolSet
SetEmpty
  (BoolSet
SetTrue  , BoolSet
SetFalse ) -> BoolSet
SetTrue
  (BoolSet
SetFalse , BoolSet
SetTrue  ) -> BoolSet
SetFalse
  (BoolSet
SetFalse , BoolSet
SetFalse ) -> BoolSet
SetEmpty
\\ :: BoolSet -> BoolSet -> BoolSet
(\\)       = BoolSet -> BoolSet -> BoolSet
difference

intersection ::  BoolSet -> BoolSet -> BoolSet
intersection :: BoolSet -> BoolSet -> BoolSet
intersection = ((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet)
-> ((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet
forall a b. (a -> b) -> a -> b
$ \case
  (BoolSet
SetEmpty , BoolSet
_        ) -> BoolSet
SetEmpty
  (BoolSet
_        , BoolSet
SetEmpty ) -> BoolSet
SetEmpty
  (BoolSet
SetBoth  , BoolSet
s        ) -> BoolSet
s
  (BoolSet
s        , BoolSet
SetBoth  ) -> BoolSet
s
  (BoolSet
SetTrue  , BoolSet
SetTrue  ) -> BoolSet
SetTrue
  (BoolSet
SetFalse , BoolSet
SetTrue  ) -> BoolSet
SetEmpty
  (BoolSet
SetTrue  , BoolSet
SetFalse ) -> BoolSet
SetEmpty
  (BoolSet
SetFalse , BoolSet
SetFalse ) -> BoolSet
SetFalse

union ::  BoolSet -> BoolSet -> BoolSet
union :: BoolSet -> BoolSet -> BoolSet
union = ((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet)
-> ((BoolSet, BoolSet) -> BoolSet) -> BoolSet -> BoolSet -> BoolSet
forall a b. (a -> b) -> a -> b
$ \case
  (BoolSet
SetBoth  , BoolSet
_        ) -> BoolSet
SetBoth
  (BoolSet
_        , BoolSet
SetBoth  ) -> BoolSet
SetBoth
  (BoolSet
SetEmpty , BoolSet
s        ) -> BoolSet
s
  (BoolSet
s        , BoolSet
SetEmpty ) -> BoolSet
s
  (BoolSet
SetTrue  , BoolSet
SetTrue  ) -> BoolSet
SetTrue
  (BoolSet
SetFalse , BoolSet
SetTrue  ) -> BoolSet
SetBoth
  (BoolSet
SetTrue  , BoolSet
SetFalse ) -> BoolSet
SetBoth
  (BoolSet
SetFalse , BoolSet
SetFalse ) -> BoolSet
SetFalse

-- * Conversion

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

fromList, fromAscList, fromDistinctAscList :: [Bool] -> BoolSet
fromList :: [Bool] -> BoolSet
fromList            = (Bool -> BoolSet -> BoolSet) -> BoolSet -> [Bool] -> BoolSet
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bool -> BoolSet -> BoolSet
insert BoolSet
SetEmpty
fromAscList :: [Bool] -> BoolSet
fromAscList         = [Bool] -> BoolSet
fromList
fromDistinctAscList :: [Bool] -> BoolSet
fromDistinctAscList = \case
  []            -> BoolSet
SetEmpty
  [Bool
False]       -> BoolSet
SetFalse
  [Bool
True]        -> BoolSet
SetTrue
  [Bool
False, Bool
True] -> BoolSet
SetBoth
  [Bool]
_             -> BoolSet
forall a. HasCallStack => a
__IMPOSSIBLE__