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

refactor(util/name): move string_to_name to name module

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-04 13:09:42 -07:00
parent b5b68613b1
commit d75a4739e4
3 changed files with 17 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/server.cpp
View file

@ -460,20 +460,6 @@ void server::show(bool valid) {
m_out << "-- ENDSHOW" << std::endl;
}
static name string_to_name(std::string const & str) {
name result;
std::string id_part;
for (unsigned i = 0; i < str.size(); i++) {
if (str[i] == '.') {
result = name(result, id_part.c_str());
id_part.clear();
} else {
id_part.push_back(str[i]);
}
}
return name(result, id_part.c_str());
}
// Return true iff the last part of p is a prefix of the last part of n
static bool is_last_prefix_of(name const & p, name const & n) {
if (p.is_string() && n.is_string()) {

15
src/util/name.cpp
View file

@ -402,6 +402,21 @@ name name::replace_prefix(name const & prefix, name const & new_prefix) const {
return name(p, get_numeral());
}
name string_to_name(std::string const & str) {
static_assert(*(lean_name_separator+1) == 0, "this function assumes the length of lean_name_separator is 1");
name result;
std::string id_part;
for (unsigned i = 0; i < str.size(); i++) {
if (str[i] == lean_name_separator[0]) {
result = name(result, id_part.c_str());
id_part.clear();
} else {
id_part.push_back(str[i]);
}
}
return name(result, id_part.c_str());
}
enum name_ll_kind { LL_ANON = 0, LL_STRING = 1, LL_INT = 2, LL_STRING_PREFIX = 3, LL_INT_PREFIX = 4 };
name_ll_kind ll_kind(name const & n) {
if (n.is_anonymous())

2
src/util/name.h
View file

@ -156,6 +156,8 @@ public:
struct ptr_eq { bool operator()(name const & n1, name const & n2) const { return n1.m_ptr == n2.m_ptr; } };
};
name string_to_name(std::string const & str);
struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } };
struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } };
struct name_cmp { int operator()(name const & n1, name const & n2) const { return cmp(n1, n2); } };