Unsafe.hs

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

{-# LANGUAGE CPP, MagicHash, UnboxedTuples #-}
-- |
-- Module      : Data.Text.Unsafe
-- 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
--
-- A module containing unsafe 'Text' operations, for very very careful
-- use in heavily tested code.
module Data.Text.Unsafe
    (
      inlineInterleaveST
    , inlinePerformIO
    , Iter(..)
    , iter
    , iter_
    , reverseIter
    , unsafeHead
    , unsafeTail
    , lengthWord16
    , takeWord16
    , dropWord16
    ) where

#if defined(ASSERTS)
import Control.Exception (assert)
#endif
import Data.Text.Encoding.Utf16 (chr2)
import Data.Text.Internal (Text(..))
import Data.Text.Unsafe.Base (inlineInterleaveST, inlinePerformIO)
import Data.Text.UnsafeChar (unsafeChr)
import qualified Data.Text.Array as A

--LIQUID
import Data.Text.Axioms
import Language.Haskell.Liquid.Prelude

-- | /O(1)/ A variant of 'head' for non-empty 'Text'. 'unsafeHead'
-- omits the check for the empty case, so there is an obligation on
-- the programmer to provide a proof that the 'Text' is non-empty.
{-@ unsafeHead :: TextNE -> Char @-}
unsafeHead :: Text -> Char
unsafeHead (Text arr off xlen)
    | m < 0xD800 || m > 0xDBFF = unsafeChr m
    | otherwise                = chr2 m n
    where m = A.unsafeIndexF arr off xlen off
          {-@ lazyvar n @-}
          n = A.unsafeIndex arr (off+1)
{-# INLINE unsafeHead #-}

-- | /O(1)/ A variant of 'tail' for non-empty 'Text'. 'unsafeHead'
-- omits the check for the empty case, so there is an obligation on
-- the programmer to provide a proof that the 'Text' is non-empty.
{-@ unsafeTail :: t:TextNE -> {v:TextLT t | (tlength v) = ((tlength t) - 1)} @-}
unsafeTail :: Text -> Text
unsafeTail t@(Text arr off len) =
--LIQUID #if defined(ASSERTS)
--LIQUID     assert (d <= len) $
--LIQUID #endif
    liquidAssert (d <= len) $
    Text arr (off+d) len'
  where d = iter_ t 0
        len' = liquidAssume (axiom_numchars_split t d) (len-d)
{-# INLINE unsafeTail #-}

data Iter = Iter {-# UNPACK #-} !Char {-# UNPACK #-} !Int

{-@ measure iter_d :: Iter -> Int
      iter_d (Iter c d) = d
  @-}

{-@ qualif IterD(v:Int, i:Iter) : v = (iter_d i) @-}
{-@ qualif ReverseIter(v:Int, i:Int, t:Text)
        : ((((i+1)+v) >= 0) && (((i+1)+v) < (i+1))
           && ((numchars (tarr t) (toff t) ((i+1)+v))
               = ((numchars (tarr t) (toff t) (i+1)) - 1))
           && ((numchars (tarr t) (toff t) ((i+1)+v)) >= -1))
  @-}


-- | /O(1)/ Iterate (unsafely) one step forwards through a UTF-16
-- array, returning the current character and the delta to add to give
-- the next offset to iterate at.
{-@ iter :: t:Text
         -> i:{v:Nat | v < (tlen t)}
         -> {v:Iter | ((BtwnEI ((iter_d v)+i) i (tlen t))
                && ((numchars (tarr t) (toff t) (i+(iter_d v)))
                    = (1 + (numchars (tarr t) (toff t) i)))
                && ((numchars (tarr t) (toff t) (i+(iter_d v)))
                    <= (tlength t)))}
  @-}
iter :: Text -> Int -> Iter
iter (Text arr off xlen) i
    | m < 0xD800 || m > 0xDBFF = Iter (unsafeChr m) 1
    | otherwise                = let k = j + 1
                                     n = A.unsafeIndex arr k
                                 in
                                 Iter (chr2 m n) 2
  where m = A.unsafeIndexF arr off xlen j
        j = off + i
        {- lazyvar n @-}
        -- n = A.unsafeIndex arr k
        {- lazyvar k @-}
        -- k = j + 1
{-# INLINE iter #-}

-- | /O(1)/ Iterate one step through a UTF-16 array, returning the
-- delta to add to give the next offset to iterate at.
{-@ iter_ :: t:Text
          -> i:{v:Nat | v < (tlen t)}
          -> {v:Int | (((BtwnEI (v+i) i (tlen t)))
                       && ((numchars (tarr t) (toff t) (i+v))
                           = (1 + (numchars (tarr t) (toff t) i)))
                       && ((numchars (tarr t) (toff t) (i+v))
                           <= (tlength t)))}
  @-}
iter_ :: Text -> Int -> Int
iter_ (Text arr off xlen) i | m < 0xD800 || m > 0xDBFF = 1
                            | otherwise                = 2
--LIQUID   where m = A.unsafeIndex arr (off+i)
  where m = A.unsafeIndexF arr off xlen (off+i)
{-# INLINE iter_ #-}

-- | /O(1)/ Iterate one step backwards through a UTF-16 array,
-- returning the current character and the delta to add (i.e. a
-- negative number) to give the next offset to iterate at.
{-@ reverseIter :: t:Text
                -> i:{v:Int | (Btwn v 0 (tlen t))}
                -> (Char,{v:Int | ((Btwn ((i+1)+v) 0 (i+1))
                          && ((numchars (tarr t) (toff t) ((i+1)+v))
                              = ((numchars (tarr t) (toff t) (i+1)) - 1))
                          && ((numchars (tarr t) (toff t) ((i+1)+v)) >= -1))})
  @-}
--LIQUID reverseIter :: Text -> Int -> (Char,Int)
--LIQUID reverseIter (Text arr off _len) i
reverseIter :: Text -> Int -> (Char,Int)
reverseIter (Text arr off xlen) i
    | m < 0xDC00 || m > 0xDFFF = (unsafeChr m, neg 1)
    | otherwise                = let k = j - 1
                                     n = A.unsafeIndex arr k
                                 in
                                  (chr2 n m,    neg 2)
  where m = A.unsafeIndexB arr off xlen j
        {- lazyvar n @-}
        -- n = A.unsafeIndex arr k
        j = off + i
        {- lazyvar k @-}
        -- k = j - 1
{-# INLINE reverseIter #-}

{-@ neg :: n:Int -> {v:Int | v = (0-n)} @-}
neg :: Int -> Int
neg n = 0-n


-- | /O(1)/ Return the length of a 'Text' in units of 'Word16'.  This
-- is useful for sizing a target array appropriately before using
-- 'unsafeCopyToPtr'.
{-@ lengthWord16 :: t:Text -> {v:Int | v = (tlen t)} @-}
lengthWord16 :: Text -> Int
lengthWord16 (Text _arr _off len) = len
{-# INLINE lengthWord16 #-}

-- | /O(1)/ Unchecked take of 'k' 'Word16's from the front of a 'Text'.
{-@ takeWord16 :: k:Nat -> {v:Text | (k <= (tlen v))} -> {v:Text | (tlen v) = k} @-}
takeWord16 :: Int -> Text -> Text
takeWord16 k (Text arr off xlen) = Text arr off k
{-# INLINE takeWord16 #-}

-- | /O(1)/ Unchecked drop of 'k' 'Word16's from the front of a 'Text'.
{-@ dropWord16 :: k:Nat -> t:{v:Text | (k <= (tlen v))}
               -> {v:Text | (tlen v) = ((tlen t) - k)} @-}
dropWord16 :: Int -> Text -> Text
dropWord16 k (Text arr off len) = Text arr (off+k) (len-k)
{-# INLINE dropWord16 #-}