{-# LANGUAGE CPP #-}

-- | Non-empty lists.
--
--   Better name @List1@ for non-empty lists, plus missing functionality.
--
--   Import:
--   @
--
--     {-# LANGUAGE PatternSynonyms #-}
--
--     import           Agda.Utils.List1 (List1, pattern (:|))
--     import qualified Agda.Utils.List1 as List1
--
--   @



{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
  -- because of https://gitlab.haskell.org/ghc/ghc/issues/10339

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

-- | Lossless 'toList', opposite of 'nonEmpty'.
--
toList' :: Maybe (List1 a) -> [a]
toList' :: forall a. Maybe (List1 a) -> [a]
toList' = [a] -> (List1 a -> [a]) -> Maybe (List1 a) -> [a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] List1 a -> [a]
List1 a -> [Item (List1 a)]
forall l. IsList l => l -> [Item l]
toList

-- | Safe version of 'Data.List.NonEmpty.fromList'.

fromListSafe
  :: List1 a  -- ^ Default value if convertee is empty.
  -> [a]      -- ^ List to convert, supposedly non-empty.
  -> List1 a  -- ^ Converted list.
fromListSafe :: forall a. List1 a -> [a] -> List1 a
fromListSafe List1 a
err   [] = List1 a
err
fromListSafe List1 a
_ (a
x:[a]
xs) = a
x a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs

-- | Return the last element and the rest.

initLast :: List1 a -> ([a], a)
initLast :: forall a. List1 a -> ([a], a)
initLast = List1 a -> [a]
forall a. NonEmpty a -> [a]
List1.init (List1 a -> [a]) -> (List1 a -> a) -> List1 a -> ([a], a)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& List1 a -> a
forall a. NonEmpty a -> a
List1.last
  -- traverses twice, but does not create intermediate pairs

-- | Last two elements (safe).
--   O(n).
last2 :: List1 a -> Maybe (a, a)
last2 :: forall a. List1 a -> Maybe (a, a)
last2 (a
x :| a
y : [a]
xs) = (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just ((a, a) -> Maybe (a, a)) -> (a, a) -> Maybe (a, a)
forall a b. (a -> b) -> a -> b
$ a -> a -> [a] -> (a, a)
forall a. a -> a -> [a] -> (a, a)
List.last2' a
x a
y [a]
xs
last2 NonEmpty a
_ = Maybe (a, a)
forall a. Maybe a
Nothing

-- | Build a list with one element.

#if !(MIN_VERSION_base(4,15,0))
singleton :: a -> List1 a
singleton = (:| [])
#endif

#if !MIN_VERSION_base(4,16,0)
-- | Append a list to a non-empty list.

appendList :: List1 a -> [a] -> List1 a
appendList (x :| xs) ys = x :| mappend xs ys

-- | Prepend a list to a non-empty list.

prependList :: [a] -> List1 a -> List1 a
prependList as bs = Prelude.foldr (<|) bs as
#endif

-- | More precise type for @snoc@.

snoc :: [a] -> a -> List1 a
snoc :: forall a. [a] -> a -> List1 a
snoc [a]
as a
a = [a] -> NonEmpty a -> NonEmpty a
forall a. [a] -> NonEmpty a -> NonEmpty a
prependList [a]
as (NonEmpty a -> NonEmpty a) -> NonEmpty a -> NonEmpty a
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| []

-- | @'groupOn' f = 'groupBy' (('==') \`on\` f) '.' 'List.sortBy' ('compare' \`on\` f)@.
-- O(n log n).
groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
groupOn :: forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
groupOn a -> b
f = (a -> a -> Bool) -> [a] -> [NonEmpty a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==) (b -> b -> Bool) -> (a -> b) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) ([a] -> [NonEmpty a]) -> ([a] -> [a]) -> [a] -> [NonEmpty a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
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 = (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
List1.groupBy1 (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==) (b -> b -> Bool) -> (a -> b) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) (NonEmpty a -> NonEmpty (NonEmpty a))
-> (NonEmpty a -> NonEmpty a)
-> NonEmpty a
-> NonEmpty (NonEmpty a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
List1.sortBy (b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)

-- | More precise type for 'Agda.Utils.List.groupBy''.
--
-- A variant of 'List.groupBy' which applies the predicate to consecutive
-- pairs.
-- O(n).
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 ([(Bool, a)] -> [List1 a]) -> [(Bool, a)] -> [List1 a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> (Bool, a)) -> [a] -> [a] -> [(Bool, a)]
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) = ((Bool, a) -> Bool) -> [(Bool, a)] -> ([(Bool, a)], [(Bool, a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.span (Bool, a) -> Bool
forall a b. (a, b) -> a
fst [(Bool, a)]
ys
    = (a
x a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| ((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
List.map (Bool, a) -> a
forall a b. (a, b) -> b
snd [(Bool, a)]
xs) List1 a -> [List1 a] -> [List1 a]
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

-- | Split a list into sublists. Generalisation of the prelude function
--   @words@.
--   Same as 'Data.List.Split.wordsBy' and 'Data.List.Extra.wordsBy',
--   but with the non-emptyness guarantee on the chunks.
--   O(n).
--
--   > words xs == wordsBy isSpace xs
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 (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhile a -> Bool
p [a]
as of
    []   -> []
    a
x:[a]
xs -> (a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
ys) NonEmpty a -> [NonEmpty a] -> [NonEmpty a]
forall a. a -> [a] -> [a]
: [a] -> [NonEmpty a]
loop [a]
zs where ([a]
ys, [a]
zs) = (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.break a -> Bool
p [a]
xs

-- | Breaks a list just /after/ an element satisfying the predicate is
--   found.
--
--   >>> breakAfter even [1,3,5,2,4,7,8]
--   ([1,3,5,2],[4,7,8])

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) = (a -> Bool) -> a -> [a] -> (NonEmpty a, [a])
forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
List.breakAfter1 a -> Bool
p a
x [a]
xs

-- | Concatenate one or more non-empty lists.

concat :: [List1 a] -> [a]
concat :: forall a. [List1 a] -> [a]
concat = (List1 a -> [a]) -> [List1 a] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap List1 a -> [a]
List1 a -> [Item (List1 a)]
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 = (a -> NonEmpty b) -> NonEmpty a -> NonEmpty b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
(=<<)

-- | Like 'Data.List.union'.  Duplicates in the first list are not removed.
-- O(nm).
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 a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
List.union [a]
as ((a -> Bool) -> NonEmpty a -> [a]
forall a. (a -> Bool) -> NonEmpty a -> [a]
filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
a) NonEmpty a
bs)

-- * Recovering non-emptyness.

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 (List1 a -> b) -> List1 a -> b
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> List1 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 (List1 a -> b) -> List1 a -> b
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> List1 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
_ = m
forall a. Null a => a
empty
unlessNull (a
x : [a]
xs) List1 a -> m
f = List1 a -> m
f (List1 a -> m) -> List1 a -> m
forall a b. (a -> b) -> a -> b
$ a
x a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| [a]
xs

-- * List functions with no special behavior for non-empty lists.

-- | Checks if all the elements in the list are equal. Assumes that
--   the 'Eq' instance stands for an equivalence relation.
--   O(n).
allEqual :: Eq a => List1 a -> Bool
allEqual :: forall a. Eq a => List1 a -> Bool
allEqual (a
x :| [a]
xs) = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs

-- | Like 'Maybe.catMaybes'.

catMaybes :: List1 (Maybe a) -> [a]
catMaybes :: forall a. List1 (Maybe a) -> [a]
catMaybes =  [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
Maybe.catMaybes ([Maybe a] -> [a])
-> (List1 (Maybe a) -> [Maybe a]) -> List1 (Maybe a) -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Maybe a) -> [Maybe a]
forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'List1.filter'.

mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
mapMaybe :: forall a b. (a -> Maybe b) -> List1 a -> [b]
mapMaybe a -> Maybe b
f = (a -> Maybe b) -> [a] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe a -> Maybe b
f ([a] -> [b]) -> (List1 a -> [a]) -> List1 a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 a -> [a]
forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.Either.partitionEithers'.

partitionEithers :: List1 (Either a b) -> ([a], [b])
partitionEithers :: forall a b. List1 (Either a b) -> ([a], [b])
partitionEithers = [Either a b] -> ([a], [b])
forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers ([Either a b] -> ([a], [b]))
-> (List1 (Either a b) -> [Either a b])
-> List1 (Either a b)
-> ([a], [b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Either a b) -> [Either a b]
forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.Either.lefts'.

lefts :: List1 (Either a b) -> [a]
lefts :: forall a b. List1 (Either a b) -> [a]
lefts = [Either a b] -> [a]
forall a b. [Either a b] -> [a]
Either.lefts  ([Either a b] -> [a])
-> (List1 (Either a b) -> [Either a b])
-> List1 (Either a b)
-> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Either a b) -> [Either a b]
forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.Either.rights'.

rights :: List1 (Either a b) -> [b]
rights :: forall a b. List1 (Either a b) -> [b]
rights = [Either a b] -> [b]
forall a b. [Either a b] -> [b]
Either.rights  ([Either a b] -> [b])
-> (List1 (Either a b) -> [Either a b])
-> List1 (Either a b)
-> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Either a b) -> [Either a b]
forall a. NonEmpty a -> [a]
List1.toList


-- | Non-efficient, monadic 'nub'.
-- O(n²).
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 a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:|) ([a] -> NonEmpty a) -> m [a] -> m (NonEmpty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do (a -> a -> m Bool) -> [a] -> m [a]
forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> [a] -> m [a]
List.nubM a -> a -> m Bool
eq ([a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a -> m Bool) -> [a] -> m [a]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not (Bool -> Bool) -> (a -> m Bool) -> a -> m Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> a -> a -> m Bool
eq a
a) [a]
as

-- | Like 'Control.Monad.zipWithM'.

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) = c -> [c] -> NonEmpty c
forall a. a -> [a] -> NonEmpty a
(:|) (c -> [c] -> NonEmpty c) -> m c -> m ([c] -> NonEmpty c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m c
f a
a b
b m ([c] -> NonEmpty c) -> m [c] -> m (NonEmpty c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> b -> m c) -> [a] -> [b] -> m [c]
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

-- | Like 'Control.Monad.zipWithM'.

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 m c -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (a -> b -> m c) -> [a] -> [b] -> m ()
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

-- | List 'Data.List.foldr' but with a base case for the singleton list.

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 (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ a -> [a] -> b
loop a
y [a]
ys