    {-# 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 { unVect :: A.Array a } deriving (NormalForm, Eq, Show)
    newtype MVect (n :: Nat) ty st = MVect { unMVect :: A.MArray ty st }

    instance Functor (Vect n) where
        fmap = map

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

    empty :: Vect 0 ty
    empty = Vect A.empty

    singleton :: ty -> Vect 1 ty
    singleton a = Vect (A.singleton a)

    create :: forall a (n :: Nat) . (Countable a n, KnownNat n) => (Offset a -> a) -> Vect n a
    create f = Vect $ A.create sz f
      where
        sz = natValCountOf (Proxy :: Proxy n)

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

    thaw :: (KnownNat n, PrimMonad prim) => Vect n ty -> prim (MVect n ty (PrimState prim))
    thaw b = MVect <$> A.thaw (unVect b)

    freeze ::  (PrimMonad prim, Countable ty n) => MVect n ty (PrimState prim) -> prim (Vect n ty)
    freeze b = Vect <$> A.freeze (unMVect b)

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

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

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

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

    map :: (a -> b) -> Vect n a -> Vect n b
    map f b = Vect (fmap f (unVect b))

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

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

    cons :: ty -> Vect n ty -> Vect (n+1) ty
    cons e = Vect . A.cons e . unVect

    snoc :: Vect n ty -> ty -> Vect (n+1) ty
    snoc b = Vect . A.snoc (unVect 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 block = Vect (A.sub (unVect block) (toOffset @i) (toOffset @j))

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

    unsnoc :: forall n ty . (CmpNat 0 n ~ 'LT, KnownNat n, Offsetable ty n)
           => Vect n ty
           -> (Vect (n-1) ty, ty)
    unsnoc b =
        ( Vect (A.sub (unVect b) 0 (toOffset @n `offsetSub` 1))
        , A.unsafeIndex (unVect b) (toOffset @n `offsetSub` 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 b =
        let (left, right) = A.splitAt (toCount @i) (unVect b)
         in (Vect left, Vect right)

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

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

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

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

    reverse :: Vect n ty -> Vect n ty
    reverse = Vect . A.reverse . unVect

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

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

    toCount :: forall n ty . (KnownNat n, Countable ty n) => CountOf ty
    toCount = natValCountOf (Proxy @n)

    toOffset :: forall n ty . (KnownNat n, Offsetable ty n) => Offset ty
    toOffset = natValOffset (Proxy @n)