feat(library/init/io): add IO.readTextFile

library/init/io.lean

@@ -100,6 +100,8 @@ open Fs
 
 @[extern 2 "lean_io_prim_put_str"]
 constant putStr (s: @& String) : IO Unit := default _
+@[extern 2 "lean_io_prim_read_text_file"]
+constant readTextFile (s : @& String) : IO String := default _
 @[extern 1 "lean_io_prim_get_line"]
 constant getLine : IO String := default _
 @[extern 4 "lean_io_prim_handle_mk"]
@@ -131,6 +133,9 @@ putStr ∘ toString $ s
 
 def println {α} [HasToString α] (s : α) : m Unit :=
 print s *> putStr "\n"
+
+def readTextFile : String → m String :=
+Prim.liftIO ∘ Prim.readTextFile
 end
 
 namespace Fs

src/runtime/io.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <iostream>
 #include <chrono>
+#include <fstream>
 #include <iomanip>
 #include <string>
 #include "runtime/object.h"
@@ -62,6 +63,17 @@ void io_mark_end_initialization() {
     g_initializing = false;
 }
 
+extern "C" obj_res lean_io_prim_read_text_file(obj_arg fname, obj_arg w) {
+    std::ifstream in(string_cstr(fname), std::ifstream::binary);
+    if (!in.good()) {
+        return set_io_error(w, "file not found");
+    } else {
+        std::stringstream buf;
+        buf << in.rdbuf();
+        return set_io_result(w, mk_string(buf.str()));
+    }
+}
+
 extern "C" obj_res lean_io_initializing(obj_arg r) {
     return set_io_result(r, box(g_initializing));
 }

tests/playground/file.lean

@@ -0,0 +1,3 @@
+def main : IO Unit :=
+do contents ← IO.readTextFile "file.lean";
+   IO.println contents