diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 54d9c3ff3..4ff20a2d2 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) +add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp univ.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 0d460be39..574aa63a6 100644 --- a/src/api/lean.h +++ b/src/api/lean.h @@ -13,5 +13,6 @@ Author: Leonardo de Moura #include "lean_exception.h" // NOLINT #include "lean_name.h" // NOLINT #include "lean_options.h" // NOLINT +#include "lean_univ.h" // NOLINT #endif diff --git a/src/api/lean_univ.h b/src/api/lean_univ.h new file mode 100644 index 000000000..d340eda56 --- /dev/null +++ b/src/api/lean_univ.h @@ -0,0 +1,106 @@ +/* +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_UNIV_H +#define _LEAN_UNIV_H + +#ifdef __cplusplus +extern "C" { +#endif + +/** + \defgroup capi C API +*/ +/*@{*/ + +/** + @name Universe API +*/ +/*@{*/ + +LEAN_DEFINE_TYPE(lean_univ); + +typedef enum { + LEAN_UNIV_ZERO, + LEAN_UNIV_SUCC, + LEAN_UNIV_MAX, + LEAN_UNIV_IMAX, + LEAN_UNIV_PARAM, + LEAN_UNIV_GLOBAL, + LEAN_UNIV_META +} lean_univ_kind; + +/** \brief Create the base universe zero */ +lean_bool lean_univ_mk_zero(lean_univ * r, lean_exception * ex); +/** \brief Create the successor universe */ +lean_bool lean_univ_mk_succ(lean_univ u, lean_univ * r, lean_exception * ex); +/** \brief r := max(u1, u2) */ +lean_bool lean_univ_mk_max(lean_univ u1, lean_univ u2, lean_univ * r, lean_exception * ex); +/** \brief r := imax(u1, u2) */ +lean_bool lean_univ_mk_imax(lean_univ u1, lean_univ u2, lean_univ * r, lean_exception * ex); +/** \brief Create a universe parameter with the given name. */ +lean_bool lean_univ_mk_param(lean_name n, lean_univ * r, lean_exception * ex); +/** \brief Create a reference to a global universe with the given name. */ +lean_bool lean_univ_mk_global(lean_name n, lean_univ * r, lean_exception * ex); +/** \brief Create a universe meta-variable with the given name. */ +lean_bool lean_univ_mk_meta(lean_name n, lean_univ * r, lean_exception * ex); + +/** \brief Store in \c r a string representation of the given options object. + \remark \c r must be deleted using #lean_string_del */ +lean_bool lean_univ_to_string(lean_univ u, char const ** r, lean_exception * ex); + +/** \brief Similar to \c lean_univ_to_string, but uses pretty printing options in \c o, + when converting objection into a string. */ +lean_bool lean_univ_to_string_using(lean_univ u, lean_options o, char const ** r, lean_exception * ex); +/** \brief Delete/dispose the given universe object. */ +void lean_univ_del(lean_univ u); +/** \brief Return the kind of the given universe. + \remark Return LEAN_UNIV_ZERO if u is null. */ +lean_univ_kind lean_univ_get_kind(lean_univ u); + +/** \brief Store \c lean_true in \c r iff the two given universe object are equal. */ +lean_bool lean_univ_eq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex); +/** \brief If \c r contains \c lean_true, then forall assignments \c A that assigns all parameters, + globals and metavariables occuring in \c u1 and \c u2, we have that the + universe level u1[A] is bigger or equal to u2[A]. */ +lean_bool lean_univ_geq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex); + +/** \brief Store the predecessor universe of \c u in \c r. + \pre lean_univ_get_kind(u) == LEAN_UNIV_SUCC +*/ +lean_bool lean_univ_get_pred(lean_univ u, lean_univ * r, lean_exception * ex); +/** \brief Store the left-hand-side of the max/imax universe \c u in \c r. + \pre lean_univ_get_kind(u) == LEAN_UNIV_MAX || lean_univ_get_kind(u) == LEAN_UNIV_IMAX +*/ + +lean_bool lean_univ_get_max_lhs(lean_univ u, lean_univ * r, lean_exception * ex); +/** \brief Store the right-hand-side of the max/imax universe \c u in \c r. + \pre lean_univ_get_kind(u) == LEAN_UNIV_MAX || lean_univ_get_kind(u) == LEAN_UNIV_IMAX +*/ +lean_bool lean_univ_get_max_rhs(lean_univ u, lean_univ * r, lean_exception * ex); +/** \brief Store the name of the given universe in \c r. + \pre lean_univ_get_kind(u) == LEAN_UNIV_PARAM || + lean_univ_get_kind(u) == LEAN_UNIV_GLOBAL || + lean_univ_get_kind(u) == LEAN_UNIV_META +*/ +lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex); +/** \brief Store in \c r the normal for of the given universe */ +lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex); + +/** \brief Instantiate the universe parameters names ns[i] with us[i] in \c u, + and store the result in \c r. + \remark \c ns and \c us are arrays of names and universes, and both have size \c sz. +*/ +lean_bool lean_univ_instantiate(lean_univ u, unsigned sz, lean_name const * ns, lean_univ const * us, + lean_univ * r, lean_exception * ex); + +/*@}*/ +/*@}*/ + +#ifdef __cplusplus +}; +#endif +#endif diff --git a/src/api/name.cpp b/src/api/name.cpp index 22d29fde8..866856786 100644 --- a/src/api/name.cpp +++ b/src/api/name.cpp @@ -7,6 +7,16 @@ Author: Leonardo de Moura #include "api/name.h" #include "api/string.h" #include "api/exception.h" +namespace lean { +void to_buffer(unsigned sz, lean_name const * ns, buffer & r) { + check_nonnull(ns); + for (unsigned i = 0; i < sz; i++) { + check_nonnull(ns[i]); + r.push_back(to_name_ref(ns[i])); + } +} +} + using namespace lean; // NOLINT lean_bool lean_name_mk_anonymous(lean_name * r, lean_exception * ex) { diff --git a/src/api/name.h b/src/api/name.h index 07793c88d..12d6156f2 100644 --- a/src/api/name.h +++ b/src/api/name.h @@ -12,4 +12,5 @@ namespace lean { inline name * to_name(lean_name n) { return reinterpret_cast(n); } inline name const & to_name_ref(lean_name n) { return *reinterpret_cast(n); } inline lean_name of_name(name * n) { return reinterpret_cast(n); } +void to_buffer(unsigned sz, lean_name const * ns, buffer & r); } diff --git a/src/api/univ.cpp b/src/api/univ.cpp new file mode 100644 index 000000000..2743c4298 --- /dev/null +++ b/src/api/univ.cpp @@ -0,0 +1,196 @@ +/* +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 +#include "util/sstream.h" +#include "api/name.h" +#include "api/string.h" +#include "api/univ.h" +#include "api/lean_univ.h" +namespace lean { +void to_buffer(unsigned sz, lean_univ const * us, buffer & r) { + check_nonnull(us); + for (unsigned i = 0; i < sz; i++) { + check_nonnull(us[i]); + r.push_back(to_level_ref(us[i])); + } +} +} +using namespace lean; // NOLINT + +lean_bool lean_univ_mk_zero(lean_univ * r, lean_exception * ex) { + LEAN_TRY; + *r = of_level(new level()); + LEAN_CATCH; +} + +lean_bool lean_univ_mk_succ(lean_univ u, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + *r = of_level(new level(mk_succ(to_level_ref(u)))); + LEAN_CATCH; +} + +lean_bool lean_univ_mk_max(lean_univ u1, lean_univ u2, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u1); + check_nonnull(u2); + *r = of_level(new level(mk_max(to_level_ref(u1), to_level_ref(u2)))); + LEAN_CATCH; +} + +lean_bool lean_univ_mk_imax(lean_univ u1, lean_univ u2, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u1); + check_nonnull(u2); + *r = of_level(new level(mk_imax(to_level_ref(u1), to_level_ref(u2)))); + LEAN_CATCH; +} + +lean_bool lean_univ_mk_param(lean_name n, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + *r = of_level(new level(mk_param_univ(to_name_ref(n)))); + LEAN_CATCH; +} + +lean_bool lean_univ_mk_global(lean_name n, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + *r = of_level(new level(mk_global_univ(to_name_ref(n)))); + LEAN_CATCH; +} + +lean_bool lean_univ_mk_meta(lean_name n, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(n); + *r = of_level(new level(mk_meta_univ(to_name_ref(n)))); + LEAN_CATCH; +} + +lean_bool lean_univ_to_string(lean_univ u, char const ** r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + std::ostringstream out; + out << pp(to_level_ref(u)); + *r = mk_string(out.str()); + LEAN_CATCH; +} + +lean_bool lean_univ_to_string_using(lean_univ u, lean_options o, char const ** r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + check_nonnull(o); + std::ostringstream out; + out << mk_pair(pp(to_level_ref(u), to_options_ref(o)), to_options_ref(o)); + *r = mk_string(out.str()); + LEAN_CATCH; +} + +void lean_univ_del(lean_univ u) { + delete to_level(u); +} + +lean_univ_kind lean_univ_get_kind(lean_univ u) { + if (!u) + return LEAN_UNIV_ZERO; + switch (to_level_ref(u).kind()) { + case level_kind::Zero: return LEAN_UNIV_ZERO; + case level_kind::Succ: return LEAN_UNIV_SUCC; + case level_kind::Max: return LEAN_UNIV_MAX; + case level_kind::IMax: return LEAN_UNIV_IMAX; + case level_kind::Param: return LEAN_UNIV_PARAM; + case level_kind::Global: return LEAN_UNIV_GLOBAL; + case level_kind::Meta: return LEAN_UNIV_META; + } + lean_unreachable(); +} + +lean_bool lean_univ_eq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u1); + check_nonnull(u2); + *r = to_level_ref(u1) == to_level_ref(u2); + LEAN_CATCH; +} + +lean_bool lean_univ_geq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u1); + check_nonnull(u2); + *r = is_geq(to_level_ref(u1), to_level_ref(u2)); + LEAN_CATCH; +} + +lean_bool lean_univ_get_pred(lean_univ u, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + if (lean_univ_get_kind(u) != LEAN_UNIV_SUCC) + throw exception("invalid argument, argument is not a successor universe"); + *r = of_level(new level(succ_of(to_level_ref(u)))); + LEAN_CATCH; +} + +lean_bool lean_univ_get_max_lhs(lean_univ u, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + if (lean_univ_get_kind(u) == LEAN_UNIV_MAX) + *r = of_level(new level(max_lhs(to_level_ref(u)))); + else if (lean_univ_get_kind(u) == LEAN_UNIV_IMAX) + *r = of_level(new level(imax_lhs(to_level_ref(u)))); + else + throw exception("invalid argument, argument is not a max/imax universe"); + LEAN_CATCH; +} + +lean_bool lean_univ_get_max_rhs(lean_univ u, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + if (lean_univ_get_kind(u) == LEAN_UNIV_MAX) + *r = of_level(new level(max_rhs(to_level_ref(u)))); + else if (lean_univ_get_kind(u) == LEAN_UNIV_IMAX) + *r = of_level(new level(imax_rhs(to_level_ref(u)))); + else + throw exception("invalid argument, argument is not a max/imax universe"); + LEAN_CATCH; +} + +lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + if (lean_univ_get_kind(u) == LEAN_UNIV_PARAM) + *r = of_name(new name(param_id(to_level_ref(u)))); + else if (lean_univ_get_kind(u) == LEAN_UNIV_GLOBAL) + *r = of_name(new name(global_id(to_level_ref(u)))); + else if (lean_univ_get_kind(u) == LEAN_UNIV_META) + *r = of_name(new name(meta_id(to_level_ref(u)))); + else + throw exception("invalid argument, argument is not a parameter/global/meta universe"); + LEAN_CATCH; +} + +lean_bool lean_univ_normalize(lean_univ u, lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + *r = of_level(new level(normalize(to_level_ref(u)))); + LEAN_CATCH; +} + +/** \brief Instantiate the universe parameters names ns[i] with us[i] in \c u, + and store the result in \c r. + \remark \c ns and \c us are arrays of names and universes, and both have size \c sz. +*/ +lean_bool lean_univ_instantiate(lean_univ u, unsigned sz, lean_name const * ns, lean_univ const * us, + lean_univ * r, lean_exception * ex) { + LEAN_TRY; + check_nonnull(u); + buffer tmp_ns; + buffer tmp_us; + to_buffer(sz, ns, tmp_ns); + to_buffer(sz, us, tmp_us); + *r = of_level(new level(instantiate(to_level_ref(u), to_list(tmp_ns), to_list(tmp_us)))); + LEAN_CATCH; +} diff --git a/src/api/univ.h b/src/api/univ.h new file mode 100644 index 000000000..4129d1c4b --- /dev/null +++ b/src/api/univ.h @@ -0,0 +1,18 @@ +/* +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 "util/name.h" +#include "kernel/level.h" +#include "api/exception.h" +#include "api/options.h" +#include "api/lean_univ.h" +namespace lean { +inline level * to_level(lean_univ n) { return reinterpret_cast(n); } +inline level const & to_level_ref(lean_univ n) { return *reinterpret_cast(n); } +inline lean_univ of_level(level * n) { return reinterpret_cast(n); } +void to_buffer(unsigned sz, lean_univ const * us, buffer & r); +}