content: {-@ LIQUID "--idirs=../../benchmarks/bytestring-0.9.2.1/" @-}
  {-@ LIQUID "--idirs=../../include" @-}
  {-@ LIQUID "--no-termination" @-}
  {-# OPTIONS_GHC -cpp -fglasgow-exts -fno-warn-orphans #-}
  
  -- look for `n0` and `n1` below. Why does this work with `n1` but not `n0` or `0-1` ?
  -- the latter is likely some weird qualifier issue.
  
  
  module Data.ByteString (
          ByteString,            -- abstract, instances: Eq, Ord, Show, Read, Data, Typeable, Monoid
          foldr                  -- :: (a -> Word8 -> a) -> a -> ByteString -> a
    , wantReadableHandleLIQUID
    ) where
  
  
  import qualified Prelude as P
  import Prelude hiding           (reverse,head,tail,last,init,null
                                  ,length,map,lines,foldl,foldr,unlines
                                  ,concat,any,take,drop,splitAt,takeWhile
                                  ,dropWhile,span,break,elem,filter,maximum
                                  ,minimum,all,concatMap,foldl1,foldr1
                                  ,scanl,scanl1,scanr,scanr1
                                  ,readFile,writeFile,appendFile,replicate
                                  ,getContents,getLine,putStr,putStrLn,interact
                                  ,zip,zipWith,unzip,notElem)
  
  import Data.ByteString.Internal
  import Data.ByteString.Unsafe
  import Data.ByteString.Fusion
  
  import qualified Data.List as List
  
  import Data.Word                (Word8)
  import Data.Maybe               (listToMaybe)
  import Data.Array               (listArray)
  import qualified Data.Array as Array ((!))
  
  -- Control.Exception.bracket not available in yhc or nhc
  #ifndef __NHC__
  import Control.Exception        (bracket, assert)
  import qualified Control.Exception as Exception
  #else
  import IO			(bracket)
  #endif
  import Control.Monad            (when)
  
  import Foreign.C.String         (CString, CStringLen)
  import Foreign.C.Types          (CSize)
  import Foreign.ForeignPtr
  import Foreign.Marshal.Alloc    (allocaBytes, mallocBytes, reallocBytes, finalizerFree)
  import Foreign.Marshal.Array    (allocaArray)
  import Foreign.Ptr
  import Foreign.Storable         (Storable(..))
  
  -- hGetBuf and hPutBuf not available in yhc or nhc
  import System.IO                (stdin,stdout,hClose,hFileSize
                                  ,hGetBuf,hPutBuf,openBinaryFile
                                  ,Handle,IOMode(..))
  
  import Data.Monoid              (Monoid, mempty, mappend, mconcat)
  
  #if !defined(__GLASGOW_HASKELL__)
  import System.IO.Unsafe
  import qualified System.Environment
  import qualified System.IO      (hGetLine)
  #endif
  
  #if defined(__GLASGOW_HASKELL__)
  
  import System.IO                (hGetBufNonBlocking)
  import System.IO.Error          (isEOFError)
  
  import GHC.Handle
  import GHC.Prim                 (Word#, (+#), writeWord8OffAddr#)
  import GHC.Base                 (build)
  import GHC.Word hiding (Word8)
  import GHC.Ptr                  (Ptr(..))
  import GHC.ST                   (ST(..))
  import GHC.IOBase
  
  #endif
  
  -- An alternative to Control.Exception (assert) for nhc98
  #ifdef __NHC__
  #define assert  assertS "__FILE__ : __LINE__"
  assertS :: String -> Bool -> a -> a
  assertS _ True  = id
  assertS s False = error ("assertion failed at "++s)
  #endif
  
  -- LIQUID
  import GHC.IO.Buffer
  import Language.Haskell.Liquid.Foreign (intCSize, eqPtr) 
  import qualified Data.ByteString.Lazy.Internal 
  import qualified Data.ByteString.Fusion
  import qualified Data.ByteString.Internal
  import qualified Data.ByteString.Unsafe
  import qualified Foreign.C.Types
  
  {-@ memcpy_ptr_baoff :: p:(Ptr a) 
                       -> RawBuffer b 
                       -> Int 
                       -> {v:CSize | (OkPLen v p)} -> IO (Ptr ())
    @-}
  memcpy_ptr_baoff :: Ptr a -> RawBuffer b -> Int -> CSize -> IO (Ptr ())
  memcpy_ptr_baoff = error "LIQUIDCOMPAT"
  
  readCharFromBuffer :: RawBuffer b -> Int -> IO (Char, Int)
  readCharFromBuffer x y = error "LIQUIDCOMPAT"
  
  wantReadableHandleLIQUID :: String -> Handle -> (Handle__ -> IO a) -> IO a
  wantReadableHandleLIQUID x y f = error $ show $ liquidCanaryFusion 12 -- "LIQUIDCOMPAT"
  
  {-@ qualif Gimme(v:a, n:b, acc:a): (len v) = (n + 1 + (len acc)) @-}
  {-@ qualif Zog(v:a, p:a)         : (plen p) <= (plen v)          @-}
  {-@ qualif Zog(v:a)              : 0 <= (plen v)                 @-}
  
  {- type ByteStringNE   = {v:ByteString | (bLength v) > 0} @-}
  {- type ByteStringSZ B = {v:ByteString | (bLength v) = (bLength B)} @-}
  -- -----------------------------------------------------------------------------
  --
  -- Useful macros, until we have bang patterns
  --
  -- -----------------------------------------------------------------------------
  {-@ foldr :: (Word8 -> a -> a) -> a -> ByteString -> a @-}
  foldr :: (Word8 -> a -> a) -> a -> ByteString -> a
  foldr k v (PS x s l) = inlinePerformIO $ withForeignPtr x $ \ptr ->
          ugo k v (ptr `plusPtr` (s+l-1)) (ptr `plusPtr` (s-1))
  
  {-@ ugo :: (Word8 -> a -> a) -> a -> p:(PtrV Word8) -> {v:Ptr Word8 | ((pbase v) = (pbase p) &&  (plen v) >= (plen p)) } -> IO a @-}
  ugo :: (Word8 -> a -> a) -> a -> Ptr Word8 -> Ptr Word8 -> IO a
  ugo k z p q | eqPtr q p   = return z
              | otherwise = do c  <- peek p
                               let n0  = -1               -- BAD  
                               let n1  = 0 - 1            -- OK
                               let p' = p `plusPtr` n1 {- BAD (0 - 1) -}
                               ugo k (c `k` z) p' q -- tail recursive
  
  
  {- liquid_thm_ptr_cmp' :: p:PtrV a
                          -> q:{v:(PtrV a) | ((plen v) >= (plen p) && v != p && (pbase v) = (pbase p))} 
                          -> {v: (PtrV a)  | ((v = p) && ((plen v) > 0) && ((plen q) > (plen p))) } 
    @-}
  liquid_thm_ptr_cmp' :: Ptr a -> Ptr a -> Ptr a
  liquid_thm_ptr_cmp' p q = undefined 
  