WIP: making readFile work correctly with binary data when compiled

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

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))
 

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

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.

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;

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);

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