-- | Tools for 3-way partitioning.

module Agda.Utils.Three where

-- | Enum type with 3 elements.
--
data Three
  = One
  | Two
  | Three
  deriving (Three -> Three -> Bool
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
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
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
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]
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
xforall a. a -> [a] -> [a]
:[a]
as, [a]
bs, [a]
cs)
      Three
Two   -> ([a]
as, a
xforall a. a -> [a] -> [a]
:[a]
bs, [a]
cs)
      Three
Three -> ([a]
as, [a]
bs, a
xforall 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
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, Either3 a b c -> Either3 a b c -> Bool
Either3 a b c -> Either3 a b c -> Ordering
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
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
aforall a. a -> [a] -> [a]
:[a]
as, [b]
bs, [c]
cs)
      In2 b
b -> ([a]
as, b
bforall a. a -> [a] -> [a]
:[b]
bs, [c]
cs)
      In3 c
c -> ([a]
as, [b]
bs, c
cforall a. a -> [a] -> [a]
:[c]
cs)
    where ([a]
as, [b]
bs, [c]
cs) = 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 = forall a b c. [Either3 a b c] -> ([a], [b], [c])
partitionEithers3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a b c d.
Applicative m =>
(a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])
mapEither3M