diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index ea40d421c..c82166353 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.cpp expr.cpp) +add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.cpp expr.cpp decl.cpp) FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h) install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include) diff --git a/src/api/decl.cpp b/src/api/decl.cpp new file mode 100644 index 000000000..768d66cbe --- /dev/null +++ b/src/api/decl.cpp @@ -0,0 +1,143 @@ +/* +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/decl.h" +using namespace lean; // NOLINT + +lean_bool lean_decl_mk_axiom(lean_name n, lean_list_name p, lean_expr t, lean_decl * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + check_nonnull(p); + check_nonnull(t); + *r = of_decl(new declaration(mk_axiom(to_name_ref(n), to_list_name_ref(p), to_expr_ref(t)))); + LEAN_CATCH; +} + +lean_bool lean_decl_mk_const(lean_name n, lean_list_name p, lean_expr t, lean_decl * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + check_nonnull(p); + check_nonnull(t); + *r = of_decl(new declaration(mk_constant_assumption(to_name_ref(n), to_list_name_ref(p), to_expr_ref(t)))); + LEAN_CATCH; +} + +lean_bool lean_decl_mk_def(lean_name n, lean_list_name p, lean_expr t, lean_expr v, unsigned h, lean_bool o, lean_decl * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + check_nonnull(p); + check_nonnull(t); + check_nonnull(v); + *r = of_decl(new declaration(mk_definition(to_name_ref(n), to_list_name_ref(p), to_expr_ref(t), to_expr_ref(v), h, static_cast(o)))); + LEAN_CATCH; +} + +lean_bool lean_decl_mk_def_with(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_bool o, lean_decl * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(e); + check_nonnull(n); + check_nonnull(p); + check_nonnull(t); + check_nonnull(v); + *r = of_decl(new declaration(mk_definition(to_env_ref(e), to_name_ref(n), to_list_name_ref(p), to_expr_ref(t), to_expr_ref(v), static_cast(o)))); + LEAN_CATCH; +} + +lean_bool lean_decl_mk_thm(lean_name n, lean_list_name p, lean_expr t, lean_expr v, unsigned h, lean_decl * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + check_nonnull(p); + check_nonnull(t); + check_nonnull(v); + *r = of_decl(new declaration(mk_theorem(to_name_ref(n), to_list_name_ref(p), to_expr_ref(t), to_expr_ref(v), h))); + LEAN_CATCH; +} + +lean_bool lean_decl_mk_thm(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(e); + check_nonnull(n); + check_nonnull(p); + check_nonnull(t); + check_nonnull(v); + *r = of_decl(new declaration(mk_theorem(to_env_ref(e), to_name_ref(n), to_list_name_ref(p), to_expr_ref(t), to_expr_ref(v)))); + LEAN_CATCH; +} + +void lean_decl_decl(lean_decl d) { + delete to_decl(d); +} + +lean_decl_kind lean_decl_get_kind(lean_decl d) { + if (!d) + return LEAN_DECL_CONST; + if (to_decl_ref(d).is_theorem()) + return LEAN_DECL_THM; + else if (to_decl_ref(d).is_definition()) + return LEAN_DECL_DEF; + else if (to_decl_ref(d).is_axiom()) + return LEAN_DECL_AXIOM; + else if (to_decl_ref(d).is_constant_assumption()) + return LEAN_DECL_CONST; + else + return LEAN_DECL_CONST; +} + +lean_bool lean_decl_get_name(lean_decl d, lean_name * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(d); + *r = of_name(new name(to_decl_ref(d).get_name())); + LEAN_CATCH; +} + +lean_bool lean_decl_get_univ_params(lean_decl d, lean_list_name * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(d); + *r = of_list_name(new list(to_decl_ref(d).get_univ_params())); + LEAN_CATCH; +} + +lean_bool lean_decl_get_type(lean_decl d, lean_expr * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(d); + *r = of_expr(new expr(to_decl_ref(d).get_type())); + LEAN_CATCH; +} + +static void check_def_thm(lean_decl d) { + check_nonnull(d); + if (lean_decl_get_kind(d) != LEAN_DECL_DEF && lean_decl_get_kind(d) != LEAN_DECL_THM) + throw exception("invalid argument, definition or theorem expected"); +} + +lean_bool lean_decl_get_value(lean_decl d, lean_expr * r, lean_exception * ex) { + LEAN_TRY; + check_def_thm(d); + *r = of_expr(new expr(to_decl_ref(d).get_value())); + LEAN_CATCH; +} + +lean_bool lean_decl_get_height(lean_decl d, unsigned * r, lean_exception * ex) { + LEAN_TRY; + check_def_thm(d); + *r = to_decl_ref(d).get_height(); + LEAN_CATCH; +} + +static void check_def(lean_decl d) { + check_nonnull(d); + if (lean_decl_get_kind(d) != LEAN_DECL_DEF) + throw exception("invalid argument, definition expected"); +} + +lean_bool lean_decl_get_conv_opt(lean_decl d, lean_bool * r, lean_exception * ex) { + LEAN_TRY; + check_def(d); + *r = to_decl_ref(d).use_conv_opt(); + LEAN_CATCH; +} diff --git a/src/api/decl.h b/src/api/decl.h new file mode 100644 index 000000000..5f37ba6b5 --- /dev/null +++ b/src/api/decl.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 +*/ +#pragma once +#include "kernel/declaration.h" +#include "api/expr.h" +#include "api/lean_decl.h" +namespace lean { +inline declaration * to_decl(lean_decl n) { return reinterpret_cast(n); } +inline declaration const & to_decl_ref(lean_decl n) { return *reinterpret_cast(n); } +inline lean_decl of_decl(declaration * n) { return reinterpret_cast(n); } + +inline environment * to_env(lean_env n) { return reinterpret_cast(n); } +inline environment const & to_env_ref(lean_env n) { return *reinterpret_cast(n); } +inline lean_env of_env(environment * n) { return reinterpret_cast(n); } +} diff --git a/src/api/expr.h b/src/api/expr.h index 8476f3808..eac34fd97 100644 --- a/src/api/expr.h +++ b/src/api/expr.h @@ -5,12 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "util/name.h" #include "kernel/expr.h" -#include "api/exception.h" -#include "api/options.h" -#include "api/lean_name.h" -#include "api/lean_univ.h" +#include "api/univ.h" #include "api/lean_expr.h" namespace lean { inline expr * to_expr(lean_expr n) { return reinterpret_cast(n); } diff --git a/src/api/lean.h b/src/api/lean.h index 666e05cad..ed6f589e4 100644 --- a/src/api/lean.h +++ b/src/api/lean.h @@ -15,5 +15,6 @@ Author: Leonardo de Moura #include "lean_options.h" // NOLINT #include "lean_univ.h" // NOLINT #include "lean_expr.h" // NOLINT +#include "lean_decl.h" // NOLINT #endif diff --git a/src/api/lean_decl.h b/src/api/lean_decl.h new file mode 100644 index 000000000..93cee50c0 --- /dev/null +++ b/src/api/lean_decl.h @@ -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 +*/ +#ifndef _LEAN_DECL_H +#define _LEAN_DECL_H + +#ifdef __cplusplus +extern "C" { +#endif + +/** + \defgroup capi C API +*/ +/*@{*/ + +/** + @name Declaration API +*/ +/*@{*/ + +LEAN_DEFINE_TYPE(lean_env); +LEAN_DEFINE_TYPE(lean_decl); + +typedef enum { + LEAN_DECL_CONST, + LEAN_DECL_AXIOM, + LEAN_DECL_DEF, + LEAN_DECL_THM +} lean_decl_kind; + +/** \brief Create an axiom with name \c n, universe parameters names \c p, and type \c t + \remark Recall that declarations are universe polymorphic in Lean. */ +lean_bool lean_decl_mk_axiom(lean_name n, lean_list_name p, lean_expr t, lean_decl * r, lean_exception * ex); +/** \brief Create an constant with name \c n, universe parameters names \c p, and type \c t + \remark Constants and axioms are essentially the same thing in Lean. */ +lean_bool lean_decl_mk_const(lean_name n, lean_list_name p, lean_expr t, lean_decl * r, lean_exception * ex); +/** \brief Create a definition with name \c n, universe parameters names \c p, type \c t, value \c v, + definitional height \c h and a flag \c o indicating whether normalization will lazily unfold it or not. */ +lean_bool lean_decl_mk_def(lean_name n, lean_list_name p, lean_expr t, lean_expr v, unsigned h, lean_bool o, lean_decl * r, lean_exception * ex); +/** \brief Create a definition with name \c n, universe parameters names \c p, type \c t, value \c v, + and a flag \c o indicating whether normalization will lazily unfold it or not. + \remark The definitional height is computed using the information in the given environment. */ +lean_bool lean_decl_mk_def_with(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_bool o, lean_decl * r, lean_exception * ex); +/** \brief Create a theorem with name \c n, universe parameters names \c p, type \c t, value \c v, definitional height \c h \remark + Theorems and definitions are essentially the same thing in Lean. The main difference is how the normalizer treats them. The + normalizer will only unfold a theorem if there is nothing else to be done when checking whether two terms are definitionally equal + or not. */ +lean_bool lean_decl_mk_thm(lean_name n, lean_list_name p, lean_expr t, lean_expr v, unsigned h, lean_decl * r, lean_exception * ex); +/** \brief Create a theorem with name \c n, universe parameters names \c p, type \c t, value \c v, definitional height \c h \remark + Theorems and definitions are essentially the same thing in Lean. The main difference is how the normalizer treats them. The + normalizer will only unfold a theorem if there is nothing else to be done when checking whether two terms are definitionally equal + or not. + \remark The definitional height is computed using the information in the given environment. */ +lean_bool lean_decl_mk_thm_with(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex); + +/** \brief Delete/dispose the given declaration. */ +void lean_decl_decl(lean_decl d); +/** \brief Return the kind of the given declaration. + \remark Return LEAN_DECL_CONST if d is null. */ +lean_decl_kind lean_decl_get_kind(lean_decl d); + +/** \brief Store in \c r the name the given declaration. */ +lean_bool lean_decl_get_name(lean_decl d, lean_name * r, lean_exception * ex); +/** \brief Store in \c r the list of universe parameter names of the given declaration. */ +lean_bool lean_decl_get_univ_params(lean_decl d, lean_list_name * r, lean_exception * ex); +/** \brief Store in \c r the type of the given declaration. */ +lean_bool lean_decl_get_type(lean_decl d, lean_expr * r, lean_exception * ex); +/** \brief Store in \c r the value of the given theorem or definition. + \pre lean_decl_get_kind(d) == LEAN_DECL_THM || lean_decl_get_kind(d) == LEAN_DECL_DEF */ +lean_bool lean_decl_get_value(lean_decl d, lean_expr * r, lean_exception * ex); +/** \brief Store in \c r the definitional height of the given theorem or definition. + \pre lean_decl_get_kind(d) == LEAN_DECL_THM || lean_decl_get_kind(d) == LEAN_DECL_DEF */ +lean_bool lean_decl_get_height(lean_decl d, unsigned * r, lean_exception * ex); +/** \brief Store in \c r whether lazy unfolding is considered for the given definition. + \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); + +/*@}*/ +/*@}*/ + +#ifdef __cplusplus +}; +#endif +#endif diff --git a/src/api/lean_expr.h b/src/api/lean_expr.h index e80e5e5a4..1ba3fae62 100644 --- a/src/api/lean_expr.h +++ b/src/api/lean_expr.h @@ -93,7 +93,7 @@ lean_bool lean_expr_get_var_idx(lean_expr e, unsigned * i, lean_exception * ex); /** \brief Stgore in \c u the universe of the given sort. \pre lean_expr_get_kind(e) == LEAN_EXPR_SORT */ lean_bool lean_expr_get_sort_univ(lean_expr e, lean_univ * u, lean_exception * ex); -/** \brief Store in \c n the name the given constant. +/** \brief Store in \c n the name of the given constant. \pre lean_expr_get_kind(e) == LEAN_EXPR_CONST */ lean_bool lean_expr_get_const_name(lean_expr e, lean_name * n, lean_exception * ex); /** \brief Store in \c us the universes parameters of the given constant.