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

Make Buffer more primitive

Browse Source 
Meaning that the FFI is aware of it, so you can send arbitrary byte data
to foreign calls. Fixes #209

This means that we no longer need the hacky way of reading and writing
binary data via scheme, so can have a more general interface for reading
and writing buffer data in files.

It will also enable more interesting high level interfaces to binary
data, with C calls being used where necessary.

Note that the Buffer primitive are unsafe! They always have been, of
course... so perhaps (later) they should have 'unsafe' as part of their
name and better high level safe interfaces on top.

This requires updating the scheme to support Buffer as an FFI primitive,
but shouldn't affect Idris2-boot which loads buffers its own way.
This commit is contained in:
Edwin Brady 2020-06-11 12:42:52 +01:00
parent d71bfef73f
commit 0a246af449
15 changed files with 10053 additions and 9989 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9895
bootstrap/idris2_app/idris2.rkt
View File

File diff suppressed because one or more lines are too long

9894
bootstrap/idris2_app/idris2.ss
View File

File diff suppressed because one or more lines are too long

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

@ -3,6 +3,13 @@ module Data.Buffer
import System.Directory
import System.File
-- 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!
-- They are used in the Idris compiler itself for reading/writing checked
-- files.
-- This is known to the compiler, so maybe ought to be moved to Builtin
export
data Buffer : Type where [external]
@ -199,50 +206,58 @@ copyData : (src : Buffer) -> (start, len : Int) ->
copyData src start len dest loc
= primIO (prim__copyData src start len dest loc)
-- %foreign "scheme:blodwen-readbuffer-bytes"
-- prim__readBufferBytes : FilePtr -> AnyPtr -> Int -> Int -> PrimIO Int
--
-- export
-- readBufferFromFile : BinaryFile -> Buffer -> (maxbytes : Int) ->
-- IO (Either FileError Buffer)
-- readBufferFromFile (FHandle h) (MkBuffer buf size loc) max
-- = do read <- primIO (prim__readBufferBytes h buf loc max)
-- if read >= 0
-- then pure (Right (MkBuffer buf size (loc + read)))
-- else pure (Left FileReadError)
%foreign "C:idris2_readBufferData,libidris2_support"
prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
%foreign "C:idris2_writeBufferData,libidris2_support"
prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
%foreign "scheme:blodwen-read-bytevec"
prim__readBufferFromFile : String -> String -> PrimIO Buffer
export
readBufferData : File -> Buffer ->
(loc : Int) -> -- position in buffer to start adding
(maxbytes : Int) -> -- maximums size to read, which must not
-- exceed buffer length
IO (Either FileError ())
readBufferData (FHandle h) buf loc max
= do read <- primIO (prim__readBufferData h buf loc max)
if read >= 0
then pure (Right ())
else pure (Left FileReadError)
%foreign "scheme:blodwen-isbytevec"
prim__isBuffer : Buffer -> Int
export
writeBufferData : File -> Buffer ->
(loc : Int) -> -- position in buffer to write from
(maxbytes : Int) -> -- maximums size to write, which must not
-- exceed buffer length
IO (Either FileError ())
writeBufferData (FHandle h) buf loc max
= do written <- primIO (prim__writeBufferData h buf loc max)
if written >= 0
then pure (Right ())
else pure (Left FileWriteError)
export
writeBufferToFile : String -> Buffer -> Int -> IO (Either FileError ())
writeBufferToFile fn buf max
= do Right f <- openFile fn WriteTruncate
| Left err => pure (Left err)
Right ok <- writeBufferData f buf 0 max
| Left err => pure (Left err)
closeFile f
pure (Right ok)
-- Create a new buffer by reading all the contents from the given file
-- Fails if no bytes can be read or buffer can't be created
export
createBufferFromFile : String -> IO (Either FileError Buffer)
createBufferFromFile fn
= do Just cwd <- currentDir
| Nothing => pure (Left FileReadError)
buf <- primIO (prim__readBufferFromFile cwd fn)
if prim__isBuffer buf /= 0
then pure (Left FileReadError)
else do let sz = prim__bufferSize buf
pure (Right buf)
%foreign "scheme:blodwen-write-bytevec"
prim__writeBuffer : String -> String -> Buffer -> Int -> PrimIO Int
export
writeBufferToFile : String -> Buffer -> (maxbytes : Int) ->
IO (Either FileError ())
writeBufferToFile fn buf max
= do Just cwd <- currentDir
| Nothing => pure (Left FileReadError)
res <- primIO (prim__writeBuffer cwd fn buf max)
if res /= 0
then pure (Left FileWriteError)
else pure (Right ())
= do Right f <- openFile fn Read
| Left err => pure (Left err)
Right size <- fileSize f
| Left err => pure (Left err)
Just buf <- newBuffer size
| Nothing => pure (Left FileReadError)
Right ok <- readBufferData f buf 0 size
| Left err => pure (Left err)
closeFile f
pure (Right buf)
export
resizeBuffer : Buffer -> Int -> IO (Maybe Buffer)

