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

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

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

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

-- | 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]
forall a. NonEmpty a -> [a]
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 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 (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 (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