From ebd8f1efa7844cf162fe3994a558d5faaa4bcca2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Sep 2021 07:29:40 -0700
Subject: [PATCH] chore: avoid `object.h` dependencies

---
 src/include/lean/io.h             | 14 +++++++-------
 tests/compiler/foreign/myfuns.cpp | 13 +++++++------
 2 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/src/include/lean/io.h b/src/include/lean/io.h
index 9cd9b7f962..43602d783d 100644
--- a/src/include/lean/io.h
+++ b/src/include/lean/io.h
@@ -7,15 +7,15 @@ Author: Leonardo de Moura
 #pragma once
 #include <stdio.h>
 #include <string>
-#include <lean/object.h>
+#include <lean/lean.h>
 
 namespace lean {
-inline obj_res io_result_mk_ok(obj_arg a) { return lean_io_result_mk_ok(a); }
-inline obj_res io_result_mk_error(obj_arg e) { return lean_io_result_mk_error(e); }
-obj_res io_result_mk_error(char const * msg);
-obj_res io_result_mk_error(std::string const & msg);
-obj_res decode_io_error(int errnum, b_obj_arg fname);
-obj_res io_wrap_handle(FILE * hfile);
+inline lean_obj_res io_result_mk_ok(lean_obj_arg a) { return lean_io_result_mk_ok(a); }
+inline lean_obj_res io_result_mk_error(lean_obj_arg e) { return lean_io_result_mk_error(e); }
+lean_obj_res io_result_mk_error(char const * msg);
+lean_obj_res io_result_mk_error(std::string const & msg);
+lean_obj_res decode_io_error(int errnum, b_lean_obj_arg fname);
+lean_obj_res io_wrap_handle(FILE * hfile);
 void initialize_io();
 void finalize_io();
 }
diff --git a/tests/compiler/foreign/myfuns.cpp b/tests/compiler/foreign/myfuns.cpp
index ee9cff6224..c8be44b344 100644
--- a/tests/compiler/foreign/myfuns.cpp
+++ b/tests/compiler/foreign/myfuns.cpp
@@ -1,5 +1,6 @@
-#include <lean/object.h>
-#include <lean/io.h>
+#include <stdio.h>
+#include <string>
+#include <lean/lean.h>
 
 struct S {
     unsigned    m_x;
@@ -38,23 +39,23 @@ extern "C" uint32_t lean_S_add_x_y(b_lean_obj_arg s) {
 }
 
 extern "C" lean_object * lean_S_string(b_lean_obj_arg s) {
-    return lean::mk_string(to_S(s)->m_s);
+    return lean_mk_string(to_S(s)->m_s.c_str());
 }
 
 static S g_s(0, 0, "");
 
 extern "C" lean_object * lean_S_global_append(b_lean_obj_arg str, lean_object /* w */) {
     g_s.m_s += lean_string_cstr(str);
-    return lean::io_result_mk_ok(lean_box(0));
+    return lean_io_result_mk_ok(lean_box(0));
 }
 
 extern "C" lean_object * lean_S_global_string(lean_object /* w */) {
-    return lean::io_result_mk_ok(lean::mk_string(g_s.m_s));
+    return lean_io_result_mk_ok(lean_mk_string(g_s.m_s.c_str()));
 }
 
 extern "C" lean_object * lean_S_update_global(b_lean_obj_arg s, lean_object /* w */) {
     g_s.m_x = to_S(s)->m_x;
     g_s.m_y = to_S(s)->m_y;
     g_s.m_s = to_S(s)->m_s;
-    return lean::io_result_mk_ok(lean_box(0));
+    return lean_io_result_mk_ok(lean_box(0));
 }