module Morley.Util.SizedList
(
SizedList
, SizedList'(.., (::<), Nil')
, SomeSizedList(..)
, SingIPeano
, IsoNatPeano
, append
, reverse
, head
, tail
, withNonEmpty
, withList
, fromList
, fromListMaybe
, fromListMaybe'
, unsafeFromList
, generate
, generate'
, replicate
, replicate'
, replicateT
, singleton
, toNonEmpty
, zipWith
, unzipWith
, zip
, unzip
, index'
, index
, indexMaybe
, length'
, 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
type SizedList (n :: Nat) a = SizedList' (ToPeano n) a
data SizedList' (n :: Peano) a where
Nil :: SizedList' 'Z a
(:<) :: ~a -> ~(SizedList' n a) -> SizedList' ('S n) a
infixr 5 :<
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 (::<) #-}
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
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
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')
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'
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
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'
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'
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'
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
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 :: 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)
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
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 :: 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 (,)
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
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)
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 :: 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 :: 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`
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 :: 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
:: 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
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
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
head :: SizedList' ('S n) a -> a
head :: forall (n :: Peano) a. SizedList' ('S n) a -> a
head (a
x :< SizedList' n a
_) = a
x
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
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
:: 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
:: 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
:: 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
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