3
src/Compiler/CompileExpr.idr
View File

@ -462,6 +462,7 @@ data NArgs : Type where
NUnit : NArgs
NPtr : NArgs
NGCPtr : NArgs
NBuffer : NArgs
NIORes : Closure [] -> NArgs
getPArgs : Defs -> Closure [] -> Core (String, Closure [])
@ -494,6 +495,7 @@ getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr
getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr
getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr
getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr
getNArgs defs (NS _ (UN "Buffer")) [] = pure NBuffer
getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit
getNArgs defs (NS _ (UN "Struct")) [n, args]
= do NPrimVal _ (Str n') <- evalClosure defs n
@ -540,6 +542,7 @@ nfToCFType _ s (NTCon fc n_in _ _ args)
NUnit => pure CFUnit
NPtr => pure CFPtr
NGCPtr => pure CFGCPtr
NBuffer => pure CFBuffer
NIORes uarg =>
do narg <- evalClosure defs uarg
carg <- nfToCFType fc s narg

8
src/Compiler/Scheme/Chez.idr
View File

@ -109,7 +109,8 @@ mutual
tySpec (NmCon fc (UN "Char") _ []) = pure "char"
tySpec (NmCon fc (NS _ n) _ [_])
= cond [(n == UN "Ptr", pure "void*"),
(n == UN "GCPtr", pure "void*")]
(n == UN "GCPtr", pure "void*"),
(n == UN "Buffer", pure "u8*")]
(throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
tySpec (NmCon fc (NS _ n) _ [])
= cond [(n == UN "Unit", pure "void"),
@ -182,6 +183,7 @@ cftySpec fc CFDouble = pure "double"
cftySpec fc CFChar = pure "char"
cftySpec fc CFPtr = pure "void*"
cftySpec fc CFGCPtr = pure "void*"
cftySpec fc CFBuffer = pure "u8*"
cftySpec fc (CFFun s t) = pure "void*"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
@ -196,6 +198,10 @@ cCall appdir fc cfn clib args (CFIORes CFGCPtr)
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args CFGCPtr
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args (CFIORes CFBuffer)
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args CFBuffer
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args ret
= do loaded <- get Loaded
lib <- if clib `elem` loaded

5
src/Compiler/Scheme/Racket.idr
View File

@ -122,6 +122,7 @@ cftySpec fc CFDouble = pure "_double"
cftySpec fc CFChar = pure "_int8"
cftySpec fc CFPtr = pure "_pointer"
cftySpec fc CFGCPtr = pure "_pointer"
cftySpec fc CFBuffer = pure "_bytes"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "_" ++ n ++ "-pointer"
cftySpec fc (CFFun s t) = funTySpec [s] t
@ -172,6 +173,10 @@ cCall appdir fc cfn clib args (CFIORes CFGCPtr)
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args CFGCPtr
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args (CFIORes CFBuffer)
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args CFBuffer
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn libspec args ret
= do loaded <- get Loaded
bound <- get Done

18
src/Core/Binary.idr
View File

@ -246,10 +246,6 @@ getSaveDefs (n :: ns) acc defs
b <- get Bin
getSaveDefs ns ((fullname gdef, b) :: acc) defs
freeDefBuffer : (Name, Binary) -> Core ()
freeDefBuffer (n, b)
= coreLift $ freeBuffer (buf b)
-- Write out the things in the context which have been defined in the
-- current source file
export
@ -283,8 +279,6 @@ writeToTTC extradata fname
Right ok <- coreLift $ writeToFile fname !(get Bin)
| Left err => throw (InternalError (fname ++ ": " ++ show err))
traverse_ freeDefBuffer gdefs
freeBinary bin
pure ()
addGlobalDef : {auto c : Ref Ctxt Defs} ->
@ -436,8 +430,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
-- Otherwise, add the data
let ex = extraData ttc
if ((modNS, importAs) `elem` map getNSas (allImported defs))
then do coreLift $ freeBuffer (buf buffer)
pure (Just (ex, ifaceHash ttc, imported ttc))
then pure (Just (ex, ifaceHash ttc, imported ttc))
else do
traverse (addGlobalDef modNS as) (context ttc)
traverse_ addUserHole (userHoles ttc)
@ -461,7 +454,6 @@ readFromTTC nestedns loc reexp fname modNS importAs
-- ttc
ust <- get UST
put UST (record { nextName = nextVar ttc } ust)
coreLift $ freeBuffer (buf buffer)
pure (Just (ex, ifaceHash ttc, imported ttc))
getImportHashes : String -> Ref Bin Binary ->
@ -490,10 +482,8 @@ readIFaceHash fname
| Left err => pure 0
b <- newRef Bin buffer
catch (do res <- getHash fname b
coreLift $ freeBuffer (buf buffer)
pure res)
(\err => do coreLift $ freeBuffer (buf buffer)
pure 0)
(\err => pure 0)
export
readImportHashes : (fname : String) -> -- file containing the module
@ -503,7 +493,5 @@ readImportHashes fname
| Left err => pure []
b <- newRef Bin buffer
catch (do res <- getImportHashes fname b
coreLift $ freeBuffer (buf buffer)
pure res)
(\err => do coreLift $ freeBuffer (buf buffer)
pure [])
(\err => pure [])

2
src/Core/CompileExpr.idr
View File

@ -117,6 +117,7 @@ data CFType : Type where
CFChar : CFType
CFPtr : CFType
CFGCPtr : CFType
CFBuffer : CFType
CFWorld : CFType
CFFun : CFType -> CFType -> CFType
CFIORes : CFType -> CFType
@ -298,6 +299,7 @@ Show CFType where
show CFChar = "Char"
show CFPtr = "Ptr"
show CFGCPtr = "GCPtr"
show CFBuffer = "Buffer"
show CFWorld = "%World"
show (CFFun s t) = show s ++ " -> " ++ show t
show (CFIORes t) = "IORes " ++ show t

2
src/Core/TTC.idr
View File

@ -689,6 +689,7 @@ TTC CFType where
toBuf b (CFStruct n a) = do tag 10; toBuf b n; toBuf b a
toBuf b (CFUser n a) = do tag 11; toBuf b n; toBuf b a
toBuf b CFGCPtr = tag 12
toBuf b CFBuffer = tag 13
fromBuf b
= case !getTag of
@ -705,6 +706,7 @@ TTC CFType where
10 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
11 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
12 => pure CFGCPtr
13 => pure CFBuffer
_ => corrupt "CFType"
export

6
src/Utils/Binary.idr
View File

@ -105,12 +105,6 @@ initBinaryS s
| Nothing => throw (InternalError "Buffer creation failed")
newRef Bin (newBinary buf s)
export
freeBinary : Ref Bin Binary -> Core ()
freeBinary b
= do b <- get Bin
coreLift $ freeBuffer (buf b)
extendBinary : Int -> Binary -> Core Binary
extendBinary need (MkBin buf l s u)
= do let newsize = s * 2

44
support/c/idris_buffer.c
View File

@ -16,7 +16,7 @@ void* idris2_newBuffer(int bytes) {
}
buf->size = bytes;
memset(buf->data, 0, bytes);
// memset(buf->data, 0, bytes);
return (void*)buf;
}
@ -142,46 +142,30 @@ void* idris2_readBufferFromFile(char* fn) {
Buffer* buf = malloc(size);
buf->size = len;
fread((buf->data), sizeof(uint8_t), (size_t)len, f);
size_t read = fread((buf->data), sizeof(uint8_t), (size_t)len, f);
fclose(f);
return buf;
if (read >= 0) {
return buf;
} else {
free(buf);
return 0;
}
}
int idris2_writeBufferToFile(char* fn, void* buffer, int max) {
Buffer* b = buffer;
FILE* f = fopen(fn, "w");
if (f == NULL) { return 0; }
if (f == NULL) { return -1; }
fwrite((b->data), sizeof(uint8_t), max, f);
fclose(f);
return -1;
return 0;
}
// To be added when the file API has moved to the C support libs
/*
int idris2_readBuffer(FILE* h, void* buffer, int loc, int max) {
Buffer* b = buffer;
size_t len;
if (loc >= 0 && loc < b->size) {
if (loc + max > b->size) {
max = b->size - loc;
}
len = fread((b->data)+loc, sizeof(uint8_t), (size_t)max, h);
return len;
} else {
return 0;
}
int idris2_readBufferData(FILE* h, char* buffer, int loc, int max) {
return fread(buffer+loc, sizeof(uint8_t), (size_t)max, h);
}
void idris2_writeBuffer(FILE* h, void* buffer, int loc, int len) {
Buffer* b = buffer;
if (loc >= 0 && loc < b->size) {
if (loc + len > b->size) {
len = b->size - loc;
}
fwrite((b->data)+loc, sizeof(uint8_t), len, h);
}
int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len) {
return fwrite(buffer+loc, sizeof(uint8_t), len, h);
}
*/

6
support/c/idris_buffer.h
View File

@ -21,9 +21,9 @@ void idris2_copyBuffer(void* from, int start, int len,
void* idris2_readBufferFromFile(char* fn);
int idris2_writeBufferToFile(char* fn, void* buffer, int max);
// To be added when the file API has moved to the C support libs
// int idris2_readBuffer(FILE* h, void* buffer, int loc, int max);
// void idris2_writeBuffer(FILE* h, void* buffer, int loc, int len);
// Reading and writing the raw data, to the pointer in the buffer
int idris2_readBufferData(FILE* h, char* buffer, int loc, int max);
int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len);
int idris2_getBufferByte(void* buffer, int loc);
int idris2_getBufferInt(void* buffer, int loc);

3
support/c/idris_directory.c
View File

@ -8,8 +8,7 @@
char* idris2_currentDirectory() {
char* cwd = malloc(1024); // probably ought to deal with the unlikely event of this being too small
getcwd(cwd, 1024);
return cwd; // freed by RTS
return getcwd(cwd, 1024); // Freed by RTS
}
int idris2_changeDir(char* dir) {

28
support/chez/support.ss
View File

@ -160,34 +160,6 @@
(define (blodwen-buffer-copydata buf start len dest loc)
(bytevector-copy! buf start dest loc len))
; 'dir' is only needed in Racket
(define (blodwen-read-bytevec curdir fname)
(guard
(x (#t #f))
(let* [(h (open-file-input-port fname
(file-options)
(buffer-mode line) #f))
(vec (get-bytevector-all h))]
(begin (close-port h)
vec))))
(define (blodwen-isbytevec v)
(if (bytevector? v)
0
-1))
; 'dir' is only needed in Racket
(define (blodwen-write-bytevec curdir fname vec max)
(guard
(x (#t -1))
(let* [(h (open-file-output-port fname (file-options no-fail)
(buffer-mode line) #f))]
(begin (put-bytevector h vec 0 max)
(close-port h)
0))))
;; Threads
(define blodwen-thread-data (make-thread-parameter #f))

37
support/racket/support.rkt
View File

@ -155,43 +155,6 @@
(define (blodwen-buffer-copydata buf start len dest loc)
(bytevector-copy! buf start dest loc len))
; The 'dir' argument is an annoying hack. Racket appears to have a different
; notion of current directory than the OS, so we pass what we think it is so
; that racket can change to it
(define (blodwen-read-bytevec dir fname)
(let ((origdir (current-directory)))
(begin
(current-directory dir)
(with-handlers
([(lambda (x) #t) (lambda (exn) (current-directory origdir) #f)])
(let* [(h (open-file-input-port fname
(file-options)
(buffer-mode line) #f))
(vec (get-bytevector-all h))]
(begin (close-port h)
(current-directory origdir)
vec))))))
(define (blodwen-isbytevec v)
(if (bytevector? v)
0
-1))
; See blodwen-read-bytevec for what 'dir' is for
(define (blodwen-write-bytevec dir fname vec max)
(let ((origdir (current-directory)))
(begin
(current-directory dir)
(with-handlers
([(lambda (x) #t) (lambda (exn) (current-directory origdir) -1)])
(let* [(h (open-file-output-port fname (file-options no-fail)
(buffer-mode line) #f))]
(begin (put-bytevector h vec 0 max)
(close-port h)
(current-directory origdir)
0))))))
;; Threads
(define blodwen-thread-data (make-thread-cell #f))