{- LIQUID "--no-pattern-inline" @-}
{-# LANGUAGE CPP, MagicHash #-}

-- |
-- Module      : Data.Text.UnsafeChar
-- Copyright   : (c) 2008, 2009 Tom Harper,
--               (c) 2009, 2010 Bryan O'Sullivan,
--               (c) 2009 Duncan Coutts
--
-- License     : BSD-style
-- Maintainer  : bos@serpentine.com, rtomharper@googlemail.com,
--               duncan@haskell.org
-- Stability   : experimental
-- Portability : GHC
--
-- Fast character manipulation functions.
module Data.Text.UnsafeChar
    (
      ord
    , unsafeChr
    , unsafeChr8
    , unsafeChr32
    , unsafeWrite
    -- , unsafeWriteRev
    ) where

#ifdef ASSERTS
import Control.Exception (assert)
#endif
import Control.Monad.ST (ST)
import Data.Bits ((.&.))
import Data.Text.UnsafeShift (shiftR)
import GHC.Exts (Char(..), Int(..), chr#, ord#, word2Int#)
import GHC.Word (Word8(..), Word16(..), Word32(..))
import qualified Data.Text.Array as A

--LIQUID
import Language.Haskell.Liquid.Prelude

{-@ measure ordP :: Char -> Int @-}
{-@ predicate One C = ((ordP C) <  65536) @-}
{-@ predicate Two C = ((ordP C) >= 65536) @-}

{-@ qualOneC :: {v:Char | (ordP v) <  65536} -> () @-}
qualOneC :: Char -> ()
qualOneC _ = ()
{-@ qualTwoC :: {v:Char | (ordP v) >= 65536} -> () @-}
qualTwoC :: Char -> ()
qualTwoC _ = ()

{-@ predicate Room MA I C = (((One C) => (MAValidIN MA I 1))
                          && ((Two C) => (MAValidIN MA I 2))) @-}
{-@ predicate MAValidIN  MA I N = (BtwnI I 0 ((maLen MA) - N)) @-}

{- predicate RoomFront MA I N = (BtwnI I N (malen MA)) @-}

{-@ ord :: c:Char -> {v:Int | v = (ordP c)} @-}
ord :: Char -> Int
ord c@(C# c#) = let i = I# (ord# c#)
                in liquidAssume (axiom_ord c i) i
{-@ axiom_ord :: c:Char -> i:Int -> {v:Bool | (v <=> (i = (ordP c)))} @-}
axiom_ord :: Char -> Int -> Bool
axiom_ord = undefined
{-# INLINE ord #-}

unsafeChr :: Word16 -> Char
unsafeChr (W16# w#) = C# (chr# (word2Int# w#))
{-# INLINE unsafeChr #-}

unsafeChr8 :: Word8 -> Char
unsafeChr8 (W8# w#) = C# (chr# (word2Int# w#))
{-# INLINE unsafeChr8 #-}

unsafeChr32 :: Word32 -> Char
unsafeChr32 (W32# w#) = C# (chr# (word2Int# w#))
{-# INLINE unsafeChr32 #-}

-- | Write a character into the array at the given offset.  Returns
-- the number of 'Word16's written.
{-@ unsafeWrite :: ma:A.MArray s -> i:Nat -> {v:Char | (Room ma i v)}
                -> ST s {v:(MAValidL i ma) | (BtwnI v 1 2)}
  @-}
unsafeWrite :: A.MArray s -> Int -> Char -> ST s Int
unsafeWrite marr i c
    | n < 0x10000 = do
-- #if defined(ASSERTS)
        liquidAssert (i >= 0) . liquidAssert (i < A.maLen marr) $ return ()
-- #endif
        A.unsafeWrite marr i (fromIntegral n)
        return 1
    | otherwise = do
-- #if defined(ASSERTS)
        liquidAssert (i >= 0) . liquidAssert (i < A.maLen marr - 1) $ return ()
-- #endif
        A.unsafeWrite marr i lo
        A.unsafeWrite marr (i+1) hi
        return 2
    where n = ord c
          m = n - 0x10000
          lo = fromIntegral $ (m `shiftR` 10) + 0xD800
          hi = fromIntegral $ (m .&. 0x3FF) + 0xDC00
{-# INLINE unsafeWrite #-}

{-
unsafeWriteRev :: A.MArray s Word16 -> Int -> Char -> ST s Int
unsafeWriteRev marr i c
    | n < 0x10000 = do
        assert (i >= 0) . assert (i < A.length marr) $
          A.unsafeWrite marr i (fromIntegral n)
        return (i-1)
    | otherwise = do
        assert (i >= 1) . assert (i < A.length marr) $
          A.unsafeWrite marr (i-1) lo
        A.unsafeWrite marr i hi
        return (i-2)
    where n = ord c
          m = n - 0x10000
          lo = fromIntegral $ (m `shiftR` 10) + 0xD800
          hi = fromIntegral $ (m .&. 0x3FF) + 0xDC00
{-# INLINE unsafeWriteRev #-}
-}