Bytes.idr

module Main

import Data.So
import Debug.Trace

%include C "bytes.h"
%link C "bytes.o"

%access public

abstract
data ByteArray : (size : Int) -> Type where
  MkByteArray : ManagedPtr -> ByteArray i

inBounds : Int -> Int -> Bool
inBounds i b = i >= 0 && i < b

read : (i : Int) -> ByteArray j -> So (inBounds i j) -> IO Bits8
read i (MkByteArray ptr) ok =
  foreign FFI_C "readByteArray" (Int -> ManagedPtr -> IO Bits8) i ptr

write : (i : Int) -> Bits8 -> ByteArray j -> So (inBounds i j) -> IO ()
write i b (MkByteArray ptr) ok =
  foreign FFI_C "writeByteArray" (Int -> Bits8 -> ManagedPtr -> IO ()) i b ptr

partial
initialize : ByteArray j -> (Int -> Bits8) -> IO ()
initialize {j} bytes f = initialize' 0
  where initialize' : Int -> IO ()
        initialize' i with (choose $ inBounds i j)
          initialize' i | Right nope = return ()
          initialize' i | Left yep   = do write i (f i) bytes yep
                                          initialize' (i + 1)


allocBytes : (i : Int) -> (Int -> Bits8) -> IO (ByteArray i)
allocBytes x init =
  do bytes <- foreign FFI_C "malloc" (Int -> IO Ptr) x
     let bytes = MkByteArray $ prim__registerPtr bytes x
     initialize bytes init
     return bytes

dump : ByteArray j -> IO ()
dump {j} arr = dump' 0
  where dump' : Int -> IO ()
        dump' i with (choose $ inBounds i j)
          dump' i | Right nope = return ()
          dump' i | Left yep   = do val <- read i arr yep
                                    print val; putStr " "
                                    dump' (i+1)


main : IO ()
main = do count <- allocBytes 256 prim__truncInt_B8
          dump count
          return ()