From 098b0edbcbe96eaab241f13665cb9acdf268a64e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Mar 2020 15:56:29 -0700
Subject: [PATCH] chore: remove dead code

---
 src/Init/Lean/Parser/Module.lean |  2 +-
 src/Init/System/IO.lean          |  5 -----
 src/runtime/io.cpp               | 16 ----------------
 3 files changed, 1 insertion(+), 22 deletions(-)

diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean
index 439db6474d..d8924f4180 100644
--- a/src/Init/Lean/Parser/Module.lean
+++ b/src/Init/Lean/Parser/Module.lean
@@ -121,7 +121,7 @@ partial def parseFileAux (env : Environment) (inputCtx : InputContext) : ModuleP
 
 def parseFile (env : Environment) (fname : String) : IO Syntax := do
 fname ← IO.realPath fname;
-contents ← IO.readTextFile fname;
+contents ← IO.FS.readFile fname;
 let inputCtx := mkInputContext contents fname;
 let (stx, state, messages) := parseHeader env inputCtx;
 parseFileAux env inputCtx state messages #[stx]
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 1e41b6292d..f52d4e3dc9 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -107,10 +107,6 @@ mode ++ bin
 
 @[extern "lean_io_prim_put_str"]
 constant putStr (s: @& String) : IO Unit := arbitrary _
-@[extern "lean_io_prim_read_text_file"]
-constant readTextFile (s : @& String) : IO String := arbitrary _
-@[extern "lean_io_prim_get_line"]
-constant getLine : IO String := arbitrary _
 @[extern "lean_io_prim_handle_mk"]
 constant Handle.mk (s : @& String) (mode : @& String) : IO Handle := arbitrary _
 @[extern "lean_io_prim_handle_is_eof"]
@@ -156,7 +152,6 @@ Prim.liftIO ∘ Prim.putStr
 
 def print {α} [HasToString α] (s : α) : m Unit := putStr ∘ toString $ s
 def println {α} [HasToString α] (s : α) : m Unit := print s *> putStr "\n"
-def readTextFile : String → m String := Prim.liftIO ∘ Prim.readTextFile
 def getEnv : String → m (Option String) := Prim.liftIO ∘ Prim.getEnv
 def realPath : String → m String := Prim.liftIO ∘ Prim.realPath
 def isDir : String → m Bool := Prim.liftIO ∘ Prim.isDir
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index acaa4a2ddd..8a25a4e425 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -104,17 +104,6 @@ static obj_res mk_file_not_found_error(b_obj_arg fname) {
     return set_io_error(lean_mk_io_error_no_file_or_directory(fname, errnum, details));
 }
 
-extern "C" obj_res lean_io_prim_read_text_file(b_obj_arg fname, obj_arg) {
-    std::ifstream in(string_cstr(fname), std::ifstream::binary);
-    if (!in.good()) {
-        return mk_file_not_found_error(fname);
-    } else {
-        std::stringstream buf;
-        buf << in.rdbuf();
-        return set_io_result(mk_string(buf.str()));
-    }
-}
-
 extern "C" obj_res lean_io_initializing(obj_arg) {
     return set_io_result(box(g_initializing));
 }
@@ -124,11 +113,6 @@ extern "C" obj_res lean_io_prim_put_str(b_obj_arg s, obj_arg) {
     return set_io_result(box(0));
 }
 
-extern "C" obj_res lean_io_prim_get_line(obj_arg /* w */) {
-    // not implemented yet
-    lean_unreachable();
-}
-
 static lean_external_class * g_io_handle_external_class = nullptr;
 
 static void io_handle_finalizer(void * h) {