michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(api): expose universe expressions in the C API

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-18 15:07:44 -07:00
parent 0909c8f08f
commit d627414f9b
7 changed files with 333 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/CMakeLists.txt
View file

@ -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)

1
src/api/lean.h
View file

@ -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

106
src/api/lean_univ.h Normal file
View file

@ -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 <tt>ns[i]</tt> with <tt>us[i]</tt> 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

10
src/api/name.cpp
View file

@ -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<name> & 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) {

1
src/api/name.h
View file

@ -12,4 +12,5 @@ namespace lean {
inline name * to_name(lean_name n) { return reinterpret_cast<name *>(n); }
inline name const & to_name_ref(lean_name n) { return *reinterpret_cast<name *>(n); }
inline lean_name of_name(name * n) { return reinterpret_cast<lean_name>(n); }
void to_buffer(unsigned sz, lean_name const * ns, buffer<name> & r);
}

196
src/api/univ.cpp Normal file
View file

@ -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 <string>
#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<level> & 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 <tt>ns[i]</tt> with <tt>us[i]</tt> 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<name> tmp_ns;
buffer<level> 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;
}

18
src/api/univ.h Normal file
View file

@ -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<level *>(n); }
inline level const & to_level_ref(lean_univ n) { return *reinterpret_cast<level *>(n); }
inline lean_univ of_level(level * n) { return reinterpret_cast<lean_univ>(n); }
void to_buffer(unsigned sz, lean_univ const * us, buffer<level> & r);
}