edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity

Update Buffer+File libraries

Browse Source 
Adding primitives - it's useful to distinguish between 32 bit and 64 bit
integers when writing to buffers.
This commit is contained in:
Edwin Brady 2020-05-19 16:06:05 +01:00
parent ba9f14a18c
commit c197c0f777
5 changed files with 49 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -46,6 +46,22 @@ getByte : Buffer -> (loc : Int) -> IO Int
getByte buf loc
= primIO (prim__getByte buf loc)
%foreign "scheme:blodwen-buffer-setint32"
prim__setInt32 : Buffer -> Int -> Int -> PrimIO ()
export
setInt32 : Buffer -> (loc : Int) -> (val : Int) -> IO ()
setInt32 buf loc val
= primIO (prim__setInt32 buf loc val)
%foreign "scheme:blodwen-buffer-getint32"
prim__getInt32 : Buffer -> Int -> PrimIO Int
export
getInt32 : Buffer -> (loc : Int) -> IO Int
getInt32 buf loc
= primIO (prim__getInt32 buf loc)
%foreign "scheme:blodwen-buffer-setint"
prim__setInt : Buffer -> Int -> Int -> PrimIO ()

18
libs/base/System/File.idr
View File

@ -23,7 +23,6 @@ prim__close : FilePtr -> PrimIO ()
%foreign support "idris2_fileError"
prim_error : FilePtr -> PrimIO Int
%foreign support "idris2_fileErrno"
prim_fileErrno : PrimIO Int
@ -31,6 +30,8 @@ prim_fileErrno : PrimIO Int
prim__readLine : FilePtr -> PrimIO (Ptr String)
%foreign support "idris2_readChars"
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
%foreign support "fgetc"
prim__readChar : FilePtr -> PrimIO Char
%foreign support "idris2_writeLine"
prim__writeLine : FilePtr -> String -> PrimIO Int
%foreign support "idris2_eof"
@ -129,6 +130,12 @@ export
closeFile : File -> IO ()
closeFile (FHandle f) = primIO (prim__close f)
export
fileError : File -> IO Bool
fileError (FHandle f)
= do x <- primIO $ prim_error f
pure (x /= 0)
export
fGetLine : (h : File) -> IO (Either FileError String)
fGetLine (FHandle f)
@ -145,6 +152,15 @@ fGetChars (FHandle f) max
then returnError
else ok (prim__getString res)
export
fGetChar : (h : File) -> IO (Either FileError Char)
fGetChar (FHandle h)
= do c <- primIO (prim__readChar h)
ferr <- primIO (prim_error h)
if (ferr /= 0)
then returnError
else ok c
export
fPutStr : (h : File) -> String -> IO (Either FileError ())
fPutStr (FHandle f) str

8
support/chez/support.ss
View File

@ -97,9 +97,15 @@
(bytevector-u8-ref buf loc))
(define (blodwen-buffer-setint buf loc val)
(bytevector-s32-set! buf loc val (native-endianness)))
(bytevector-s64-set! buf loc val (native-endianness)))
(define (blodwen-buffer-getint buf loc)
(bytevector-s64-ref buf loc (native-endianness)))
(define (blodwen-buffer-setint32 buf loc val)
(bytevector-s32-set! buf loc val (native-endianness)))
(define (blodwen-buffer-getint32 buf loc)
(bytevector-s32-ref buf loc (native-endianness)))
(define (blodwen-buffer-setdouble buf loc val)

8
support/racket/support.rkt
View File

@ -85,9 +85,15 @@
(bytevector-u8-ref buf loc))
(define (blodwen-buffer-setint buf loc val)
(bytevector-s32-set! buf loc val (native-endianness)))
(bytevector-s64-set! buf loc val (native-endianness)))
(define (blodwen-buffer-getint buf loc)
(bytevector-s64-ref buf loc (native-endianness)))
(define (blodwen-buffer-setint32 buf loc val)
(bytevector-s32-set! buf loc val (native-endianness)))
(define (blodwen-buffer-getint32 buf loc)
(bytevector-s32-ref buf loc (native-endianness)))
(define (blodwen-buffer-setdouble buf loc val)

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

@ -8,9 +8,9 @@ main
s <- rawSize buf
printLn s
setInt buf 1 94
setInt32 buf 1 94
setString buf 5 "AAAA"
val <- getInt buf 1
val <- getInt32 buf 1
printLn val
setDouble buf 10 94.42