{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--diffcheck"      @-}
{-@ LIQUID "--short-names"    @-}
{-# LANGUAGE ForeignFunctionInterface #-}
module Bytestring where

import Prelude hiding (null)
import Data.Char
import Data.Word
import Foreign.C.Types
import Foreign.ForeignPtr
import Foreign.Ptr
import Foreign.Storable
import System.IO.Unsafe
import Language.Haskell.Liquid.Prelude


data ByteString = PS { bPayload :: ForeignPtr Word8
                     , bOffset  :: !Int
                     , bLength  :: !Int
                     }

{- measure fplen :: ForeignPtr a -> Int -}

{-@ data ByteString = PS
      { bPayload :: ForeignPtr Word8
      , bOffset  :: {v:Nat | v           <= fplen bPayload}
      , bLength  :: {v:Nat | bOffset + v <= fplen bPayload}
      }
  @-}

{-@ type ByteStringN N = {v:ByteString | bLength v = N} @-}

{-@ type ForeignN a N = {v:ForeignPtr a | fplen v = N} @-}
{-@ assume mallocForeignPtrBytes :: n:Nat -> IO (ForeignN a n) @-}

bs = do fp <- mallocForeignPtrBytes 5
        return $ PS fp 2 3

{-@ create :: l:Nat -> (PtrN Word8 l -> IO ()) -> IO (ByteStringN l) @-}
create l f = do
    fp <- mallocForeignPtrBytes  l
    withForeignPtr fp $ \p -> f p
    return $! PS fp 0 l

foo = create 5 $ \p -> poke (p `plusPtr` 4) (0 :: Word8)

{-@ pack :: s:[Word8] -> ByteStringN (len s) @-}
pack str = unsafeCreate (length str) $ \p -> go p  str
  where
    go _ []     = return  ()
    go p (x:xs) = poke p x >> go (p `plusPtr` 1) xs


-- uncomment this spec and then twiddle the definition to rerun diffcheck, it 
-- will only resolve the type error on the line you twiddle.
{- unsafeIndex :: b:ByteString -> {v:Nat | v < bLength b} -> Word8 @-}
unsafeIndex (PS x s l) i = liquidAssert (i >= 0 && i < l)  $
    unsafePerformIO $ withForeignPtr x $ \p -> peekByteOff p (s + i) --FIXME: diffcheck breaks here





good = let b = pack [1,2,3]
       in unsafeIndex b 2






















-----------------------------------------------------------------------
-- Helper Code
-----------------------------------------------------------------------
{-@ unsafeCreate :: l:Nat -> (PtrN Word8 l -> IO ()) -> (ByteStringN l) @-}
unsafeCreate n f = unsafePerformIO $ create n f

{-@ invariant {v:ByteString   | bLength  v >= 0} @-}

{-@ qualif PLLen(v:a, p:b) : (len v) <= (plen p) @-}
{-@ qualif ForeignPtrN(v:ForeignPtr a, n:int): fplen v = n @-}
{-@ qualif FPLenPLen(v:Ptr a, fp:ForeignPtr a): fplen fp = plen v @-}
{-@ qualif PtrLen(v:Ptr a, xs:List b): plen v = len xs @-}
{-@ qualif PlenEq(v: Ptr a, x: int): x <= (plen v) @-}

-- Local Variables:
-- flycheck-checker: haskell-liquid
-- End:

create :: Int -> (Ptr Word8 -> IO ()) -> IO ByteString
unsafeIndex :: ByteString -> Int -> Word8