Remove use of deprecated getByte function (#3190)

* Add CHANGELOG_NEXT entry

CHANGELOG_NEXT.md

@@ -46,6 +46,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added append `(++)` for `List` version of `All`.
 
+* Deprecate `bufferData` in favor of `bufferData'`. These functions are the same
+  with the exception of the latter dealing in `Bits8` which is more correct than
+  `Int`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

libs/base/Data/Buffer.idr

@@ -378,6 +378,8 @@ getString : HasIO io => Buffer -> (offset : Int) -> (len : Int) -> io String
 getString buf offset len
     = primIO (prim__getString buf offset len)
 
+||| Use `bufferData'` instead, as its value is correctly limited.
+%deprecate
 export
 covering
 bufferData : HasIO io => Buffer -> io (List Int)
@@ -389,7 +391,23 @@ bufferData buf
     unpackTo : List Int -> Int -> io (List Int)
     unpackTo acc 0 = pure acc
     unpackTo acc offset
-        = do val <- getByte buf (offset - 1)
+        = do val <- getBits8 buf (offset - 1)
+             unpackTo (cast val :: acc) (offset - 1)
+
+||| This function performs the same task as `bufferData` but it
+||| returns `List Bits8` which is more correct than `List Int`.
+export
+covering
+bufferData' : HasIO io => Buffer -> io (List Bits8)
+bufferData' buf
+    = do len <- rawSize buf
+         unpackTo [] len
+  where
+    covering
+    unpackTo : List Bits8 -> Int -> io (List Bits8)
+    unpackTo acc 0 = pure acc
+    unpackTo acc offset
+        = do val <- getBits8 buf (offset - 1)
              unpackTo (val :: acc) (offset - 1)
 
 

libs/contrib/Debug/Buffer.idr

@@ -7,8 +7,9 @@ import Data.String
 toHex : Int -> Int -> String
 toHex d n = pack $ reverse $ foldl toHexDigit [] (slice d n [])
     where
-        toHexDigit : List Char ->Int -> List Char
+        toHexDigit : List Char -> Int -> List Char
         toHexDigit acc i = chr (if i < 10 then i + ord '0' else (i-10) + ord 'A')::acc
+
         slice : Int -> Int -> List Int -> List Int
         slice 0 _ acc = acc
         slice d n acc = slice (d-1) (n `div` 16) ((n `mod` 16)::acc)
@@ -19,9 +20,9 @@ showSep sep n [x] = x ++ replicate (3*n) ' '
 showSep sep Z (x :: xs) = x ++ sep ++ showSep sep Z xs
 showSep sep (S n) (x :: xs) = x ++ sep ++ showSep sep n xs
 
-renderRow : List Int -> String
-renderRow dat =  showSep " " 16 (map (toHex 2) dat) ++
-                "      " ++ pack (map (\i => if i > 0x1f && i < 0x80 then chr i else '.') dat)
+renderRow : List Bits8 -> String
+renderRow dat = showSep " " 16 (map (toHex 2 . cast) dat) ++
+                "      " ++ pack (map (\i => if i > 0x1f && i < 0x80 then chr (cast i) else '.') dat)
 
 group : Nat -> List a -> List (List a)
 group n xs = worker [] xs
@@ -34,7 +35,7 @@ export
 dumpBuffer : HasIO io => Buffer -> io String
 dumpBuffer buf = do
     size <- liftIO $ rawSize buf
-    dat <- liftIO $ bufferData buf
+    dat <- liftIO $ bufferData' buf
     let rows = group 16 dat
     let hex = showSep "\n" 0 (map renderRow rows)
     pure $ hex ++ "\n\ntotal size = " ++ show size

src/Libraries/Utils/Binary.idr

@@ -43,12 +43,27 @@ export
 incLoc : Integer -> Binary -> Binary
 incLoc i c = { loc $= (+i) } c
 
+-- TODO: remove this function once Idris2 v0.8.0 has been released
+--       and use the version from base instead.
+covering
+bufferData' : HasIO io => Buffer -> io (List Bits8)
+bufferData' buf
+    = do len <- rawSize buf
+         unpackTo [] len
+  where
+    covering
+    unpackTo : List Bits8 -> Int -> io (List Bits8)
+    unpackTo acc 0 = pure acc
+    unpackTo acc offset
+        = do val <- getBits8 buf (offset - 1)
+             unpackTo (val :: acc) (offset - 1)
+
 export
 dumpBin : Binary -> IO ()
 dumpBin chunk
-   = do -- printLn !(traverse bufferData (map buf done))
-        printLn !(bufferData (buf chunk))
-        -- printLn !(traverse bufferData (map buf rest))
+   = do -- printLn !(traverse Binary.bufferData' (map buf done))
+        printLn !(Binary.bufferData' (buf chunk))
+        -- printLn !(traverse Binary.bufferData' (map buf rest))
 
 export
 nonEmptyRev : {xs : _} ->

tests/chez/chez004/Buffer.idr

@@ -35,21 +35,21 @@ main
          val <- getBits16 buf 32
          printLn val
 
-         ds <- bufferData buf
+         ds <- bufferData' buf
          printLn ds
 
          Right _ <- writeBufferToFile "test.buf" buf 100
              | Left err => putStrLn "Buffer write fail"
          Right buf2 <- createBufferFromFile "test.buf"
              | Left err => putStrLn "Buffer read fail"
 
-         ds <- bufferData buf2
+         ds <- bufferData' buf2
          printLn ds
 
          setBits8 buf2 0 1
          Just ccBuf <- concatBuffers [buf, buf2]
             | Nothing => putStrLn "Buffer concat failed"
-         printLn !(bufferData ccBuf)
+         printLn !(bufferData' ccBuf)
 
          Just (a, b) <- splitBuffer buf 20
             | Nothing => putStrLn "Buffer split failed"

tests/node/node004/Buffer.idr

@@ -28,15 +28,15 @@ main
          val <- getBits16 buf 32
          printLn val
 
-         ds <- bufferData buf
+         ds <- bufferData' buf
          printLn ds
 
          Right _ <- writeBufferToFile "test.buf" buf 100
              | Left err => putStrLn "Buffer write fail"
          Right buf2 <- createBufferFromFile "test.buf"
              | Left err => putStrLn "Buffer read fail"
 
-         ds <- bufferData buf2
+         ds <- bufferData' buf2
          printLn ds
 
 -- Put back when the File API is moved to C and these can work again

tests/refc/buffer/TestBuffer.idr

@@ -38,7 +38,7 @@ main = do
     put $ getDouble buf 16
     put $ getString buf 24 12
 
-    put $ bufferData buf
+    put $ bufferData' buf
 
     Just readBuf <- newBuffer 8
         | Nothing => pure ()
@@ -47,7 +47,7 @@ main = do
     Right 8 <- readBufferData f readBuf 0 8
         | Right size => put $ pure "\{show size} bytes have been read, 8 expected"
         | Left err => put $ pure err
-    put $ bufferData readBuf
+    put $ bufferData' readBuf
 
     Just writeBuf <- newBuffer 8
         | Nothing => pure ()