From bdd8fae14d093372d0246b6ad689cf59fb286aac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Aug 2015 13:01:48 -0700 Subject: [PATCH] feat(api): add lean_inductive API --- src/api/CMakeLists.txt | 2 +- src/api/inductive.cpp | 189 +++++++++++++++++++++++++++++++++++++++ src/api/inductive.h | 28 ++++++ src/api/lean.h | 1 + src/api/lean_inductive.h | 91 +++++++++++++++++++ 5 files changed, 310 insertions(+), 1 deletion(-) create mode 100644 src/api/inductive.cpp create mode 100644 src/api/inductive.h create mode 100644 src/api/lean_inductive.h diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 9294ffaba..82852d39c 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 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) diff --git a/src/api/inductive.cpp b/src/api/inductive.cpp new file mode 100644 index 000000000..484df13c4 --- /dev/null +++ b/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()); + 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(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(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 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; +} diff --git a/src/api/inductive.h b/src/api/inductive.h new file mode 100644 index 000000000..abdf0b56b --- /dev/null +++ b/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(n); } +inline inductive_decl const & to_inductive_type_ref(lean_inductive_type n) { return *reinterpret_cast(n); } +inline lean_inductive_type of_inductive_type(inductive_decl * n) { return reinterpret_cast(n); } + +inline list * to_list_inductive_type(lean_list_inductive_type n) { return reinterpret_cast *>(n); } +inline list const & to_list_inductive_type_ref(lean_list_inductive_type n) { return *reinterpret_cast *>(n); } +inline lean_list_inductive_type of_list_inductive_type(list * n) { return reinterpret_cast(n); } + +inline inductive_decls * to_inductive_decl(lean_inductive_decl n) { return reinterpret_cast(n); } +inline inductive_decls const & to_inductive_decl_ref(lean_inductive_decl n) { return *reinterpret_cast(n); } +inline lean_inductive_decl of_inductive_decl(inductive_decls * n) { return reinterpret_cast(n); } +} diff --git a/src/api/lean.h b/src/api/lean.h index a7b9c5475..8e954b332 100644 --- a/src/api/lean.h +++ b/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 diff --git a/src/api/lean_inductive.h b/src/api/lean_inductive.h new file mode 100644 index 000000000..6c26f9537 --- /dev/null +++ b/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 h :: t */ +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