-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Defines lists with length fixed on the type level
module Morley.Util.SizedList
  ( -- * Base types
    SizedList
  , SizedList'(.., (::<), Nil')
  , SomeSizedList(..)

  -- * Utility type synonyms (re-exports)
  , SingIPeano
  , IsoNatPeano

  -- * Basic
  , append
  , reverse
  , head
  , tail

  -- * Construction
  , withNonEmpty
  , withList
  , fromList
  , fromListMaybe
  , fromListMaybe'
  , unsafeFromList
  , generate
  , generate'
  , replicate
  , replicate'
  , replicateT
  , singleton

  -- * Conversion
  , toNonEmpty

  -- * Zips
  , zipWith
  , unzipWith
  , zip
  , unzip

  -- * Index access
  , index'
  , index
  , indexMaybe
  , length'

  -- * Sublists
  , take
  , drop
  , splitAt
  ) where

import Prelude hiding
  (drop, fromList, head, replicate, reverse, splitAt, tail, take, unzip, zip, zipWith)
import Prelude qualified (fromList)

import Data.Constraint ((\\))
import Data.List qualified as List
import Data.Singletons (SingI(..))
import Fmt (Buildable(..))
import GHC.TypeNats (Nat)
import Text.Show (Show(..), showParen, showString)

import Morley.Util.Peano

-- $setup
--
-- >>> import Prelude hiding (drop, fromList, head, replicate, reverse, splitAt, tail, take, unzip, zip, zipWith)
-- >>> import Morley.Util.Peano
-- >>> import Data.Constraint ((\\))

-- | The primary fixed-size list type. Parametrized by a type-level 'Nat' as length and type
-- as element type.
--
-- Internally powered by 'Peano' numbers
type SizedList (n :: Nat) a = SizedList' (ToPeano n) a

