content: {-@ LIQUID "--pruneunsorted" @-}
  {-@ LIQUID "--maxparams=3" @-}
  {-@ LIQUID "--bscope" @-}
  {-@ LIQUID "--no-check-imports" @-}
  {- LIQUID "--trust-sizes" @-}
  
  {-# LANGUAGE BangPatterns, DeriveDataTypeable #-}
  -- |
  -- Module      : Data.Text.Lazy.Internal
  -- Copyright   : (c) 2009, 2010 Bryan O'Sullivan
  --
  -- 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.Lazy.Internal
      (
        Text(..)
      , chunk
      , empty
      , foldrChunks
      , foldlChunks
      -- * Data type invariant and abstraction functions
  
      -- $invariant
      , strictInvariant
      , lazyInvariant
      , showStructure
  
      -- * Chunk allocation sizes
      , defaultChunkSize
      , smallChunkSize
      , chunkOverhead
      ) where
  
  import Data.Text ()
  import Data.Text.UnsafeShift (shiftL)
  import Data.Typeable (Typeable)
  import Foreign.Storable (sizeOf)
  import Foreign.ForeignPtr
  import qualified Data.Text.Internal as T
  
  
  --LIQUID
  import Language.Haskell.Liquid.Prelude
  import qualified Data.Text.Fusion.Size as TODO_REBARE
  import qualified Data.Text.Array       as TODO_REBARE
  import qualified Data.Text             as TODO_REBARE
  
  data Text = Empty
            | Chunk {-# UNPACK #-} !T.Text Text
  --LIQUID            deriving (Typeable)
  
  {-@ data Text [ltlen] = Empty
                        | Chunk { txtHead :: TextNE, txtRest :: Text }
    @-}
  
  {-@ measure ltlen :: Text -> Integer
        ltlen Empty      = 0
        ltlen (Chunk t ts) = (tlen t) + (ltlen ts)
    @-}
  
  
  
  {-@ measure ltlength :: Text -> Integer
        ltlength Empty      = 0
        ltlength (Chunk t ts) = (tlength t) + (ltlength ts)
    @-}
  
  {-@ measure sum_ltlengths :: [Text] -> Integer
        sum_ltlengths [] = 0
        sum_ltlengths (t:ts) = (ltlength t) + (sum_ltlengths ts)
    @-}
  
  {-@ qualif SumLTLengthsAcc(v:Text, ts:List Text, t:Text):
          ltlength(v) = sum_ltlengths(ts) + ltlength(t)
    @-}
  
  {-@ type LTextN N  = {v:Text | (ltlen v) = N} @-}
  {-@ type LTextNC N = {v:Text | (ltlength v) = N} @-}
  {-@ type LTextNE   = {v:Text | (((ltlen v) > 0) && (ltlength v) > 0)} @-}
  {-@ type LTextLE T = {v:Text | (ltlen v) <= (ltlen T)} @-}
  {-@ type LTextLT T = {v:Text | (ltlen v) <  (ltlen T)} @-}
  
  {-@ qualif LTLenLe(v:Text, t:Text): (ltlen v) <= (ltlen t) @-}
  
  {-@ invariant {v:Text | (ltlen v) >= 0} @-}
  {-@ invariant {v:Text | (ltlength v) >= 0} @-}
  {-@ invariant {v:Text | (((ltlength v) = 0) <=> ((ltlen v) = 0))} @-}
  {-@ invariant {v0:[Text] | (sum_ltlengths v0) >= 0} @-}
  {-@ invariant {v0:[{v:Text | (sum_ltlengths v0) >= (ltlength v)}] | true} @-}
  
  
  -- $invariant
  --
  -- The data type invariant for lazy 'Text': Every 'Text' is either 'Empty' or
  -- consists of non-null 'T.Text's.  All functions must preserve this,
  -- and the QC properties must check this.
  
  -- | Check the invariant strictly.
  {-@ strictInvariant :: Text -> Bool @-}
  strictInvariant :: Text -> Bool
  strictInvariant Empty = True
  strictInvariant x@(Chunk (T.Text _ _ len) cs)
      | len > 0   = strictInvariant cs
      | otherwise = liquidError $ "Data.Text.Lazy: invariant violation: "
                    ++ showStructure x
  
  -- | Check the invariant lazily.
  {-@ lazyInvariant :: Text -> Text @-}
  lazyInvariant :: Text -> Text
  lazyInvariant Empty = Empty
  lazyInvariant x@(Chunk c@(T.Text _ _ len) cs)
      | len > 0   = Chunk c (lazyInvariant cs)
      | otherwise = liquidError $ "Data.Text.Lazy: invariant violation: "
                    ++ showStructure x
  
  -- | Display the internal structure of a lazy 'Text'.
  {-@ showStructure :: Text -> String @-}
  showStructure :: Text -> String
  showStructure Empty           = "Empty"
  showStructure (Chunk t Empty) = "Chunk " ++ show t ++ " Empty"
  showStructure (Chunk t ts)    =
      "Chunk " ++ show t ++ " (" ++ showStructure ts ++ ")"
  
  -- | Smart constructor for 'Chunk'. Guarantees the data type invariant.
  {-@ chunk :: t:_ -> ts:Text
            -> {v:Text | (((ltlength v) = ((tlength t) + (ltlength ts)))
                        && ((ltlen v) = ((tlen t) + (ltlen ts))))}
    @-}
  chunk :: T.Text -> Text -> Text
  {-# INLINE chunk #-}
  chunk t@(T.Text _ _ len) ts | len == 0 = ts
                              | otherwise = Chunk t ts
  
  -- | Smart constructor for 'Empty'.
  {-@ empty :: {v:Text | (ltlength v) = 0} @-}
  empty :: Text
  {-# INLINE [0] empty #-}
  empty = Empty
  
  -- | Consume the chunks of a lazy 'Text' with a natural right fold.
  {-@ foldrChunks :: forall <p :: Text -> a -> Bool>.
                     (ts:Text -> t:TextNE -> a<p ts> -> a<p (Chunk t ts)>)
                  -> a<p Empty>
                  -> t:Text
                  -> a<p t>
    @-}
  foldrChunks :: (Text -> T.Text -> a -> a) -> a -> Text -> a
  foldrChunks f z = go
    where go Empty        = z
          go (Chunk c cs) = f cs c (go cs)
  --LIQUID foldrChunks :: (T.Text -> a -> a) -> a -> Text -> a
  --LIQUID foldrChunks f z = go
  --LIQUID   where go Empty        = z
  --LIQUID         go (Chunk c cs) = f c (go cs)
  {-# INLINE foldrChunks #-}
  
  -- | Consume the chunks of a lazy 'Text' with a strict, tail-recursive,
  -- accumulating left fold.
  {-@ foldlChunks :: (a -> TextNE -> a) -> a -> Text -> a @-}
  foldlChunks :: (a -> T.Text -> a) -> a -> Text -> a
  foldlChunks f z = go z
    where go !a Empty        = a
          go !a (Chunk c cs) = go (f a c) cs
  {-# INLINE foldlChunks #-}
  
  -- | Currently set to 16 KiB, less the memory management overhead.
  {-@ defaultChunkSize :: {v:Nat | v = 16368} @-}
  defaultChunkSize :: Int
  defaultChunkSize = 16384 - chunkOverhead
  {-# INLINE defaultChunkSize #-}
  
  -- | Currently set to 128 bytes, less the memory management overhead.
  {-@ smallChunkSize :: {v:Nat | v = 112} @-}
  smallChunkSize :: Int
  smallChunkSize = 128 - chunkOverhead
  {-# INLINE smallChunkSize #-}
  
  -- | The memory management overhead. Currently this is tuned for GHC only.
  {-@ chunkOverhead :: {v:Nat | v = 16} @-}
  chunkOverhead :: Int
  chunkOverhead = sizeOf (undefined :: Int) `shiftL` 1
  {-# INLINE chunkOverhead #-}
  