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

Rename get_kind() -> kind()

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-22 04:14:01 -07:00
parent 34ebbb2727
commit a2e72dbd92
5 changed files with 69 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

98
src/sexpr/sexpr.cpp
View file

@ -17,54 +17,54 @@ namespace lean {
struct sexpr_cell { struct sexpr_cell {
void dealloc(); void dealloc();
MK_LEAN_RC() MK_LEAN_RC()
sexpr::kind m_kind; sexpr_kind m_kind;
unsigned m_hash; unsigned m_hash;
sexpr_cell(sexpr::kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {} sexpr_cell(sexpr_kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {}
}; };
struct sexpr_string : public sexpr_cell { struct sexpr_string : public sexpr_cell {
std::string m_value; std::string m_value;
sexpr_string(char const * v): sexpr_string(char const * v):
sexpr_cell(sexpr::kind::STRING, hash(v, strlen(v), 13)), sexpr_cell(sexpr_kind::STRING, hash(v, strlen(v), 13)),
m_value(v) {} m_value(v) {}
sexpr_string(std::string const & v): sexpr_string(std::string const & v):
sexpr_cell(sexpr::kind::STRING, hash(v.c_str(), v.size(), 13)), sexpr_cell(sexpr_kind::STRING, hash(v.c_str(), v.size(), 13)),
m_value(v) {} m_value(v) {}
}; };
struct sexpr_int : public sexpr_cell { struct sexpr_int : public sexpr_cell {
int m_value; int m_value;
sexpr_int(int v): sexpr_int(int v):
sexpr_cell(sexpr::kind::INT, v), sexpr_cell(sexpr_kind::INT, v),
m_value(v) {} m_value(v) {}
}; };
struct sexpr_double : public sexpr_cell { struct sexpr_double : public sexpr_cell {
double m_value; double m_value;
sexpr_double(double v): sexpr_double(double v):
sexpr_cell(sexpr::kind::DOUBLE, static_cast<unsigned>(v)), sexpr_cell(sexpr_kind::DOUBLE, static_cast<unsigned>(v)),
m_value(v) {} m_value(v) {}
}; };
struct sexpr_name : public sexpr_cell { struct sexpr_name : public sexpr_cell {
name m_value; name m_value;
sexpr_name(name const & v): sexpr_name(name const & v):
sexpr_cell(sexpr::kind::NAME, v.hash()), sexpr_cell(sexpr_kind::NAME, v.hash()),
m_value(v) {} m_value(v) {}
}; };
struct sexpr_mpz : public sexpr_cell { struct sexpr_mpz : public sexpr_cell {
mpz m_value; mpz m_value;
sexpr_mpz(mpz const & v): sexpr_mpz(mpz const & v):
sexpr_cell(sexpr::kind::MPZ, v.hash()), sexpr_cell(sexpr_kind::MPZ, v.hash()),
m_value(v) {} m_value(v) {}
}; };
struct sexpr_mpq : public sexpr_cell { struct sexpr_mpq : public sexpr_cell {
mpq m_value; mpq m_value;
sexpr_mpq(mpq const & v): sexpr_mpq(mpq const & v):
sexpr_cell(sexpr::kind::MPQ, v.hash()), sexpr_cell(sexpr_kind::MPQ, v.hash()),
m_value(v) {} m_value(v) {}
}; };
@ -72,21 +72,21 @@ struct sexpr_cons : public sexpr_cell {
sexpr m_head; sexpr m_head;
sexpr m_tail; sexpr m_tail;
sexpr_cons(sexpr const & h, sexpr const & t): sexpr_cons(sexpr const & h, sexpr const & t):
sexpr_cell(sexpr::kind::CONS, hash(h.hash(), t.hash())), sexpr_cell(sexpr_kind::CONS, hash(h.hash(), t.hash())),
m_head(h), m_head(h),
m_tail(t) {} m_tail(t) {}
}; };
void sexpr_cell::dealloc() { void sexpr_cell::dealloc() {
switch (m_kind) { switch (m_kind) {
case sexpr::kind::NIL: lean_unreachable(); break; case sexpr_kind::NIL: lean_unreachable(); break;
case sexpr::kind::STRING: delete static_cast<sexpr_string*>(this); break; case sexpr_kind::STRING: delete static_cast<sexpr_string*>(this); break;
case sexpr::kind::INT: delete static_cast<sexpr_int*>(this); break; case sexpr_kind::INT: delete static_cast<sexpr_int*>(this); break;
case sexpr::kind::DOUBLE: delete static_cast<sexpr_double*>(this); break; case sexpr_kind::DOUBLE: delete static_cast<sexpr_double*>(this); break;
case sexpr::kind::NAME: delete static_cast<sexpr_name*>(this); break; case sexpr_kind::NAME: delete static_cast<sexpr_name*>(this); break;
case sexpr::kind::MPZ: delete static_cast<sexpr_mpz*>(this); break; case sexpr_kind::MPZ: delete static_cast<sexpr_mpz*>(this); break;
case sexpr::kind::MPQ: delete static_cast<sexpr_mpq*>(this); break; case sexpr_kind::MPQ: delete static_cast<sexpr_mpq*>(this); break;
case sexpr::kind::CONS: delete static_cast<sexpr_cons*>(this); break; case sexpr_kind::CONS: delete static_cast<sexpr_cons*>(this); break;
} }
} }
@ -110,7 +110,7 @@ sexpr::~sexpr() {
m_ptr->dec_ref(); m_ptr->dec_ref();
} }
sexpr::kind sexpr::get_kind() const { return m_ptr ? m_ptr->m_kind : kind::NIL; } sexpr_kind sexpr::kind() const { return m_ptr ? m_ptr->m_kind : sexpr_kind::NIL; }
sexpr const & head(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_head; } sexpr const & head(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_head; }
sexpr const & tail(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_tail; } sexpr const & tail(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_tail; }
std::string const & sexpr::get_string() const { return static_cast<sexpr_string*>(m_ptr)->m_value; } std::string const & sexpr::get_string() const { return static_cast<sexpr_string*>(m_ptr)->m_value; }
@ -170,21 +170,21 @@ unsigned length(sexpr const & s) {
bool operator==(sexpr const & a, sexpr const & b) { bool operator==(sexpr const & a, sexpr const & b) {
if (eqp(a, b)) if (eqp(a, b))
return true; return true;
sexpr::kind ka = a.get_kind(); sexpr_kind ka = a.kind();
sexpr::kind kb = b.get_kind(); sexpr_kind kb = b.kind();
if (ka != kb) if (ka != kb)
return false; return false;
if (a.hash() != b.hash()) if (a.hash() != b.hash())
return false; return false;
switch (ka) { switch (ka) {
case sexpr::kind::NIL: return true; case sexpr_kind::NIL: return true;
case sexpr::kind::STRING: return to_string(a) == to_string(b); case sexpr_kind::STRING: return to_string(a) == to_string(b);
case sexpr::kind::INT: return to_int(a) == to_int(b); case sexpr_kind::INT: return to_int(a) == to_int(b);
case sexpr::kind::DOUBLE: return to_double(a) == to_double(b); case sexpr_kind::DOUBLE: return to_double(a) == to_double(b);
case sexpr::kind::NAME: return to_name(a) == to_name(b); case sexpr_kind::NAME: return to_name(a) == to_name(b);
case sexpr::kind::MPZ: return to_mpz(a) == to_mpz(b); case sexpr_kind::MPZ: return to_mpz(a) == to_mpz(b);
case sexpr::kind::MPQ: return to_mpq(a) == to_mpq(b); case sexpr_kind::MPQ: return to_mpq(a) == to_mpq(b);
case sexpr::kind::CONS: return head(a) == head(b) && tail(a) == tail(b); case sexpr_kind::CONS: return head(a) == head(b) && tail(a) == tail(b);
} }
return false; return false;
} }
@ -192,8 +192,8 @@ bool operator==(sexpr const & a, sexpr const & b) {
int cmp(sexpr const & a, sexpr const & b) { int cmp(sexpr const & a, sexpr const & b) {
if (eqp(a, b)) if (eqp(a, b))
return 0; return 0;
sexpr::kind ka = a.get_kind(); sexpr_kind ka = a.kind();
sexpr::kind kb = b.get_kind(); sexpr_kind kb = b.kind();
if (ka != kb) if (ka != kb)
return ka < kb ? -1 : 1; return ka < kb ? -1 : 1;
if (a.hash() == b.hash()) { if (a.hash() == b.hash()) {
@ -201,14 +201,14 @@ int cmp(sexpr const & a, sexpr const & b) {
return 0; return 0;
} }
switch (ka) { switch (ka) {
case sexpr::kind::NIL: return 0; case sexpr_kind::NIL: return 0;
case sexpr::kind::STRING: return strcmp(to_string(a).c_str(), to_string(b).c_str()); case sexpr_kind::STRING: return strcmp(to_string(a).c_str(), to_string(b).c_str());
case sexpr::kind::INT: return to_int(a) == to_int(b) ? 0 : (to_int(a) < to_int(b) ? -1 : 1); case sexpr_kind::INT: return to_int(a) == to_int(b) ? 0 : (to_int(a) < to_int(b) ? -1 : 1);
case sexpr::kind::DOUBLE: return to_double(a) == to_double(b) ? 0 : (to_double(a) < to_double(b) ? -1 : 1); case sexpr_kind::DOUBLE: return to_double(a) == to_double(b) ? 0 : (to_double(a) < to_double(b) ? -1 : 1);
case sexpr::kind::NAME: return cmp(to_name(a), to_name(b)); case sexpr_kind::NAME: return cmp(to_name(a), to_name(b));
case sexpr::kind::MPZ: return cmp(to_mpz(a), to_mpz(b)); case sexpr_kind::MPZ: return cmp(to_mpz(a), to_mpz(b));
case sexpr::kind::MPQ: return cmp(to_mpq(a), to_mpq(b)); case sexpr_kind::MPQ: return cmp(to_mpq(a), to_mpq(b));
case sexpr::kind::CONS: { case sexpr_kind::CONS: {
int r = cmp(head(a), head(b)); int r = cmp(head(a), head(b));
if (r != 0) if (r != 0)
return r; return r;
@ -218,15 +218,15 @@ int cmp(sexpr const & a, sexpr const & b) {
} }
std::ostream & operator<<(std::ostream & out, sexpr const & s) { std::ostream & operator<<(std::ostream & out, sexpr const & s) {
switch (s.get_kind()) { switch (s.kind()) {
case sexpr::kind::NIL: out << "nil"; break; case sexpr_kind::NIL: out << "nil"; break;
case sexpr::kind::STRING: out << "\"" << to_string(s) << "\""; break; case sexpr_kind::STRING: out << "\"" << to_string(s) << "\""; break;
case sexpr::kind::INT: out << to_int(s); break; case sexpr_kind::INT: out << to_int(s); break;
case sexpr::kind::DOUBLE: out << to_double(s); break; case sexpr_kind::DOUBLE: out << to_double(s); break;
case sexpr::kind::NAME: out << to_name(s); break; case sexpr_kind::NAME: out << to_name(s); break;
case sexpr::kind::MPZ: out << to_mpz(s); break; case sexpr_kind::MPZ: out << to_mpz(s); break;
case sexpr::kind::MPQ: out << to_mpq(s); break; case sexpr_kind::MPQ: out << to_mpq(s); break;
case sexpr::kind::CONS: { case sexpr_kind::CONS: {
out << "("; out << "(";
sexpr const * curr = &s; sexpr const * curr = &s;
while (true) { while (true) {

22
src/sexpr/sexpr.h
View file

@ -13,6 +13,8 @@ class mpq;
class mpz; class mpz;
struct sexpr_cell; struct sexpr_cell;
enum class sexpr_kind { NIL, STRING, INT, DOUBLE, NAME, MPZ, MPQ, CONS };
/** /**
\brief Simple LISP-like S-expressions. \brief Simple LISP-like S-expressions.
1. Atoms: nil, string, int, name, mpz or mpq 1. Atoms: nil, string, int, name, mpz or mpq
@ -25,7 +27,6 @@ struct sexpr_cell;
class sexpr { class sexpr {
sexpr_cell * m_ptr; sexpr_cell * m_ptr;
public: public:
enum class kind { NIL, STRING, INT, DOUBLE, NAME, MPZ, MPQ, CONS };
sexpr():m_ptr(nullptr) {} sexpr():m_ptr(nullptr) {}
explicit sexpr(char const * v); explicit sexpr(char const * v);
explicit sexpr(std::string const & v); explicit sexpr(std::string const & v);
@ -51,7 +52,7 @@ public:
} }
~sexpr(); ~sexpr();
kind get_kind() const; sexpr_kind kind() const;
friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; } friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; }
friend sexpr const & head(sexpr const & s); friend sexpr const & head(sexpr const & s);
@ -84,15 +85,14 @@ inline sexpr nil() { return sexpr(); }
inline sexpr cons(sexpr const & head, sexpr const & tail) { return sexpr(head, tail); } inline sexpr cons(sexpr const & head, sexpr const & tail) { return sexpr(head, tail); }
inline sexpr const & car(sexpr const & s) { return head(s); } inline sexpr const & car(sexpr const & s) { return head(s); }
inline sexpr const & cdr(sexpr const & s) { return tail(s); } inline sexpr const & cdr(sexpr const & s) { return tail(s); }
inline bool is_atom(sexpr const & s) { return s.get_kind() != sexpr::kind::CONS; } inline bool is_atom(sexpr const & s) { return s.kind() != sexpr_kind::CONS; }
inline bool is_cons(sexpr const & s) { return s.get_kind() == sexpr::kind::CONS; } inline bool is_cons(sexpr const & s) { return s.kind() == sexpr_kind::CONS; }
inline bool is_string(sexpr const & s) { return s.kind() == sexpr_kind::STRING; }
inline bool is_string(sexpr const & s) { return s.get_kind() == sexpr::kind::STRING; } inline bool is_int(sexpr const & s) { return s.kind() == sexpr_kind::INT; }
inline bool is_int(sexpr const & s) { return s.get_kind() == sexpr::kind::INT; } inline bool is_double(sexpr const & s) { return s.kind() == sexpr_kind::DOUBLE; }
inline bool is_double(sexpr const & s) { return s.get_kind() == sexpr::kind::DOUBLE; } inline bool is_name(sexpr const & s) { return s.kind() == sexpr_kind::NAME; }
inline bool is_name(sexpr const & s) { return s.get_kind() == sexpr::kind::NAME; } inline bool is_mpz(sexpr const & s) { return s.kind() == sexpr_kind::MPZ; }
inline bool is_mpz(sexpr const & s) { return s.get_kind() == sexpr::kind::MPZ; } inline bool is_mpq(sexpr const & s) { return s.kind() == sexpr_kind::MPQ; }
inline bool is_mpq(sexpr const & s) { return s.get_kind() == sexpr::kind::MPQ; }
inline std::string const & to_string(sexpr const & s) { return s.get_string(); } inline std::string const & to_string(sexpr const & s) { return s.get_string(); }
inline int to_int(sexpr const & s) { return s.get_int(); } inline int to_int(sexpr const & s) { return s.get_int(); }

2
src/tests/util/name.cpp
View file

@ -21,7 +21,7 @@ static void tst1() {
lean_assert(name(name(n, "foo"), 1) != name(name(n, "bla"), 1)); lean_assert(name(name(n, "foo"), 1) != name(name(n, "bla"), 1));
lean_assert(name(name(name("f"), "bla"), 1) != name(name(n, "bla"), 1)); lean_assert(name(name(name("f"), "bla"), 1) != name(name(n, "bla"), 1));
lean_assert(n != name()); lean_assert(n != name());
lean_assert(name().get_kind() == name::kind::ANONYMOUS); lean_assert(name().kind() == name_kind::ANONYMOUS);
lean_assert(name(name(), "foo") == name("foo")); lean_assert(name(name(), "foo") == name("foo"));
lean_assert(name(n, 1) < name(n, 2)); lean_assert(name(n, 1) < name(n, 2));

6
src/util/name.cpp
View file

@ -133,11 +133,11 @@ name & name::operator=(name && other) {
return *this; return *this;
} }
name::kind name::get_kind() const { name_kind name::kind() const {
if (m_imp == nullptr) if (m_imp == nullptr)
return kind::ANONYMOUS; return name_kind::ANONYMOUS;
else else
return m_imp->m_is_string ? kind::STRING : kind::NUMERAL; return m_imp->m_is_string ? name_kind::STRING : name_kind::NUMERAL;
} }
unsigned name::get_numeral() const { unsigned name::get_numeral() const {

10
src/util/name.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
constexpr char const * default_name_separator = "::"; constexpr char const * default_name_separator = "::";
enum class name_kind { ANONYMOUS, STRING, NUMERAL };
/** /**
\brief Hierarchical names. \brief Hierarchical names.
@ -20,7 +21,6 @@ class name {
imp * m_imp; imp * m_imp;
explicit name(imp * p); explicit name(imp * p);
public: public:
enum class kind { ANONYMOUS, STRING, NUMERAL };
name(); name();
explicit name(char const * name); explicit name(char const * name);
explicit name(unsigned k); explicit name(unsigned k);
@ -39,10 +39,10 @@ public:
friend bool operator>(name const & a, name const & b) { return cmp(a, b) > 0; } friend bool operator>(name const & a, name const & b) { return cmp(a, b) > 0; }
friend bool operator<=(name const & a, name const & b) { return cmp(a, b) <= 0; } friend bool operator<=(name const & a, name const & b) { return cmp(a, b) <= 0; }
friend bool operator>=(name const & a, name const & b) { return cmp(a, b) >= 0; } friend bool operator>=(name const & a, name const & b) { return cmp(a, b) >= 0; }
kind get_kind() const; name_kind kind() const;
bool is_anonymous() const { return get_kind() == kind::ANONYMOUS; } bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; }
bool is_string() const { return get_kind() == kind::STRING; } bool is_string() const { return kind() == name_kind::STRING; }
bool is_numeral() const { return get_kind() == kind::NUMERAL; } bool is_numeral() const { return kind() == name_kind::NUMERAL; }
unsigned get_numeral() const; unsigned get_numeral() const;
char const * get_string() const; char const * get_string() const;
bool is_atomic() const; bool is_atomic() const;