-- | Actual fixed-size list GADT, parametrized by 'Peano' natural. You generally don't want to
-- use this directly, since 'Peano' is not very ergonomic. Prefer using 'SizedList' unless
-- writing utility functions that need to do type-level arithmetic.
--
-- Note that while this has the usual instances, 'Applicative' and 'Monad' are not the same
-- as for regular lists: they implement "zipper" semantics, i.e. @f \<*\> x@ is the same as
-- @zipWith ($) f x@
data SizedList' (n :: Peano) a where
  Nil :: SizedList' 'Z a -- ^ Empty list
  (:<) :: ~a -> ~(SizedList' n a) -> SizedList' ('S n) a -- ^ Cons
infixr 5 :<

-- | Sized list cons pattern. Unlike ':<' this pattern can be used to auto-deduce the type of
-- the result, e.g.
--
-- >>> a ::< b ::< c ::< Nil' = pure 'a'
-- >>> (a, b, c)
-- ('a','a','a')
infixr 5 ::<
pattern (::<) :: a -> SizedList' n a -> SizedList' ('S n) a
pattern a $m::< :: forall {r} {a} {n :: Peano}.
SizedList' ('S n) a
-> (a -> SizedList' n a -> r) -> ((# #) -> r) -> r
::< l <- a :< l
{-# COMPLETE (::<) #-}

-- | Sized list Nil pattern. Unlike 'Nil' this pattern can be used to auto-deduce the type of
-- the result, see '::<'.
pattern Nil' :: SizedList' 'Z a
pattern $mNil' :: forall {r} {a}.
SizedList' 'Z a -> ((# #) -> r) -> ((# #) -> r) -> r
Nil' <- Nil
{-# COMPLETE Nil' #-}

deriving stock instance Eq a => Eq (SizedList' n a)
deriving stock instance Foldable (SizedList' n)
deriving stock instance Traversable (SizedList' n)
deriving stock instance Functor (SizedList' n)
instance Show a => Show (SizedList' n a) where
  showsPrec :: Int -> SizedList' n a -> ShowS
showsPrec Int
d (a
x :< SizedList' n a
xs) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :< " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SizedList' n a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
prec SizedList' n a
xs
    where prec :: Int
prec = Int
5
  showsPrec Int
_ SizedList' n a
Nil = String -> ShowS
showString String
"Nil"
deriving stock instance Ord a => Ord (SizedList' n a)

instance Buildable a => Buildable (SizedList' n a) where
  build :: SizedList' n a -> Doc
build = [a] -> Doc
forall a. Buildable a => a -> Doc
build ([a] -> Doc) -> (SizedList' n a -> [a]) -> SizedList' n a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizedList' n a -> [a]
SizedList' n a -> [Element (SizedList' n a)]
forall t. Container t => t -> [Element t]
toList

instance Container (SizedList' n a)

instance SingI n => Applicative (SizedList' n) where
  pure :: forall a. a -> SizedList' n a
pure = SingNat n -> a -> SizedList' n a
forall (n :: Peano) a. SingNat n -> a -> SizedList' n a
replicate' (forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n)
  <*> :: forall a b.
SizedList' n (a -> b) -> SizedList' n a -> SizedList' n b
(<*>) = ((a -> b) -> a -> b)
-> SizedList' n (a -> b)
-> SizedList' n a
-> SizedList' (MinPeano n n) b
forall a b c (n :: Peano) (m :: Peano).
(a -> b -> c)
-> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($) ((MinPeano n n ~ n) =>
 SizedList' n (a -> b) -> SizedList' n a -> SizedList' n b)
-> (MinPeano n n :~: n)
-> SizedList' n (a -> b)
-> SizedList' n a
-> SizedList' n b
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n -> MinPeano n n :~: n
forall (n :: Peano). SingNat n -> MinPeano n n :~: n
minIdempotency (forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n)

instance SingI n => Monad (SizedList' n) where
  SizedList' n a
f >>= :: forall a b.
SizedList' n a -> (a -> SizedList' n b) -> SizedList' n b
>>= (a -> SizedList' n b
k :: a -> SizedList' n b) = SingNat 'Z -> SizedList' n a -> SizedList' n b
forall (k :: Peano) (m :: Peano).
(AddPeano k m ~ n) =>
SingNat k -> SizedList' m a -> SizedList' m b
go SingNat 'Z
SZ SizedList' n a
f
    where
      go :: forall k m. (AddPeano k m ~ n)
         => SingNat k -> SizedList' m a -> SizedList' m b
      go :: forall (k :: Peano) (m :: Peano).
(AddPeano k m ~ n) =>
SingNat k -> SizedList' m a -> SizedList' m b
go SingNat k
_ SizedList' m a
Nil = SizedList' m b
SizedList' 'Z b
forall a. SizedList' 'Z a
Nil
      go SingNat k
i (a
el :< (SizedList' n a
rest :: SizedList' m' a)) =
        SingNat k -> SizedList' n b -> b
forall (m :: Peano) (n :: Peano) a.
((m > n) ~ 'True) =>
SingNat n -> SizedList' m a -> a
index' SingNat k
i (a -> SizedList' n b
k a
el) b -> SizedList' n b -> SizedList' ('S n) b
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SingNat ('S k) -> SizedList' n a -> SizedList' n b
forall (k :: Peano) (m :: Peano).
(AddPeano k m ~ n) =>
SingNat k -> SizedList' m a -> SizedList' m b
go (Sing k -> SingNat ('S k)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing k
SingNat k
i) SizedList' n a
rest
        ((n ~ 'S (AddPeano k n)) => SizedList' m b)
-> (n :~: 'S (AddPeano k n)) -> SizedList' m b
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (y :: Peano) (x :: Peano).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity @m' SingNat k
i (((n > k) ~ 'True) => SizedList' m b)
-> ((n > k) :~: 'True) -> SizedList' m b
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: Peano) (m :: Peano) (n :: Peano).
(AddPeano k ('S m) ~ n) =>
SingNat k -> (n > k) :~: 'True
additivity @k @m' @n SingNat k
i

-- | Existential capturing a fixed-size list whose length is only known at runtime.
--
-- In most cases, it's probably better to use regular lists, but this can be occasionally
-- useful.
--
-- We do not provide the 'Applicative' and 'Monad' instances, since "zipper" applicative is
-- ill-defined for lists of different length, and having inconsistent instances between
-- this and 'SizedList' is more confusing than useful.
--
-- Unlike regular sized list, @SomeSizedList@ is a 'Semigroup' and a 'Monoid':
--
-- >>> fromList "ab" <> fromList "de" <> mempty :: SomeSizedList Char
-- SomeSizedList (SS (SS (SS (SS SZ)))) ('a' :< 'b' :< 'd' :< 'e' :< Nil)
data SomeSizedList a where
  SomeSizedList :: SingNat n -> SizedList' n a -> SomeSizedList a

deriving stock instance Foldable SomeSizedList
deriving stock instance Traversable SomeSizedList
deriving stock instance Functor SomeSizedList
deriving stock instance Show a => Show (SomeSizedList a)

instance Semigroup (SomeSizedList a) where
  (SomeSizedList SingNat n
sl SizedList' n a
l) <> :: SomeSizedList a -> SomeSizedList a -> SomeSizedList a
<> (SomeSizedList SingNat n
sr SizedList' n a
r) = SingNat (AddPeano n n)
-> SizedList' (AddPeano n n) a -> SomeSizedList a
forall (n :: Peano) a.
SingNat n -> SizedList' n a -> SomeSizedList a
SomeSizedList (SingNat n -> SingNat n -> SingNat (AddPeano n n)
forall (n :: Peano) (m :: Peano).
SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd SingNat n
sl SingNat n
sr) (SizedList' (AddPeano n n) a -> SomeSizedList a)
-> SizedList' (AddPeano n n) a -> SomeSizedList a
forall a b. (a -> b) -> a -> b
$ SizedList' n a
l SizedList' n a -> SizedList' n a -> SizedList' (AddPeano n n) a
forall (n :: Peano) a (m :: Peano).
SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a
`append` SizedList' n a
r

instance Monoid (SomeSizedList a) where
  mempty :: SomeSizedList a
mempty = SingNat 'Z -> SizedList' 'Z a -> SomeSizedList a
forall (n :: Peano) a.
SingNat n -> SizedList' n a -> SomeSizedList a
SomeSizedList SingNat 'Z
SZ SizedList' 'Z a
forall a. SizedList' 'Z a
Nil

instance Buildable a => Buildable (SomeSizedList a) where
  build :: SomeSizedList a -> Doc
build = [a] -> Doc
forall a. Buildable a => a -> Doc
build ([a] -> Doc) -> (SomeSizedList a -> [a]) -> SomeSizedList a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeSizedList a -> [a]
SomeSizedList a -> [Element (SomeSizedList a)]
forall t. Container t => t -> [Element t]
toList

instance Container (SomeSizedList a)

instance (n ~ 'S 'Z) => One (SizedList' n a) where
  type OneItem (SizedList' n a) = a
  one :: OneItem (SizedList' n a) -> SizedList' n a
one = a -> SizedList 1 a
OneItem (SizedList' n a) -> SizedList' n a
forall a. a -> SizedList 1 a
singleton

instance FromList (SomeSizedList a) where
  type ListElement (SomeSizedList a) = a

  fromList :: FromListC (SomeSizedList a) =>
[ListElement (SomeSizedList a)] -> SomeSizedList a
fromList = [a] -> SomeSizedList a
[ListElement (SomeSizedList a)] -> SomeSizedList a
forall a. [a] -> SomeSizedList a
fromList

-- A type-specific `fromList` for use in qualified imports
fromList :: forall a. [a] -> SomeSizedList a
fromList :: forall a. [a] -> SomeSizedList a
fromList [] = SingNat 'Z -> SizedList' 'Z a -> SomeSizedList a
forall (n :: Peano) a.
SingNat n -> SizedList' n a -> SomeSizedList a
SomeSizedList SingNat 'Z
SZ SizedList' 'Z a
forall a. SizedList' 'Z a
Nil
fromList (a
x:[a]
xs) = case [a] -> SomeSizedList a
forall a. [a] -> SomeSizedList a
fromList [a]
xs of
  SomeSizedList SingNat n
n SizedList' n a
xs' -> SingNat ('S n) -> SizedList' ('S n) a -> SomeSizedList a
forall (n :: Peano) a.
SingNat n -> SizedList' n a -> SomeSizedList a
SomeSizedList (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
SingNat n
n) (a
x a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' n a
xs')

-- | Try to make a fixed-size list from a regular list, given a 'Nat'. Returns 'Nothing' if
-- the regular list has incorrect length.
--
-- >>> fromListMaybe @3 [1, 2, 3]
-- Just (1 :< 2 :< 3 :< Nil)
--
-- >>> fromListMaybe @4 [1, 2, 3]
-- Nothing
fromListMaybe :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => [a] -> Maybe (SizedList n a)
fromListMaybe :: forall (n :: Nat) (n' :: Peano) a.
(SingIPeano n, IsoNatPeano n n') =>
[a] -> Maybe (SizedList n a)
fromListMaybe = SingNat (ToPeano n) -> [a] -> Maybe (SizedList' (ToPeano n) a)
forall (m :: Peano) a. SingNat m -> [a] -> Maybe (SizedList' m a)
fromListMaybe' (SingNat (ToPeano n) -> [a] -> Maybe (SizedList' (ToPeano n) a))
-> SingNat (ToPeano n) -> [a] -> Maybe (SizedList' (ToPeano n) a)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n'

-- | Same as 'fromListMaybe', but accepts an explicit 'Peano' singleton.
fromListMaybe' :: SingNat m -> [a] -> Maybe (SizedList' m a)
fromListMaybe' :: forall (m :: Peano) a. SingNat m -> [a] -> Maybe (SizedList' m a)
fromListMaybe' SingNat m
SZ [] = SizedList' m a -> Maybe (SizedList' m a)
forall a. a -> Maybe a
Just SizedList' m a
SizedList' 'Z a
forall a. SizedList' 'Z a
Nil
fromListMaybe' (SS Sing n
n) (a
x:[a]
xs) = (a
x a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:<) (SizedList' n a -> SizedList' m a)
-> Maybe (SizedList' n a) -> Maybe (SizedList' m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SingNat n -> [a] -> Maybe (SizedList' n a)
forall (m :: Peano) a. SingNat m -> [a] -> Maybe (SizedList' m a)
fromListMaybe' Sing n
SingNat n
n [a]
xs
fromListMaybe' SingNat m
_ [a]
_ = Maybe (SizedList' m a)
forall a. Maybe a
Nothing

-- | Run some computation with a 'NonEmpty' list converted to 'SizedList'. Similar
-- to pattern-matching on 'SomeSizedList', but asserts on the type level that list is
-- in fact not empty.
withNonEmpty
  :: forall a r. NonEmpty a
  -> (forall n. SingNat ('S n) -> SizedList' ('S n) a -> r)
  -> r
withNonEmpty :: forall a r.
NonEmpty a
-> (forall (n :: Peano).
    SingNat ('S n) -> SizedList' ('S n) a -> r)
-> r
withNonEmpty (a
x :| [a]
xs) forall (n :: Peano). SingNat ('S n) -> SizedList' ('S n) a -> r
f = case [a] -> SomeSizedList a
forall a. [a] -> SomeSizedList a
fromList [a]
xs of
  SomeSizedList SingNat n
n SizedList' n a
xs' -> SingNat ('S n) -> SizedList' ('S n) a -> r
forall (n :: Peano). SingNat ('S n) -> SizedList' ('S n) a -> r
f (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
SingNat n
n) (SizedList' ('S n) a -> r) -> SizedList' ('S n) a -> r
forall a b. (a -> b) -> a -> b
$ a
x a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' n a
xs'

-- | Run some computation with a list converted to 'SizedList'. The same as
-- pattern-matching on 'SomeSizedList'.
withList :: forall a r. [a] -> (forall n. SingNat n -> SizedList' n a -> r) -> r
withList :: forall a r.
[a] -> (forall (n :: Peano). SingNat n -> SizedList' n a -> r) -> r
withList [a]
xs forall (n :: Peano). SingNat n -> SizedList' n a -> r
f = case [a] -> SomeSizedList a
forall a. [a] -> SomeSizedList a
fromList [a]
xs of
  SomeSizedList SingNat n
n SizedList' n a
xs' -> SingNat n -> SizedList' n a -> r
forall (n :: Peano). SingNat n -> SizedList' n a -> r
f SingNat n
n SizedList' n a
xs'

-- | Construct a list of given length from a regular list. Raise error
-- if length is inconsistent.
--
-- >>> unsafeFromList @3 [1, 2, 3]
-- 1 :< 2 :< 3 :< Nil
--
-- >>> unsafeFromList @1 [1, 2, 3]
-- *** Exception: Invalid list size in Morley.Util.SizedList.unsafeFromList
-- ...
unsafeFromList
  :: forall n n' a. (SingIPeano n, IsoNatPeano n n', HasCallStack)
  => [a] -> SizedList n a
unsafeFromList :: forall (n :: Nat) (n' :: Peano) a.
(SingIPeano n, IsoNatPeano n n', HasCallStack) =>
[a] -> SizedList n a
unsafeFromList = SingNat (ToPeano n) -> [a] -> SizedList' (ToPeano n) a
forall (n :: Peano) a.
HasCallStack =>
SingNat n -> [a] -> SizedList' n a
unsafeFromList' (SingNat (ToPeano n) -> [a] -> SizedList' (ToPeano n) a)
-> SingNat (ToPeano n) -> [a] -> SizedList' (ToPeano n) a
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n'

-- | Same as 'unsafeFromList', but accepts explicit 'Peano' singleton
unsafeFromList' :: forall n a. HasCallStack => SingNat n -> [a] -> SizedList' n a
unsafeFromList' :: forall (n :: Peano) a.
HasCallStack =>
SingNat n -> [a] -> SizedList' n a
unsafeFromList' SingNat n
sg [a]
xs =
  SizedList' n a -> Maybe (SizedList' n a) -> SizedList' n a
forall a. a -> Maybe a -> a
fromMaybe (Text -> SizedList' n a
forall a. HasCallStack => Text -> a
error Text
"Invalid list size in Morley.Util.SizedList.unsafeFromList") (Maybe (SizedList' n a) -> SizedList' n a)
-> Maybe (SizedList' n a) -> SizedList' n a
forall a b. (a -> b) -> a -> b
$
  SingNat n -> [a] -> Maybe (SizedList' n a)
forall (m :: Peano) a. SingNat m -> [a] -> Maybe (SizedList' m a)
fromListMaybe' SingNat n
sg [a]
xs

-- | Convert a 'SizedList' to 'NonEmpty'
toNonEmpty :: SizedList' ('S n) a -> NonEmpty a
toNonEmpty :: forall (n :: Peano) a. SizedList' ('S n) a -> NonEmpty a
toNonEmpty (a
x :< SizedList' n a
xs) = a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| SizedList' n a -> [Element (SizedList' n a)]
forall t. Container t => t -> [Element t]
toList SizedList' n a
xs

-- | Replicate a value @n@ times. This is a version
-- returning an existential. You probably want
-- 'replicateT' or `replicate'`.
replicate :: Natural -> a -> SomeSizedList a
replicate :: forall a. Nat -> a -> SomeSizedList a
replicate Nat
0 a
_ = SingNat 'Z -> SizedList' 'Z a -> SomeSizedList a
forall (n :: Peano) a.
SingNat n -> SizedList' n a -> SomeSizedList a
SomeSizedList SingNat 'Z
SZ SizedList' 'Z a
forall a. SizedList' 'Z a
Nil
replicate Nat
n a
x = case Nat -> a -> SomeSizedList a
forall a. Nat -> a -> SomeSizedList a
replicate (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) a
x of
  SomeSizedList SingNat n
m SizedList' n a
xs -> SingNat ('S n) -> SizedList' ('S n) a -> SomeSizedList a
forall (n :: Peano) a.
SingNat n -> SizedList' n a -> SomeSizedList a
SomeSizedList (Sing n -> SingNat ('S n)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing n
SingNat n
m) (a
x a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' n a
xs)

-- | Replicate a value @n@ times, where @n@ is passed as a type-level natural.
-- This is essentially a synonym for 'pure'.
--
-- >>> replicateT @5 'a'
-- 'a' :< 'a' :< 'a' :< 'a' :< 'a' :< Nil
replicateT :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => a -> SizedList n a
replicateT :: forall (n :: Nat) (n' :: Peano) a.
(SingIPeano n, IsoNatPeano n n') =>
a -> SizedList n a
replicateT = a -> SizedList' n' a
a -> SizedList' (ToPeano n) a
forall a. a -> SizedList' n' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | As 'replicateT', but accepts an explicit 'Peano' singleton.
replicate' :: SingNat n -> a -> SizedList' n a
replicate' :: forall (n :: Peano) a. SingNat n -> a -> SizedList' n a
replicate' SingNat n
SZ a
_ = SizedList' n a
SizedList' 'Z a
forall a. SizedList' 'Z a
Nil
replicate' (SS Sing n
n) a
x = a
x a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SingNat n -> a -> SizedList' n a
forall (n :: Peano) a. SingNat n -> a -> SizedList' n a
replicate' Sing n
SingNat n
n a
x

-- | Zip two lists of potentially different lengths. If one list is
-- longer, extraneous elements will be ignored.
--
-- >>> zip (unsafeFromList @3 "abc") (unsafeFromList @4 "defg")
-- ('a','d') :< ('b','e') :< ('c','f') :< Nil
zip :: SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) (a, b)
zip :: forall (n :: Peano) a (m :: Peano) b.
SizedList' n a
-> SizedList' m b -> SizedList' (MinPeano n m) (a, b)
zip = (a -> b -> (a, b))
-> SizedList' n a
-> SizedList' m b
-> SizedList' (MinPeano n m) (a, b)
forall a b c (n :: Peano) (m :: Peano).
(a -> b -> c)
-> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c
zipWith (,)

-- | Zip using a binary operation.
zipWith :: (a -> b -> c) -> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c
zipWith :: forall a b c (n :: Peano) (m :: Peano).
(a -> b -> c)
-> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c
zipWith a -> b -> c
_ SizedList' n a
Nil SizedList' m b
_ = SizedList' 'Z c
SizedList' (MinPeano n m) c
forall a. SizedList' 'Z a
Nil
zipWith a -> b -> c
_ SizedList' n a
_ SizedList' m b
Nil = SizedList' 'Z c
SizedList' (MinPeano n m) c
forall a. SizedList' 'Z a
Nil
zipWith a -> b -> c
f (a
x :< SizedList' n a
xs) (b
y :< SizedList' n b
ys) = a -> b -> c
f a
x b
y c
-> SizedList' (MinPeano n n) c -> SizedList' ('S (MinPeano n n)) c
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< (a -> b -> c)
-> SizedList' n a -> SizedList' n b -> SizedList' (MinPeano n n) c
forall a b c (n :: Peano) (m :: Peano).
(a -> b -> c)
-> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c
zipWith a -> b -> c
f SizedList' n a
xs SizedList' n b
ys

-- | Given a type-level 'Nat' and a generator function, make a 'SizedList'
--
-- Indexing starts at @0@
--
-- >>> generate @3 (+1)
-- 1 :< 2 :< 3 :< Nil
generate :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => (Natural -> a) -> SizedList' n' a
generate :: forall (n :: Nat) (n' :: Peano) a.
(SingIPeano n, IsoNatPeano n n') =>
(Nat -> a) -> SizedList' n' a
generate Nat -> a
f = SingNat n'
-> (forall (m :: Peano).
    ((n' > m) ~ 'True) =>
    (SingNat m, Nat) -> a)
-> SizedList' n' a
forall (n :: Peano) a.
SingNat n
-> (forall (m :: Peano).
    ((n > m) ~ 'True) =>
    (SingNat m, Nat) -> a)
-> SizedList' n a
generate' (forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n') (Nat -> a
f (Nat -> a) -> ((SingNat m, Nat) -> Nat) -> (SingNat m, Nat) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SingNat m, Nat) -> Nat
forall a b. (a, b) -> b
snd)

-- | Same as 'generate', but accepts an explicit 'Peano' singleton, and passes an explicit
-- singleton as index to the generator function
generate' :: forall n a. SingNat n
          -> (forall m. (n > m ~ 'True) => (SingNat m, Natural) -> a)
          -> SizedList' n a
generate' :: forall (n :: Peano) a.
SingNat n
-> (forall (m :: Peano).
    ((n > m) ~ 'True) =>
    (SingNat m, Nat) -> a)
-> SizedList' n a
generate' SingNat n
n forall (m :: Peano). ((n > m) ~ 'True) => (SingNat m, Nat) -> a
f = Nat -> SingNat 'Z -> SingNat n -> SizedList' n a
forall (k :: Peano) (m :: Peano).
(AddPeano k m ~ n) =>
Nat -> SingNat k -> SingNat m -> SizedList' m a
go Nat
0 SingNat 'Z
SZ SingNat n
n
  where
  go :: forall k m. (AddPeano k m ~ n)
     => Natural -> SingNat k -> SingNat m -> SizedList' m a
  go :: forall (k :: Peano) (m :: Peano).
(AddPeano k m ~ n) =>
Nat -> SingNat k -> SingNat m -> SizedList' m a
go Nat
_ SingNat k
_ SingNat m
SZ = SizedList' m a
SizedList' 'Z a
forall a. SizedList' 'Z a
Nil
  go Nat
i SingNat k
k (SS (SingNat n
m :: SingNat m')) =
    (SingNat k, Nat) -> a
forall (m :: Peano). ((n > m) ~ 'True) => (SingNat m, Nat) -> a
f (SingNat k
k, Nat
i) a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< Nat -> SingNat ('S k) -> SingNat n -> SizedList' n a
forall (k :: Peano) (m :: Peano).
(AddPeano k m ~ n) =>
Nat -> SingNat k -> SingNat m -> SizedList' m a
go (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) (Sing k -> SingNat ('S k)
forall (n :: Peano). Sing n -> SingNat ('S n)
SS Sing k
SingNat k
k) SingNat n
m ((n ~ 'S (AddPeano k n)) => SizedList' m a)
-> (n :~: 'S (AddPeano k n)) -> SizedList' m a
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (y :: Peano) (x :: Peano).
SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity @m' SingNat k
k (((n > k) ~ 'True) => SizedList' m a)
-> ((n > k) :~: 'True) -> SizedList' m a
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: Peano) (m :: Peano) (n :: Peano).
(AddPeano k ('S m) ~ n) =>
SingNat k -> (n > k) :~: 'True
additivity @k @m' @n SingNat k
k


-- | Reverse a 'SizedList'
--
-- >>> reverse $ generate @3 (+1)
-- 3 :< 2 :< 1 :< Nil
reverse :: forall n a. SingI n => SizedList' n a -> SizedList' n a
reverse :: forall (n :: Peano) a. SingI n => SizedList' n a -> SizedList' n a
reverse = SingNat n -> [a] -> SizedList' n a
forall (n :: Peano) a.
HasCallStack =>
SingNat n -> [a] -> SizedList' n a
unsafeFromList' (forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n) ([a] -> SizedList' n a)
-> (SizedList' n a -> [a]) -> SizedList' n a -> SizedList' n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
forall a. [a] -> [a]
List.reverse ([a] -> [a]) -> (SizedList' n a -> [a]) -> SizedList' n a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizedList' n a -> [a]
SizedList' n a -> [Element (SizedList' n a)]
forall t. Container t => t -> [Element t]
toList

-- | Append two sized lists.
--
-- >>> generate @3 (+1) `append` generate @3 (+11)
-- 1 :< 2 :< 3 :< 11 :< 12 :< 13 :< Nil
append :: SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a
append :: forall (n :: Peano) a (m :: Peano).
SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a
append SizedList' n a
Nil SizedList' m a
ys = SizedList' m a
SizedList' (AddPeano n m) a
ys
append (a
x :< SizedList' n a
xs) SizedList' m a
ys = a
x a
-> SizedList' (AddPeano n m) a -> SizedList' ('S (AddPeano n m)) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a
forall (n :: Peano) a (m :: Peano).
SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a
append SizedList' n a
xs SizedList' m a
ys
infixr 5 `append`

-- | Unzip a sized list using a function
unzipWith :: (a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)
unzipWith :: forall a b c (n :: Peano).
(a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)
unzipWith a -> (b, c)
_ SizedList' n a
Nil = (SizedList' n b
SizedList' 'Z b
forall a. SizedList' 'Z a
Nil, SizedList' n c
SizedList' 'Z c
forall a. SizedList' 'Z a
Nil)
unzipWith a -> (b, c)
f (a
a :< SizedList' n a
as) =
  let (b
b, c
c) = a -> (b, c)
f a
a
      (SizedList' n b
bs, SizedList' n c
cs) = (a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)
forall a b c (n :: Peano).
(a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)
unzipWith a -> (b, c)
f SizedList' n a
as
  in (b
b b -> SizedList' n b -> SizedList' ('S n) b
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' n b
bs, c
c c -> SizedList' n c -> SizedList' ('S n) c
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' n c
cs)

-- | Unzip a sized list of pairs
unzip :: SizedList' n (b, c) -> (SizedList' n b, SizedList' n c)
unzip :: forall (n :: Peano) b c.
SizedList' n (b, c) -> (SizedList' n b, SizedList' n c)
unzip = ((b, c) -> (b, c))
-> SizedList' n (b, c) -> (SizedList' n b, SizedList' n c)
forall a b c (n :: Peano).
(a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)
unzipWith (b, c) -> (b, c)
forall a. a -> a
id

-- | Index into a list using a type-level constant
--
-- >>> index @2 $ unsafeFromList @5 [1..5]
-- 3
index
  :: forall i m a. (m > ToPeano i ~ 'True, SingIPeano i)
  => SizedList' m a -> a
index :: forall (i :: Nat) (m :: Peano) a.
((m > ToPeano i) ~ 'True, SingIPeano i) =>
SizedList' m a -> a
index = SingNat (ToPeano i) -> SizedList' m a -> a
forall (m :: Peano) (n :: Peano) a.
((m > n) ~ 'True) =>
SingNat n -> SizedList' m a -> a
index' (SingNat (ToPeano i) -> SizedList' m a -> a)
-> SingNat (ToPeano i) -> SizedList' m a -> a
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingIPeano n => SingNat (ToPeano n)
peanoSing @i

-- | Same as 'index', but accepts an explicit 'Peano' singleton
--
-- Note, that if you wish to use this with `generate'`, indexing into some
-- other list, for one, you may want to rethink your approach, since it's
-- pretty inefficient.
-- For two, you may run into arcane compiler error messages, e.g.
--
-- >>> let someList = 'a' :< 'b' :< 'c' :< Nil
-- >>> generate' @_ @Char (peanoSing @2) $ \(sg, _) -> index' sg someList
-- ...
-- ... Could not deduce (('S ('S ('S 'Z)) > m) ~ 'True)
-- ...
--
-- To make this work, use 'transitivity' proof:
--
-- >>> let slLen = length' someList
-- >>> let len = peanoSing @2
-- >>> generate' @_ @Char len $ \(sg, _) -> index' sg someList \\ transitivity slLen len sg
-- 'a' :< 'b' :< Nil
index' :: (m > n ~ 'True) => SingNat n -> SizedList' m a -> a
index' :: forall (m :: Peano) (n :: Peano) a.
((m > n) ~ 'True) =>
SingNat n -> SizedList' m a -> a
index' SingNat n
SZ (a
x :< SizedList' n a
_)= a
x
index' (SS Sing n
n) (a
_ :< SizedList' n a
xs) = SingNat n -> SizedList' n a -> a
forall (m :: Peano) (n :: Peano) a.
((m > n) ~ 'True) =>
SingNat n -> SizedList' m a -> a
index' Sing n
SingNat n
n SizedList' n a
xs

-- | Use a term-level 'Natural' to index into a list. Since the natural can
-- be larger than the length of the list, returns a 'Maybe'.
indexMaybe :: Natural -> SizedList' m a -> Maybe a
indexMaybe :: forall (m :: Peano) a. Nat -> SizedList' m a -> Maybe a
indexMaybe Nat
_ SizedList' m a
Nil = Maybe a
forall a. Maybe a
Nothing
indexMaybe Nat
0 (a
x :< SizedList' n a
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
indexMaybe Nat
n (a
_ :< SizedList' n a
xs) = Nat -> SizedList' n a -> Maybe a
forall (m :: Peano) a. Nat -> SizedList' m a -> Maybe a
indexMaybe (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) SizedList' n a
xs

-- | Get the first element of a non-empty list
head :: SizedList' ('S n) a -> a
head :: forall (n :: Peano) a. SizedList' ('S n) a -> a
head (a
x :< SizedList' n a
_) = a
x

-- | Get elements after the first
tail :: SizedList' ('S n) a -> SizedList' n a
tail :: forall (n :: Peano) a. SizedList' ('S n) a -> SizedList' n a
tail (a
_ :< SizedList' n a
xs) = SizedList' n a
SizedList' n a
xs

-- | Construct a list of one element
singleton :: a -> SizedList 1 a
singleton :: forall a. a -> SizedList 1 a
singleton a
x = a
x a -> SizedList' 'Z a -> SizedList' ('S 'Z) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:< SizedList' 'Z a
forall a. SizedList' 'Z a
Nil

-- | Take a fixed number of elements, given by a type-level 'Nat'. Must be
-- smaller than the size of the list
--
-- >>> take @3 $ unsafeFromList @5 [1..5]
-- 1 :< 2 :< 3 :< Nil
take
  :: forall n n' m a. (m >= ToPeano n ~ 'True, SingIPeano n, IsoNatPeano n n')
  => SizedList' m a -> SizedList n a
take :: forall (n :: Nat) (n' :: Peano) (m :: Peano) a.
((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') =>
SizedList' m a -> SizedList n a
take = (SizedList' n' a, SizedList' (SubPeano m n') a) -> SizedList' n' a
forall a b. (a, b) -> a
fst ((SizedList' n' a, SizedList' (SubPeano m n') a)
 -> SizedList' n' a)
-> (SizedList' m a
    -> (SizedList' n' a, SizedList' (SubPeano m n') a))
-> SizedList' m a
-> SizedList' n' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (n' :: Peano) (m :: Peano) a.
((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') =>
SizedList' m a -> (SizedList n a, SizedList' (SubPeano m n') a)
splitAt @n

-- | Drop a fixed number of elements, given by a type-level 'Nat'. Must be
-- smaller than the size of the list
--
-- >>> drop @3 $ unsafeFromList @5 [1..5]
-- 4 :< 5 :< Nil
drop
  :: forall n n' m a. (m >= ToPeano n ~ 'True, SingIPeano n, IsoNatPeano n n')
  => SizedList' m a -> SizedList' (SubPeano m (ToPeano n)) a
drop :: forall (n :: Nat) (n' :: Peano) (m :: Peano) a.
((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') =>
SizedList' m a -> SizedList' (SubPeano m (ToPeano n)) a
drop = (SizedList' n' a, SizedList' (SubPeano m n') a)
-> SizedList' (SubPeano m n') a
forall a b. (a, b) -> b
snd ((SizedList' n' a, SizedList' (SubPeano m n') a)
 -> SizedList' (SubPeano m n') a)
-> (SizedList' m a
    -> (SizedList' n' a, SizedList' (SubPeano m n') a))
-> SizedList' m a
-> SizedList' (SubPeano m n') a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (n' :: Peano) (m :: Peano) a.
((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') =>
SizedList' m a -> (SizedList n a, SizedList' (SubPeano m n') a)
splitAt @n

-- | @splitAt \@n xs = (take \@n xs, drop \@n xs)@, but traverses the list only
-- once
--
-- >>> splitAt @3 $ unsafeFromList @5 [1..5]
-- (1 :< 2 :< 3 :< Nil,4 :< 5 :< Nil)
splitAt
  :: forall n n' m a. (m >= ToPeano n ~ 'True, SingIPeano n, IsoNatPeano n n')
  => SizedList' m a -> (SizedList n a, SizedList' (SubPeano m n') a)
splitAt :: forall (n :: Nat) (n' :: Peano) (m :: Peano) a.
((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') =>
SizedList' m a -> (SizedList n a, SizedList' (SubPeano m n') a)
splitAt = SingNat (ToPeano n)
-> SizedList' m a
-> (SizedList' (ToPeano n) a,
    SizedList' (SubPeano m (ToPeano n)) a)
forall (l :: Peano) (k :: Peano).
((l >= k) ~ 'True) =>
SingNat k
-> SizedList' l a -> (SizedList' k a, SizedList' (SubPeano l k) a)
go (SingNat (ToPeano n)
 -> SizedList' m a
 -> (SizedList' (ToPeano n) a,
     SizedList' (SubPeano m (ToPeano n)) a))
-> SingNat (ToPeano n)
-> SizedList' m a
-> (SizedList' (ToPeano n) a,
    SizedList' (SubPeano m (ToPeano n)) a)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n'
  where
  go :: (l >= k ~ 'True)
     => SingNat k -> SizedList' l a
     -> (SizedList' k a, SizedList' (SubPeano l k) a)
  go :: forall (l :: Peano) (k :: Peano).
((l >= k) ~ 'True) =>
SingNat k
-> SizedList' l a -> (SizedList' k a, SizedList' (SubPeano l k) a)
go SingNat k
SZ SizedList' l a
xs = (SizedList' k a
SizedList' 'Z a
forall a. SizedList' 'Z a
Nil, SizedList' l a
SizedList' (SubPeano l k) a
xs)
  go (SS Sing n
n) (a
x :< SizedList' n a
xs) = (SizedList' n a -> SizedList' k a)
-> (SizedList' n a, SizedList' (SubPeano l k) a)
-> (SizedList' k a, SizedList' (SubPeano l k) a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (a
x a -> SizedList' n a -> SizedList' ('S n) a
forall a (n :: Peano). a -> SizedList' n a -> SizedList' ('S n) a
:<) ((SizedList' n a, SizedList' (SubPeano l k) a)
 -> (SizedList' k a, SizedList' (SubPeano l k) a))
-> (SizedList' n a, SizedList' (SubPeano l k) a)
-> (SizedList' k a, SizedList' (SubPeano l k) a)
forall a b. (a -> b) -> a -> b
$ SingNat n
-> SizedList' n a -> (SizedList' n a, SizedList' (SubPeano n n) a)
forall (l :: Peano) (k :: Peano).
((l >= k) ~ 'True) =>
SingNat k
-> SizedList' l a -> (SizedList' k a, SizedList' (SubPeano l k) a)
go Sing n
SingNat n
n SizedList' n a
xs

-- | Return a Peano singleton representing the list length
length' :: forall n a. (SingI n) => SizedList' n a -> SingNat n
length' :: forall (n :: Peano) a. SingI n => SizedList' n a -> SingNat n
length' SizedList' n a
_ = forall {k} (a :: k). SingI a => Sing a
forall (a :: Peano). SingI a => Sing a
sing @n