content: {-@ LIQUID "--maxparams=3"      @-}
  {-@ LIQUID "--prune-unsorted"   @-}
  {-@ LIQUID "--bscope"           @-}
  {-@ LIQUID "--no-check-imports" @-}
  {- LIQUID "--trust-sizes" @-}
  
  {-# LANGUAGE CPP, DeriveDataTypeable #-}
  
  -- |
  -- Module      : Data.Text.Internal
  -- 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
  --
  -- A module containing private 'Text' internals. This exposes the
  -- 'Text' representation and low level construction functions.
  -- Modules which extend the 'Text' system may need to use this module.
  --
  -- You should not use this module unless you are determined to monkey
  -- with the internals, as the functions here do just about nothing to
  -- preserve data invariants.  You have been warned!
  
  module Data.Text.Internal
      (
      -- * Types
        Text(..)
      -- * Construction
      , text
      , textP
      -- * Safety
      , safe
      -- * Code that must be here for accessibility
      , empty
      -- * Utilities
      , firstf
      -- * Debugging
      , showText
      ) where
  
  --LIQUID #if defined(ASSERTS)
  import Control.Exception (assert)
  --LIQUID #endif
  import Data.Bits ((.&.))
  import qualified Data.Text.Array as A
  import Data.Text.UnsafeChar (ord)
  import Data.Typeable (Typeable)
  
  --LIQUID
  import Language.Haskell.Liquid.Prelude
  
  {-@ data Text [tlen] = Text { ttarr :: Data.Text.Array.Array
                              , ttoff :: AValidO ttarr
                              , ttlen :: AValidL ttoff ttarr
                              }
    @-}
  
  {-@ measure tarr :: Text -> Data.Text.Array.Array
        tarr (Text a o l) = a
    @-}
  
  {-@ measure toff :: Text -> Int
        toff (Text a o l) = o
    @-}
  
  {-@ measure tlen :: Text -> Int 
        tlen (Text a o l) = l  
    @-}
  
  {-@ type TextN  N = {v:Text | (tlen v) = N} @-}
  {-@ type TextNC N = {v:Text | (tlength v) = N} @-}
  {-@ type TextNE   = {v:Text | (tlen v) > 0} @-}
  {-@ type TextLE T = {v:Text | (tlen v) <= (tlen T)} @-}
  {-@ type TextLT T = {v:Text | (tlen v) <  (tlen T)} @-}
  
  {-@ type TValidI  T   = {v:Nat | v <  (tlen T)} @-}
  {-@ type TValidIN T N = {v:Nat | v <= ((tlen T) - N)} @-}
  {-@ type TValidIC T   = {v:Nat | v <  (tlength T)} @-}
  
  {-@ qualif TextNE(v:Text): tlen(v) > 0 @-}
  {-@ qualif TextNE(v:Text): tlength(v) > 0 @-}
  
  {-@ measure sum_tlens :: [Text] -> Int
        sum_tlens []   = 0
        sum_tlens (t:ts) = (tlen t) + (sum_tlens ts)
    @-}
  
  {-@ measure tlength :: Text -> Int
        tlength (Text a o l) = numchars a o l
    @-}
  
  {-@ type IncrTList a = [a]<{\x y -> (tlength x) < (tlength y)}> @-}
  {-@ type DecrTList a = [a]<{\x y -> (tlength x) > (tlength y)}> @-}
  
  {-@ qualif TLengthEq(v:Text, t:Text):
          tlength(v) = tlength(t)
    @-}
  {-@ qualif TLengthLe(v:Text, t:Text):
          tlength(v) <= tlength(t)
    @-}
  {-@ qualif TLenLe(v:Text, t:Text):
          (tlen v) <= (tlen t)
    @-}
  
  {-@ qualif MinTLength(v:Text, n:Int, t:Text):
          tlength(v) = if tlength(t) > n then n else (tlength t)
    @-}
  
  {-@ qualif TLengthAcc(v:int, t:Text, l:int):
          v = ((tlength t) + l)
    @-}
  
  {-@ qualif TLengthDiff(v:Text, t1:Text, t2:Text):
          tlength(v) = tlength(t1) - tlength(t2)
    @-}
  {-@ qualif TLenDiff(v:Text, t1:Text, t2:Text):
          tlen(v) = tlen(t1) - tlen(t2)
    @-}
  
  {-@ measure sum_tlengths :: [Text] -> Int
        sum_tlengths [] = 0
        sum_tlengths (t:ts) = (tlength t) + (sum_tlengths ts)
    @-}
  
  {-@ invariant {v:Text | (numchars (tarr v) (toff v) 0) = 0} @-}
  {-@ invariant {v:Text | (numchars (tarr v) (toff v) (tlen v)) >= 0} @-}
  {-@ invariant {v:Text | (numchars (tarr v) (toff v) (tlen v)) <= (tlen v)} @-}
  
  {-@ invariant {v:Text | (((tlength v) = 0) <=> ((tlen v) = 0))} @-}
  {-@ invariant {v:Text | (tlength v) >= 0} @-}
  {-@ invariant {v:Text | (tlen v) >= 0} @-}
  {-@ invariant {v:Text | (tlength v) = (numchars (tarr v) (toff v) (tlen v))} @-}
  
  {-@ invariant {v:[Text] | (sum_tlens v) >= 0} @-}
  
  {-@ invariant {v:[{ v0:Text | ((((len v) > 1) && ((tlen v0) > 0)) => ((tlen v0) < (sum_tlens v))) }] | true} @-}
  {-@ invariant {v:[{ v0:Text | ((((tlen v0) > 0) && (((len v) > 0))) => ((sum_tlens v) > 0)) }] | true} @-}
  
  -- | A space efficient, packed, unboxed Unicode text type.
  data Text = Text
      {-# UNPACK #-} !A.Array          -- payload
      {-# UNPACK #-} !Int              -- offset
      {-# UNPACK #-} !Int              -- length
  --LIQUID    deriving (Typeable)
  
  -- | Smart constructor.
  {-@ text :: a:A.Array -> o:AValidO a -> l:AValidL o a
           -> {v:Text | (((tarr v) = a) && ((toff v) = o) && ((tlen v) = l)
                         && ((tlength v) = (numchars a o l)))}
    @-}
  text :: A.Array -> Int -> Int -> Text
  text arr off len =
  --LIQUID pushing bindings inward to prove safety
  --LIQUID #if defined(ASSERTS)
  --LIQUID  let c    = A.unsafeIndex arr off
  --LIQUID      alen = A.length arr
    let zzzalen = A.aLen arr
    in liquidAssert (len >= 0) .
       liquidAssert (off >= 0) .
       liquidAssert (zzzalen == 0 || len == 0 || off < zzzalen) $
  --LIQUID     assert (len == 0 || c < 0xDC00 || c > 0xDFFF) $
       let t = if len == 0 then Text arr off len else
                  let c = A.unsafeIndex arr off in
                  assert (c < 0xDC00 || c > 0xDFFF) $
  --LIQUID #endif
                  Text arr off len
       in liquidAssume (tlEqNumchars t arr off len) t
  {-# INLINE text #-}
  
  -- | /O(1)/ The empty 'Text'.
  {-@ empty :: {v:Text | (tlen v) = 0} @-}
  empty :: Text
  empty = Text A.empty 0 0
  {-# INLINE [1] empty #-}
  
  -- | Construct a 'Text' without invisibly pinning its byte array in
  -- memory if its length has dwindled to zero.
  {-@ textP :: a:A.Array -> o:AValidO a -> l:AValidL o a
            -> {v:Text | (((tlen v) = l) && ((tlength v) = (numchars a o l)))}
    @-}
  textP :: A.Array -> Int -> Int -> Text
  textP arr off len | len == 0  = liquidAssume (numcharsZ arr off len) empty
                    | otherwise = text arr off len
  {-# INLINE textP #-}
  
  -- | A useful 'show'-like function for debugging purposes.
  showText :: Text -> String
  showText (Text arr off len) =
      "Text " ++ show (A.toList arr off len) ++ ' ' :
              show off ++ ' ' : show len
  
  -- | Map a 'Char' to a 'Text'-safe value.
  --
  -- UTF-16 surrogate code points are not included in the set of Unicode
  -- scalar values, but are unfortunately admitted as valid 'Char'
  -- values by Haskell.  They cannot be represented in a 'Text'.  This
  -- function remaps those code points to the Unicode replacement
  -- character \"&#xfffd;\", and leaves other code points unchanged.
  safe :: Char -> Char
  safe c
      | ord c .&. 0x1ff800 /= 0xd800 = c
      | otherwise                    = '\xfffd'
  {-# INLINE safe #-}
  
  -- | Apply a function to the first element of an optional pair.
  firstf :: (a -> c) -> Maybe (a,b) -> Maybe (c,b)
  firstf f (Just (a, b)) = Just (f a, b)
  firstf _  Nothing      = Nothing
  
  
  --LIQUID
  {-@ tlEqNumchars :: t:Text -> a:A.Array -> o:Int -> l:Int
                   -> {v:Bool | (v <=> ((tlength t) = (numchars a o l)))}
    @-}
  tlEqNumchars :: Text -> A.Array -> Int -> Int -> Bool
  tlEqNumchars = undefined
  
  {-@ numcharsZ :: a:A.Array -> o:Int -> l:Int
                -> {v:Bool | (v <=> ((numchars a o l) = 0))}
    @-}
  numcharsZ :: A.Array -> Int -> Int -> Bool
  numcharsZ = undefined
  