Revert "feat: add std streams"

This reverts commit 7575a32035.

src/Init/System/IO.lean

@@ -82,22 +82,11 @@ pure (fn ())
 inductive FS.Mode
 | read | write | readWrite | append
 
-constant FS.HandleDecl : PointedType := arbitrary _
-
-def FS.Handle : Type := FS.HandleDecl.1
-
-instance FS.HandleInh : Inhabited FS.Handle := ⟨ FS.HandleDecl.2 ⟩
+constant FS.Handle : Type := Unit
 
 namespace Prim
 open FS
 
-@[extern "lean_get_stdin"]
-constant getStdin  : IO FS.Handle := arbitrary _
-@[extern "lean_get_stderr"]
-constant getStderr : IO FS.Handle := arbitrary _
-@[extern "lean_get_stdout"]
-constant getStdout : IO FS.Handle := arbitrary _
-
 @[specialize] partial def iterate {α β : Type} : α → (α → IO (Sum α β)) → IO β
 | a, f => do
   v ← f a;
@@ -116,6 +105,12 @@ let mode :=
 let bin := if b then "b" else "t";
 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"]
@@ -153,6 +148,27 @@ constant appPath : IO String := arbitrary _
 monadLift x
 end Prim
 
+section
+variables {m : Type → Type} [Monad m] [MonadIO m]
+
+private def putStr : String → m Unit :=
+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
+def fileExists : String → m Bool := Prim.liftIO ∘ Prim.fileExists
+def appPath : m String := Prim.liftIO Prim.appPath
+
+def appDir : m String := do
+p ← appPath;
+realPath (System.FilePath.dirName p)
+
+end
+
 namespace FS
 variables {m : Type → Type} [Monad m] [MonadIO m]
 
@@ -192,43 +208,16 @@ Prim.liftIO $ Prim.iterate "" $ fun r => do
     c ← h.getLine;
     pure $ Sum.inl (r ++ c) -- continue
 
-end FS
-
-section
-variables {m : Type → Type} [Monad m] [MonadIO m]
-
-def getStderr : m FS.Handle :=
-Prim.liftIO Prim.getStderr
-
-def getStdout : m FS.Handle :=
-Prim.liftIO Prim.getStdout
-
-def getStdin : m FS.Handle :=
-Prim.liftIO Prim.getStdin
-
-private def putStr (s : String) : m Unit := do
-out ← getStdout;
-out.putStr s
-
-def print {α} [HasToString α] (s : α) : m Unit := putStr ∘ toString $ s
-def println {α} [HasToString α] (s : α) : m Unit := print s *> putStr "\n"
-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
-def fileExists : String → m Bool := Prim.liftIO ∘ Prim.fileExists
-def appPath : m String := Prim.liftIO Prim.appPath
-
-def appDir : m String := do
-p ← appPath;
-realPath (System.FilePath.dirName p)
-
 def readFile (fname : String) (bin := false) : m String := do
-IO.println fname;
-h ← FS.Handle.mk fname Mode.read bin;
+h ← Handle.mk fname Mode.read bin;
 r ← h.readToEnd;
 pure r
 
-end
+end FS
+
+-- constant stdin : IO FS.Handle
+-- constant stderr : IO FS.Handle
+-- constant stdout : IO FS.Handle
 
 /-
 namespace Proc
@@ -322,7 +311,7 @@ class HasEval (α : Type u) :=
 (eval : α → IO Unit)
 
 instance HasRepr.HasEval {α : Type u} [HasRepr α] : HasEval α :=
-⟨fun a => IO.print (repr a)⟩
+⟨fun a => IO.println (repr a)⟩
 
 instance IO.HasEval {α : Type} [HasEval α] : HasEval (IO α) :=
 ⟨fun x => do a ← x; HasEval.eval a⟩

src/runtime/io.cpp

@@ -123,6 +123,15 @@ extern "C" obj_res lean_io_initializing(obj_arg) {
     return set_io_result(box(g_initializing));
 }
 
