{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
module Agda.Utils.List1
( module Agda.Utils.List1
, module List1
, module IsList
) 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 Data.Function ( on )
import qualified Data.List as List
import qualified Data.Maybe as Maybe
import Data.List.NonEmpty as List1 hiding (fromList, toList)
import qualified Data.List.NonEmpty as List1 (toList)
import GHC.Exts as IsList ( IsList(..) )
import Agda.Utils.Functor ((<.>), (<&>))
import Agda.Utils.Null (Null(..))
import qualified Agda.Utils.List as List
type List1 = NonEmpty
type String1 = List1 Char
toList' :: Maybe (List1 a) -> [a]
toList' :: forall a. Maybe (List1 a) -> [a]
toList' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] forall l. IsList l => l -> [Item l]
toList
liftList1 :: (List1 a -> List1 b) -> [a] -> [b]
liftList1 :: forall a b. (List1 a -> List1 b) -> [a] -> [b]
liftList1 List1 a -> List1 b
f = forall a. Maybe (List1 a) -> [a]
toList' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap List1 a -> List1 b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe (NonEmpty a)
nonEmpty
fromListSafe
:: List1 a
-> [a]
-> List1 a
fromListSafe :: forall a. List1 a -> [a] -> List1 a
fromListSafe List1 a
err [] = List1 a
err
fromListSafe List1 a
_ (a
x:[a]
xs) = a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs
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
last2 :: List1 a -> Maybe (a, a)
last2 :: forall a. List1 a -> Maybe (a, a)
last2 (a
x :| a
y : [a]
xs) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> [a] -> (a, a)
List.last2' a
x a
y [a]
xs
last2 NonEmpty a
_ = forall a. Maybe a
Nothing
#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 = Prelude.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
:| []
groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
groupOn :: forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
groupOn a -> b
f = forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)
groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a)
groupOn1 :: forall b a. Ord b => (a -> b) -> List1 a -> List1 (List1 a)
groupOn1 a -> b
f = forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
List1.groupBy1 (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
List1.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)
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
groupByFst :: forall a b. Eq a => [(a,b)] -> [(a, List1 b)]
groupByFst :: forall a b. Eq a => [(a, b)] -> [(a, List1 b)]
groupByFst =
forall a b. (a -> b) -> [a] -> [b]
List.map (\ ((a
tag, b
b) :| [(a, b)]
xs) -> (a
tag, b
b forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> b
snd [(a, b)]
xs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
groupByFst1 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
groupByFst1 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
groupByFst1 =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ ((a
tag, b
b) :| [(a, b)]
xs) -> (a
tag, b
b forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> b
snd [(a, b)]
xs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
List1.groupBy1 (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
wordsBy :: (a -> Bool) -> [a] -> [List1 a]
wordsBy :: forall a. (a -> Bool) -> [a] -> [List1 a]
wordsBy a -> Bool
p = [a] -> [NonEmpty a]
loop
where
loop :: [a] -> [NonEmpty a]
loop [a]
as = case forall a. (a -> Bool) -> [a] -> [a]
List.dropWhile a -> Bool
p [a]
as of
[] -> []
a
x:[a]
xs -> (a
x forall a. a -> [a] -> NonEmpty a
:| [a]
ys) forall a. a -> [a] -> [a]
: [a] -> [NonEmpty a]
loop [a]
zs where ([a]
ys, [a]
zs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.break a -> Bool
p [a]
xs
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 l. IsList l => l -> [Item l]
toList
concatMap1 :: (a -> List1 b) -> List1 a -> List1 b
concatMap1 :: forall a b. (a -> List1 b) -> List1 a -> List1 b
concatMap1 = forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
(=<<)
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
find :: (a -> Bool) -> List1 a -> Maybe a
find :: forall a. (a -> Bool) -> List1 a -> Maybe a
find a -> Bool
f = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find a -> Bool
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
unwords :: List1 String -> String
unwords :: List1 String -> String
unwords = [String] -> String
List.unwords 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
foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b
foldr :: forall a b. (a -> b -> b) -> (a -> b) -> List1 a -> b
foldr a -> b -> b
f a -> b
g (a
x :| [a]
xs) = a -> [a] -> b
loop a
x [a]
xs
where
loop :: a -> [a] -> b
loop a
x [] = a -> b
g a
x
loop a
x (a
y : [a]
ys) = a -> b -> b
f a
x forall a b. (a -> b) -> a -> b
$ a -> [a] -> b
loop a
y [a]
ys
updateHead :: (a -> a) -> List1 a -> List1 a
updateHead :: forall a. (a -> a) -> List1 a -> List1 a
updateHead a -> a
f (a
a :| [a]
as) = a -> a
f a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as
updateLast :: (a -> a) -> List1 a -> List1 a
updateLast :: forall a. (a -> a) -> List1 a -> List1 a
updateLast a -> a
f (a
a :| [a]
as) = a -> [a] -> NonEmpty a
loop a
a [a]
as
where
loop :: a -> [a] -> NonEmpty a
loop a
a [] = forall a. a -> NonEmpty a
singleton forall a b. (a -> b) -> a -> b
$ a -> a
f a
a
loop a
a (a
b : [a]
bs) = forall a. a -> NonEmpty a -> NonEmpty a
cons a
a forall a b. (a -> b) -> a -> b
$ a -> [a] -> NonEmpty a
loop a
b [a]
bs
lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
lensHead :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> List1 a -> f (List1 a)
lensHead a -> f a
f (a
a :| [a]
as) = a -> f a
f a
a forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. a -> [a] -> NonEmpty a
:| [a]
as)
lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
lensLast :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> List1 a -> f (List1 a)
lensLast a -> f a
f (a
a :| [a]
as) = a -> [a] -> f (NonEmpty a)
loop a
a [a]
as
where
loop :: a -> [a] -> f (NonEmpty a)
loop a
a [] = forall a. a -> NonEmpty a
singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
a
loop a
a (a
b : [a]
bs) = forall a. a -> NonEmpty a -> NonEmpty a
cons a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a] -> f (NonEmpty a)
loop a
b [a]
bs