idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-23 22:22:07 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #408 from melted/buffer_api

Browse Source 
Add concatBuffers and splitBuffer to Data.Buffer
This commit is contained in:
Niklas Larsson 2020-07-21 10:43:17 +02:00 committed by GitHub
commit 8a210d536e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 55 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
libs/base/Data/Buffer.idr
View File

@ -3,6 +3,8 @@ module Data.Buffer
import System.Directory
import System.File
import Data.List
-- Reading and writing binary buffers. Note that this primitives are unsafe,
-- in that they don't check that buffer locations are within bounds.
-- We really need a safe wrapper!
@ -298,3 +300,33 @@ resizeBuffer old newsize
copyData old 0 len buf 0
freeBuffer old
pure (Just buf)
||| Create a buffer containing the concatenated content from a
||| list of buffers.
export
concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
concatBuffers xs
= do let sizes = map prim__bufferSize xs
let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
let cumulative = reverse revCumulative
Just buf <- newBuffer totalSize
| Nothing => pure Nothing
traverse (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
pure (Just buf)
where
scanSize : (Int, List Int) -> Int -> (Int, List Int)
scanSize (s, cs) x = (s+x, s::cs)
||| Split a buffer into two at a position.
export
splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
splitBuffer buf pos = do size <- rawSize buf
if pos > 0 && pos < size
then do Just first <- newBuffer pos
| Nothing => pure Nothing
Just second <- newBuffer (size - pos)
| Nothing => pure Nothing
copyData buf 0 pos first 0
copyData buf pos (size-pos) second 0
pure $ Just (first, second)
else pure Nothing

10
tests/chez/chez004/Buffer.idr
View File

@ -1,5 +1,6 @@
import Data.Buffer
import System.File
import Debug.Buffer
main : IO ()
main
@ -39,6 +40,15 @@ main
ds <- bufferData buf2
printLn ds
setByte buf2 0 1
Just ccBuf <- concatBuffers [buf, buf2]
| Nothing => putStrLn "Buffer concat failed"
printLn !(bufferData ccBuf)
Just (a, b) <- splitBuffer buf 20
| Nothing => putStrLn "Buffer split failed"
printBuffer a
printBuffer b
freeBuffer buf
freeBuffer buf2

12
tests/chez/chez004/expected
View File

@ -6,5 +6,17 @@
65535
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
00 5E 00 00 00 41 41 41 41 00 7B 14 AE 47 E1 9A .^...AAAA.{..G..
57 40 00 00 W@..
total size = 20
48 65 6C 6C 6F 20 74 68 65 72 65 21 FF FF 00 00 Hello there!....
00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
total size = 80
1/1: Building Buffer (Buffer.idr)
Main> Main> Bye for now!

2
tests/chez/chez004/run
View File

@ -1,2 +1,2 @@
$1 --no-banner Buffer.idr < input
$1 -p contrib --no-banner Buffer.idr < input
rm -rf build test.buf