Array.hs

{- LIQUID "--no-pattern-inline" @-}

{-# LANGUAGE BangPatterns, CPP, ForeignFunctionInterface, MagicHash, Rank2Types,
    RecordWildCards, UnboxedTuples, UnliftedFFITypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
-- |
-- Module      : Data.Text.Array
-- Copyright   : (c) 2009, 2010, 2011 Bryan O'Sullivan
--
-- License     : BSD-style
-- Maintainer  : bos@serpentine.com, rtomharper@googlemail.com,
--               duncan@haskell.org
-- Stability   : experimental
-- Portability : portable
--
-- Packed, unboxed, heap-resident arrays.  Suitable for performance
-- critical use, both in terms of large data quantities and high
-- speed.
--
-- This module is intended to be imported @qualified@, to avoid name
-- clashes with "Prelude" functions, e.g.
--
-- > import qualified Data.Text.Array as A
--
-- The names in this module resemble those in the 'Data.Array' family
-- of modules, but are shorter due to the assumption of qualifid
-- naming.
module Data.Text.Array
    (
    -- * Types
    --LIQUID added Array dataCon export
      Array(..)
--LIQUID     , MArray(maBA)
    , MArray(..)

    -- * Functions
    , copyM
    , copyI
    , empty
    , equal
--LIQUID #if defined(ASSERTS)
    , length
--LIQUID #endif
    , run
    , run2
    , toList
    , unsafeFreeze
    , unsafeIndex
    , new
    , unsafeWrite
    --LIQUID
    , unsafeIndexF
    , unsafeIndexB
    ) where

#if defined(ASSERTS)
-- This fugly hack is brought by GHC's apparent reluctance to deal
-- with MagicHash and UnboxedTuples when inferring types. Eek!
# define CHECK_BOUNDS(_func_,_len_,_k_) \
if (_k_) < 0 || (_k_) >= (_len_) then error ("Data.Text.Array." ++ (_func_) ++ ": bounds error, offset " ++ show (_k_) ++ ", length " ++ show (_len_)) else
#else
# define CHECK_BOUNDS(_func_,_len_,_k_)
#endif

#include "MachDeps.h"

--LIQUID #if defined(ASSERTS)
import Control.Exception (assert)
--LIQUID #endif
#if __GLASGOW_HASKELL__ >= 702
import Control.Monad.ST.Unsafe (unsafeIOToST)
#else
import Control.Monad.ST (unsafeIOToST)
#endif
import Data.Bits ((.&.), xor)
import Data.Text.Unsafe.Base (inlinePerformIO)
import Data.Text.UnsafeShift (shiftL, shiftR)
#if __GLASGOW_HASKELL__ >= 703
import Foreign.C.Types (CInt(CInt), CSize(CSize))
#else
import Foreign.C.Types (CInt, CSize)
#endif
import GHC.Base (ByteArray#, MutableByteArray#, Int(..),
                 indexWord16Array#, newByteArray#, writeWord16Array#)
import GHC.Exts (unsafeCoerce#) -- Importing from GHC.Exts makes this future-proof (i.e. works for GHC >= 9)
import GHC.ST (ST(..), runST)
import GHC.Word (Word16(..))
import Prelude hiding (error, length, read)

--LIQUID
import Language.Haskell.Liquid.Prelude

{-@ predicate Btwn V X Y   = ((X <= V) && (V < Y)) @-}
{-@ predicate BtwnE V X Y  = ((X < V)  && (V < Y)) @-}
{-@ predicate BtwnI V X Y  = ((X <= V) && (V <= Y)) @-}
{-@ predicate BtwnEI V X Y = ((X < V)  && (V <= Y)) @-}

{-@ qualif LenDiff(v:List a, i:int, l:int): (len v) = (l - i) @-}
{-@ qualif Diff(v:int, d:int, l:int): v = l - d @-}

{-@ lazy error @-}
error msg = error msg

-- | Immutable array type.
data Array = Array {
      aBA :: ByteArray#
--LIQUID #if defined(ASSERTS)
    , aLen :: {-# UNPACK #-} !Int -- length (in units of Word16, not bytes)
--LIQUID #endif
    }

{-@ data Array = Array { aBA  :: ByteArray#
                       , aLen :: Nat }
  @-}




{-@ type ArrayN N = {v:Array | (aLen v) = N} @-}

{-@ type AValidI A   = {v:Nat | v     <  (aLen A)} @-}
{-@ type AValidO A   = {v:Nat | v     <= (aLen A)} @-}
{-@ type AValidL O A = {v:Nat | (v+O) <= (aLen A)} @-}

{-@ qualif ALen(v:Int, a:Array): v = aLen(a) @-}
{-@ qualif ALen(v:Array, i:Int): i = aLen(v) @-}

{-@ invariant {v:Array | (aLen v) >= 0} @-}

{-@ measure numchars :: Array -> Int -> Int -> Int @-}

-- | Mutable array type, for use in the ST monad.
data MArray s = MArray {
      maBA :: MutableByteArray# s
--LIQUID #if defined(ASSERTS)
    , maLen :: {-# UNPACK #-} !Int -- length (in units of Word16, not bytes)
--LIQUID #endif
    }

{-@ data MArray s = MArray { maBA  :: MutableByteArray# s
                           , maLen :: Nat
                           }
  @-}


{-@ type MArrayN s N = {v:MArray s | (maLen v) = N} @-}

{-@ type MAValidI A   = {v:Nat | v     <  (maLen A)} @-}
{-@ type MAValidO A   = {v:Nat | v     <= (maLen A)} @-}
{-@ type MAValidL O A = {v:Nat | (v+O) <= (maLen A)} @-}

{-@ qualif MALen(v:Int, a:MArray s): v = maLen(a) @-}
{-@ qualif MALen(v:MArray s, i:Int): i = maLen(v) @-}

{-@ invariant {v:MArray s | (maLen v) >= 0} @-}

{-@ qualif FreezeMArr(v:Array, ma:MArray s):
        aLen(v) = maLen(ma)
  @-}

--LIQUID #if defined(ASSERTS)
-- | Operations supported by all arrays.
class IArray a where
    -- | Return the length of an array.
    length :: a -> Int

instance IArray Array where
    length = aLen
    {-# INLINE length #-}

instance IArray (MArray s) where
    length = maLen
    {-# INLINE length #-}
--LIQUID #endif

-- | Create an uninitialized mutable array.
{-@ assume new :: n:Nat -> ST s (MArrayN s n) @-}
-- TODO: losing information in cast
new :: Int -> ST s (MArray s)
new n
  | n < 0 || n .&. highBit /= 0 = error $ "Data.Text.Array.new: size overflow"
  | otherwise = ST $ \s1# ->
       case newByteArray# len# s1# of
         (# s2#, marr# #) -> (# s2#, MArray marr#
--LIQUID #if defined(ASSERTS)
                                n
--LIQUID #endif
                                #)
  where !(I# len#) = bytesInArray n
        highBit    = maxBound `xor` (maxBound `shiftR` 1)
{-# INLINE new #-}

-- | Freeze a mutable array. Do not mutate the 'MArray' afterwards!
{-@ assume unsafeFreeze :: ma:MArray s -> (ST s (ArrayN (maLen ma))) @-}
-- TODO: losing information in cast
unsafeFreeze :: MArray s -> ST s Array
unsafeFreeze MArray{..} = ST $ \s# ->
                          (# s#, Array (unsafeCoerce# maBA)
--LIQUID #if defined(ASSERTS)
                             maLen
--LIQUID #endif
                             #)
{-# INLINE unsafeFreeze #-}

-- | Indicate how many bytes would be used for an array of the given
-- size.
bytesInArray :: Int -> Int
bytesInArray n = n `shiftL` 1
{-# INLINE bytesInArray #-}

-- | Unchecked read of an immutable array.  May return garbage or
-- crash on an out-of-bounds access.
{-@ unsafeIndex :: a:Array -> AValidI a -> Word16 @-}
unsafeIndex :: Array -> Int -> Word16
unsafeIndex Array{..} i@(I# i#) =
  CHECK_BOUNDS("unsafeIndex",aLen,i)
    case indexWord16Array# aBA i# of r# -> (W16# r#)
{-# INLINE unsafeIndex #-}

--LIQUID
{-@ predicate SpanChar D A O L I = (((numchars (A) (O) ((I-O)+D)) = (1 + (numchars (A) (O) (I-O))))
                                 && ((numchars (A) (O) ((I-O)+D)) <= (numchars A O L))
                                 && (((I-O)+D) <= L))
  @-}

{-@ unsafeIndexF :: a:Array -> o:AValidO a -> l:AValidL o a
                 -> i:{v:Int | (Btwn (v) (o) (o + l))}
                 -> {v:Word16 | (if (BtwnI v 55296 56319)
                                 then (SpanChar 2 a o l i)
                                 else (SpanChar 1 a o l i))}
  @-}
unsafeIndexF :: Array -> Int -> Int -> Int -> Word16
unsafeIndexF a o l i = let x = unsafeIndex a i
                       in liquidAssume (unsafeIndexFQ x a o l i) x

{-@ unsafeIndexFQ :: x:Word16 -> a:Array -> o:Int -> l:Int -> i:Int
                  -> {v:Bool | (v <=> (if (BtwnI x 55296 56319)
                                              then (SpanChar 2 a o l i)
                                              else (SpanChar 1 a o l i)))}
  @-}
unsafeIndexFQ :: Word16 -> Array -> Int -> Int -> Int -> Bool
unsafeIndexFQ = undefined

{-@ unsafeIndexB :: a:Array -> o:AValidO a -> l:AValidL o a
                 -> i:{v:Int | Btwn v o (o + l)}
                 -> {v:Word16 | (
       if (v >= 56320 && v <= 57343)
       then ( (numchars a o ((i - o)+1)) = (1 + (numchars a o ((i-o)-1)))
         && ( (numchars a o (i-o-1)) >= 0)
         && ( ((i-o)-1) >= 0))
       else ( ((numchars a o ((i-o)+1)) = (1 + (numchars a o (i-o))))
         && ( (numchars a o (i-o)) >= 0)))}
  @-}
unsafeIndexB :: Array -> Int -> Int -> Int -> Word16
unsafeIndexB a o l i = let x = unsafeIndex a i
                       in liquidAssume (unsafeIndexBQ x a o i) x

{-@ unsafeIndexBQ :: x:Word16 -> a:Array -> o:Int -> i:Int
                  -> {v:Bool | (v <=>
       if (x >= 56320 && x <= 57343)
       then ( (numchars a o ((i - o)+1)) = (1 + (numchars a o ((i-o)-1)))
         && ( (numchars a o (i-o-1)) >= 0)
         && ( ((i-o)-1) >= 0))
       else ( ((numchars a o ((i-o)+1)) = (1 + (numchars a o (i-o))))
         && ( (numchars a o (i-o)) >= 0)))}
  @-}
unsafeIndexBQ :: Word16 -> Array -> Int -> Int -> Bool
unsafeIndexBQ = undefined

-- | Unchecked write of a mutable array.  May return garbage or crash
-- on an out-of-bounds access.
{-@ unsafeWrite :: ma:MArray s -> MAValidI ma -> Word16 -> ST s () @-}
unsafeWrite :: MArray s -> Int -> Word16 -> ST s ()
unsafeWrite MArray{..} i@(I# i#) (W16# e#) = ST $ \s1# ->
  CHECK_BOUNDS("unsafeWrite",maLen,i)
  case writeWord16Array# maBA i# e# s1# of
    s2# -> (# s2#, () #)
{-# INLINE unsafeWrite #-}

-- | Convert an immutable array to a list.
{-@ toList :: a:Array -> o:AValidO a -> l:AValidL o a -> {v:[Word16] | (len v) = l} @-}
toList :: Array -> Int -> Int -> [Word16]
toList ary off len = loop len 0
          {- LIQUID WITNESS -}
    where loop (d :: Int) i
              | i < len   = unsafeIndex ary (off+i) : loop (d-1) (i+1)
              | otherwise = []

-- | An empty immutable array.
{-@ empty :: {v:Array | (aLen v) = 0}  @-}
empty :: Array
empty = runST (new 0 >>= unsafeFreeze)

-- | Run an action in the ST monad and return an immutable array of
-- its result.

{-
run :: forall <p :: Int -> Bool>.
       (forall s. GHC.ST.ST s (Data.Text.Array.MArray s)<p>)
     -> exists[z:Int<p>]. Data.Text.Array.Array<p>
@-}
{- run :: (forall s. GHC.ST.ST s ma:(Data.Text.Array.MArray s))
        -> {v:Data.Text.Array.Array | (aLen v) = (len ma)}
  @-}
run :: (forall s. ST s (MArray s)) -> Array
run k = runST (k >>= unsafeFreeze)

-- | Run an action in the ST monad and return an immutable array of
-- its result paired with whatever else the action returns.
{- run2 :: (forall s. GHC.ST.ST s (ma:Data.Text.Array.MArray s, a:a))
         -> ({v:Data.Text.Array.Array | (aLen v) = (maLen ma)}, {v:a | v = a})
  @-}
run2 :: (forall s. ST s (MArray s, a)) -> (Array, a)
run2 k = runST (do
                 (marr,b) <- k
                 arr <- unsafeFreeze marr
                 return (arr,b))

-- | 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)
{-# INLINE copyM #-}

-- | Copy some elements of an immutable array.
{-@ copyI :: dest:MArray s -> i0:MAValidO dest
          -> src:Array     -> j0:AValidO src
          -> top:{v:MAValidO dest | ((v-i0)+j0) <= (aLen src)}
          -> GHC.ST.ST s ()
  @-}
copyI :: MArray s               -- ^ Destination
      -> Int                    -- ^ Destination offset
      -> Array                  -- ^ Source
      -> Int                    -- ^ Source offset
      -> Int                    -- ^ First offset in destination /not/ to
                                -- copy (i.e. /not/ length)
      -> ST s ()
copyI dest i0 src j0 top
    | i0 >= top = return ()
    | otherwise = unsafeIOToST $
                  memcpyI (maBA dest) (fromIntegral i0)
                          (aBA src) (fromIntegral j0)
                          (fromIntegral (top-i0))
{-# INLINE copyI #-}

-- | Compare portions of two arrays for equality.  No bounds checking
-- is performed.
--LIQUID TODO: this is not correct because we're just comparing sub-arrays
{- equal :: a1:Data.Text.Array.Array
          -> o1:{v:Int | ((v >= 0) && (v < (aLen a1)))}
          -> a2:Data.Text.Array.Array
          -> o2:{v:Int | ((v >= 0) && (v < (aLen a2)))}
          -> cnt:{v:Int | ((v >= 0) && ((v+o1) < (aLen a1)) && ((v+o2) < (aLen a2)))}
          -> {v:Bool | (v <=> (a1 = a2))}
  @-}
equal :: Array                  -- ^ First
      -> Int                    -- ^ Offset into first
      -> Array                  -- ^ Second
      -> Int                    -- ^ Offset into second
      -> Int                    -- ^ Count
      -> Bool
equal arrA offA arrB offB count = inlinePerformIO $ do
  i <- memcmp (aBA arrA) (fromIntegral offA)
                     (aBA arrB) (fromIntegral offB) (fromIntegral count)
  return $! i == 0
{-# INLINE equal #-}

foreign import ccall unsafe "_hs_text_memcpy" memcpyI
    :: MutableByteArray# s -> CSize -> ByteArray# -> CSize -> CSize -> IO ()
{-@ memcpyI :: MutableByteArray# s -> CSize -> ByteArray# -> CSize -> CSize -> IO () @-}

foreign import ccall unsafe "_hs_text_memcmp" memcmp
    :: ByteArray# -> CSize -> ByteArray# -> CSize -> CSize -> IO CInt
{-@ memcmp :: ByteArray# -> CSize -> ByteArray# -> CSize -> CSize -> IO CInt @-}

foreign import ccall unsafe "_hs_text_memcpy" memcpyM
    :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize
    -> IO ()
{-@ memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () @-}