chore: Revert "feat: Revamp file reading and writing" (#4948)

Reverts #4906

src/Init/System/IO.lean

@@ -470,23 +470,31 @@ def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α :=
 def Handle.putStrLn (h : Handle) (s : String) : IO Unit :=
   h.putStr (s.push '\n')
 
-partial def Handle.readBinToEndInto (h : Handle) (buf : ByteArray) : IO ByteArray := do
+partial def Handle.readBinToEnd (h : Handle) : IO ByteArray := do
   let rec loop (acc : ByteArray) : IO ByteArray := do
     let buf ← h.read 1024
     if buf.isEmpty then
       return acc
     else
       loop (acc ++ buf)
-  loop buf
+  loop ByteArray.empty
 
-partial def Handle.readBinToEnd (h : Handle) : IO ByteArray := do
-  h.readBinToEndInto .empty
+partial def Handle.readToEnd (h : Handle) : IO String := do
+  let rec loop (s : String) := do
+    let line ← h.getLine
+    if line.isEmpty then
+      return s
+    else
+      loop (s ++ line)
+  loop ""
 
-def Handle.readToEnd (h : Handle) : IO String := do
-  let data ← h.readBinToEnd
-  match String.fromUTF8? data with
-  | some s => return s
-  | none => throw <| .userError s!"Tried to read from handle containing non UTF-8 data."
+def readBinFile (fname : FilePath) : IO ByteArray := do
+  let h ← Handle.mk fname Mode.read
+  h.readBinToEnd
+
+def readFile (fname : FilePath) : IO String := do
+  let h ← Handle.mk fname Mode.read
+  h.readToEnd
 
 partial def lines (fname : FilePath) : IO (Array String) := do
   let h ← Handle.mk fname Mode.read
@@ -592,28 +600,6 @@ end System.FilePath
 
 namespace IO
 
-namespace FS
-
-def readBinFile (fname : FilePath) : IO ByteArray := do
-  -- Requires metadata so defined after metadata
-  let mdata ← fname.metadata
-  let size := mdata.byteSize.toUSize
-  let handle ← IO.FS.Handle.mk fname .read
-  let buf ←
-    if size > 0 then
-      handle.read mdata.byteSize.toUSize
-    else
-      pure <| ByteArray.mkEmpty 0
-  handle.readBinToEndInto buf
-
-def readFile (fname : FilePath) : IO String := do
-  let data ← readBinFile fname
-  match String.fromUTF8? data with
-  | some s => return s
-  | none => throw <| .userError s!"Tried to read file '{fname}' containing non UTF-8 data."
-
-end FS
-
 def withStdin [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do
   let prev ← setStdin h
   try x finally discard <| setStdin prev

src/runtime/io.cpp

@@ -485,30 +485,43 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg
     }
 }
 
-/* Handle.getLine : (@& Handle) → IO Unit */
+/*
+  Handle.getLine : (@& Handle) → IO Unit
+  The line returned by `lean_io_prim_handle_get_line`
+  is truncated at the first '\0' character and the
+  rest of the line is discarded. */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) {
     FILE * fp = io_get_handle(h);
-    char* buf = NULL;
-    size_t n = 0;
-    ssize_t read = getline(&buf, &n, fp);
-    if (read != -1) {
-        obj_res ret = io_result_mk_ok(mk_string_from_bytes(buf, read));
-        free(buf);
-        return ret;
-    } else if (std::feof(fp)) {
-        clearerr(fp);
-        return io_result_mk_ok(mk_string(""));
-    } else {
-        return io_result_mk_error(decode_io_error(errno, nullptr));
+    const int buf_sz = 64;
+    char buf_str[buf_sz]; // NOLINT
+    std::string result;
+    bool first = true;
+    while (true) {
+        char * out = std::fgets(buf_str, buf_sz, fp);
+        if (out != nullptr) {
+            if (strlen(buf_str) < buf_sz-1 || buf_str[buf_sz-2] == '\n') {
+                if (first) {
+                    return io_result_mk_ok(mk_string(out));
+                } else {
+                    result.append(out);
+                    return io_result_mk_ok(mk_string(result));
+                }
+            }
+            result.append(out);
+        } else if (std::feof(fp)) {
+            clearerr(fp);
+            return io_result_mk_ok(mk_string(result));
+        } else {
+            return io_result_mk_error(decode_io_error(errno, nullptr));
+        }
+        first = false;
     }
 }
 
 /* Handle.putStr : (@& Handle) → (@& String) → IO Unit */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg /* w */) {
     FILE * fp = io_get_handle(h);
-    usize n = lean_string_size(s) - 1; // - 1 to ignore the terminal NULL byte.
-    usize m = std::fwrite(lean_string_cstr(s), 1, n, fp);
-    if (m == n) {
+    if (std::fputs(lean_string_cstr(s), fp) != EOF) {
         return io_result_mk_ok(box(0));
     } else {
         return io_result_mk_error(decode_io_error(errno, nullptr));

src/runtime/object.h

@@ -238,7 +238,6 @@ inline size_t string_capacity(object * o) { return lean_string_capacity(o); }
 inline uint32 char_default_value() { return lean_char_default_value(); }
 inline obj_res alloc_string(size_t size, size_t capacity, size_t len) { return lean_alloc_string(size, capacity, len); }
 inline obj_res mk_string(char const * s) { return lean_mk_string(s); }
-inline obj_res mk_string_from_bytes(char const * s, size_t sz) { return lean_mk_string_from_bytes(s, sz); }
 LEAN_EXPORT obj_res mk_ascii_string_unchecked(std::string const & s);
 LEAN_EXPORT obj_res mk_string(std::string const & s);
 LEAN_EXPORT std::string string_to_std(b_obj_arg o);