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