+extern "C" obj_res lean_io_prim_put_str(b_obj_arg s, obj_arg) {
+    std::cout << string_to_std(s); // TODO(Leo): use out handle
+    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;
 
@@ -137,25 +146,6 @@ static lean_object * io_wrap_handle(FILE *hfile) {
     return lean_alloc_external(g_io_handle_external_class, hfile);
 }
 
-static object * g_handle_stdout = nullptr;
-static object * g_handle_stderr = nullptr;
-static object * g_handle_stdin  = nullptr;
-
-/* constant stdin  : IO FS.Handle := arbitrary _ */
-extern "C" obj_res lean_get_stdin(obj_arg /* w */) {
-    return set_io_result(g_handle_stdin);
-}
-
-/* stderr  : IO FS.Handle */
-extern "C" obj_res lean_get_stderr(obj_arg /* w */) {
-    return set_io_result(g_handle_stderr);
-}
-
-/* stdout : IO FS.Handle */
-extern "C" obj_res lean_get_stdout(obj_arg /* w */) {
-    return set_io_result(g_handle_stdout);
-}
-
 static FILE * io_get_handle(lean_object * hfile) {
     return static_cast<FILE *>(lean_get_external_data(hfile));
 }
@@ -624,14 +614,8 @@ extern "C" obj_res lean_io_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
 
 void initialize_io() {
     g_io_error_nullptr_read = mk_string("null reference read");
-    g_io_handle_external_class = lean_register_external_class(io_handle_finalizer, io_handle_foreach);
-    g_handle_stdout = io_wrap_handle(stdout);
-    g_handle_stderr = io_wrap_handle(stderr);
-    g_handle_stdin  = io_wrap_handle(stdin);
-    mark_persistent(g_handle_stdout);
-    mark_persistent(g_handle_stderr);
-    mark_persistent(g_handle_stdin);
     mark_persistent(g_io_error_nullptr_read);
+    g_io_handle_external_class = lean_register_external_class(io_handle_finalizer, io_handle_foreach);
 }
 
 void finalize_io() {

tests/lean/abst.lean.expected.out

@@ -5,4 +5,3 @@ f a (f b) (f a)
 f #0 a (f #0)
 f #0 y (f #0)
 f #1 #0 (f #1)
-

tests/lean/binsearch.lean.expected.out

@@ -19,4 +19,3 @@
 >> 17 ==> none
 >> 18 ==> none
 >> 19 ==> none
-

tests/lean/bytearray.lean.expected.out

@@ -3,4 +3,3 @@
 [1, 20, 30, 4]
 [1, 20, 3, 4]
 4
-

tests/lean/ctor_layout.lean.expected.out

@@ -10,4 +10,3 @@ obj@1
 ---
 obj@0
 ◾
-

tests/lean/inst.lean.expected.out

@@ -5,4 +5,3 @@ f a (f b) a
 f (f b) a (f b)
 f a #0 a
 f a #0 a
-

tests/lean/ref1.lean.expected.out

@@ -18,4 +18,3 @@
 [7]: 14
 [8]: 16
 [9]: 18
-

tests/lean/run/IO_test.lean

@@ -75,7 +75,7 @@ ys ← withFile fn2 Mode.read $ fun h => do
     pure ys };
 let rs := [xs₀ ++ xs₀ ++ "\n", xs₂ ++ "\n", xs₁ ++ "\n", xs₁ ++ "\n", ""];
 check_eq "2" rs ys;
-ys ← IO.readFile fn2;
+ys ← readFile fn2;
 check_eq "3" (String.join rs) ys;
 pure ()
 

tests/lean/stdio.lean

@@ -1,6 +0,0 @@
-
-#eval do
-out ← IO.getStdout;
-err ← IO.getStderr;
-out.putStr "print stdout";
-(err.putStrLn "print stderr" : IO Unit)

tests/lean/stdio.lean.expected.out

@@ -1,2 +0,0 @@
-print stderr
-print stdout

tests/lean/zipper.lean.expected.out

@@ -1,2 +1 @@
 [10, 0, 11, 13, 20, 0, 22, 0, 40, 0, 11]
-