{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Type-level non-empty lists
module Data.SOP.NonEmpty (
    NonEmpty (..)
    -- * Proofs
  , IsNonEmpty (..)
  , ProofNonEmpty (..)
  , checkIsNonEmpty
    -- * Working with 'NonEmpty'
  , nonEmptyFromList
  , nonEmptyHead
  , nonEmptyInit
  , nonEmptyLast
  , nonEmptyMapOne
  , nonEmptyMapTwo
  , nonEmptyStrictPrefixes
  , nonEmptyToList
  ) where

import           Control.Applicative
import qualified Data.Foldable as Foldable
import           Data.Kind (Type)
import           Data.Proxy
import           Data.SOP.Sing

{-------------------------------------------------------------------------------
  NonEmpty
-------------------------------------------------------------------------------}

-- | Non-empty variation on 'AtMost'
type NonEmpty :: [Type] -> Type -> Type
data NonEmpty xs a where
  NonEmptyOne  :: !a -> NonEmpty (x ': xs) a
  NonEmptyCons :: !a -> !(NonEmpty xs a) -> NonEmpty (x ': xs) a

deriving instance Eq a   => Eq          (NonEmpty xs a)
deriving instance Show a => Show        (NonEmpty xs a)
deriving instance           Functor     (NonEmpty xs)
deriving instance           Foldable    (NonEmpty xs)
deriving instance           Traversable (NonEmpty xs)

instance (IsNonEmpty xs, SListI xs) => Applicative (NonEmpty xs) where
  pure :: forall a. a -> NonEmpty xs a
  pure :: forall a. a -> NonEmpty xs a
pure a
a = case Proxy xs -> ProofNonEmpty xs
forall {a} (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
forall (proxy :: [*] -> *). proxy xs -> ProofNonEmpty xs
isNonEmpty (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) of
             ProofNonEmpty{} -> Shape xs -> NonEmpty (x : xs) a
forall x (xs' :: [*]). Shape xs' -> NonEmpty (x : xs') a
go Shape xs
forall k (xs :: [k]). SListI xs => Shape xs
shape
    where
      go :: forall x xs'. Shape xs' -> NonEmpty (x : xs') a
      go :: forall x (xs' :: [*]). Shape xs' -> NonEmpty (x : xs') a
go Shape xs'
ShapeNil        = a -> NonEmpty (x : xs') a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
a
      go (ShapeCons Shape xs
xs') = a -> NonEmpty xs' a -> NonEmpty (x : xs') a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
a (Shape xs -> NonEmpty (x : xs) a
forall x (xs' :: [*]). Shape xs' -> NonEmpty (x : xs') a
go Shape xs
xs')
  <*> :: forall a b. NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
(<*>) = NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go
    where
      go :: NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
      go :: forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go (NonEmptyOne  a -> b
f)    (NonEmptyOne  a
x)    = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  (a -> b
f a
x)
      go (NonEmptyCons a -> b
f NonEmpty xs (a -> b)
_)  (NonEmptyOne  a
x)    = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  (a -> b
f a
x)
      go (NonEmptyOne  a -> b
f)    (NonEmptyCons a
x NonEmpty xs a
_)  = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  (a -> b
f a
x)
      go (NonEmptyCons a -> b
f NonEmpty xs (a -> b)
fs) (NonEmptyCons a
x NonEmpty xs a
xs) = b -> NonEmpty xs b -> NonEmpty (x : xs) b
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons (a -> b
f a
x) (NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go NonEmpty xs (a -> b)
fs NonEmpty xs a
NonEmpty xs a
xs)

{-------------------------------------------------------------------------------
  Working with 'NonEmpty'
-------------------------------------------------------------------------------}

-- | Analogue of 'head'
nonEmptyHead :: NonEmpty xs a -> a
nonEmptyHead :: forall (xs :: [*]) a. NonEmpty xs a -> a
nonEmptyHead (NonEmptyOne  a
x)   = a
x
nonEmptyHead (NonEmptyCons a
x NonEmpty xs a
_) = a
x

-- | Analogue of 'last'
nonEmptyLast :: NonEmpty xs a -> a
nonEmptyLast :: forall (xs :: [*]) a. NonEmpty xs a -> a
nonEmptyLast = (Maybe (NonEmpty xs a), a) -> a
forall a b. (a, b) -> b
snd ((Maybe (NonEmpty xs a), a) -> a)
-> (NonEmpty xs a -> (Maybe (NonEmpty xs a), a))
-> NonEmpty xs a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit

-- | Analogue of 'init'
nonEmptyInit :: NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit :: forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit (NonEmptyOne  a
x)    = (Maybe (NonEmpty xs a)
forall a. Maybe a
Nothing, a
x)
nonEmptyInit (NonEmptyCons a
x NonEmpty xs a
xs) =
    case NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit NonEmpty xs a
xs of
      (Maybe (NonEmpty xs a)
Nothing  , a
final) -> (NonEmpty xs a -> Maybe (NonEmpty xs a)
forall a. a -> Maybe a
Just (a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  a
x)     , a
final)
      (Just NonEmpty xs a
xs' , a
final) -> (NonEmpty xs a -> Maybe (NonEmpty xs a)
forall a. a -> Maybe a
Just (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x NonEmpty xs a
xs') , a
final)

-- | Build a 'NonEmpty' from a list. Returns 'Nothing' when the list is empty
-- or when it's longer than @xs@.
nonEmptyFromList :: forall xs a. SListI xs => [a] -> Maybe (NonEmpty xs a)
nonEmptyFromList :: forall (xs :: [*]) a. SListI xs => [a] -> Maybe (NonEmpty xs a)
nonEmptyFromList = SList xs -> [a] -> Maybe (NonEmpty xs a)
forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go (forall (xs :: [*]). SListI xs => SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList @xs)
  where
    go :: forall xs'. SList xs' -> [a] -> Maybe (NonEmpty xs' a)
    go :: forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go SList xs'
s [a]
ys = case (SList xs'
s, [a]
ys) of
        (SList xs'
SCons, [a
y])   -> NonEmpty xs' a -> Maybe (NonEmpty xs' a)
forall a. a -> Maybe a
Just (NonEmpty xs' a -> Maybe (NonEmpty xs' a))
-> NonEmpty xs' a -> Maybe (NonEmpty xs' a)
forall a b. (a -> b) -> a -> b
$ a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
y
        (SList xs'
SCons, a
y:[a]
ys') -> a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
y (NonEmpty xs a -> NonEmpty xs' a)
-> Maybe (NonEmpty xs a) -> Maybe (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SList xs -> [a] -> Maybe (NonEmpty xs a)
forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList [a]
ys'
        (SList xs'
SCons, [])    -> Maybe (NonEmpty xs' a)
forall a. Maybe a
Nothing
        (SList xs'
SNil,  [a]
_)     -> Maybe (NonEmpty xs' a)
forall a. Maybe a
Nothing

-- | Convert a 'NonEmpty' to a list.
nonEmptyToList :: forall xs a. NonEmpty xs a -> [a]
nonEmptyToList :: forall (xs :: [*]) a. NonEmpty xs a -> [a]
nonEmptyToList = NonEmpty xs a -> [a]
forall (xs' :: [*]). NonEmpty xs' a -> [a]
go
  where
    go :: forall xs'. NonEmpty xs' a -> [a]
    go :: forall (xs' :: [*]). NonEmpty xs' a -> [a]
go (NonEmptyOne  a
x)    = [a
x]
    go (NonEmptyCons a
x NonEmpty xs a
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NonEmpty xs a -> [a]
forall (xs' :: [*]). NonEmpty xs' a -> [a]
go NonEmpty xs a
xs

-- | A strict prefixes
--
-- >    nonEmptyStrictPrefixes (fromJust (nonEmptyFromList [1..4]))
-- > == [ NonEmptyOne  1
-- >    , NonEmptyCons 1 $ NonEmptyOne  2
-- >    , NonEmptyCons 1 $ NonEmptyCons 2 $ NonEmptyOne 3
-- >    ]
nonEmptyStrictPrefixes :: NonEmpty xs a -> [NonEmpty xs a]
nonEmptyStrictPrefixes :: forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
nonEmptyStrictPrefixes = NonEmpty xs a -> [NonEmpty xs a]
forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go
  where
    go :: NonEmpty xs a -> [NonEmpty xs a]
    go :: forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go (NonEmptyOne  a
_)    = []
    go (NonEmptyCons a
x NonEmpty xs a
xs) = a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
x NonEmpty xs a -> [NonEmpty xs a] -> [NonEmpty xs a]
forall a. a -> [a] -> [a]
: (NonEmpty xs a -> NonEmpty xs a)
-> [NonEmpty xs a] -> [NonEmpty xs a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x) (NonEmpty xs a -> [NonEmpty xs a]
forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go NonEmpty xs a
xs)

-- | Apply the specified function to exactly one element
nonEmptyMapOne :: forall m xs a. Alternative m
               => (a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapOne :: forall (m :: * -> *) (xs :: [*]) a.
Alternative m =>
(a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapOne a -> m a
f = NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go
  where
    go :: NonEmpty xs' a -> m (NonEmpty xs' a)
    go :: forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go (NonEmptyOne  a
x)    = a -> NonEmpty xs' a
a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> NonEmpty xs' a) -> m a -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
    go (NonEmptyCons a
x NonEmpty xs a
xs) = [m (NonEmpty xs' a)] -> m (NonEmpty xs' a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum [
          (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
`NonEmptyCons` NonEmpty xs a
xs) (a -> NonEmpty xs' a) -> m a -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
        , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty xs' a)
-> m (NonEmpty xs a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
        ]

-- | Variation on 'nonEmptyMapOne' where we try to apply the function to
-- /pairs/ of elements
nonEmptyMapTwo :: forall m xs a. Alternative m
               => (a -> m a) -- Used when we reached the end of the list
               -> (a -> a -> m (a, a))
               -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapTwo :: forall (m :: * -> *) (xs :: [*]) a.
Alternative m =>
(a -> m a)
-> (a -> a -> m (a, a)) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapTwo a -> m a
f a -> a -> m (a, a)
g = NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go
  where
    go :: NonEmpty xs' a -> m (NonEmpty xs' a)
    go :: forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go (NonEmptyOne a
x) =
        a -> NonEmpty xs' a
a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> NonEmpty xs' a) -> m a -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
    go (NonEmptyCons a
x xs :: NonEmpty xs a
xs@(NonEmptyOne a
y)) = [m (NonEmpty xs' a)] -> m (NonEmpty xs' a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum [
          (\(a
x', a
y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x' (a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
y')) ((a, a) -> NonEmpty xs' a) -> m (a, a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> m (a, a)
g a
x a
y
        , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty xs' a)
-> m (NonEmpty xs a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
        ]
    go (NonEmptyCons a
x xs :: NonEmpty xs a
xs@(NonEmptyCons a
y NonEmpty xs a
zs)) = [m (NonEmpty xs' a)] -> m (NonEmpty xs' a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum [
          (\(a
x', a
y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x' (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
y' NonEmpty xs a
zs)) ((a, a) -> NonEmpty xs' a) -> m (a, a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> m (a, a)
g a
x a
y
        , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (x :: [*]) xs. a -> NonEmpty x a -> NonEmpty (xs : x) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty xs' a)
-> m (NonEmpty xs a) -> m (NonEmpty xs' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
        ]


{-------------------------------------------------------------------------------
  Proofs
-------------------------------------------------------------------------------}

type ProofNonEmpty :: [a] -> Type
data ProofNonEmpty xs where
  ProofNonEmpty :: Proxy x -> Proxy xs -> ProofNonEmpty (x ': xs)

class IsNonEmpty xs where
  isNonEmpty :: proxy xs -> ProofNonEmpty xs

instance IsNonEmpty (x ': xs) where
  isNonEmpty :: forall (proxy :: [a] -> *).
proxy (x : xs) -> ProofNonEmpty (x : xs)
isNonEmpty proxy (x : xs)
_ = Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
forall {k} (x :: k) (xs :: [k]).
Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
ProofNonEmpty (forall (t :: a). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x) (forall (t :: [a]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs)

checkIsNonEmpty :: forall xs. SListI xs => Proxy xs -> Maybe (ProofNonEmpty xs)
checkIsNonEmpty :: forall {a} (xs :: [a]).
SListI xs =>
Proxy xs -> Maybe (ProofNonEmpty xs)
checkIsNonEmpty Proxy xs
_ = case forall (xs :: [a]). SListI xs => SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList @xs of
    SList xs
SNil  -> Maybe (ProofNonEmpty xs)
forall a. Maybe a
Nothing
    SList xs
SCons -> ProofNonEmpty xs -> Maybe (ProofNonEmpty xs)
forall a. a -> Maybe a
Just (ProofNonEmpty xs -> Maybe (ProofNonEmpty xs))
-> ProofNonEmpty xs -> Maybe (ProofNonEmpty xs)
forall a b. (a -> b) -> a -> b
$ Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
forall {k} (x :: k) (xs :: [k]).
Proxy x -> Proxy xs -> ProofNonEmpty (x : xs)
ProofNonEmpty Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy xs
forall {k} (t :: k). Proxy t
Proxy