From 42d41fb276b731a9b5e4145051778ca2c9b2c8af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Aug 2015 17:23:10 -0700 Subject: [PATCH] feat(api): expose hierarchical names in the C API --- src/CMakeLists.txt | 3 +- src/api/CMakeLists.txt | 4 ++ src/api/exception.cpp | 53 ++++++++++++++++++++++++ src/api/exception.h | 58 +++++++++++++++++++++++++++ src/api/lean.h | 16 ++++++++ src/api/lean_bool.h | 14 +++++++ src/api/lean_exception.h | 46 +++++++++++++++++++++ src/api/lean_macros.h | 26 ++++++++++++ src/api/lean_name.h | 54 +++++++++++++++++++++++++ src/api/lean_string.h | 19 +++++++++ src/api/name.cpp | 87 ++++++++++++++++++++++++++++++++++++++++ src/api/name.h | 15 +++++++ src/api/string.cpp | 35 ++++++++++++++++ src/api/string.h | 13 ++++++ 14 files changed, 442 insertions(+), 1 deletion(-) create mode 100644 src/api/CMakeLists.txt create mode 100644 src/api/exception.cpp create mode 100644 src/api/exception.h create mode 100644 src/api/lean.h create mode 100644 src/api/lean_bool.h create mode 100644 src/api/lean_exception.h create mode 100644 src/api/lean_macros.h create mode 100644 src/api/lean_name.h create mode 100644 src/api/lean_string.h create mode 100644 src/api/name.cpp create mode 100644 src/api/name.h create mode 100644 src/api/string.cpp create mode 100644 src/api/string.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 43a8a31e6..9268fe249 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -363,7 +363,8 @@ add_library(leanstatic ${LEAN_OBJS}) if (${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all") endif() -add_library(leanshared SHARED shared/init.cpp ${LEAN_OBJS}) +add_subdirectory(api) +add_library(leanshared SHARED shared/init.cpp ${LEAN_OBJS} $) target_link_libraries(leanshared ${EXTRA_LIBS}) add_subdirectory(shell) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt new file mode 100644 index 000000000..e4f5c59a8 --- /dev/null +++ b/src/api/CMakeLists.txt @@ -0,0 +1,4 @@ +add_library(api OBJECT string.cpp exception.cpp name.cpp) + +FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h) +install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include) diff --git a/src/api/exception.cpp b/src/api/exception.cpp new file mode 100644 index 000000000..074acb91e --- /dev/null +++ b/src/api/exception.cpp @@ -0,0 +1,53 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/kernel_exception.h" +#include "api/exception.h" +#include "api/string.h" + +namespace lean { +memout_exception * get_memout_exception() { + static memout_exception g_memout; + return &g_memout; +} + +void check_nonnull(void const * ptr) { + if (!ptr) + throw exception("invalid argument, it must be a nonnull pointer"); +} +} + +void lean_del_exception(lean_exception e) { + lean::throwable * t = lean::to_exception(e); + if (t != lean::get_memout_exception()) { + delete t; + } +} + +char const * lean_get_exception_message(lean_exception e) { + if (!e) + return 0; + try { + return lean::mk_string(lean::to_exception(e)->what()); + } catch (...) { + return 0; + } +} + +lean_exception_kind lean_get_exception_kind(lean_exception e) { + lean::throwable * ex = lean::to_exception(e); + if (!ex) + return LEAN_NULL_EXCEPTION; + if (dynamic_cast(ex)) + return LEAN_OUT_OF_MEMORY; + if (dynamic_cast(ex)) + return LEAN_SYSTEM_EXCEPTION; + if (dynamic_cast(ex)) + return LEAN_KERNEL_EXCEPTION; + if (dynamic_cast(ex)) + return LEAN_INTERRUPTED; + return LEAN_OTHER_EXCEPTION; +} diff --git a/src/api/exception.h b/src/api/exception.h new file mode 100644 index 000000000..6f566a7dc --- /dev/null +++ b/src/api/exception.h @@ -0,0 +1,58 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "api/lean_bool.h" +#include "api/lean_macros.h" +#include "api/lean_bool.h" +#include "api/lean_exception.h" +#include "api/exception.h" +#include "util/exception.h" + +namespace lean { +inline throwable * to_exception(lean_exception e) { return reinterpret_cast(e); } +inline lean_exception of_exception(throwable * e) { return reinterpret_cast(e); } + +class memout_exception : public throwable { +public: + memout_exception() {} + virtual ~memout_exception() noexcept {} + virtual char const * what() const noexcept { return "out of memory"; } + virtual throwable * clone() const { return new memout_exception(); } + virtual void rethrow() const { throw *this; } +}; + +class system_exception : public throwable { +public: + system_exception():throwable("unknown exception") {} + system_exception(std::string const & msg):throwable(msg) {} + system_exception(std::exception const & ex):throwable(ex.what()) {} + virtual ~system_exception() noexcept {} + virtual throwable * clone() const { return new system_exception(what()); } + virtual void rethrow() const { throw *this; } +}; + +memout_exception * get_memout_exception(); +void check_nonnull(void const *); +} + +#define LEAN_TRY try { + +#define LEAN_CATCH \ +} catch (lean::exception & e) { \ + *ex = of_exception(e.clone()); \ + return lean_false; \ +} catch (std::bad_alloc &) { \ + *ex = of_exception(lean::get_memout_exception()); \ + return lean_false; \ +} catch (std::exception & e) { \ + *ex = of_exception(new lean::system_exception(e)); \ + return lean_false; \ +} catch (...) { \ + *ex = of_exception(new lean::system_exception()); \ + return lean_false; \ +} \ +return lean_true diff --git a/src/api/lean.h b/src/api/lean.h new file mode 100644 index 000000000..9cecbf23e --- /dev/null +++ b/src/api/lean.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifndef _LEAN_H +#define _LEAN_H + +#include "lean_macros.h" +#include "lean_bool.h" +#include "lean_string.h" +#include "lean_exception.h" +#include "lean_name.h" + +#endif diff --git a/src/api/lean_bool.h b/src/api/lean_bool.h new file mode 100644 index 000000000..ba7389eee --- /dev/null +++ b/src/api/lean_bool.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifndef _LEAN_BOOL_H +#define _LEAN_BOOL_H + +#define lean_bool int +#define lean_true 1 +#define lean_false 0 + +#endif diff --git a/src/api/lean_exception.h b/src/api/lean_exception.h new file mode 100644 index 000000000..d10d4e1d6 --- /dev/null +++ b/src/api/lean_exception.h @@ -0,0 +1,46 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifndef _LEAN_EXCEPTION_H +#define _LEAN_EXCEPTION_H + +#ifdef __cplusplus +extern "C" { +#endif + +LEAN_DEFINE_TYPE(lean_exception); + +/** \brief Delete an exception object allocated by Lean. + This is a NOOP if \c e is null. +*/ +void lean_del_exception(lean_exception e); + +/** \brief Return basic string/message describing the exception. + \remark The string must be deallocated using #lean_del_string. + + \remark After we define the Lean environment object, we can + provide richer messages. + + \remark The result is null if the operation failed or \c e is null. +*/ +char const * lean_get_exception_message(lean_exception e); + +typedef enum { + LEAN_NULL_EXCEPTION, // null (aka there is no exception) + LEAN_SYSTEM_EXCEPTION, // exception generated by the C++ runtime + LEAN_OUT_OF_MEMORY, // out of memory exception + LEAN_INTERRUPTED, // execution was interrupted by user request + LEAN_KERNEL_EXCEPTION, // type checking error + LEAN_OTHER_EXCEPTION // other (TODO) lean exceptions +} lean_exception_kind; + +/** \brief Return the kind of the given exception. */ +lean_exception_kind lean_get_exception_kind(lean_exception e); + +#ifdef __cplusplus +}; +#endif +#endif diff --git a/src/api/lean_macros.h b/src/api/lean_macros.h new file mode 100644 index 000000000..9e36247b1 --- /dev/null +++ b/src/api/lean_macros.h @@ -0,0 +1,26 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifndef _LEAN_MACROS_H +#define _LEAN_MACROS_H + +#ifndef LEAN_API + #ifdef __GNUC__ + #define LEAN_API __attribute__ ((visibility ("default"))) + #else + #define LEAN_API + #endif +#endif + +#ifndef LEAN_DEFINE_TYPE +#define LEAN_DEFINE_TYPE(T) typedef struct _ ## T *T +#endif + +#ifndef LEAN_DEFINE_VOID +#define LEAN_DEFINE_VOID(T) typedef void* T +#endif + +#endif diff --git a/src/api/lean_name.h b/src/api/lean_name.h new file mode 100644 index 000000000..aac1b2050 --- /dev/null +++ b/src/api/lean_name.h @@ -0,0 +1,54 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifndef _LEAN_NAME_H +#define _LEAN_NAME_H + +#ifdef __cplusplus +extern "C" { +#endif + +LEAN_DEFINE_TYPE(lean_name); + +/** \brief Create the anonymous name */ +lean_bool lean_mk_anonymous_name(lean_name * r, lean_exception * e); +/** \brief Create the name pre.s + \remark \c r must be disposed using #lean_del_name */ +lean_bool lean_mk_str_name(lean_name pre, char const * s, lean_name * r, lean_exception * e); +/** \brief Create the name pre.i. + \pre !lean_is_anonymous_name(pre) + \remark \c r must be disposed using #lean_del_name */ +lean_bool lean_mk_idx_name(lean_name pre, unsigned i, lean_name * r, lean_exception * e); +void lean_del_name(lean_name n); +/** \brief Return lean_true iff \c n is the anonymous */ +lean_bool lean_is_anonymous_name(lean_name n); +/** \brief Return lean_true iff \c n is a name of the form pre.s where \c s is a string. */ +lean_bool lean_is_str_name(lean_name n); +/** \brief Return lean_true iff \c n is a name of the form pre.i where \c i is an unsigned integer. */ +lean_bool lean_is_idx_name(lean_name n); +/** \brief Return the prefix of the given name. + \pre !lean_is_anonymous_name(n) +*/ +lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * e); +/** \brief Store in \c r the suffix of the given name as a string. + \pre lean_is_str_name(n) + \remark \c r must be disposed using #lean_del_name +*/ +lean_bool lean_get_name_str(lean_name n, char const ** r, lean_exception * e); +/** \brief Store in \c r the suffix of the given name as a unsigned integer. + \pre lean_is_idx_name(n) + \remark \c r must be deleted using #lean_del_string +*/ +lean_bool lean_get_name_idx(lean_name n, unsigned * r, lean_exception * e); +/** \brief Store in \c r a string representation of the given hierarchical name. + \remark \c r must be deleted using #lean_del_string +*/ +lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * e); + +#ifdef __cplusplus +}; +#endif +#endif diff --git a/src/api/lean_string.h b/src/api/lean_string.h new file mode 100644 index 000000000..4a2b045f6 --- /dev/null +++ b/src/api/lean_string.h @@ -0,0 +1,19 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifndef _LEAN_STRING_H +#define _LEAN_STRING_H +#ifdef __cplusplus +extern "C" { +#endif + +/** \brief Delete a string allocated by Lean */ +void lean_del_string(char const * s); + +#ifdef __cplusplus +}; +#endif +#endif diff --git a/src/api/name.cpp b/src/api/name.cpp new file mode 100644 index 000000000..4dd3ea052 --- /dev/null +++ b/src/api/name.cpp @@ -0,0 +1,87 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "api/name.h" +#include "api/string.h" +#include "api/exception.h" +using namespace lean; + +lean_bool lean_mk_anonymous_name(lean_name * r, lean_exception * ex) { + LEAN_TRY; + *r = of_name(new name()); + LEAN_CATCH; +} + +lean_bool lean_mk_str_name(lean_name pre, char const * s, lean_name * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(pre); + check_nonnull(s); + *r = of_name(new name(to_name_ref(pre), s)); + LEAN_CATCH; +} + +lean_bool lean_mk_idx_name(lean_name pre, unsigned i, lean_name * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(pre); + name const & p = to_name_ref(pre); + if (p.is_anonymous()) + throw lean::exception("invalid argument, prefix is an anonymous name"); + *r = of_name(new name(to_name_ref(pre), i)); + LEAN_CATCH; +} + +void lean_del_name(lean_name n) { + delete to_name(n); +} + +lean_bool lean_is_anonymous_name(lean_name n) { + return n && to_name_ref(n).is_anonymous(); +} + +lean_bool lean_is_str_name(lean_name n) { + return n && to_name_ref(n).is_string(); +} + +lean_bool lean_is_idx_name(lean_name n) { + return n && to_name_ref(n).is_numeral(); +} + +lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + if (to_name_ref(n).is_anonymous()) + throw lean::exception("invalid argument, anonymous names does not have a prefix"); + else if (to_name_ref(n).is_atomic()) + *r = of_name(new name()); + else + *r = of_name(new name(to_name_ref(n).get_prefix())); + LEAN_CATCH; +} + +lean_bool lean_get_name_str(lean_name n, char const ** r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + if (!lean_is_str_name(n)) + throw lean::exception("invalid argument, it is not a string name"); + *r = mk_string(to_name_ref(n).get_string()); + LEAN_CATCH; +} + +lean_bool lean_get_name_idx(lean_name n, unsigned * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + if (!lean_is_idx_name(n)) + throw lean::exception("invalid argument, it is not an indexed name"); + *r = to_name_ref(n).get_numeral(); + LEAN_CATCH; +} + +lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + *r = mk_string(to_name_ref(n).to_string()); + LEAN_CATCH; +} diff --git a/src/api/name.h b/src/api/name.h new file mode 100644 index 000000000..07793c88d --- /dev/null +++ b/src/api/name.h @@ -0,0 +1,15 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/name.h" +#include "api/exception.h" +#include "api/lean_name.h" +namespace lean { +inline name * to_name(lean_name n) { return reinterpret_cast(n); } +inline name const & to_name_ref(lean_name n) { return *reinterpret_cast(n); } +inline lean_name of_name(name * n) { return reinterpret_cast(n); } +} diff --git a/src/api/string.cpp b/src/api/string.cpp new file mode 100644 index 000000000..ce7293ba3 --- /dev/null +++ b/src/api/string.cpp @@ -0,0 +1,35 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "api/string.h" + +namespace lean { +char const * mk_string(std::string const & s) { + char * r = new char[s.size() + 1]; + for (unsigned i = 0; i < s.size(); i++) + r[i] = s[i]; + r[s.size()] = 0; + return r; +} + +char const * mk_string(char const * s) { + unsigned sz = strlen(s); + char * r = new char[sz + 1]; + for (unsigned i = 0; i < sz; i++) + r[i] = s[i]; + r[sz] = 0; + return r; +} + +void del_string(char const * s) { + delete[] s; +} +} + +void lean_del_string(char const * s) { + lean::del_string(s); +} diff --git a/src/api/string.h b/src/api/string.h new file mode 100644 index 000000000..ddf212715 --- /dev/null +++ b/src/api/string.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +namespace lean { +char const * mk_string(std::string const &); +char const * mk_string(char const *); +void del_string(char const *); +}