    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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__