feat(api): add lean_inductive API

src/api/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.cpp
-  expr.cpp decl.cpp env.cpp ios.cpp module.cpp type_checker.cpp)
+  expr.cpp decl.cpp env.cpp ios.cpp module.cpp type_checker.cpp inductive.cpp)
 
 FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h)
 install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include)

src/api/inductive.cpp

@@ -0,0 +1,189 @@
+/*
+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 "library/module.h"
+#include "api/decl.h"
+#include "api/inductive.h"
+#include "api/string.h"
+#include "api/exception.h"
+using namespace lean; // NOLINT
+using namespace lean::inductive; // NOLINT
+
+lean_bool lean_inductive_type_mk(lean_name n, lean_expr t, lean_list_expr cs, lean_inductive_type * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(n);
+    check_nonnull(t);
+    check_nonnull(cs);
+    for (expr const & c : to_list_expr_ref(cs)) {
+        if (!is_local(c))
+            throw exception("invalid inductive type, constructor must be a local constant");
+    }
+    *r = of_inductive_type(new inductive_decl(to_name_ref(n), to_expr_ref(t), to_list_expr_ref(cs)));
+    LEAN_CATCH;
+}
+
+void lean_inductive_type_del(lean_inductive_type t) {
+    delete to_inductive_type(t);
+}
+
+lean_bool lean_list_inductive_type_mk_nil(lean_list_inductive_type * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_list_inductive_type(new list<inductive_decl>());
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_inductive_type_mk_cons(lean_inductive_type h, lean_list_inductive_type t, lean_list_inductive_type * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(h);
+    check_nonnull(t);
+    *r = of_list_inductive_type(new list<inductive_decl>(to_inductive_type_ref(h), to_list_inductive_type_ref(t)));
+    LEAN_CATCH;
+}
+
+void lean_list_inductive_type_del(lean_list_inductive_type l) {
+    delete to_list_inductive_type(l);
+}
+
+lean_bool lean_list_inductive_type_is_cons(lean_list_inductive_type l) {
+    return l && !is_nil(to_list_inductive_type_ref(l));
+}
+
+lean_bool lean_list_inductive_type_eq(lean_list_inductive_type l1, lean_list_inductive_type l2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l1);
+    check_nonnull(l2);
+    *b = to_list_inductive_type_ref(l1) == to_list_inductive_type_ref(l2);
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_inductive_type_head(lean_list_inductive_type l, lean_inductive_type * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    if (!lean_list_inductive_type_is_cons(l))
+        throw lean::exception("invalid argument, non-nil list expected");
+    *r = of_inductive_type(new inductive_decl(head(to_list_inductive_type_ref(l))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_list_inductive_type_tail(lean_list_inductive_type l, lean_list_inductive_type * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l);
+    if (!lean_list_inductive_type_is_cons(l))
+        throw lean::exception("invalid argument, non-nil list expected");
+    *r = of_list_inductive_type(new list<inductive_decl>(tail(to_list_inductive_type_ref(l))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_inductive_decl_mk(lean_list_name ps, unsigned n, lean_list_inductive_type ts, lean_inductive_decl * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(ps);
+    check_nonnull(ts);
+    if (!lean_list_inductive_type_is_cons(ts))
+        throw exception("invalid argument, non-nil list expected");
+    *r = of_inductive_decl(new inductive_decls(to_list_name_ref(ps), n, to_list_inductive_type_ref(ts)));
+    LEAN_CATCH;
+}
+
+void lean_inductive_decl_del(lean_inductive_decl d) {
+    delete to_inductive_decl(d);
+}
+
+lean_bool lean_env_add_inductive(lean_env env, lean_inductive_decl d, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(d);
+    level_param_names    ps = std::get<0>(to_inductive_decl_ref(d));
+    unsigned             n  = std::get<1>(to_inductive_decl_ref(d));
+    list<inductive_decl> ds = std::get<2>(to_inductive_decl_ref(d));
+    *r = of_env(new environment(module::add_inductive(to_env_ref(env), ps, n, ds)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_is_inductive_type(lean_env env, lean_name n, lean_inductive_decl * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    if (auto d = is_inductive_decl(to_env_ref(env), to_name_ref(n))) {
+        *r = of_inductive_decl(new inductive_decls(*d));
+        return lean_true;
+    } else {
+        return lean_false;
+    }
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_is_constructor(lean_env env, lean_name n, lean_name * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    if (auto d = is_intro_rule(to_env_ref(env), to_name_ref(n))) {
+        *r = of_name(new name(*d));
+        return lean_true;
+    } else {
+        return lean_false;
+    }
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_is_recursor(lean_env env, lean_name n, lean_name * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    if (auto d = is_elim_rule(to_env_ref(env), to_name_ref(n))) {
+        *r = of_name(new name(*d));
+        return lean_true;
+    } else {
+        return lean_false;
+    }
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_get_inductive_type_num_indices(lean_env env, lean_name n, unsigned * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    if (auto d = get_num_indices(to_env_ref(env), to_name_ref(n))) {
+        *r = *d;
+        return lean_true;
+    } else {
+        return lean_false;
+    }
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_get_inductive_type_num_minor_premises(lean_env env, lean_name n, unsigned * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    if (auto d = get_num_minor_premises(to_env_ref(env), to_name_ref(n))) {
+        *r = *d;
+        return lean_true;
+    } else {
+        return lean_false;
+    }
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_get_inductive_type_num_type_formers(lean_env env, lean_name n, unsigned * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    if (auto d = get_num_type_formers(to_env_ref(env), to_name_ref(n))) {
+        *r = *d;
+        return lean_true;
+    } else {
+        return lean_false;
+    }
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_get_inductive_type_has_dep_elim(lean_env env, lean_name n, lean_bool * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(n);
+    *r = has_dep_elim(to_env_ref(env), to_name_ref(n));
+    LEAN_CATCH;
+}

src/api/inductive.h

@@ -0,0 +1,28 @@
+/*
+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 "kernel/inductive/inductive.h"
+#include "api/expr.h"
+#include "api/lean_decl.h"
+#include "api/lean_inductive.h"
+namespace lean {
+using inductive::intro_rule;
+using inductive::inductive_decl;
+using inductive::inductive_decls;
+
+inline inductive_decl * to_inductive_type(lean_inductive_type n) { return reinterpret_cast<inductive_decl *>(n); }
+inline inductive_decl const & to_inductive_type_ref(lean_inductive_type n) { return *reinterpret_cast<inductive_decl *>(n); }
+inline lean_inductive_type of_inductive_type(inductive_decl * n) { return reinterpret_cast<lean_inductive_type>(n); }
+
+inline list<inductive_decl> * to_list_inductive_type(lean_list_inductive_type n) { return reinterpret_cast<list<inductive_decl> *>(n); }
+inline list<inductive_decl> const & to_list_inductive_type_ref(lean_list_inductive_type n) { return *reinterpret_cast<list<inductive_decl> *>(n); }
+inline lean_list_inductive_type of_list_inductive_type(list<inductive_decl> * n) { return reinterpret_cast<lean_list_inductive_type>(n); }
+
+inline inductive_decls * to_inductive_decl(lean_inductive_decl n) { return reinterpret_cast<inductive_decls *>(n); }
+inline inductive_decls const & to_inductive_decl_ref(lean_inductive_decl n) { return *reinterpret_cast<inductive_decls *>(n); }
+inline lean_inductive_decl of_inductive_decl(inductive_decls * n) { return reinterpret_cast<lean_inductive_decl>(n); }
+}

src/api/lean.h

@@ -20,5 +20,6 @@ Author: Leonardo de Moura
 #include "lean_ios.h"           // NOLINT
 #include "lean_module.h"        // NOLINT
 #include "lean_type_checker.h"  // NOLINT
+#include "lean_inductive.h"     // NOLINT
 
 #endif

src/api/lean_inductive.h

@@ -0,0 +1,91 @@
+/*
+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_INDUCTIVE_H
+#define _LEAN_INDUCTIVE_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+   \defgroup capi C API
+*/
+/*@{*/
+
+/**
+   @name Inductive datatypes API
+*/
+/*@{*/
+
+LEAN_DEFINE_TYPE(lean_inductive_type);
+LEAN_DEFINE_TYPE(lean_list_inductive_type);
+LEAN_DEFINE_TYPE(lean_inductive_decl);
+
+/** \brief Create a new inductive type with name \c n, type \c t, and constructors (aka introduction rules \c cs)
+    \remark \c cs must be a list of local constants. */
+lean_bool lean_inductive_type_mk(lean_name n, lean_expr t, lean_list_expr cs, lean_inductive_type * r, lean_exception * ex);
+/** \brief Dispose/delete the given inductive type */
+void lean_inductive_type_del(lean_inductive_type t);
+
+/** \brief Create the empty list of inductive_types */
+lean_bool lean_list_inductive_type_mk_nil(lean_list_inductive_type * r, lean_exception * ex);
+/** \brief Create the list <tt>h :: t</tt> */
+lean_bool lean_list_inductive_type_mk_cons(lean_inductive_type h, lean_list_inductive_type t, lean_list_inductive_type * r, lean_exception * ex);
+/** \brief Delete/dispose the given list of inductive_types */
+void lean_list_inductive_type_del(lean_list_inductive_type l);
+/** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
+lean_bool lean_list_inductive_type_is_cons(lean_list_inductive_type l);
+/** \brief Return true in \c b iff the two given lists are equal */
+lean_bool lean_list_inductive_type_eq(lean_list_inductive_type l1, lean_list_inductive_type l2, lean_bool * b, lean_exception * ex);
+/** \brief Store in \c r the head of the given list
+    \pre lean_list_inductive_type_is_cons(l) */
+lean_bool lean_list_inductive_type_head(lean_list_inductive_type l, lean_inductive_type * r, lean_exception * ex);
+/** \brief Store in \c r the tail of the given list
+    \pre lean_list_inductive_type_is_cons(l) */
+lean_bool lean_list_inductive_type_tail(lean_list_inductive_type l, lean_list_inductive_type * r, lean_exception * ex);
+
+/** \brief Create a mutually recursive inductive datatype declaration with universe parameters \c ps,
+    \c n parameters and the given inductive types.
+    \remark The remaining inductive datatype arguments are treated as indices. */
+lean_bool lean_inductive_decl_mk(lean_list_name ps, unsigned n, lean_list_inductive_type ts, lean_inductive_decl * r, lean_exception * ex);
+/** \brief Delete/dispose the given inductive declaration */
+void lean_inductive_decl_del(lean_inductive_decl d);
+
+/** \brief Add the inductive declaration \c d to the given environment */
+lean_bool lean_env_add_inductive(lean_env env, lean_inductive_decl d, lean_env * r, lean_exception * ex);
+
+/** \brief Return lean_true if \c n is the name of an inductive type in the given environment,
+    and store the inductive declaration that it is part of in \c r. */
+lean_bool lean_env_is_inductive_type(lean_env env, lean_name n, lean_inductive_decl * r, lean_exception * ex);
+
+/** \brief Return lean_true if \c n is the name of a constructor in the given environment, and
+    store the name of the associated inductive type in \c r. */
+lean_bool lean_env_is_constructor(lean_env env, lean_name n, lean_name * r, lean_exception * ex);
+
+/** \brief Return lean_true if \c n is the name of a recursor (aka eliminator) in the given environment, and
+    store the name of the associated inductive type in \c r. */
+lean_bool lean_env_is_recursor(lean_env env, lean_name n, lean_name * r, lean_exception * ex);
+
+/** \brief Return lean_true if \c n is the name of an inductive type in the given environment, and
+    store the number of indices in \c r. */
+lean_bool lean_env_get_inductive_type_num_indices(lean_env env, lean_name n, unsigned * r, lean_exception * ex);
+/** \brief Return lean_true if \c n is the name of an inductive type in the given environment, and
+    store the number of minor premises in \c r. */
+lean_bool lean_env_get_inductive_type_num_minor_premises(lean_env env, lean_name n, unsigned * r, lean_exception * ex);
+/** \brief Return lean_true if \c n is the name of an inductive type in the given environment, and
+    store the number of type formers in \c r. */
+lean_bool lean_env_get_inductive_type_num_type_formers(lean_env env, lean_name n, unsigned * r, lean_exception * ex);
+/** \brief Return lean_true if \c n is the name of an inductive type in the given environment, and
+    store lean_true in \c r if the inductive type supports dependent elimination. */
+lean_bool lean_env_get_inductive_type_has_dep_elim(lean_env env, lean_name n, lean_bool * r, lean_exception * ex);
+/*@}*/
+/*@}*/
+
+#ifdef __cplusplus
+};
+#endif
+#endif