-- | Copy some elements of a mutable array.
{-@ copyM :: dest:MArray s -> didx:MAValidO dest
          -> src:MArray s  -> sidx:MAValidO src
          -> {v:Nat | (((v + didx) <= (malen dest))
                    && ((v + sidx) <= (malen src)))}
          -> ST s ()
  @-}
copyM :: MArray s               -- ^ Destination
      -> Int                    -- ^ Destination offset
      -> MArray s               -- ^ Source
      -> Int                    -- ^ Source offset
      -> Int                    -- ^ Count
      -> ST s ()
copyM dest didx src sidx count
    | count <= 0 = return ()
    | otherwise =
--LIQUID #if defined(ASSERTS)
--LIQUID     assert (sidx + count <= length src) .
--LIQUID     assert (didx + count <= length dest) .
--LIQUID #endif
    liquidAssert (sidx + count <= maLen src) .
    liquidAssert (didx + count <= maLen dest) .
    unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
                           (maBA src) (fromIntegral sidx)
                           (fromIntegral count)
copyM :: MArray s               -- ^ Destination
      -> Int                    -- ^ Destination offset
      -> MArray s               -- ^ Source
      -> Int                    -- ^ Source offset
      -> Int                    -- ^ Count
      -> ST s ()
copyM dest didx src sidx count
    | count <= 0 = return ()
    | otherwise =
--LIQUID #if defined(ASSERTS)
--LIQUID     assert (sidx + count <= length src) .
--LIQUID     assert (didx + count <= length dest) .
--LIQUID #endif
    liquidAssert (sidx + count <= maLen src) .
    liquidAssert (didx + count <= maLen dest) .
    unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
                           (maBA src) (fromIntegral sidx)
                           (fromIntegral count)
copyM dest didx src sidx count
    | count <= 0 = return ()
    | otherwise =
--LIQUID #if defined(ASSERTS)
--LIQUID     assert (sidx + count <= length src) .
--LIQUID     assert (didx + count <= length dest) .
--LIQUID #endif
    liquidAssert (sidx + count <= maLen src) .
    liquidAssert (didx + count <= maLen dest) .
    unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
                           (maBA src) (fromIntegral sidx)
                           (fromIntegral count)