    -- | Tools for 3-way partitioning.

    module Agda.Utils.Three where

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

    -- | Partition a list into 3 groups.
    --
    --   Preserves the relative order or elements.
    --
    partition3 :: (a -> Three) -> [a] -> ([a], [a], [a])
    partition3 :: forall a. (a -> Three) -> [a] -> ([a], [a], [a])
    partition3  a -> Three
    f = [a] -> ([a], [a], [a])
    loop where
      loop :: [a] -> ([a], [a], [a])
    loop []     = ([], [], [])
      loop (a
    x:[a]
    xs) = case a -> Three
    f a
    x of
          Three
    One   -> (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    as, [a]
    bs, [a]
    cs)
          Three
    Two   -> ([a]
    as, a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    bs, [a]
    cs)
          Three
    Three -> ([a]
    as, [a]
    bs, a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    cs)
        where ([a]
    as, [a]
    bs, [a]
    cs) = [a] -> ([a], [a], [a])
    loop [a]
    xs

    -- | Disjoint sum of three.
    --
    data Either3 a b c
      = In1 a
      | In2 b
      | In3 c
      deriving (Either3 a b c -> Either3 a b c -> Bool
    (Either3 a b c -> Either3 a b c -> Bool)
    -> (Either3 a b c -> Either3 a b c -> Bool) -> Eq (Either3 a b c)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall a b c.
    (Eq a, Eq b, Eq c) =>
    Either3 a b c -> Either3 a b c -> Bool
    /= :: Either3 a b c -> Either3 a b c -> Bool
    $c/= :: forall a b c.
    (Eq a, Eq b, Eq c) =>
    Either3 a b c -> Either3 a b c -> Bool
    == :: Either3 a b c -> Either3 a b c -> Bool
    $c== :: forall a b c.
    (Eq a, Eq b, Eq c) =>
    Either3 a b c -> Either3 a b c -> Bool
    Eq, Eq (Either3 a b c)
    Eq (Either3 a b c)
    -> (Either3 a b c -> Either3 a b c -> Ordering)
    -> (Either3 a b c -> Either3 a b c -> Bool)
    -> (Either3 a b c -> Either3 a b c -> Bool)
    -> (Either3 a b c -> Either3 a b c -> Bool)
    -> (Either3 a b c -> Either3 a b c -> Bool)
    -> (Either3 a b c -> Either3 a b c -> Either3 a b c)
    -> (Either3 a b c -> Either3 a b c -> Either3 a b c)
    -> Ord (Either3 a b c)
    Either3 a b c -> Either3 a b c -> Bool
    Either3 a b c -> Either3 a b c -> Ordering
    Either3 a b c -> Either3 a b c -> Either3 a b c
    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
    forall {a} {b} {c}. (Ord a, Ord b, Ord c) => Eq (Either3 a b c)
    forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Bool
    forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Ordering
    forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Either3 a b c
    min :: Either3 a b c -> Either3 a b c -> Either3 a b c
    $cmin :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Either3 a b c
    max :: Either3 a b c -> Either3 a b c -> Either3 a b c
    $cmax :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Either3 a b c
    >= :: Either3 a b c -> Either3 a b c -> Bool
    $c>= :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Bool
    > :: Either3 a b c -> Either3 a b c -> Bool
    $c> :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Bool
    <= :: Either3 a b c -> Either3 a b c -> Bool
    $c<= :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Bool
    < :: Either3 a b c -> Either3 a b c -> Bool
    $c< :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Bool
    compare :: Either3 a b c -> Either3 a b c -> Ordering
    $ccompare :: forall a b c.
    (Ord a, Ord b, Ord c) =>
    Either3 a b c -> Either3 a b c -> Ordering
    Ord, Int -> Either3 a b c -> ShowS
    [Either3 a b c] -> ShowS
    Either3 a b c -> String
    (Int -> Either3 a b c -> ShowS)
    -> (Either3 a b c -> String)
    -> ([Either3 a b c] -> ShowS)
    -> Show (Either3 a b c)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall a b c.
    (Show a, Show b, Show c) =>
    Int -> Either3 a b c -> ShowS
    forall a b c. (Show a, Show b, Show c) => [Either3 a b c] -> ShowS
    forall a b c. (Show a, Show b, Show c) => Either3 a b c -> String
    showList :: [Either3 a b c] -> ShowS
    $cshowList :: forall a b c. (Show a, Show b, Show c) => [Either3 a b c] -> ShowS
    show :: Either3 a b c -> String
    $cshow :: forall a b c. (Show a, Show b, Show c) => Either3 a b c -> String
    showsPrec :: Int -> Either3 a b c -> ShowS
    $cshowsPrec :: forall a b c.
    (Show a, Show b, Show c) =>
    Int -> Either3 a b c -> ShowS
    Show)

    -- | Partition a list into 3 groups.
    --
    --   Preserves the relative order or elements.
    --
    partitionEithers3 :: [Either3 a b c] -> ([a], [b], [c])
    partitionEithers3 :: forall a b c. [Either3 a b c] -> ([a], [b], [c])
    partitionEithers3 = \case
      []     -> ([], [], [])
      (Either3 a b c
    x:[Either3 a b c]
    xs) -> case Either3 a b c
    x of
          In1 a
    a -> (a
    aa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    as, [b]
    bs, [c]
    cs)
          In2 b
    b -> ([a]
    as, b
    bb -> [b] -> [b]
    forall a. a -> [a] -> [a]
    :[b]
    bs, [c]
    cs)
          In3 c
    c -> ([a]
    as, [b]
    bs, c
    cc -> [c] -> [c]
    forall a. a -> [a] -> [a]
    :[c]
    cs)
        where ([a]
    as, [b]
    bs, [c]
    cs) = [Either3 a b c] -> ([a], [b], [c])
    forall a b c. [Either3 a b c] -> ([a], [b], [c])
    partitionEithers3 [Either3 a b c]
    xs

    mapEither3M :: Applicative m => (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])
    mapEither3M :: forall (m :: * -> *) a b c d.
    Applicative m =>
    (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])
    mapEither3M a -> m (Either3 b c d)
    f [a]
    xs = [Either3 b c d] -> ([b], [c], [d])
    forall a b c. [Either3 a b c] -> ([a], [b], [c])
    partitionEithers3 ([Either3 b c d] -> ([b], [c], [d]))
    -> m [Either3 b c d] -> m ([b], [c], [d])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (a -> m (Either3 b c d)) -> [a] -> m [Either3 b c d]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m (Either3 b c d)
    f [a]
    xs

    forEither3M :: Applicative m => [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
    forEither3M :: forall (m :: * -> *) a b c d.
    Applicative m =>
    [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
    forEither3M = ((a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d]))
    -> [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])
    forall (m :: * -> *) a b c d.
    Applicative m =>
    (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])
    mapEither3M