{-# 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 qualified Data.List as List
import qualified Data.Maybe as Maybe
import qualified Data.Semigroup as Semigroup

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

-- | 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 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 = 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
  -- traverses twice, but does not create intermediate pairs

-- | 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 = 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
:| []

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

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

-- | 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) = 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall l. IsList l => l -> [Item l]
toList

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

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

-- * 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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 =  forall a. [Maybe a] -> [a]
Maybe.catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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

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

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

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

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

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

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


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

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

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

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