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

refactor(api): uniform names

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-18 11:01:46 -07:00
parent 617f55b947
commit e8e315ff14
7 changed files with 69 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/exception.cpp
View file

@ -20,14 +20,14 @@ void check_nonnull(void const * ptr) {
}
}
void lean_del_exception(lean_exception e) {
void lean_exception_del(lean_exception e) {
lean::throwable * t = lean::to_exception(e);
if (t != lean::get_memout_exception()) {
delete t;
}
}
char const * lean_get_exception_message(lean_exception e) {
char const * lean_exception_get_message(lean_exception e) {
if (!e)
return 0;
try {
@ -37,7 +37,7 @@ char const * lean_get_exception_message(lean_exception e) {
}
}
lean_exception_kind lean_get_exception_kind(lean_exception e) {
lean_exception_kind lean_exception_get_kind(lean_exception e) {
lean::throwable * ex = lean::to_exception(e);
if (!ex)
return LEAN_NULL_EXCEPTION;

8
src/api/lean_exception.h
View file

@ -16,17 +16,17 @@ LEAN_DEFINE_TYPE(lean_exception);
/** \brief Delete an exception object allocated by Lean.
This is a NOOP if \c e is null.
*/
void lean_del_exception(lean_exception e);
void lean_exception_del(lean_exception e);
/** \brief Return basic string/message describing the exception.
\remark The string must be deallocated using #lean_del_string.
\remark The string must be deallocated using #lean_string_del.
\remark After we define the Lean environment object, we can
provide richer messages.
\remark The result is null if the operation failed or \c e is null.
*/
char const * lean_get_exception_message(lean_exception e);
char const * lean_exception_get_message(lean_exception e);
typedef enum {
LEAN_NULL_EXCEPTION, // null (aka there is no exception)
@ -38,7 +38,7 @@ typedef enum {
} lean_exception_kind;
/** \brief Return the kind of the given exception. */
lean_exception_kind lean_get_exception_kind(lean_exception e);
lean_exception_kind lean_exception_get_kind(lean_exception e);
#ifdef __cplusplus
};

41
src/api/lean_name.h
View file

@ -14,41 +14,42 @@ extern "C" {
LEAN_DEFINE_TYPE(lean_name);
/** \brief Create the anonymous name */
lean_bool lean_mk_anonymous_name(lean_name * r, lean_exception * e);
lean_bool lean_name_mk_anonymous(lean_name * r, lean_exception * ex);
/** \brief Create the name <tt>pre.s</tt>
\remark \c r must be disposed using #lean_del_name */
lean_bool lean_mk_str_name(lean_name pre, char const * s, lean_name * r, lean_exception * e);
\remark \c r must be disposed using #lean_name_del */
lean_bool lean_name_mk_str(lean_name pre, char const * s, lean_name * r, lean_exception * ex);
/** \brief Create the name <tt>pre.i</tt>.
\pre !lean_is_anonymous_name(pre)
\remark \c r must be disposed using #lean_del_name */
lean_bool lean_mk_idx_name(lean_name pre, unsigned i, lean_name * r, lean_exception * e);
void lean_del_name(lean_name n);
\pre !lean_name_is_anonymous(pre)
\remark \c r must be disposed using #lean_name_del */
lean_bool lean_name_mk_idx(lean_name pre, unsigned i, lean_name * r, lean_exception * ex);
/** \brief Delete/dispose a Lean hierarchical name */
void lean_name_del(lean_name n);
/** \brief Return lean_true iff \c n is the anonymous */
lean_bool lean_is_anonymous_name(lean_name n);
lean_bool lean_name_is_anonymous(lean_name n);
/** \brief Return lean_true iff \c n is a name of the form <tt>pre.s</tt> where \c s is a string. */
lean_bool lean_is_str_name(lean_name n);
lean_bool lean_name_is_str(lean_name n);
/** \brief Return lean_true iff \c n is a name of the form <tt>pre.i</tt> where \c i is an unsigned integer. */
lean_bool lean_is_idx_name(lean_name n);
lean_bool lean_name_is_idx(lean_name n);
/** \brief Return true iff the two given hierarchical names are equal */
lean_bool lean_name_eq(lean_name n1, lean_name n2);
/** \brief Return the prefix of the given name.
\pre !lean_is_anonymous_name(n)
\pre !lean_name_is_anonymous(n)
*/
lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * e);
lean_bool lean_name_get_prefix(lean_name n, lean_name * r, lean_exception * ex);
/** \brief Store in \c r the suffix of the given name as a string.
\pre lean_is_str_name(n)
\remark \c r must be disposed using #lean_del_name
\pre lean_name_is_str(n)
\remark \c r must be disposed using #lean_name_del
*/
lean_bool lean_get_name_str(lean_name n, char const ** r, lean_exception * e);
lean_bool lean_name_get_str(lean_name n, char const ** r, lean_exception * ex);
/** \brief Store in \c r the suffix of the given name as a unsigned integer.
\pre lean_is_idx_name(n)
\remark \c r must be deleted using #lean_del_string
\pre lean_name_is_idx(n)
\remark \c r must be deleted using #lean_string_del
*/
lean_bool lean_get_name_idx(lean_name n, unsigned * r, lean_exception * e);
lean_bool lean_name_get_idx(lean_name n, unsigned * r, lean_exception * ex);
/** \brief Store in \c r a string representation of the given hierarchical name.
\remark \c r must be deleted using #lean_del_string
\remark \c r must be deleted using #lean_string_del
*/
lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * e);
lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex);
#ifdef __cplusplus
};

2
src/api/lean_string.h
View file

@ -11,7 +11,7 @@ extern "C" {
#endif
/** \brief Delete a string allocated by Lean */
void lean_del_string(char const * s);
void lean_string_del(char const * s);
#ifdef __cplusplus
};

24
src/api/name.cpp
View file

@ -9,13 +9,13 @@ Author: Leonardo de Moura
#include "api/exception.h"
using namespace lean; // NOLINT
lean_bool lean_mk_anonymous_name(lean_name * r, lean_exception * ex) {
lean_bool lean_name_mk_anonymous(lean_name * r, lean_exception * ex) {
LEAN_TRY;
*r = of_name(new name());
LEAN_CATCH;
}
lean_bool lean_mk_str_name(lean_name pre, char const * s, lean_name * r, lean_exception * ex) {
lean_bool lean_name_mk_str(lean_name pre, char const * s, lean_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(pre);
check_nonnull(s);
@ -23,7 +23,7 @@ lean_bool lean_mk_str_name(lean_name pre, char const * s, lean_name * r, lean_ex
LEAN_CATCH;
}
lean_bool lean_mk_idx_name(lean_name pre, unsigned i, lean_name * r, lean_exception * ex) {
lean_bool lean_name_mk_idx(lean_name pre, unsigned i, lean_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(pre);
name const & p = to_name_ref(pre);
@ -33,19 +33,19 @@ lean_bool lean_mk_idx_name(lean_name pre, unsigned i, lean_name * r, lean_except
LEAN_CATCH;
}
void lean_del_name(lean_name n) {
void lean_name_del(lean_name n) {
delete to_name(n);
}
lean_bool lean_is_anonymous_name(lean_name n) {
lean_bool lean_name_is_anonymous(lean_name n) {
return n && to_name_ref(n).is_anonymous();
}
lean_bool lean_is_str_name(lean_name n) {
lean_bool lean_name_is_str(lean_name n) {
return n && to_name_ref(n).is_string();
}
lean_bool lean_is_idx_name(lean_name n) {
lean_bool lean_name_is_idx(lean_name n) {
return n && to_name_ref(n).is_numeral();
}
@ -53,7 +53,7 @@ lean_bool lean_name_eq(lean_name n1, lean_name n2) {
return n1 && n2 && to_name_ref(n1) == to_name_ref(n2);
}
lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * ex) {
lean_bool lean_name_get_prefix(lean_name n, lean_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(n);
if (to_name_ref(n).is_anonymous())
@ -65,19 +65,19 @@ lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * ex)
LEAN_CATCH;
}
lean_bool lean_get_name_str(lean_name n, char const ** r, lean_exception * ex) {
lean_bool lean_name_get_str(lean_name n, char const ** r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(n);
if (!lean_is_str_name(n))
if (!lean_name_is_str(n))
throw lean::exception("invalid argument, it is not a string name");
*r = mk_string(to_name_ref(n).get_string());
LEAN_CATCH;
}
lean_bool lean_get_name_idx(lean_name n, unsigned * r, lean_exception * ex) {
lean_bool lean_name_get_idx(lean_name n, unsigned * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(n);
if (!lean_is_idx_name(n))
if (!lean_name_is_idx(n))
throw lean::exception("invalid argument, it is not an indexed name");
*r = to_name_ref(n).get_numeral();
LEAN_CATCH;

2
src/api/string.cpp
View file

@ -32,6 +32,6 @@ void del_string(char const * s) {
}
}
void lean_del_string(char const * s) {
void lean_string_del(char const * s) {
lean::del_string(s);
}

54
src/tests/shared/name.c
View file

@ -12,12 +12,12 @@ void check(int v) {
void anonymous_unique() {
lean_exception ex;
lean_name a1, a2;
check(lean_mk_anonymous_name(&a1, &ex));
check(lean_mk_anonymous_name(&a2, &ex));
check(lean_name_mk_anonymous(&a1, &ex));
check(lean_name_mk_anonymous(&a2, &ex));
check(lean_name_eq(a1, a2));
lean_del_name(a1);
lean_del_name(a2);
lean_del_exception(ex);
lean_name_del(a1);
lean_name_del(a2);
lean_exception_del(ex);
}
int main() {
@ -28,35 +28,35 @@ int main() {
char const * s3;
unsigned idx;
printf("Started name test\n");
check(lean_mk_anonymous_name(&a, &ex));
check(lean_is_anonymous_name(a));
check(lean_mk_str_name(a, "foo", &n1, &ex));
check(lean_mk_str_name(n1, "bla", &n2, &ex));
check(lean_name_mk_anonymous(&a, &ex));
check(lean_name_is_anonymous(a));
check(lean_name_mk_str(a, "foo", &n1, &ex));
check(lean_name_mk_str(n1, "bla", &n2, &ex));
check(lean_name_to_string(n2, &s1, &ex));
printf("Lean name: %s\n", s1);
check(lean_is_str_name(n2));
check(!lean_is_anonymous_name(n2));
check(!lean_is_idx_name(n2));
check(lean_mk_idx_name(n2, 1, &n3, &ex));
check(lean_name_is_str(n2));
check(!lean_name_is_anonymous(n2));
check(!lean_name_is_idx(n2));
check(lean_name_mk_idx(n2, 1, &n3, &ex));
check(lean_name_to_string(n3, &s2, &ex));
printf("Lean name: %s\n", s2);
check(lean_is_idx_name(n3));
check(lean_get_name_prefix(n3, &n4, &ex));
check(lean_name_is_idx(n3));
check(lean_name_get_prefix(n3, &n4, &ex));
check(lean_name_eq(n2, n4));
check(lean_get_name_idx(n3, &idx, &ex));
check(lean_name_get_idx(n3, &idx, &ex));
check(idx == 1);
check(!lean_get_name_prefix(a, &n5, &ex));
s3 = lean_get_exception_message(ex);
check(!lean_name_get_prefix(a, &n5, &ex));
s3 = lean_exception_get_message(ex);
printf("Lean exception: %s\n", s3);
anonymous_unique();
lean_del_name(a);
lean_del_name(n1);
lean_del_name(n2);
lean_del_name(n3);
lean_del_name(n4);
lean_del_string(s1);
lean_del_string(s2);
lean_del_string(s3);
lean_del_exception(ex);
lean_name_del(a);
lean_name_del(n1);
lean_name_del(n2);
lean_name_del(n3);
lean_name_del(n4);
lean_string_del(s1);
lean_string_del(s2);
lean_string_del(s3);
lean_exception_del(ex);
return 0;
}