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

feat(api/name): add lean_list_name API

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

15
src/api/lean_name.h
View file

@ -60,6 +60,21 @@ lean_bool lean_name_get_idx(lean_name n, unsigned * r, lean_exception * ex);
*/ */
lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex); lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex);
LEAN_DEFINE_TYPE(lean_list_name);
/** \brief Create the empty list of names */
lean_bool lean_list_name_mk_nil(lean_list_name * r, lean_exception * ex);
/** \brief Create the list <tt>h :: t</tt> */
lean_bool lean_list_name_mk_cons(lean_name h, lean_list_name t, lean_list_name * r, lean_exception * ex);
/** \brief Delete/dispose the given list of names */
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 */
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 */
lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex);
/*@}*/ /*@}*/
/*@}*/ /*@}*/

36
src/api/name.cpp
View file

@ -99,3 +99,39 @@ lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex)
*r = mk_string(to_name_ref(n).to_string()); *r = mk_string(to_name_ref(n).to_string());
LEAN_CATCH; LEAN_CATCH;
} }
lean_bool lean_list_name_mk_nil(lean_list_name * r, lean_exception * ex) {
LEAN_TRY;
*r = of_list_name(new list<name>());
LEAN_CATCH;
}
lean_bool lean_list_name_mk_cons(lean_name h, lean_list_name t, lean_list_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(h);
check_nonnull(t);
*r = of_list_name(new list<name>(to_name_ref(h), to_list_name_ref(t)));
LEAN_CATCH;
}
void lean_list_name_del(lean_list_name l) {
delete to_list_name(l);
}
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_head(lean_list_name l, lean_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(l);
*r = of_name(new name(head(to_list_name_ref(l))));
LEAN_CATCH;
}
lean_bool lean_list_name_tail(lean_list_name l, lean_list_name * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(l);
*r = of_list_name(new list<name>(tail(to_list_name_ref(l))));
LEAN_CATCH;
}

4
src/api/name.h
View file

@ -13,4 +13,8 @@ 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 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); } 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); void to_buffer(unsigned sz, lean_name const * ns, buffer<name> & r);
inline list<name> * to_list_name(lean_list_name n) { return reinterpret_cast<list<name> *>(n); }
inline list<name> const & to_list_name_ref(lean_list_name n) { return *reinterpret_cast<list<name> *>(n); }
inline lean_list_name of_list_name(list<name> * n) { return reinterpret_cast<lean_list_name>(n); }
} }