git.iko.soy/Idris-dev
on 181dddb help sign in
Idris-dev/test/primitives006/Data/ByteArray.idr
100 lines 2.7 kB history raw
1module Data.ByteArray
3%include C "array.h"
4%link C "array.o"
6%access public export
7%default total
9namespace Byte
10 Byte : Type
11 Byte = Bits8
13 toInt : Byte -> Int
14 toInt = prim__zextB8_Int
16 fromInt : Int -> Byte
17 fromInt = prim__truncInt_B8
19export
20record ByteArray where
21 constructor BA
22 ptr : CData
23 sz : Int
25-- This needn't be precise; it just needs to be enough to be safe.
26export
27bytesPerInt : Int
28bytesPerInt = 8
30export
31allocate : Int -> IO ByteArray
32allocate sz = do
33 ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz
34 return $ BA ptr sz
36export
37reallocate : Int -> ByteArray -> IO ()
38reallocate newSz (BA ptr sz)
39 = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr
41export
42peek : Int -> ByteArray -> IO Byte
43peek ofs (BA ptr sz)
44 = if (ofs < 0 || ofs >= sz)
45 then return 0
46 else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr
48export
49peekInt : Int -> ByteArray -> IO Int
50peekInt ofs (BA ptr sz)
51 = if (ofs < 0 || ofs+bytesPerInt > sz)
52 then return 0
53 else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr
55export
56poke : Int -> Byte -> ByteArray -> IO ()
57poke ofs b (BA ptr sz)
58 = if (ofs < 0 || ofs >= sz)
59 then return ()
60 else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr
62export
63pokeInt : Int -> Int -> ByteArray -> IO ()
64pokeInt ofs i (BA ptr sz)
65 = if (ofs < 0 || ofs+bytesPerInt > sz)
66 then return ()
67 else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr
69export
70copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()
71copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count
72 = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)
73 then return ()
74 else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count
76export
77fill : Int -> Int -> Byte -> ByteArray -> IO ()
78fill ofs count b (BA ptr sz)
79 = if (ofs < 0 || ofs+count > sz)
80 then return ()
81 else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr
83export
84size : ByteArray -> Int
85size (BA ptr sz) = sz
87export
88compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int
89compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count
90 = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)
91 then return 0
92 else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count
94export
95find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)
96find b (BA ptr sz) ofs end = do
97 ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end
98 if ofs < 0
99 then return $ Nothing
100 else return $ Just ofs