feat(api): expose hierarchical names in the C API

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_OBJECTS:api>)
 target_link_libraries(leanshared ${EXTRA_LIBS})
 
 add_subdirectory(shell)

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)

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<lean::memout_exception*>(ex))
+        return LEAN_OUT_OF_MEMORY;
+    if (dynamic_cast<lean::system_exception*>(ex))
+        return LEAN_SYSTEM_EXCEPTION;
+    if (dynamic_cast<lean::kernel_exception*>(ex))
+        return LEAN_KERNEL_EXCEPTION;
+    if (dynamic_cast<lean::interrupted*>(ex))
+        return LEAN_INTERRUPTED;
+    return LEAN_OTHER_EXCEPTION;
+}

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<throwable *>(e); }
+inline lean_exception of_exception(throwable * e) { return reinterpret_cast<lean_exception>(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

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

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

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

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

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 <tt>pre.s</tt>
+    \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 <tt>pre.i</tt>.
+    \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 <tt>pre.s</tt> 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 <tt>pre.i</tt> 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

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

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;
+}

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<name *>(n); }
+inline name const & to_name_ref(lean_name n) { return *reinterpret_cast<name *>(n); }
+inline lean_name of_name(name * n) { return reinterpret_cast<lean_name>(n); }
+}

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 <string.h>
+#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);
+}

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 <string>
+namespace lean {
+char const * mk_string(std::string const &);
+char const * mk_string(char const *);
+void del_string(char const *);
+}