{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ConstraintKinds            #-}
module Basement.Sized.Vect
    ( Vect
    , MVect
    , unVect
    , toVect
    , empty
    , singleton
    , replicate
    , thaw
    , freeze
    , index
    , map
    , foldl'
    , foldr
    , cons
    , snoc
    , elem
    , sub
    , uncons
    , unsnoc
    , splitAt
    , all
    , any
    , find
    , reverse
    , sortBy
    , intersperse
    ) where

import           Basement.Compat.Base
import           Basement.Nat
import           Basement.NormalForm
import           Basement.Types.OffsetSize
import           Basement.Monad
import           Basement.PrimType (PrimType)
import qualified Basement.BoxedArray as A
--import qualified Basement.BoxedArray.Mutable as A hiding (sub)
import           Data.Proxy

newtype Vect (n :: Nat) a = Vect { forall (n :: Nat) a. Vect n a -> Array a
unVect :: A.Array a } deriving (Vect n a -> ()
forall (n :: Nat) a. NormalForm a => Vect n a -> ()
forall a. (a -> ()) -> NormalForm a
toNormalForm :: Vect n a -> ()
$ctoNormalForm :: forall (n :: Nat) a. NormalForm a => Vect n a -> ()
NormalForm, Vect n a -> Vect n a -> Bool
forall (n :: Nat) a. Eq a => Vect n a -> Vect n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Vect n a -> Vect n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => Vect n a -> Vect n a -> Bool
== :: Vect n a -> Vect n a -> Bool
$c== :: forall (n :: Nat) a. Eq a => Vect n a -> Vect n a -> Bool
Eq, Int -> Vect n a -> ShowS
forall (n :: Nat) a. Show a => Int -> Vect n a -> ShowS
forall (n :: Nat) a. Show a => [Vect n a] -> ShowS
forall (n :: Nat) a. Show a => Vect n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Vect n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [Vect n a] -> ShowS
show :: Vect n a -> String
$cshow :: forall (n :: Nat) a. Show a => Vect n a -> String
showsPrec :: Int -> Vect n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> Vect n a -> ShowS
Show)
newtype MVect (n :: Nat) ty st = MVect { forall (n :: Nat) ty st. MVect n ty st -> MArray ty st
unMVect :: A.MArray ty st }

instance Functor (Vect n) where
    fmap :: forall a b. (a -> b) -> Vect n a -> Vect n b
fmap = forall a b (n :: Nat). (a -> b) -> Vect n a -> Vect n b
map

toVect :: forall n ty . (KnownNat n, Countable ty n) => A.Array ty -> Maybe (Vect n ty)
toVect :: forall (n :: Nat) ty.
(KnownNat n, Countable ty n) =>
Array ty -> Maybe (Vect n ty)
toVect Array ty
b
    | CountOf ty
expected forall a. Eq a => a -> a -> Bool
== forall a. Array a -> CountOf a
A.length Array ty
b = forall a. a -> Maybe a
Just (forall (n :: Nat) a. Array a -> Vect n a
Vect Array ty
b)
    | Bool
otherwise = forall a. Maybe a
Nothing
  where
    expected :: CountOf ty
expected = forall (n :: Nat) ty. (KnownNat n, Countable ty n) => CountOf ty
toCount @n

empty :: Vect 0 ty
empty :: forall ty. Vect 0 ty
empty = forall (n :: Nat) a. Array a -> Vect n a
Vect forall a. Array a
A.empty

singleton :: ty -> Vect 1 ty
singleton :: forall ty. ty -> Vect 1 ty
singleton ty
a = forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. ty -> Array ty
A.singleton ty
a)

create :: forall a (n :: Nat) . (Countable a n, KnownNat n) => (Offset a -> a) -> Vect n a
create :: forall a (n :: Nat).
(Countable a n, KnownNat n) =>
(Offset a -> a) -> Vect n a
create Offset a -> a
f = forall (n :: Nat) a. Array a -> Vect n a
Vect forall a b. (a -> b) -> a -> b
$ forall ty. CountOf ty -> (Offset ty -> ty) -> Array ty
A.create CountOf a
sz Offset a -> a
f
  where
    sz :: CountOf a
