From 23a490f3f19efaa97a3b97fdc65ce4868c8a54e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 23 Aug 2015 09:34:31 -0700 Subject: [PATCH] feat(api): add lean_type_checker API --- src/api/CMakeLists.txt | 2 +- src/api/lean.h | 1 + src/api/lean_type_checker.h | 58 ++++++++++++++++++++++++++++++++ src/api/type_checker.cpp | 66 +++++++++++++++++++++++++++++++++++++ src/api/type_checker.h | 21 ++++++++++++ 5 files changed, 147 insertions(+), 1 deletion(-) create mode 100644 src/api/lean_type_checker.h create mode 100644 src/api/type_checker.cpp create mode 100644 src/api/type_checker.h diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 1e5da515f..9294ffaba 100644 --- a/src/api/CMakeLists.txt +++ b/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) diff --git a/src/api/lean.h b/src/api/lean.h index 4e3fff272..a7b9c5475 100644 --- a/src/api/lean.h +++ b/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 diff --git a/src/api/lean_type_checker.h b/src/api/lean_type_checker.h new file mode 100644 index 000000000..13bd7d20c --- /dev/null +++ b/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 diff --git a/src/api/type_checker.cpp b/src/api/type_checker.cpp new file mode 100644 index 000000000..af309fdde --- /dev/null +++ b/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; +} diff --git a/src/api/type_checker.h b/src/api/type_checker.h new file mode 100644 index 000000000..3153fe222 --- /dev/null +++ b/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(n); } +inline type_checker & to_type_checker_ref(lean_type_checker n) { return *reinterpret_cast(n); } +inline lean_type_checker of_type_checker(type_checker * n) { return reinterpret_cast(n); } + +inline constraint_seq * to_cnstr_seq(lean_cnstr_seq n) { return reinterpret_cast(n); } +inline constraint_seq const & to_cnstr_seq_ref(lean_type_checker n) { return *reinterpret_cast(n); } +inline lean_cnstr_seq of_cnstr_seq(constraint_seq * n) { return reinterpret_cast(n); } +}