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

test(tests/shared/name): add tests for lean_list_name API

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-21 15:12:21 -07:00
parent adeba5c05e
commit 35d3c6f5a5
3 changed files with 33 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/lean_name.h
View file

@ -70,9 +70,13 @@ lean_bool lean_list_name_mk_cons(lean_name h, lean_list_name t, lean_list_name *
void lean_list_name_del(lean_list_name l);
/** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
lean_bool lean_list_name_is_cons(lean_list_name l);
/** \brief Store in \c r the head of the given list */
/** \brief Return true iff the two given lists are equal */
lean_bool lean_list_name_eq(lean_list_name n1, lean_list_name n2);
/** \brief Store in \c r the head of the given list
\pre lean_list_name_is_cons(l) */
lean_bool lean_list_name_head(lean_list_name l, lean_name * r, lean_exception * ex);
/** \brief Store in \c r the tail of the given list */
/** \brief Store in \c r the tail of the given list
\pre lean_list_name_is_cons(l) */
lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex);
/*@}*/

8
src/api/name.cpp
View file

@ -122,9 +122,15 @@ lean_bool lean_list_name_is_cons(lean_list_name l) {
return l && !is_nil(to_list_name_ref(l));
}
lean_bool lean_list_name_eq(lean_list_name l1, lean_list_name l2) {
return l1 && l2 && to_list_name_ref(l1) == to_list_name_ref(l2);
}
lean_bool lean_list_name_head(lean_list_name l, lean_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(l);
if (!lean_list_name_is_cons(l))
throw lean::exception("invalid argument, non-nil list expected");
*r = of_name(new name(head(to_list_name_ref(l))));
LEAN_CATCH;
}
@ -132,6 +138,8 @@ lean_bool lean_list_name_head(lean_list_name l, lean_name * r, lean_exception *
lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(l);
if (!lean_list_name_is_cons(l))
throw lean::exception("invalid argument, non-nil list expected");
*r = of_list_name(new list<name>(tail(to_list_name_ref(l))));
LEAN_CATCH;
}

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

@ -29,10 +29,11 @@ void anonymous_unique() {
int main() {
lean_exception ex;
lean_name a, n1, n2, n3, n4, n5;
lean_name a, n1, n2, n3, n4, n5, n6;
char const * s1;
char const * s2;
char const * s3;
lean_list_name l1, l2, l3, l4;
unsigned idx;
printf("Started name test\n");
check(lean_name_mk_anonymous(&a, &ex));
@ -55,12 +56,29 @@ int main() {
check(!lean_name_get_prefix(a, &n5, &ex));
s3 = lean_exception_get_message(ex);
printf("Lean exception: %s\n", s3);
check(lean_list_name_mk_nil(&l1, &ex));
check(!lean_list_name_is_cons(l1));
check(lean_list_name_mk_cons(n1, l1, &l2, &ex));
check(lean_list_name_is_cons(l2));
check(lean_list_name_mk_cons(n2, l2, &l3, &ex));
check(lean_list_name_head(l3, &n6, &ex));
check(lean_name_eq(n6, n2));
check(lean_list_name_tail(l3, &l4, &ex));
check(lean_list_name_eq(l4, l2));
anonymous_unique();
lean_name_del(a);
lean_name_del(n1);
lean_name_del(n2);
lean_name_del(n3);
lean_name_del(n4);
lean_name_del(n5);
lean_name_del(n6);
lean_list_name_del(l1);
lean_list_name_del(l2);
lean_list_name_del(l3);
lean_list_name_del(l4);
lean_string_del(s1);
lean_string_del(s2);
lean_string_del(s3);