idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 05:01:34 +03:00
Code Issues Projects Releases Wiki Activity

[ perf ] use integers in the buffer state

Browse Source
This commit is contained in:
Guillaume Allais 2022-12-06 17:07:37 +00:00 committed by G. Allais
parent ebc406c519
commit 085ea348ae
2 changed files with 46 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

64
src/Core/Binary/Prims.idr
View File

@ -40,22 +40,22 @@ initBinary : Core (Ref Bin Binary)
initBinary initBinary
= do Just buf <- coreLift $ newBuffer blockSize = do Just buf <- coreLift $ newBuffer blockSize
| Nothing => throw (InternalError "Buffer creation failed") | Nothing => throw (InternalError "Buffer creation failed")
newRef Bin (newBinary buf blockSize) newRef Bin (newBinary buf (cast blockSize))
export export
initBinaryS : Int -> Core (Ref Bin Binary) initBinaryS : Int -> Core (Ref Bin Binary)
initBinaryS s initBinaryS s
= do Just buf <- coreLift $ newBuffer s = do Just buf <- coreLift $ newBuffer s
| Nothing => throw (InternalError "Buffer creation failed") | Nothing => throw (InternalError "Buffer creation failed")
newRef Bin (newBinary buf s) newRef Bin (newBinary buf (cast s))
extendBinary : Int -> Binary -> Core Binary extendBinary : Integer -> Binary -> Core Binary
extendBinary need (MkBin buf l s u) extendBinary need (MkBin buf l s u)
= do let newsize = s * 2 = do let newsize = s * 2
let s' = if (newsize - l) < need let s' = if (newsize - l) < need
then newsize + need then newsize + need
else newsize else newsize
Just buf' <- coreLift $ resizeBuffer buf s' Just buf' <- coreLift $ resizeBuffer buf (cast s')
| Nothing => throw (InternalError "Buffer expansion failed") | Nothing => throw (InternalError "Buffer expansion failed")
pure (MkBin buf' l s' u) pure (MkBin buf' l s' u)
@ -71,10 +71,10 @@ tag {b} val
= do chunk <- get Bin = do chunk <- get Bin
if avail chunk >= 1 if avail chunk >= 1
then then
do coreLift $ setBits8 (buf chunk) (loc chunk) $ cast val do coreLift $ setBits8 (buf chunk) (cast $ loc chunk) $ cast val
put Bin (appended 1 chunk) put Bin (appended 1 chunk)
else do chunk' <- extendBinary 1 chunk else do chunk' <- extendBinary 1 chunk
coreLift $ setBits8 (buf chunk') (loc chunk') $ cast val coreLift $ setBits8 (buf chunk') (cast $ loc chunk') $ cast val
put Bin (appended 1 chunk') put Bin (appended 1 chunk')
export export
@ -83,7 +83,7 @@ getTag {b}
= do chunk <- get Bin = do chunk <- get Bin
if toRead chunk >= 1 if toRead chunk >= 1
then then
do val <- coreLift $ getBits8 (buf chunk) (loc chunk) do val <- coreLift $ getBits8 (buf chunk) (cast $ loc chunk)
put Bin (incLoc 1 chunk) put Bin (incLoc 1 chunk)
pure $ cast val pure $ cast val
else throw (TTCError (EndOfBuffer "Bits8")) else throw (TTCError (EndOfBuffer "Bits8"))
@ -99,17 +99,17 @@ export
= do chunk <- get Bin = do chunk <- get Bin
if avail chunk >= 8 if avail chunk >= 8
then then
do coreLift $ setInt (buf chunk) (loc chunk) val do coreLift $ setInt (buf chunk) (cast $ loc chunk) val
put Bin (appended 8 chunk) put Bin (appended 8 chunk)
else do chunk' <- extendBinary 8 chunk else do chunk' <- extendBinary 8 chunk
coreLift $ setInt (buf chunk') (loc chunk') val coreLift $ setInt (buf chunk') (cast $ loc chunk') val
put Bin (appended 8 chunk') put Bin (appended 8 chunk')
fromBuf b fromBuf b
= do chunk <- get Bin = do chunk <- get Bin
if toRead chunk >= 8 if toRead chunk >= 8
then then
do val <- coreLift $ getInt (buf chunk) (loc chunk) do val <- coreLift $ getInt (buf chunk) (cast $ loc chunk)
put Bin (incLoc 8 chunk) put Bin (incLoc 8 chunk)
pure val pure val
else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk)))) else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
@ -123,10 +123,10 @@ TTC Int where
chunk <- get Bin chunk <- get Bin
if avail chunk >= 8 if avail chunk >= 8
then then
do coreLift $ setInt (buf chunk) (loc chunk) val do coreLift $ setInt (buf chunk) (cast $ loc chunk) val
put Bin (appended 8 chunk) put Bin (appended 8 chunk)
else do chunk' <- extendBinary 8 chunk else do chunk' <- extendBinary 8 chunk
coreLift $ setInt (buf chunk') (loc chunk') val coreLift $ setInt (buf chunk') (cast $ loc chunk') val
put Bin (appended 8 chunk') put Bin (appended 8 chunk')
fromBuf b fromBuf b
@ -134,7 +134,7 @@ TTC Int where
255 => do chunk <- get Bin 255 => do chunk <- get Bin
if toRead chunk >= 8 if toRead chunk >= 8
then then
do val <- coreLift $ getInt (buf chunk) (loc chunk) do val <- coreLift $ getInt (buf chunk) (cast $ loc chunk)
put Bin (incLoc 8 chunk) put Bin (incLoc 8 chunk)
pure val pure val
else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk)))) else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
@ -145,24 +145,26 @@ TTC String where
toBuf b val toBuf b val
-- To support UTF-8 strings, this has to get the length of the string -- To support UTF-8 strings, this has to get the length of the string
-- in bytes, not the length in characters. -- in bytes, not the length in characters.
= do let req = stringByteLength val = do let ireq = stringByteLength val
toBuf b req let req : Integer = cast ireq
toBuf b ireq
chunk <- get Bin chunk <- get Bin
if avail chunk >= req if avail chunk >= req
then then
do coreLift $ setString (buf chunk) (loc chunk) val do coreLift $ setString (buf chunk) (cast $ loc chunk) val
put Bin (appended req chunk) put Bin (appended req chunk)
else do chunk' <- extendBinary req chunk else do chunk' <- extendBinary req chunk
coreLift $ setString (buf chunk') (loc chunk') val coreLift $ setString (buf chunk') (cast $ loc chunk') val
put Bin (appended req chunk') put Bin (appended req chunk')
fromBuf b fromBuf b
= do len <- fromBuf {a = Int} b = do ilen <- fromBuf {a = Int} b
chunk <- get Bin chunk <- get Bin
let len = cast ilen
when (len < 0) $ corrupt "String" when (len < 0) $ corrupt "String"
if toRead chunk >= len if toRead chunk >= len
then then
do val <- coreLift $ getString (buf chunk) (loc chunk) len do val <- coreLift $ getString (buf chunk) (cast $ loc chunk) ilen
put Bin (incLoc len chunk) put Bin (incLoc len chunk)
pure val pure val
else throw (TTCError (EndOfBuffer ("String length " ++ show len ++ else throw (TTCError (EndOfBuffer ("String length " ++ show len ++
@ -172,26 +174,28 @@ export
TTC Binary where TTC Binary where
toBuf b val toBuf b val
= do let len = used val = do let len = used val
toBuf b len let ilen : Int = cast len
toBuf b ilen
chunk <- get Bin chunk <- get Bin
if avail chunk >= len if avail chunk >= len
then then
do coreLift $ copyData (buf val) 0 len do coreLift $ copyData (buf val) 0 ilen
(buf chunk) (loc chunk) (buf chunk) (cast $ loc chunk)
put Bin (appended len chunk) put Bin (appended len chunk)
else do chunk' <- extendBinary len chunk else do chunk' <- extendBinary len chunk
coreLift $ copyData (buf val) 0 len coreLift $ copyData (buf val) 0 ilen
(buf chunk') (loc chunk') (buf chunk') (cast $ loc chunk')
put Bin (appended len chunk') put Bin (appended len chunk')
fromBuf b fromBuf b
= do len <- fromBuf b = do ilen <- fromBuf b
let len : Integer = cast ilen
chunk <- get Bin chunk <- get Bin
if toRead chunk >= len if toRead chunk >= len
then then
do Just newbuf <- coreLift $ newBuffer len do Just newbuf <- coreLift $ newBuffer ilen
| Nothing => corrupt "Binary" | Nothing => corrupt "Binary"
coreLift $ copyData (buf chunk) (loc chunk) len coreLift $ copyData (buf chunk) (cast $ loc chunk) ilen
newbuf 0 newbuf 0
put Bin (incLoc len chunk) put Bin (incLoc len chunk)
pure (MkBin newbuf 0 len len) pure (MkBin newbuf 0 len len)
@ -220,17 +224,17 @@ TTC Double where
= do chunk <- get Bin = do chunk <- get Bin
if avail chunk >= 8 if avail chunk >= 8
then then
do coreLift $ setDouble (buf chunk) (loc chunk) val do coreLift $ setDouble (buf chunk) (cast $ loc chunk) val
put Bin (appended 8 chunk) put Bin (appended 8 chunk)
else do chunk' <- extendBinary 8 chunk else do chunk' <- extendBinary 8 chunk
coreLift $ setDouble (buf chunk') (loc chunk') val coreLift $ setDouble (buf chunk') (cast $ loc chunk') val
put Bin (appended 8 chunk') put Bin (appended 8 chunk')
fromBuf b fromBuf b
= do chunk <- get Bin = do chunk <- get Bin
if toRead chunk >= 8 if toRead chunk >= 8
then then
do val <- coreLift $ getDouble (buf chunk) (loc chunk) do val <- coreLift $ getDouble (buf chunk) (cast $ loc chunk)
put Bin (incLoc 8 chunk) put Bin (incLoc 8 chunk)
pure val pure val
else throw (TTCError (EndOfBuffer "Double")) else throw (TTCError (EndOfBuffer "Double"))

22
src/Libraries/Utils/Binary.idr
View File

@ -15,32 +15,32 @@ public export
record Binary where record Binary where
constructor MkBin constructor MkBin
buf : Buffer buf : Buffer
loc : Int loc : Integer
size : Int -- Capacity size : Integer -- Capacity
used : Int -- Amount used used : Integer -- Amount used
export export
newBinary : Buffer -> Int -> Binary newBinary : Buffer -> Integer -> Binary
newBinary b s = MkBin b 0 s 0 newBinary b s = MkBin b 0 s 0
export %inline export
blockSize : Int blockSize : Int
blockSize = 655360 blockSize = 655360
export export
avail : Binary -> Int avail : Binary -> Integer
avail c = (size c - loc c) - 1 avail c = (size c - loc c) - 1
export export
toRead : Binary -> Int toRead : Binary -> Integer
toRead c = used c - loc c toRead c = used c - loc c
export export
appended : Int -> Binary -> Binary appended : Integer -> Binary -> Binary
appended i (MkBin b loc s used) = MkBin b (loc+i) s (used + i) appended i (MkBin b loc s used) = MkBin b (loc+i) s (used + i)
export export
incLoc : Int -> Binary -> Binary incLoc : Integer -> Binary -> Binary
incLoc i c = { loc $= (+i) } c incLoc i c = { loc $= (+i) } c
export export
@ -60,12 +60,13 @@ export
fromBuffer : Buffer -> IO Binary fromBuffer : Buffer -> IO Binary
fromBuffer buf fromBuffer buf
= do len <- rawSize buf = do len <- rawSize buf
let len = cast len
pure (MkBin buf 0 len len) pure (MkBin buf 0 len len)
export export
writeToFile : (fname : String) -> Binary -> IO (Either FileError ()) writeToFile : (fname : String) -> Binary -> IO (Either FileError ())
writeToFile fname c writeToFile fname c
= do Right ok <- writeBufferToFile fname (buf c) (used c) = do Right ok <- writeBufferToFile fname (buf c) (cast $ used c)
| Left (err, size) => pure (Left err) | Left (err, size) => pure (Left err)
pure (Right ok) pure (Right ok)
@ -75,4 +76,5 @@ readFromFile fname
= do Right b <- createBufferFromFile fname = do Right b <- createBufferFromFile fname
| Left err => pure (Left err) | Left err => pure (Left err)
bsize <- rawSize b bsize <- rawSize b
let bsize = cast bsize
pure (Right (MkBin b 0 bsize bsize)) pure (Right (MkBin b 0 bsize bsize))