From 79545f55c098b71208bef41f3ba405aea20ea4a7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Jul 2019 17:31:31 -0700
Subject: [PATCH] feat(library/init/io): add `IO.readTextFile`

---
 library/init/io.lean       |  5 +++++
 src/runtime/io.cpp         | 12 ++++++++++++
 tests/playground/file.lean |  3 +++
 3 files changed, 20 insertions(+)
 create mode 100644 tests/playground/file.lean

diff --git a/library/init/io.lean b/library/init/io.lean
index 5efde885d7..e2594c3e9d 100644
--- a/library/init/io.lean
+++ b/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
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 9467cbf340..7ae096c380 100644
--- a/src/runtime/io.cpp
+++ b/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));
 }
diff --git a/tests/playground/file.lean b/tests/playground/file.lean
new file mode 100644
index 0000000000..c4154c9d83
--- /dev/null
+++ b/tests/playground/file.lean
@@ -0,0 +1,3 @@
+def main : IO Unit :=
+do contents ← IO.readTextFile "file.lean";
+   IO.println contents