feat(api): add lean_type_checker 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)
+  expr.cpp decl.cpp env.cpp ios.cpp module.cpp type_checker.cpp)
 
 FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h)
 install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include)

src/api/lean.h

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

src/api/lean_type_checker.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
+*/
+#ifndef _LEAN_TYPE_CHECKER_H
+#define _LEAN_TYPE_CHECKER_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+   \defgroup capi C API
+*/
+/*@{*/
+
+/**
+   @name Type checker API
+*/
+/*@{*/
+
+LEAN_DEFINE_TYPE(lean_type_checker);
+LEAN_DEFINE_TYPE(lean_cnstr_seq);
+
+/** \brief Create a type checker object for the given environment. */
+lean_bool lean_type_checker_mk(lean_env e, lean_type_checker * r, lean_exception * ex);
+
+/** \brief Dispose/delete the given type checker */
+void lean_type_checker_del(lean_type_checker t);
+
+/** \brief Dispose/delete the given constraint sequence. */
+void lean_cnstr_seq_del(lean_cnstr_seq s);
+
+/** \brief Infer the type of \c e using \c t. Store the result in \c r and any generated constraints in \c s.
+    \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */
+lean_bool lean_type_checker_infer(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex);
+
+/** \brief Type check and infer the type of \c e using \c t. Store the result in \c r and any generated constraints in \c s.
+    \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */
+lean_bool lean_type_checker_check(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex);
+
+/** \brief Compute the weak-head-normal-form of \c e using \c t. Store the result in \c r and any generated constraints in \c s.
+    \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */
+lean_bool lean_type_checker_whnf(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex);
+
+/** \brief Store true in \c r iff \c e1 and \c e2 are definitionally equal. Store any generated constraints in \c s.
+    \remark \c e must not contain any subterm v s.t. lean_expr_get_kind(v) == LEAN_EXPR_VAR */
+lean_bool lean_type_checker_is_def_eq(lean_type_checker t, lean_expr e1, lean_expr e2, lean_bool * r, lean_cnstr_seq * s, lean_exception * ex);
+
+/*@}*/
+/*@}*/
+
+#ifdef __cplusplus
+};
+#endif
+#endif

src/api/type_checker.cpp

@@ -0,0 +1,66 @@
+/*
+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/string.h"
+#include "api/exception.h"
+#include "api/type_checker.h"
+using namespace lean; // NOLINT
+
+lean_bool lean_type_checker_mk(lean_env e, lean_type_checker * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(e);
+    *r = of_type_checker(new type_checker(to_env_ref(e), name_generator()));
+    LEAN_CATCH;
+}
+
+void lean_type_checker_del(lean_type_checker t) {
+    delete to_type_checker(t);
+}
+
+void lean_cnstr_seq_del(lean_cnstr_seq s) {
+    delete to_cnstr_seq(s);
+}
+
+lean_bool lean_type_checker_infer(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(t);
+    check_nonnull(e);
+    auto ecs = to_type_checker_ref(t).infer(to_expr_ref(e));
+    *r = of_expr(new expr(ecs.first));
+    *s = of_cnstr_seq(new constraint_seq(ecs.second));
+    LEAN_CATCH;
+}
+
+lean_bool lean_type_checker_check(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(t);
+    check_nonnull(e);
+    auto ecs = to_type_checker_ref(t).check(to_expr_ref(e));
+    *r = of_expr(new expr(ecs.first));
+    *s = of_cnstr_seq(new constraint_seq(ecs.second));
+    LEAN_CATCH;
+}
+
+lean_bool lean_type_checker_whnf(lean_type_checker t, lean_expr e, lean_expr * r, lean_cnstr_seq * s, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(t);
+    check_nonnull(e);
+    auto ecs = to_type_checker_ref(t).whnf(to_expr_ref(e));
+    *r = of_expr(new expr(ecs.first));
+    *s = of_cnstr_seq(new constraint_seq(ecs.second));
+    LEAN_CATCH;
+}
+
+lean_bool lean_type_checker_is_def_eq(lean_type_checker t, lean_expr e1, lean_expr e2, lean_bool * r, lean_cnstr_seq * s, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(t);
+    check_nonnull(e1);
+    check_nonnull(e2);
+    auto bcs = to_type_checker_ref(t).is_def_eq(to_expr_ref(e1), to_expr_ref(e2));
+    *r = bcs.first;
+    *s = of_cnstr_seq(new constraint_seq(bcs.second));
+    LEAN_CATCH;
+}

src/api/type_checker.h

@@ -0,0 +1,21 @@
+/*
+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/declaration.h"
+#include "kernel/type_checker.h"
+#include "api/expr.h"
+#include "api/decl.h"
+#include "api/lean_type_checker.h"
+namespace lean {
+inline type_checker * to_type_checker(lean_type_checker n) { return reinterpret_cast<type_checker *>(n); }
+inline type_checker & to_type_checker_ref(lean_type_checker n) { return *reinterpret_cast<type_checker *>(n); }
+inline lean_type_checker of_type_checker(type_checker * n) { return reinterpret_cast<lean_type_checker>(n); }
+
+inline constraint_seq * to_cnstr_seq(lean_cnstr_seq n) { return reinterpret_cast<constraint_seq *>(n); }
+inline constraint_seq const & to_cnstr_seq_ref(lean_type_checker n) { return *reinterpret_cast<constraint_seq *>(n); }
+inline lean_cnstr_seq of_cnstr_seq(constraint_seq * n) { return reinterpret_cast<lean_cnstr_seq>(n); }
+}