From e8e315ff142583d14a4ee0add9f9692056c6ad9c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Aug 2015 11:01:46 -0700 Subject: [PATCH] refactor(api): uniform names --- src/api/exception.cpp | 6 ++--- src/api/lean_exception.h | 8 +++--- src/api/lean_name.h | 41 +++++++++++++++--------------- src/api/lean_string.h | 2 +- src/api/name.cpp | 24 +++++++++--------- src/api/string.cpp | 2 +- src/tests/shared/name.c | 54 ++++++++++++++++++++-------------------- 7 files changed, 69 insertions(+), 68 deletions(-) diff --git a/src/api/exception.cpp b/src/api/exception.cpp index 074acb91e..93ca5e311 100644 --- a/src/api/exception.cpp +++ b/src/api/exception.cpp @@ -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; diff --git a/src/api/lean_exception.h b/src/api/lean_exception.h index d10d4e1d6..6aad6e217 100644 --- a/src/api/lean_exception.h +++ b/src/api/lean_exception.h @@ -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 }; diff --git a/src/api/lean_name.h b/src/api/lean_name.h index 13c9dc4a8..8f430f51b 100644 --- a/src/api/lean_name.h +++ b/src/api/lean_name.h @@ -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 pre.s - \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 pre.i. - \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 pre.s 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 pre.i 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 }; diff --git a/src/api/lean_string.h b/src/api/lean_string.h index 4a2b045f6..c83832b00 100644 --- a/src/api/lean_string.h +++ b/src/api/lean_string.h @@ -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 }; diff --git a/src/api/name.cpp b/src/api/name.cpp index 204924fd8..22d29fde8 100644 --- a/src/api/name.cpp +++ b/src/api/name.cpp @@ -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; diff --git a/src/api/string.cpp b/src/api/string.cpp index fc671017f..50fc3e1fd 100644 --- a/src/api/string.cpp +++ b/src/api/string.cpp @@ -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); } diff --git a/src/tests/shared/name.c b/src/tests/shared/name.c index b5c15f2f3..e8b09d6c9 100644 --- a/src/tests/shared/name.c +++ b/src/tests/shared/name.c @@ -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; }