sz = forall (n :: Nat) ty (proxy :: Nat -> *).
(KnownNat n, NatWithinBound (CountOf ty) n) =>
proxy n -> CountOf ty
natValCountOf (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

replicate :: forall n ty . (KnownNat n, Countable ty n) => ty -> Vect n ty
replicate :: forall (n :: Nat) ty.
(KnownNat n, Countable ty n) =>
ty -> Vect n ty
replicate ty
a = forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. CountOf ty -> ty -> Array ty
A.replicate (forall (n :: Nat) ty. (KnownNat n, Countable ty n) => CountOf ty
toCount @n) ty
a)

thaw :: (KnownNat n, PrimMonad prim) => Vect n ty -> prim (MVect n ty (PrimState prim))
thaw :: forall (n :: Nat) (prim :: * -> *) ty.
(KnownNat n, PrimMonad prim) =>
Vect n ty -> prim (MVect n ty (PrimState prim))
thaw Vect n ty
b = forall (n :: Nat) ty st. MArray ty st -> MVect n ty st
MVect forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (prim :: * -> *) ty.
PrimMonad prim =>
Array ty -> prim (MArray ty (PrimState prim))
A.thaw (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

freeze ::  (PrimMonad prim, Countable ty n) => MVect n ty (PrimState prim) -> prim (Vect n ty)
freeze :: forall (prim :: * -> *) ty (n :: Nat).
(PrimMonad prim, Countable ty n) =>
MVect n ty (PrimState prim) -> prim (Vect n ty)
freeze MVect n ty (PrimState prim)
b = forall (n :: Nat) a. Array a -> Vect n a
Vect forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (prim :: * -> *) ty.
PrimMonad prim =>
MArray ty (PrimState prim) -> prim (Array ty)
A.freeze (forall (n :: Nat) ty st. MVect n ty st -> MArray ty st
unMVect MVect n ty (PrimState prim)
b)

write :: PrimMonad prim => MVect n ty (PrimState prim) -> Offset ty -> ty -> prim ()
write :: forall (prim :: * -> *) (n :: Nat) ty.
PrimMonad prim =>
MVect n ty (PrimState prim) -> Offset ty -> ty -> prim ()
write (MVect MArray ty (PrimState prim)
ma) Offset ty
ofs ty
v = forall (prim :: * -> *) ty.
PrimMonad prim =>
MArray ty (PrimState prim) -> Offset ty -> ty -> prim ()
A.write MArray ty (PrimState prim)
ma Offset ty
ofs ty
v

read :: PrimMonad prim => MVect n ty (PrimState prim) -> Offset ty -> prim ty
read :: forall (prim :: * -> *) (n :: Nat) ty.
PrimMonad prim =>
MVect n ty (PrimState prim) -> Offset ty -> prim ty
read (MVect MArray ty (PrimState prim)
ma) Offset ty
ofs = forall (prim :: * -> *) ty.
PrimMonad prim =>
MArray ty (PrimState prim) -> Offset ty -> prim ty
A.read MArray ty (PrimState prim)
ma Offset ty
ofs

indexStatic :: forall i n ty . (KnownNat i, CmpNat i n ~ 'LT, Offsetable ty i) => Vect n ty -> ty
indexStatic :: forall (i :: Nat) (n :: Nat) ty.
(KnownNat i, CmpNat i n ~ 'LT, Offsetable ty i) =>
Vect n ty -> ty
indexStatic Vect n ty
b = forall ty. Array ty -> Offset ty -> ty
A.unsafeIndex (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b) (forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset @i)

index :: Vect n ty -> Offset ty -> ty
index :: forall (n :: Nat) ty. Vect n ty -> Offset ty -> ty
index Vect n ty
b Offset ty
ofs = forall ty. Array ty -> Offset ty -> ty
A.index (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b) Offset ty
ofs

map :: (a -> b) -> Vect n a -> Vect n b
map :: forall a b (n :: Nat). (a -> b) -> Vect n a -> Vect n b
map a -> b
f Vect n a
b = forall (n :: Nat) a. Array a -> Vect n a
Vect (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n a
b))

foldl' :: (a -> ty -> a) -> a -> Vect n ty -> a
foldl' :: forall a ty (n :: Nat). (a -> ty -> a) -> a -> Vect n ty -> a
foldl' a -> ty -> a
f a
acc Vect n ty
b = forall a ty. (a -> ty -> a) -> a -> Array ty -> a
A.foldl' a -> ty -> a
f a
acc (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

foldr :: (ty -> a -> a) -> a -> Vect n ty -> a
foldr :: forall ty a (n :: Nat). (ty -> a -> a) -> a -> Vect n ty -> a
foldr ty -> a -> a
f a
acc Vect n ty
b = forall ty a. (ty -> a -> a) -> a -> Array ty -> a
A.foldr ty -> a -> a
f a
acc (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

cons :: ty -> Vect n ty -> Vect (n+1) ty
cons :: forall ty (n :: Nat). ty -> Vect n ty -> Vect (n + 1) ty
cons ty
e = forall (n :: Nat) a. Array a -> Vect n a
Vect forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall ty. ty -> Array ty -> Array ty
A.cons ty
e forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (n :: Nat) a. Vect n a -> Array a
unVect

snoc :: Vect n ty -> ty -> Vect (n+1) ty
snoc :: forall (n :: Nat) ty. Vect n ty -> ty -> Vect (n + 1) ty
snoc Vect n ty
b = forall (n :: Nat) a. Array a -> Vect n a
Vect forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall ty. Array ty -> ty -> Array ty
A.snoc (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

sub :: forall i j n ty
     . ( (i <=? n) ~ 'True
       , (j <=? n) ~ 'True
       , (i <=? j) ~ 'True
       , KnownNat i
       , KnownNat j
       , Offsetable ty i
       , Offsetable ty j )
    => Vect n ty
    -> Vect (j-i) ty
sub :: forall (i :: Nat) (j :: Nat) (n :: Nat) ty.
((i <=? n) ~ 'True, (j <=? n) ~ 'True, (i <=? j) ~ 'True,
 KnownNat i, KnownNat j, Offsetable ty i, Offsetable ty j) =>
Vect n ty -> Vect (j - i) ty
sub Vect n ty
block = forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. Array ty -> Offset ty -> Offset ty -> Array ty
A.sub (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
block) (forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset @i) (forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset @j))

uncons :: forall n ty . (CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n)
       => Vect n ty
       -> (ty, Vect (n-1) ty)
uncons :: forall (n :: Nat) ty.
(CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n) =>
Vect n ty -> (ty, Vect (n - 1) ty)
uncons Vect n ty
b = (forall (i :: Nat) (n :: Nat) ty.
(KnownNat i, CmpNat i n ~ 'LT, Offsetable ty i) =>
Vect n ty -> ty
indexStatic @0 Vect n ty
b, forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. Array ty -> Offset ty -> Offset ty -> Array ty
A.sub (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b) Offset ty
1 (forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset @n)))

unsnoc :: forall n ty . (CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n)
       => Vect n ty
       -> (Vect (n-1) ty, ty)
unsnoc :: forall (n :: Nat) ty.
(CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n) =>
Vect n ty -> (Vect (n - 1) ty, ty)
unsnoc Vect n ty
b =
    ( forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. Array ty -> Offset ty -> Offset ty -> Array ty
A.sub (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b) Offset ty
0 (forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset @n forall a. Offset a -> Offset a -> Offset a
`offsetSub` Offset ty
1))
    , forall ty. Array ty -> Offset ty -> ty
A.unsafeIndex (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b) (forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset @n forall a. Offset a -> Offset a -> Offset a
`offsetSub` Offset ty
1))

splitAt :: forall i n ty . (CmpNat i n ~ 'LT, KnownNat i, Countable ty i) => Vect n ty -> (Vect i ty, Vect (n-i) ty)
splitAt :: forall (i :: Nat) (n :: Nat) ty.
(CmpNat i n ~ 'LT, KnownNat i, Countable ty i) =>
Vect n ty -> (Vect i ty, Vect (n - i) ty)
splitAt Vect n ty
b =
    let (Array ty
left, Array ty
right) = forall ty. CountOf ty -> Array ty -> (Array ty, Array ty)
A.splitAt (forall (n :: Nat) ty. (KnownNat n, Countable ty n) => CountOf ty
toCount @i) (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)
     in (forall (n :: Nat) a. Array a -> Vect n a
Vect Array ty
left, forall (n :: Nat) a. Array a -> Vect n a
Vect Array ty
right)

elem :: Eq ty => ty -> Vect n ty -> Bool
elem :: forall ty (n :: Nat). Eq ty => ty -> Vect n ty -> Bool
elem ty
e Vect n ty
b = forall ty. Eq ty => ty -> Array ty -> Bool
A.elem ty
e (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

all :: (ty -> Bool) -> Vect n ty -> Bool
all :: forall ty (n :: Nat). (ty -> Bool) -> Vect n ty -> Bool
all ty -> Bool
p Vect n ty
b = forall ty. (ty -> Bool) -> Array ty -> Bool
A.all ty -> Bool
p (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

any :: (ty -> Bool) -> Vect n ty -> Bool
any :: forall ty (n :: Nat). (ty -> Bool) -> Vect n ty -> Bool
any ty -> Bool
p Vect n ty
b = forall ty. (ty -> Bool) -> Array ty -> Bool
A.any ty -> Bool
p (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

find :: (ty -> Bool) -> Vect n ty -> Maybe ty
find :: forall ty (n :: Nat). (ty -> Bool) -> Vect n ty -> Maybe ty
find ty -> Bool
p Vect n ty
b = forall ty. (ty -> Bool) -> Array ty -> Maybe ty
A.find ty -> Bool
p (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b)

reverse :: Vect n ty -> Vect n ty
reverse :: forall (n :: Nat) ty. Vect n ty -> Vect n ty
reverse = forall (n :: Nat) a. Array a -> Vect n a
Vect forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall ty. Array ty -> Array ty
A.reverse forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (n :: Nat) a. Vect n a -> Array a
unVect

sortBy :: (ty -> ty -> Ordering) -> Vect n ty -> Vect n ty
sortBy :: forall ty (n :: Nat).
(ty -> ty -> Ordering) -> Vect n ty -> Vect n ty
sortBy ty -> ty -> Ordering
f Vect n ty
b = forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. (ty -> ty -> Ordering) -> Array ty -> Array ty
A.sortBy ty -> ty -> Ordering
f (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b))

intersperse :: (CmpNat n 1 ~ 'GT) => ty -> Vect n ty -> Vect (n+n-1) ty
intersperse :: forall (n :: Nat) ty.
(CmpNat n 1 ~ 'GT) =>
ty -> Vect n ty -> Vect ((n + n) - 1) ty
intersperse ty
sep Vect n ty
b = forall (n :: Nat) a. Array a -> Vect n a
Vect (forall ty. ty -> Array ty -> Array ty
A.intersperse ty
sep (forall (n :: Nat) a. Vect n a -> Array a
unVect Vect n ty
b))

toCount :: forall n ty . (KnownNat n, Countable ty n) => CountOf ty
toCount :: forall (n :: Nat) ty. (KnownNat n, Countable ty n) => CountOf ty
toCount = forall (n :: Nat) ty (proxy :: Nat -> *).
(KnownNat n, NatWithinBound (CountOf ty) n) =>
proxy n -> CountOf ty
natValCountOf (forall {k} (t :: k). Proxy t
Proxy @n)

toOffset :: forall n ty . (KnownNat n, Offsetable ty n) => Offset ty
toOffset :: forall (n :: Nat) ty. (KnownNat n, Offsetable ty n) => Offset ty
toOffset = forall (n :: Nat) ty (proxy :: Nat -> *).
(KnownNat n, NatWithinBound (Offset ty) n) =>
proxy n -> Offset ty
natValOffset (forall {k} (t :: k). Proxy t
Proxy @n)