content: {- LIQUID "--no-pattern-inline" @-}
  {-@ LIQUID "--pruneunsorted" @-}
  
  {-# LANGUAGE BangPatterns, CPP, GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  -- |
  -- Module      : Data.Text.Foreign
  -- Copyright   : (c) 2009, 2010 Bryan O'Sullivan
  --
  -- License     : BSD-style
  -- Maintainer  : bos@serpentine.com, rtomharper@googlemail.com,
  --               duncan@haskell.org
  -- Stability   : experimental
  -- Portability : GHC
  --
  -- Support for using 'Text' data with native code via the Haskell
  -- foreign function interface.
  
  module Data.Text.Foreign
      (
      -- * Interoperability with native code
      -- $interop
        I16(..)
      -- * Safe conversion functions
      , fromPtr
      , useAsPtr
      , asForeignPtr
      -- * Unsafe conversion code
      , lengthWord16
      , unsafeCopyToPtr
      -- * Low-level manipulation
      -- $lowlevel
      , dropWord16
      , takeWord16
      ) where
  
  #if defined(ASSERTS)
  import Control.Exception (assert)
  #endif
  #if __GLASGOW_HASKELL__ >= 702
  import Control.Monad.ST.Unsafe (unsafeIOToST)
  #else
  import Control.Monad.ST (unsafeIOToST)
  #endif
  import Data.Text.Internal (Text(..), empty)
  import Data.Text.Unsafe (lengthWord16)
  import qualified Data.Text.Array as A
  import Data.Word (Word16)
  import Foreign.Marshal.Alloc (allocaBytes)
  import Foreign.Ptr (Ptr, castPtr, plusPtr)
  import Foreign.ForeignPtr (ForeignPtr, mallocForeignPtrArray, withForeignPtr)
  import Foreign.Storable (peek, poke)
  
  --LIQUID
  import Foreign.Storable (Storable)
  import Language.Haskell.Liquid.Prelude
  
  
  -- $interop
  --
  -- The 'Text' type is implemented using arrays that are not guaranteed
  -- to have a fixed address in the Haskell heap. All communication with
  -- native code must thus occur by copying data back and forth.
  --
  -- The 'Text' type's internal representation is UTF-16, using the
  -- platform's native endianness.  This makes copied data suitable for
  -- use with native libraries that use a similar representation, such
  -- as ICU.  To interoperate with native libraries that use different
  -- internal representations, such as UTF-8 or UTF-32, consider using
  -- the functions in the 'Data.Text.Encoding' module.
  
  -- | A type representing a number of UTF-16 code units.
  --LIQUID newtype I16 = I16 Int
  --LIQUID     deriving (Bounded, Enum, Eq, Integral, Num, Ord, --LIQUID Read,
  --LIQUID               Real, Show)
  
  --LIQUID FIXME: we don't seem to handle `newtype`s properly, the underlying `Int`
  --LIQUID        is still typed as an `I16` in our refinements...
  data I16 = I16 Int
      deriving (Eq, Ord)
  
  {-@ data I16 = I16 { i16Val ::Nat } @-}
  
  {-@ measure getI16 :: I16 -> Int
        getI16 (I16 n) = n
    @-}
  
  {-@ qualif PtrFree(v:Int, p:Ptr a, l:Int): ((l+l)-(v+v)) <= (plen p) @-}
  
  --LIQUID specializing the type for Word16
  {-@ Foreign.ForeignPtr.mallocForeignPtrArray :: (Storable a) => n:Nat -> IO {v:(ForeignPtr a) | (fplen v) = (n + n)} @-}
  {-@ qualif FPLenNN(v:ForeignPtr a, n:int): (fplen v) = (n + n) @-}
  
  
  -- | /O(n)/ Create a new 'Text' from a 'Ptr' 'Word16' by copying the
  -- contents of the array.
  {-@ fromPtr :: p:(PtrV Word16) -> l:{v:I16 | ((getI16 v)*2) = (plen p)} -> IO Text @-}
  fromPtr :: Ptr Word16           -- ^ source array
          -> I16                  -- ^ length of source array (in 'Word16' units)
          -> IO Text
  fromPtr _   (I16 0)   = return empty
  fromPtr ptr (I16 len) =
  --LIQUID #if defined(ASSERTS)
      liquidAssert (len > 0) $
  --LIQUID #endif
      return $! Text (liquidAssume (A.aLen arr == len) arr) 0 len
    where
      arr = A.run (A.new len >>= copy)
      copy marr = loop len ptr 0
        where
          {- LIQUID WITNESS -}
          loop (d :: Int) !p !i | i == len = return marr
                                | otherwise = do
            A.unsafeWrite marr i =<< unsafeIOToST (peek p)
            loop (d-1) (p `plusPtr` 2) (i + 1)
  
  -- $lowlevel
  --
  -- Foreign functions that use UTF-16 internally may return indices in
  -- units of 'Word16' instead of characters.  These functions may
  -- safely be used with such indices, as they will adjust offsets if
  -- necessary to preserve the validity of a Unicode string.
  
  -- | /O(1)/ Return the prefix of the 'Text' of @n@ 'Word16' units in
  -- length.
  --
  -- If @n@ would cause the 'Text' to end inside a surrogate pair, the
  -- end of the prefix will be advanced by one additional 'Word16' unit
  -- to maintain its validity.
  takeWord16 :: I16 -> Text -> Text
  takeWord16 (I16 n) t@(Text arr off len)
      | n <= 0               = empty
  --LIQUID     | n >= len || m >= len = t
  --LIQUID     | otherwise            = Text arr off m
      | n >= len = t
      | otherwise = let w = A.unsafeIndex arr (off+n-1)
                        m | w < 0xDB00 || w > 0xD8FF = n
                          | otherwise                = n+1
  
                    in if m >= len then t
                       else Text arr off m
  --LIQUID   where
  --LIQUID     w = A.unsafeIndex arr (off+n-1)
  --LIQUID     m | w < 0xDB00 || (liquidAssert False w) > 0xD8FF = n
  --LIQUID       | otherwise                = n+1
  
  -- | /O(1)/ Return the suffix of the 'Text', with @n@ 'Word16' units
  -- dropped from its beginning.
  --
  -- If @n@ would cause the 'Text' to begin inside a surrogate pair, the
  -- beginning of the suffix will be advanced by one additional 'Word16'
  -- unit to maintain its validity.
  dropWord16 :: I16 -> Text -> Text
  dropWord16 (I16 n) t@(Text arr off len)
      | n <= 0               = t
  --LIQUID     | n >= len || m >= len = empty
  --LIQUID     | otherwise            = Text arr (off+m) (len-m)
      | n >= len = empty
      | otherwise = let m | w < 0xD800 || w > 0xDBFF = n
                          | otherwise                = n+1
                        w = A.unsafeIndex arr (off+n-1)
                    in if m >= len then empty
                       else Text arr (off+m) (len-m)
  --LIQUID   where
  --LIQUID     m | w < 0xD800 || w > 0xDBFF = n
  --LIQUID       | otherwise                = n+1
  --LIQUID     w = A.unsafeIndex arr (off+n-1)
  
  -- | /O(n)/ Copy a 'Text' to an array.  The array is assumed to be big
  -- enough to hold the contents of the entire 'Text'.
  {-@ unsafeCopyToPtr :: t:Text -> {v:PtrV Word16 | (plen v) >= ((tlen t)*2)}
                      -> IO ()
    @-}
  unsafeCopyToPtr :: Text -> Ptr Word16 -> IO ()
  unsafeCopyToPtr (Text arr off len) ptr = loop len ptr off
    where
      end = off + len
      {- LIQUID WITNESS -}
      loop (d :: Int) !p !i | i == end  = return ()
                            | otherwise = do
        poke p (A.unsafeIndex arr i)
        loop (d-1) (p `plusPtr` 2) (i + 1)
  
  
  -- | /O(n)/ Perform an action on a temporary, mutable copy of a
  -- 'Text'.  The copy is freed as soon as the action returns.
  {-@ useAsPtr :: Text -> (PtrV Word16 -> I16 -> IO a) -> IO a @-}
  useAsPtr :: Text -> (Ptr Word16 -> I16 -> IO a) -> IO a
  useAsPtr t@(Text _arr _off len) action =
      allocaBytes (len + len) {-LIQUID (len * 2)-} $ \buf -> do
        unsafeCopyToPtr t buf
  --LIQUID      action (castPtr buf) (fromIntegral len)
        action (castPtr buf) (I16 $ fromIntegral len)
  
  
  -- | /O(n)/ Make a mutable copy of a 'Text'.
  {-@ asForeignPtr :: Text -> IO (ForeignPtr Word16, I16) @-}
  asForeignPtr :: Text -> IO (ForeignPtr Word16, I16)
  asForeignPtr t@(Text _arr _off len) = do
    fp <- mallocForeignPtrArray len
    withForeignPtr fp $ unsafeCopyToPtr t
    return (fp, I16 len)
  
  
  
  
  
  
  
  
  
  
  
  