    {-# LANGUAGE CPP                   #-}
    {-# LANGUAGE DataKinds             #-}
    {-# LANGUAGE ConstraintKinds      #-}
    {-# LANGUAGE KindSignatures        #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE TypeFamilies          #-}
    {-# LANGUAGE RankNTypes            #-}
    {-# LANGUAGE ScopedTypeVariables   #-}
    {-# LANGUAGE TypeOperators         #-}

    -- | Tuples of unboxed values with type level length encoding.
    module Raaz.Core.Types.Tuple
           ( -- * Length encoded tuples
             Tuple, Dimension, dimension, initial, diagonal
           , repeatM, zipWith
             -- ** Unsafe operations
           , unsafeFromList
           ) where

    import           Control.Applicative
    import qualified Data.List           as L
    import           Data.Monoid

    #if MIN_VERSION_base(4,7,0)
    import           Data.Proxy
    #endif

    import qualified Data.Vector.Unboxed as V
    import           GHC.TypeLits
    import           Foreign.Ptr                 ( castPtr, Ptr )
    import           Foreign.Storable            ( Storable(..) )
    import           Prelude hiding              ( length, zipWith )

    import Raaz.Core.Types.Equality
    import Raaz.Core.Types.Endian
    import Raaz.Core.Transfer
    import Raaz.Core.Parse.Applicative

    -- | Tuples that encode their length in their types. For tuples, we call
    -- the length its dimension.
    newtype Tuple (dim :: Nat) a = Tuple { Tuple dim a -> Vector a
    unTuple :: V.Vector a }
                                 deriving Int -> Tuple dim a -> ShowS
    [Tuple dim a] -> ShowS
    Tuple dim a -> String
    (Int -> Tuple dim a -> ShowS)
    -> (Tuple dim a -> String)
    -> ([Tuple dim a] -> ShowS)
    -> Show (Tuple dim a)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall (dim :: Nat) a.
    (Show a, Unbox a) =>
    Int -> Tuple dim a -> ShowS
    forall (dim :: Nat) a. (Show a, Unbox a) => [Tuple dim a] -> ShowS
    forall (dim :: Nat) a. (Show a, Unbox a) => Tuple dim a -> String
    showList :: [Tuple dim a] -> ShowS
    $cshowList :: forall (dim :: Nat) a. (Show a, Unbox a) => [Tuple dim a] -> ShowS
    show :: Tuple dim a -> String
    $cshow :: forall (dim :: Nat) a. (Show a, Unbox a) => Tuple dim a -> String
    showsPrec :: Int -> Tuple dim a -> ShowS
    $cshowsPrec :: forall (dim :: Nat) a.
    (Show a, Unbox a) =>
    Int -> Tuple dim a -> ShowS
    Show

    instance (V.Unbox a, Equality a) => Equality (Tuple dim a) where
      eq :: Tuple dim a -> Tuple dim a -> Result
    eq (Tuple u :: Vector a
    u) (Tuple v :: Vector a
    v) = (Result -> Result -> Result) -> Result -> Vector Result -> Result
    forall b a. Unbox b => (a -> b -> a) -> a -> Vector b -> a
    V.foldl' Result -> Result -> Result
    forall a. Monoid a => a -> a -> a
    mappend Result
    forall a. Monoid a => a
    mempty (Vector Result -> Result) -> Vector Result -> Result
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> Result) -> Vector a -> Vector a -> Vector Result
    forall a b c.
    (Unbox a, Unbox b, Unbox c) =>
    (a -> b -> c) -> Vector a -> Vector b -> Vector c
    V.zipWith a -> a -> Result
    forall a. Equality a => a -> a -> Result
    eq Vector a
    u Vector a
    v

    -- | Equality checking is timing safe.
    instance (V.Unbox a, Equality a) => Eq (Tuple dim a) where
      == :: Tuple dim a -> Tuple dim a -> Bool
    (==) = Tuple dim a -> Tuple dim a -> Bool
    forall a. Equality a => a -> a -> Bool
    (===)

    -- | Function to make the type checker happy
    getA :: Tuple dim a -> a
    getA :: Tuple dim a -> a
    getA _ = a
    forall a. HasCallStack => a
    undefined

    -- | Function that returns the dimension of the tuple. The dimension
    -- is calculated without inspecting the tuple and hence the term
    -- @`dimension` (undefined :: Tuple 5 Int)@ will evaluate to 5.
    #if MIN_VERSION_base(4,7,0)

    -- | The constaint on the dimension of the tuple (since base 4.7.0)
    type Dimension (dim :: Nat) = KnownNat dim

    {-@ assume natValInt :: Dimension dim => proxy dim -> { v : Int | v == dim } @-}
    natValInt :: Dimension dim => proxy dim -> Int
    natValInt :: proxy dim -> Int
    natValInt = Integer -> Int
    forall a. Enum a => a -> Int
    fromEnum (Integer -> Int) -> (proxy dim -> Integer) -> proxy dim -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . proxy dim -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal

    -- | This combinator returns the dimension of the tuple.
    {-@ dimension :: Dimension dim  => Raaz.Core.Types.Tuple.Tuple dim a -> {n: Int | n == dim } @-}
    dimension  :: Dimension dim => Tuple dim a -> Int
    dimensionP :: Dimension dim
               => Proxy dim
               -> Tuple dim a
               -> Int
    dimensionP :: Proxy dim -> Tuple dim a -> Int
    dimensionP sz :: Proxy dim
    sz _ = Proxy dim -> Int
    forall (dim :: Nat) (proxy :: Nat -> *).
    Dimension dim =>
    proxy dim -> Int
    natValInt Proxy dim
    sz
    dimension :: Tuple dim a -> Int
    dimension = Proxy dim -> Tuple dim a -> Int
    forall (dim :: Nat) a.
    Dimension dim =>
    Proxy dim -> Tuple dim a -> Int
    dimensionP Proxy dim
    forall k (t :: k). Proxy t
    Proxy

    #else

    -- | The constaint on the dimension of the tuple (pre base 4.7.0)
    type Dimension (dim :: Nat) = SingI dim

    -- | This combinator returns the dimension of the tuple.
    dimension  :: Dimension dim => Tuple dim a -> Int
    dimensionP :: Dimension dim
               => Sing dim
               -> Tuple dim a
               -> Int
    dimension       = withSing dimensionP
    dimensionP sz _ = fromEnum $ fromSing sz

    #endif

    -- | Get the dimension to parser
    getParseDimension :: (V.Unbox a, Dimension dim)
                      => Parser (Tuple dim a) -> Int
    getTupFromP       :: (V.Unbox a, Dimension dim)
                      => Parser (Tuple dim a) -> Tuple dim a

    getParseDimension :: Parser (Tuple dim a) -> Int
    getParseDimension = Tuple dim a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension (Tuple dim a -> Int)
    -> (Parser (Tuple dim a) -> Tuple dim a)
    -> Parser (Tuple dim a)
    -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Parser (Tuple dim a) -> Tuple dim a
    forall a (dim :: Nat).
    (Unbox a, Dimension dim) =>
    Parser (Tuple dim a) -> Tuple dim a
    getTupFromP
    getTupFromP :: Parser (Tuple dim a) -> Tuple dim a
    getTupFromP _     = Tuple dim a
    forall a. HasCallStack => a
    undefined

    instance (V.Unbox a, Storable a, Dimension dim)
             => Storable (Tuple dim a) where

      sizeOf :: Tuple dim a -> Int
    sizeOf tup :: Tuple dim a
    tup = Tuple dim a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension Tuple dim a
    tup Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * a -> Int
    forall a. Storable a => a -> Int
    sizeOf (Tuple dim a -> a
    forall (dim :: Nat) a. Tuple dim a -> a
    getA Tuple dim a
    tup)
      alignment :: Tuple dim a -> Int
    alignment  = a -> Int
    forall a. Storable a => a -> Int
    alignment (a -> Int) -> (Tuple dim a -> a) -> Tuple dim a -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tuple dim a -> a
    forall (dim :: Nat) a. Tuple dim a -> a
    getA

      peek :: Ptr (Tuple dim a) -> IO (Tuple dim a)
    peek  = Parser (Tuple dim a) -> Pointer -> IO (Tuple dim a)
    forall a. Parser a -> Pointer -> IO a
    unsafeRunParser Parser (Tuple dim a)
    tupParser (Pointer -> IO (Tuple dim a))
    -> (Ptr (Tuple dim a) -> Pointer)
    -> Ptr (Tuple dim a)
    -> IO (Tuple dim a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ptr (Tuple dim a) -> Pointer
    forall a b. Ptr a -> Ptr b
    castPtr
        where len :: Int
    len = Parser (Tuple dim a) -> Int
    forall a (dim :: Nat).
    (Unbox a, Dimension dim) =>
    Parser (Tuple dim a) -> Int
    getParseDimension Parser (Tuple dim a)
    tupParser
              tupParser :: Parser (Tuple dim a)
    tupParser = Vector a -> Tuple dim a
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector a -> Tuple dim a)
    -> TwistRF ParseAction BytesMonoid (Vector a)
    -> Parser (Tuple dim a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TwistRF ParseAction BytesMonoid (Vector a)
    forall a (v :: * -> *).
    (Storable a, Vector v a) =>
    Int -> Parser (v a)
    unsafeParseStorableVector Int
    len

      poke :: Ptr (Tuple dim a) -> Tuple dim a -> IO ()
    poke ptr :: Ptr (Tuple dim a)
    ptr tup :: Tuple dim a
    tup = WriteM IO -> Pointer -> IO ()
    forall (m :: * -> *). WriteM m -> Pointer -> m ()
    unsafeWrite WriteM IO
    writeTup Pointer
    cptr
        where writeTup :: WriteM IO
    writeTup = Vector a -> WriteM IO
    forall a (v :: * -> *) (m :: * -> *).
    (Storable a, Vector v a, MonadIO m) =>
    v a -> WriteM m
    writeStorableVector (Vector a -> WriteM IO) -> Vector a -> WriteM IO
    forall a b. (a -> b) -> a -> b
    $ Tuple dim a -> Vector a
    forall (dim :: Nat) a. Tuple dim a -> Vector a
    unTuple Tuple dim a
    tup
              cptr :: Pointer
    cptr     = Ptr (Tuple dim a) -> Pointer
    forall a b. Ptr a -> Ptr b
    castPtr Ptr (Tuple dim a)
    ptr

    instance (V.Unbox a, EndianStore a, Dimension dim)
             => EndianStore (Tuple dim a) where

      load :: Ptr (Tuple dim a) -> IO (Tuple dim a)
    load = Parser (Tuple dim a) -> Pointer -> IO (Tuple dim a)
    forall a. Parser a -> Pointer -> IO a
    unsafeRunParser Parser (Tuple dim a)
    tupParser (Pointer -> IO (Tuple dim a))
    -> (Ptr (Tuple dim a) -> Pointer)
    -> Ptr (Tuple dim a)
    -> IO (Tuple dim a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ptr (Tuple dim a) -> Pointer
    forall a b. Ptr a -> Ptr b
    castPtr
         where tupParser :: Parser (Tuple dim a)
    tupParser = Vector a -> Tuple dim a
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector a -> Tuple dim a)
    -> TwistRF ParseAction BytesMonoid (Vector a)
    -> Parser (Tuple dim a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TwistRF ParseAction BytesMonoid (Vector a)
    forall a (v :: * -> *).
    (EndianStore a, Vector v a) =>
    Int -> Parser (v a)
    unsafeParseVector Int
    len
               len :: Int
    len       = Parser (Tuple dim a) -> Int
    forall a (dim :: Nat).
    (Unbox a, Dimension dim) =>
    Parser (Tuple dim a) -> Int
    getParseDimension Parser (Tuple dim a)
    tupParser

      store :: Ptr (Tuple dim a) -> Tuple dim a -> IO ()
    store ptr :: Ptr (Tuple dim a)
    ptr tup :: Tuple dim a
    tup = WriteM IO -> Pointer -> IO ()
    forall (m :: * -> *). WriteM m -> Pointer -> m ()
    unsafeWrite WriteM IO
    writeTup Pointer
    cptr
         where writeTup :: WriteM IO
    writeTup = Vector a -> WriteM IO
    forall a (v :: * -> *) (m :: * -> *).
    (EndianStore a, Vector v a, MonadIO m) =>
    v a -> WriteM m
    writeVector (Vector a -> WriteM IO) -> Vector a -> WriteM IO
    forall a b. (a -> b) -> a -> b
    $ Tuple dim a -> Vector a
    forall (dim :: Nat) a. Tuple dim a -> Vector a
    unTuple Tuple dim a
    tup
               cptr :: Pointer
    cptr     = Ptr (Tuple dim a) -> Pointer
    forall a b. Ptr a -> Ptr b
    castPtr Ptr (Tuple dim a)
    ptr

      adjustEndian :: Ptr (Tuple dim a) -> Int -> IO ()
    adjustEndian ptr :: Ptr (Tuple dim a)
    ptr n :: Int
    n = Ptr a -> Int -> IO ()
    forall w. EndianStore w => Ptr w -> Int -> IO ()
    adjustEndian (Ptr (Tuple dim a) -> Ptr a
    unTupPtr Ptr (Tuple dim a)
    ptr) (Int -> IO ()) -> Int -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Ptr (Tuple dim a) -> Tuple dim a -> Int
    nos Ptr (Tuple dim a)
    ptr Tuple dim a
    forall a. HasCallStack => a
    undefined
           where nos     :: Ptr (Tuple dim a) -> Tuple dim a -> Int
                 nos :: Ptr (Tuple dim a) -> Tuple dim a -> Int
    nos _ w :: Tuple dim a
    w = Tuple dim a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension Tuple dim a
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    n
                 unTupPtr   :: Ptr (Tuple dim a) -> Ptr a
                 unTupPtr :: Ptr (Tuple dim a) -> Ptr a
    unTupPtr   = Ptr (Tuple dim a) -> Ptr a
    forall a b. Ptr a -> Ptr b
    castPtr

    -- | Construct a tuple by repeating a monadic action.
    repeatM :: (Functor m, Monad m, V.Unbox a, Dimension dim) => m a -> m (Tuple dim a)
    repeatM :: m a -> m (Tuple dim a)
    repeatM = Tuple dim a -> m a -> m (Tuple dim a)
    forall (m :: * -> *) a (dim :: Nat).
    (Functor m, Unbox a, Monad m, Dimension dim) =>
    Tuple dim a -> m a -> m (Tuple dim a)
    mkTupM Tuple dim a
    forall a. HasCallStack => a
    undefined
      where mkTupM :: (Functor m, V.Unbox a, Monad m, Dimension dim) => Tuple dim a -> m a -> m (Tuple dim a)
            mkTupM :: Tuple dim a -> m a -> m (Tuple dim a)
    mkTupM uTup :: Tuple dim a
    uTup action :: m a
    action = Vector a -> Tuple dim a
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector a -> Tuple dim a) -> m (Vector a) -> m (Tuple dim a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m a -> m (Vector a)
    forall (m :: * -> *) a.
    (Monad m, Unbox a) =>
    Int -> m a -> m (Vector a)
    V.replicateM (Tuple dim a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension Tuple dim a
    uTup) m a
    action

    -- | Construct a tuple out of the list. This function is unsafe and
    -- will result in run time error if the list is not of the correct
    -- dimension.
    {-@ unsafeFromList :: (V.Unbox a, Dimension dim)
                       => { xs:[a] | len xs = dim }
                       -> Raaz.Core.Types.Tuple.Tuple dim a

    @-}
    unsafeFromList :: (V.Unbox a, Dimension dim) => [a] -> Tuple dim a
    unsafeFromList :: [a] -> Tuple dim a
    unsafeFromList xs :: [a]
    xs
      | Tuple dim a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension Tuple dim a
    tup Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    L.length [a]
    xs = Tuple dim a
    tup
      | Bool
    otherwise                    = Tuple dim a
    forall a. a
    wrongLengthMesg
      where tup :: Tuple dim a
    tup = Vector a -> Tuple dim a
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector a -> Tuple dim a) -> Vector a -> Tuple dim a
    forall a b. (a -> b) -> a -> b
    $ [a] -> Vector a
    forall a. Unbox a => [a] -> Vector a
    V.fromList [a]
    xs
            wrongLengthMesg :: a
    wrongLengthMesg = String -> a
    forall a. HasCallStack => String -> a
    error "tuple: unsafeFromList: wrong length"

    -- | Computes the initial fragment of a tuple. No length needs to be given
    -- as it is infered from the types.
    {-@ lazy initial @-}
    initial ::  (V.Unbox a, Dimension dim0)
             => Tuple dim1 a
             -> Tuple dim0 a
    initial :: Tuple dim1 a -> Tuple dim0 a
    initial = Tuple dim0 a -> Tuple dim1 a -> Tuple dim0 a
    forall a (dim0 :: Nat) (dim1 :: Nat).
    (Unbox a, Dimension dim0) =>
    Tuple dim0 a -> Tuple dim1 a -> Tuple dim0 a
    mkTuple Tuple dim0 a
    forall a. HasCallStack => a
    undefined
      where mkTuple :: (V.Unbox a, Dimension dim0) => Tuple dim0 a -> Tuple dim1 a  -> Tuple dim0 a
            mkTuple :: Tuple dim0 a -> Tuple dim1 a -> Tuple dim0 a
    mkTuple uTup :: Tuple dim0 a
    uTup tup :: Tuple dim1 a
    tup = Vector a -> Tuple dim0 a
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector a -> Tuple dim0 a) -> Vector a -> Tuple dim0 a
    forall a b. (a -> b) -> a -> b
    $ Int -> Vector a -> Vector a
    forall a. Unbox a => Int -> Vector a -> Vector a
    V.take (Tuple dim0 a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension Tuple dim0 a
    uTup) (Vector a -> Vector a) -> Vector a -> Vector a
    forall a b. (a -> b) -> a -> b
    $ Tuple dim1 a -> Vector a
    forall (dim :: Nat) a. Tuple dim a -> Vector a
    unTuple Tuple dim1 a
    tup

    -- TODO: Put a constraint that dim0 <= dim1

    -- | The @diagonal a@ gives a tuple, all of whose entries is @a@.
    diagonal :: (V.Unbox a, Dimension dim) => a -> Tuple dim a
    diagonal :: a -> Tuple dim a
    diagonal = Tuple dim a -> a -> Tuple dim a
    forall a (dim :: Nat).
    (Unbox a, Dimension dim) =>
    Tuple dim a -> a -> Tuple dim a
    mkTup Tuple dim a
    forall a. HasCallStack => a
    undefined
      where mkTup :: (V.Unbox a, Dimension dim) => Tuple dim a -> a -> Tuple dim a
            mkTup :: Tuple dim a -> a -> Tuple dim a
    mkTup uTup :: Tuple dim a
    uTup a :: a
    a = Vector a -> Tuple dim a
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector a -> Tuple dim a) -> Vector a -> Tuple dim a
    forall a b. (a -> b) -> a -> b
    $ Int -> a -> Vector a
    forall a. Unbox a => Int -> a -> Vector a
    V.replicate (Tuple dim a -> Int
    forall (dim :: Nat) a. Dimension dim => Tuple dim a -> Int
    dimension Tuple dim a
    uTup) a
    a

    -- | A zipwith function for tuples

    zipWith :: (V.Unbox a, V.Unbox b, V.Unbox c)
            => (a -> b -> c)
            -> Tuple dim a
            -> Tuple dim b
            -> Tuple dim c
    zipWith :: (a -> b -> c) -> Tuple dim a -> Tuple dim b -> Tuple dim c
    zipWith f :: a -> b -> c
    f (Tuple at :: Vector a
    at) (Tuple bt :: Vector b
    bt)= Vector c -> Tuple dim c
    forall (dim :: Nat) a. Vector a -> Tuple dim a
    Tuple (Vector c -> Tuple dim c) -> Vector c -> Tuple dim c
    forall a b. (a -> b) -> a -> b
    $ (a -> b -> c) -> Vector a -> Vector b -> Vector c
    forall a b c.
    (Unbox a, Unbox b, Unbox c) =>
    (a -> b -> c) -> Vector a -> Vector b -> Vector c
    V.zipWith a -> b -> c
    f Vector a
    at Vector b
    bt