feat(api): add lean_env API

src/api/CMakeLists.txt

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

src/api/decl.cpp

@@ -141,3 +141,15 @@ lean_bool lean_decl_get_conv_opt(lean_decl d, lean_bool * r, lean_exception * ex
     *r = to_decl_ref(d).use_conv_opt();
     LEAN_CATCH;
 }
+
+lean_bool lean_decl_check(lean_env e, lean_decl d, lean_cert_decl * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    check_nonnull(d);
+    *r = of_cert_decl(new certified_declaration(check(to_env_ref(e), to_decl_ref(d))));
+    LEAN_CATCH;
+}
+
+void lean_cert_decl_del(lean_cert_decl d) {
+    delete to_cert_decl(d);
+}

src/api/decl.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/declaration.h"
+#include "kernel/type_checker.h"
 #include "api/expr.h"
 #include "api/lean_decl.h"
 namespace lean {
@@ -13,6 +14,10 @@ inline declaration * to_decl(lean_decl n) { return reinterpret_cast<declaration
 inline declaration const & to_decl_ref(lean_decl n) { return *reinterpret_cast<declaration *>(n); }
 inline lean_decl of_decl(declaration * n) { return reinterpret_cast<lean_decl>(n); }
 
+inline certified_declaration * to_cert_decl(lean_cert_decl n) { return reinterpret_cast<certified_declaration *>(n); }
+inline certified_declaration const & to_cert_decl_ref(lean_cert_decl n) { return *reinterpret_cast<certified_declaration *>(n); }
+inline lean_cert_decl of_cert_decl(certified_declaration * n) { return reinterpret_cast<lean_cert_decl>(n); }
+
 inline environment * to_env(lean_env n) { return reinterpret_cast<environment *>(n); }
 inline environment const & to_env_ref(lean_env n) { return *reinterpret_cast<environment *>(n); }
 inline lean_env of_env(environment * n) { return reinterpret_cast<lean_env>(n); }

src/api/env.cpp

@@ -0,0 +1,113 @@
+/*
+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/environment.h"
+#include "library/standard_kernel.h"
+#include "library/hott_kernel.h"
+#include "api/decl.h"
+#include "api/string.h"
+#include "api/exception.h"
+#include "api/lean_env.h"
+using namespace lean; // NOLINT
+
+lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_env(new environment(mk_environment(t)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_mk_hott(unsigned t, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_env(new environment(mk_hott_environment(t)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    check_nonnull(u);
+    *r = of_env(new environment(to_env_ref(e).add_universe(to_name_ref(u))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    check_nonnull(d);
+    *r = of_env(new environment(to_env_ref(e).add(to_cert_decl_ref(d))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_replace(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    check_nonnull(d);
+    *r = of_env(new environment(to_env_ref(e).replace(to_cert_decl_ref(d))));
+    LEAN_CATCH;
+}
+
+void lean_env_del(lean_env e) {
+    delete to_env(e);
+}
+
+unsigned lean_env_trust_level(lean_env e) {
+    return e ? to_env_ref(e).trust_lvl() : 0;
+}
+
+lean_bool lean_env_proof_irrel(lean_env e) {
+    return e && to_env_ref(e).prop_proof_irrel();
+}
+
+lean_bool lean_env_impredicative(lean_env e) {
+    return e && to_env_ref(e).impredicative();
+}
+
+lean_bool lean_env_contains_univ(lean_env e, lean_name n) {
+    return e && n && to_env_ref(e).is_universe(to_name_ref(n));
+}
+
+lean_bool lean_env_contains_decl(lean_env e, lean_name n) {
+    return e && n && to_env_ref(e).find(to_name_ref(n));
+}
+
+lean_bool lean_env_get_decl(lean_env e, lean_name n, lean_decl * d, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    check_nonnull(n);
+    *d = of_decl(new declaration(to_env_ref(e).get(to_name_ref(n))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_is_descendant(lean_env e1, lean_env e2) {
+    return e1 && e2 && to_env_ref(e1).is_descendant(to_env_ref(e2));
+}
+
+lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    *r = of_env(new environment(to_env_ref(e).forget()));
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    to_env_ref(e).for_each_declaration([&](declaration const & d) {
+            f(of_decl(const_cast<declaration*>(&d)));
+        });
+    return lean_true;
+    LEAN_CATCH;
+}
+
+lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    to_env_ref(e).for_each_universe([&](name const & u) {
+            f(of_name(const_cast<name*>(&u)));
+        });
+    return lean_true;
+    LEAN_CATCH;
+}

src/api/lean_decl.h

@@ -23,6 +23,7 @@ extern "C" {
 
 LEAN_DEFINE_TYPE(lean_env);
 LEAN_DEFINE_TYPE(lean_decl);
+LEAN_DEFINE_TYPE(lean_cert_decl);
 
 typedef enum {
     LEAN_DECL_CONST,
@@ -78,6 +79,11 @@ lean_bool lean_decl_get_height(lean_decl d, unsigned * r, lean_exception * ex);
     \pre lean_decl_get_kind(d) == LEAN_DECL_DEF */
 lean_bool lean_decl_get_conv_opt(lean_decl d, lean_bool * r, lean_exception * ex);
 
+/** \brief Create a certified declaration by type checking the given declaration with respect to the given environment */
+lean_bool lean_decl_check(lean_env e, lean_decl d, lean_cert_decl * r, lean_exception * ex);
+/** \brief Delete/dispose the given certified declaration. */
+void lean_cert_decl_del(lean_cert_decl d);
+
 /*@}*/
 /*@}*/
 

src/api/lean_env.h

@@ -0,0 +1,74 @@
+/*
+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_ENV_H
+#define _LEAN_ENV_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+   \defgroup capi C API
+*/
+/*@{*/
+
+/**
+   @name Environment API
+*/
+/*@{*/
+
+/** \brief Create a standard environment (i.e., proof irrelevant, and containing an impredicative Prop) with trust level \c t.
+    If the trust level is 0, then all imported modules are retype-checked, and declarations containing macros are rejected. */
+lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex);
+/** \brief Create a HoTT environment (i.e., proof relevant, no Prop) with trust level \c t. */
+lean_bool lean_env_mk_hott(unsigned t, lean_env * r, lean_exception * ex);
+
+/** \brief Add a new global universe with name \c u. */
+lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex);
+/** \brief Create a new environment by adding the given certified declaration \c d to the environment \c e. */
+lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex);
+/** \brief Replace the axiom with the name of the given certified theorem \c d with \c d.
+    This procedure throws an exception if:
+    - The theorem was certified in an environment which is not an ancestor of \c e.
+    - The environment does not contain an axiom with the given name. */
+lean_bool lean_env_replace(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex);
+
+/** \brief Delete/dispose the given environment. */
+void lean_env_del(lean_env e);
+
+/** \brief Return the trust level of the given environment */
+unsigned lean_env_trust_level(lean_env e);
+/** \brief Return true iff the given environment has a proof irrelevant Prop (i.e., Type.{0}). */
+lean_bool lean_env_proof_irrel(lean_env e);
+/** \brief Return true iff in the given environment Prop is impredicative. */
+lean_bool lean_env_impredicative(lean_env e);
+
+/** \brief Return true iff \c e contains a global universe with name \c n. */
+lean_bool lean_env_contains_univ(lean_env e, lean_name n);
+/** \brief Return true iff \c e contains a declaration with name \c n. */
+lean_bool lean_env_contains_decl(lean_env e, lean_name n);
+/** \brief Store in \c d the declaration with name \c n in \c e. */
+lean_bool lean_env_get_decl(lean_env e, lean_name n, lean_decl * d, lean_exception * ex);
+
+/** \brief Return true when \c e1 is a descendant of \c e2, that is, \c e1 was created by adding declarations to \c e2. */
+lean_bool lean_env_is_descendant(lean_env e1, lean_env e2);
+/** \brief Return a new environment, where its "history" has been truncated/forgotten.
+    That is, <tt>is_descendant(r, e2)</tt> will return false for any environment \c e2 that
+    is not pointer equal to the result. */
+lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex);
+
+/** \brief Execute \c f for each declaration in \c env. */
+lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex);
+/** \brief Execute \c f for each global universe in \c env. */
+lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex);
+/*@}*/
+/*@}*/
+
+#ifdef __cplusplus
+};
+#endif
+#endif