diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr index e02b374843..ca462b0bbe 100644 --- a/libs/prelude/Builtins.idr +++ b/libs/prelude/Builtins.idr @@ -197,7 +197,7 @@ export data ManagedPtr : Type export data CData : Type %extern prim__readFile : prim__WorldType -> Ptr -> String -%extern prim__readChars : prim__WorldType -> Int -> Ptr -> String +%extern prim__readChars : prim__WorldType -> Int -> Ptr -> (String, Int) %extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int %extern prim__vm : prim__WorldType -> Ptr diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr index 292472e7d8..7a02f6c3e7 100644 --- a/libs/prelude/IO.idr +++ b/libs/prelude/IO.idr @@ -135,7 +135,7 @@ prim_write s prim_fread : Ptr -> IO' l String prim_fread h = MkIO (\w => prim_io_pure (prim__readFile (world w) h)) -prim_freadChars : Int -> Ptr -> IO' l String +prim_freadChars : Int -> Ptr -> IO' l (String, Int) prim_freadChars len h = MkIO (\w => prim_io_pure (prim__readChars (world w) len h)) diff --git a/libs/prelude/Prelude/File.idr b/libs/prelude/Prelude/File.idr index 8ed2fbd73e..4f58eee33d 100644 --- a/libs/prelude/Prelude/File.idr +++ b/libs/prelude/Prelude/File.idr @@ -158,7 +158,7 @@ do_fread : Ptr -> IO' l String do_fread h = prim_fread h private -do_freadChars : Ptr -> Int -> IO' l String +do_freadChars : Ptr -> Int -> IO' l (String, Int) do_freadChars h len = prim_freadChars len h export @@ -202,11 +202,11 @@ fGetLine (FHandle h) = do ||| Read up to a number of characters from a file ||| @h a file handle which must be open for reading export -fGetChars : (h : File) -> (len : Int) -> IO (Either FileError String) -fGetChars (FHandle h) len = do str <- do_freadChars h len +fGetChars : (h : File) -> (len : Int) -> IO (Either FileError (String, Int)) +fGetChars (FHandle h) len = do (str, resultlen) <- do_freadChars h len if !(ferror (FHandle h)) then pure (Left FileReadError) - else pure (Right str) + else pure (Right (str, resultlen)) private @@ -265,15 +265,15 @@ readFile fn = do Right h <- openFile fn Read pure c where readFile' : File -> Int -> StringBuffer -> IO (Either FileError String) - readFile' h max contents = + readFile' h max sbuf = do x <- fEOF h if not x && max > 0 - then do Right l <- fGetChars h 1024000 + then do Right (chars, len) <- fGetChars h 1024000 | Left err => pure (Left err) - addToStringBuffer contents l + addToStringBuffer sbuf chars len assert_total $ - readFile' h (max - 1024000) contents - else do str <- getStringFromBuffer contents + readFile' h (max - 1024000) sbuf + else do str <- getStringFromBuffer sbuf pure (Right str) ||| Write a string to a file diff --git a/libs/prelude/Prelude/Strings.idr b/libs/prelude/Prelude/Strings.idr index 1c2ff93f7d..1ee2d39a65 100644 --- a/libs/prelude/Prelude/Strings.idr +++ b/libs/prelude/Prelude/Strings.idr @@ -53,10 +53,10 @@ newStringBuffer len = do ptr <- foreign FFI_C "idris_makeStringBuffer" ||| Append a string to the end of a string buffer export -addToStringBuffer : StringBuffer -> String -> IO () -addToStringBuffer (MkString ptr) str = - foreign FFI_C "idris_addToString" (Ptr -> String -> IO ()) - ptr str +addToStringBuffer : StringBuffer -> String -> (len : Int) -> IO () +addToStringBuffer (MkString ptr) str len = + foreign FFI_C "idris_addToString" (Ptr -> String -> Int -> IO ()) + ptr str len ||| Get the string from a string buffer. The buffer is invalid after ||| this. diff --git a/rts/idris_stdfgn.c b/rts/idris_stdfgn.c index 0fe9a1c106..eb9d5e7cdf 100644 --- a/rts/idris_stdfgn.c +++ b/rts/idris_stdfgn.c @@ -203,9 +203,8 @@ void* idris_makeStringBuffer(int len) { return sb; } -void idris_addToString(void* buffer, char* str) { +void idris_addToString(void* buffer, char* str, int len) { StrBuffer* sb = (StrBuffer*)buffer; - int len = strlen(str); memcpy(sb->string + sb->len, str, len+1); sb->len += len; diff --git a/rts/idris_stdfgn.h b/rts/idris_stdfgn.h index ab9e49d682..23a16e87e8 100644 --- a/rts/idris_stdfgn.h +++ b/rts/idris_stdfgn.h @@ -34,7 +34,7 @@ VAL idris_mkFileError(VM* vm); // Some machinery for building a large string without reallocating // Create a string with space for 'len' bytes void* idris_makeStringBuffer(int len); -void idris_addToString(void* buffer, char* str); +void idris_addToString(void* buffer, char* str, int len); VAL idris_getString(VM* vm, void* buffer); void* do_popen(const char* cmd, const char* mode); diff --git a/src/Idris/Core/Execute.hs b/src/Idris/Core/Execute.hs index 951ea3ac22..594ea0a5ce 100644 --- a/src/Idris/Core/Execute.hs +++ b/src/Idris/Core/Execute.hs @@ -438,14 +438,15 @@ execForeign env ctxt arity ty fn xs onfail "The argument to idris_makeStringBuffer should be an Int, but it was " ++ show len ++ ". Are all cases covered?" - | Just (FFun "idris_addToString" [(_, strBuf), (_, str)] _) <- foreignFromTT arity ty fn xs - = case (strBuf, str) of - (EStringBuf ref, EConstant (Str add)) -> + -- The len argument isn't actually consumed by the haskell interpreter + | Just (FFun "idris_addToString" [(_, strBuf), (_, str), (_, len)] _) <- foreignFromTT arity ty fn xs + = case (strBuf, str, len) of + (EStringBuf ref, EConstant (Str add), EConstant (Int len)) -> do execIO $ modifyIORef ref (++add) execApp env ctxt ioUnit (drop arity xs) _ -> execFail . Msg $ - "The arguments to idris_addToString should be a StringBuffer and a String, but were " ++ - show strBuf ++ " and " ++ show str ++ + "The arguments to idris_addToString should be a StringBuffer, a String, and an Int, but were " ++ + show strBuf ++ ", " ++ show str ++ " and " ++ show len ++ ". Are all cases covered?" | Just (FFun "idris_getString" [_, (_, str)] _) <- foreignFromTT arity ty fn xs = case str of @@ -537,7 +538,7 @@ getOp fn (_ : EHandle h : xs) getOp fn (_ : EConstant (I len) : EHandle h : xs) | fn == prc = Just (do contents <- execIO $ hGetChars h len - return (EConstant (Str contents)), xs) + return (EConstant (Str contents), EConstant (I (length contents))), xs) where hGetChars h 0 = return "" hGetChars h i = do eof <- hIsEOF h if eof then return "" else do