max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: avoid object.h dependencies

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-07 07:29:40 -07:00
parent b36baa143f
commit ebd8f1efa7
2 changed files with 14 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/include/lean/io.h
View file

@ -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();
}

13
tests/compiler/foreign/myfuns.cpp
View file

@ -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));
}