{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
module Agda.Utils.List1
( module Agda.Utils.List1
, module List1
) where
import Prelude hiding (filter)
import Control.Arrow ((&&&))
import Control.Monad (filterM)
import qualified Control.Monad as List (zipWithM, zipWithM_)
import qualified Data.Either as Either
import qualified Data.List as List
import qualified Data.Maybe as Maybe
import qualified Data.Semigroup as Semigroup
import qualified Data.List.NonEmpty (NonEmpty)
import Data.List.NonEmpty as List1 hiding (NonEmpty)
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Null (Null(..))
import qualified Agda.Utils.List as List
type List1 = Data.List.NonEmpty.NonEmpty
initLast :: List1 a -> ([a], a)
initLast :: forall a. List1 a -> ([a], a)
initLast = forall a. NonEmpty a -> [a]
List1.init forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. NonEmpty a -> a
List1.last
#if !(MIN_VERSION_base(4,15,0))
singleton :: a -> List1 a
singleton = (:| [])
#endif
#if !MIN_VERSION_base(4,16,0)
appendList :: List1 a -> [a] -> List1 a
appendList (x :| xs) ys = x :| mappend xs ys
prependList :: [a] -> List1 a -> List1 a
prependList as bs = foldr (<|) bs as
#endif
snoc :: [a] -> a -> List1 a
snoc :: forall a. [a] -> a -> List1 a
snoc [a]
as a
a = forall a. [a] -> NonEmpty a -> NonEmpty a
prependList [a]
as forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| []
groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
groupBy' a -> a -> Bool
_ [] = []
groupBy' a -> a -> Bool
p xxs :: [a]
xxs@(a
x : [a]
xs) = a -> [(Bool, a)] -> [List1 a]
grp a
x forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
List.zipWith (\ a
x a
y -> (a -> a -> Bool
p a
x a
y, a
y)) [a]
xxs [a]
xs
where
grp :: a -> [(Bool,a)] -> [List1 a]
grp :: a -> [(Bool, a)] -> [List1 a]
grp a
x [(Bool, a)]
ys
| let ([(Bool, a)]
xs, [(Bool, a)]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.span forall a b. (a, b) -> a
fst [(Bool, a)]
ys
= (a
x forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> b
snd [(Bool, a)]
xs) forall a. a -> [a] -> [a]
: case [(Bool, a)]
rest of
[] -> []
((Bool
_false, a
z) : [(Bool, a)]
zs) -> a -> [(Bool, a)] -> [List1 a]
grp a
z [(Bool, a)]
zs
breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
breakAfter :: forall a. (a -> Bool) -> List1 a -> (List1 a, [a])
breakAfter a -> Bool
p (a
x :| [a]
xs) = forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
List.breakAfter1 a -> Bool
p a
x [a]
xs
concat :: [List1 a] -> [a]
concat :: forall a. [List1 a] -> [a]
concat = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. NonEmpty a -> [a]
toList
union :: Eq a => List1 a -> List1 a -> List1 a
union :: forall a. Eq a => List1 a -> List1 a -> List1 a
union (a
a :| [a]
as) NonEmpty a
bs = a
a forall a. a -> [a] -> NonEmpty a
:| forall a. Eq a => [a] -> [a] -> [a]
List.union [a]
as (forall a. (a -> Bool) -> NonEmpty a -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= a
a) NonEmpty a
bs)
ifNull :: [a] -> b -> (List1 a -> b) -> b
ifNull :: forall a b. [a] -> b -> (List1 a -> b) -> b
ifNull [] b
b List1 a -> b
_ = b
b
ifNull (a
a : [a]
as) b
_ List1 a -> b
f = List1 a -> b
f forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as
ifNotNull :: [a] -> (List1 a -> b) -> b -> b
ifNotNull :: forall a b. [a] -> (List1 a -> b) -> b -> b
ifNotNull [] List1 a -> b
_ b
b = b
b
ifNotNull (a
a : [a]
as) List1 a -> b
f b
_ = List1 a -> b
f forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as
unlessNull :: Null m => [a] -> (List1 a -> m) -> m
unlessNull :: forall m a. Null m => [a] -> (List1 a -> m) -> m
unlessNull [] List1 a -> m
_ = forall a. Null a => a
empty
unlessNull (a
x : [a]
xs) List1 a -> m
f = List1 a -> m
f forall a b. (a -> b) -> a -> b
$ a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs
allEqual :: Eq a => List1 a -> Bool
allEqual :: forall a. Eq a => List1 a -> Bool
allEqual (a
x :| [a]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs
catMaybes :: List1 (Maybe a) -> [a]
catMaybes :: forall a. List1 (Maybe a) -> [a]
catMaybes = forall a. [Maybe a] -> [a]
Maybe.catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList
mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
mapMaybe :: forall a b. (a -> Maybe b) -> List1 a -> [b]
mapMaybe a -> Maybe b
f = forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe a -> Maybe b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList
partitionEithers :: List1 (Either a b) -> ([a], [b])
partitionEithers :: forall a b. List1 (Either a b) -> ([a], [b])
partitionEithers = forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList
lefts :: List1 (Either a b) -> [a]
lefts :: forall a b. List1 (Either a b) -> [a]
lefts = forall a b. [Either a b] -> [a]
Either.lefts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList
rights :: List1 (Either a b) -> [b]
rights :: forall a b. List1 (Either a b) -> [b]
rights = forall a b. [Either a b] -> [b]
Either.rights forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList
nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
nubM :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> List1 a -> m (List1 a)
nubM a -> a -> m Bool
eq (a
a :| [a]
as) = (a
a forall a. a -> [a] -> NonEmpty a
:|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> [a] -> m [a]
List.nubM a -> a -> m Bool
eq forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> a -> a -> m Bool
eq a
a) [a]
as
zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
zipWithM :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
zipWithM a -> b -> m c
f (a
a :| [a]
as) (b
b :| [b]
bs) = forall a. a -> [a] -> NonEmpty a
(:|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m c
f a
a b
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
List.zipWithM a -> b -> m c
f [a]
as [b]
bs
zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
zipWithM_ :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> List1 a -> List1 b -> m ()
zipWithM_ a -> b -> m c
f (a
a :| [a]
as) (b
b :| [b]
bs) = a -> b -> m c
f a
a b
b forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
List.zipWithM_ a -> b -> m c
f [a]
as [b]
bs