diff --git a/src/sexpr/sexpr.cpp b/src/sexpr/sexpr.cpp index 2d2b0ed15..998615a0c 100644 --- a/src/sexpr/sexpr.cpp +++ b/src/sexpr/sexpr.cpp @@ -17,54 +17,54 @@ namespace lean { struct sexpr_cell { void dealloc(); MK_LEAN_RC() - sexpr::kind m_kind; - unsigned m_hash; + sexpr_kind m_kind; + 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 { std::string m_value; 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) {} 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) {} }; struct sexpr_int : public sexpr_cell { int m_value; sexpr_int(int v): - sexpr_cell(sexpr::kind::INT, v), + sexpr_cell(sexpr_kind::INT, v), m_value(v) {} }; struct sexpr_double : public sexpr_cell { double m_value; sexpr_double(double v): - sexpr_cell(sexpr::kind::DOUBLE, static_cast(v)), + sexpr_cell(sexpr_kind::DOUBLE, static_cast(v)), m_value(v) {} }; struct sexpr_name : public sexpr_cell { name m_value; sexpr_name(name const & v): - sexpr_cell(sexpr::kind::NAME, v.hash()), + sexpr_cell(sexpr_kind::NAME, v.hash()), m_value(v) {} }; struct sexpr_mpz : public sexpr_cell { mpz m_value; sexpr_mpz(mpz const & v): - sexpr_cell(sexpr::kind::MPZ, v.hash()), + sexpr_cell(sexpr_kind::MPZ, v.hash()), m_value(v) {} }; struct sexpr_mpq : public sexpr_cell { mpq m_value; sexpr_mpq(mpq const & v): - sexpr_cell(sexpr::kind::MPQ, v.hash()), + sexpr_cell(sexpr_kind::MPQ, v.hash()), m_value(v) {} }; @@ -72,21 +72,21 @@ struct sexpr_cons : public sexpr_cell { sexpr m_head; sexpr m_tail; 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_tail(t) {} }; void sexpr_cell::dealloc() { switch (m_kind) { - case sexpr::kind::NIL: lean_unreachable(); break; - case sexpr::kind::STRING: delete static_cast(this); break; - case sexpr::kind::INT: delete static_cast(this); break; - case sexpr::kind::DOUBLE: delete static_cast(this); break; - case sexpr::kind::NAME: delete static_cast(this); break; - case sexpr::kind::MPZ: delete static_cast(this); break; - case sexpr::kind::MPQ: delete static_cast(this); break; - case sexpr::kind::CONS: delete static_cast(this); break; + case sexpr_kind::NIL: lean_unreachable(); break; + case sexpr_kind::STRING: delete static_cast(this); break; + case sexpr_kind::INT: delete static_cast(this); break; + case sexpr_kind::DOUBLE: delete static_cast(this); break; + case sexpr_kind::NAME: delete static_cast(this); break; + case sexpr_kind::MPZ: delete static_cast(this); break; + case sexpr_kind::MPQ: delete static_cast(this); break; + case sexpr_kind::CONS: delete static_cast(this); break; } } @@ -110,7 +110,7 @@ sexpr::~sexpr() { 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(s.m_ptr)->m_head; } sexpr const & tail(sexpr const & s) { lean_assert(is_cons(s)); return static_cast(s.m_ptr)->m_tail; } std::string const & sexpr::get_string() const { return static_cast(m_ptr)->m_value; } @@ -170,21 +170,21 @@ unsigned length(sexpr const & s) { bool operator==(sexpr const & a, sexpr const & b) { if (eqp(a, b)) return true; - sexpr::kind ka = a.get_kind(); - sexpr::kind kb = b.get_kind(); + sexpr_kind ka = a.kind(); + sexpr_kind kb = b.kind(); if (ka != kb) return false; if (a.hash() != b.hash()) return false; switch (ka) { - case sexpr::kind::NIL: return true; - 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::DOUBLE: return to_double(a) == to_double(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::MPQ: return to_mpq(a) == to_mpq(b); - case sexpr::kind::CONS: return head(a) == head(b) && tail(a) == tail(b); + case sexpr_kind::NIL: return true; + 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::DOUBLE: return to_double(a) == to_double(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::MPQ: return to_mpq(a) == to_mpq(b); + case sexpr_kind::CONS: return head(a) == head(b) && tail(a) == tail(b); } return false; } @@ -192,8 +192,8 @@ bool operator==(sexpr const & a, sexpr const & b) { int cmp(sexpr const & a, sexpr const & b) { if (eqp(a, b)) return 0; - sexpr::kind ka = a.get_kind(); - sexpr::kind kb = b.get_kind(); + sexpr_kind ka = a.kind(); + sexpr_kind kb = b.kind(); if (ka != kb) return ka < kb ? -1 : 1; if (a.hash() == b.hash()) { @@ -201,14 +201,14 @@ int cmp(sexpr const & a, sexpr const & b) { return 0; } switch (ka) { - 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::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::NAME: return cmp(to_name(a), to_name(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::CONS: { + 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::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::NAME: return cmp(to_name(a), to_name(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::CONS: { int r = cmp(head(a), head(b)); if (r != 0) return r; @@ -218,15 +218,15 @@ int cmp(sexpr const & a, sexpr const & b) { } std::ostream & operator<<(std::ostream & out, sexpr const & s) { - switch (s.get_kind()) { - case sexpr::kind::NIL: out << "nil"; break; - case sexpr::kind::STRING: out << "\"" << to_string(s) << "\""; break; - case sexpr::kind::INT: out << to_int(s); break; - case sexpr::kind::DOUBLE: out << to_double(s); break; - case sexpr::kind::NAME: out << to_name(s); break; - case sexpr::kind::MPZ: out << to_mpz(s); break; - case sexpr::kind::MPQ: out << to_mpq(s); break; - case sexpr::kind::CONS: { + switch (s.kind()) { + case sexpr_kind::NIL: out << "nil"; break; + case sexpr_kind::STRING: out << "\"" << to_string(s) << "\""; break; + case sexpr_kind::INT: out << to_int(s); break; + case sexpr_kind::DOUBLE: out << to_double(s); break; + case sexpr_kind::NAME: out << to_name(s); break; + case sexpr_kind::MPZ: out << to_mpz(s); break; + case sexpr_kind::MPQ: out << to_mpq(s); break; + case sexpr_kind::CONS: { out << "("; sexpr const * curr = &s; while (true) { diff --git a/src/sexpr/sexpr.h b/src/sexpr/sexpr.h index 448f62833..ce214115d 100644 --- a/src/sexpr/sexpr.h +++ b/src/sexpr/sexpr.h @@ -13,6 +13,8 @@ class mpq; class mpz; struct sexpr_cell; +enum class sexpr_kind { NIL, STRING, INT, DOUBLE, NAME, MPZ, MPQ, CONS }; + /** \brief Simple LISP-like S-expressions. 1. Atoms: nil, string, int, name, mpz or mpq @@ -25,7 +27,6 @@ struct sexpr_cell; class sexpr { sexpr_cell * m_ptr; public: - enum class kind { NIL, STRING, INT, DOUBLE, NAME, MPZ, MPQ, CONS }; sexpr():m_ptr(nullptr) {} explicit sexpr(char const * v); explicit sexpr(std::string const & v); @@ -51,7 +52,7 @@ public: } ~sexpr(); - kind get_kind() const; + sexpr_kind kind() const; friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; } 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 const & car(sexpr const & s) { return head(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_cons(sexpr const & s) { return s.get_kind() == sexpr::kind::CONS; } - -inline bool is_string(sexpr const & s) { return s.get_kind() == sexpr::kind::STRING; } -inline bool is_int(sexpr const & s) { return s.get_kind() == sexpr::kind::INT; } -inline bool is_double(sexpr const & s) { return s.get_kind() == sexpr::kind::DOUBLE; } -inline bool is_name(sexpr const & s) { return s.get_kind() == sexpr::kind::NAME; } -inline bool is_mpz(sexpr const & s) { return s.get_kind() == sexpr::kind::MPZ; } -inline bool is_mpq(sexpr const & s) { return s.get_kind() == sexpr::kind::MPQ; } +inline bool is_atom(sexpr const & s) { return s.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_int(sexpr const & s) { return s.kind() == sexpr_kind::INT; } +inline bool is_double(sexpr const & s) { return s.kind() == sexpr_kind::DOUBLE; } +inline bool is_name(sexpr const & s) { return s.kind() == sexpr_kind::NAME; } +inline bool is_mpz(sexpr const & s) { return s.kind() == sexpr_kind::MPZ; } +inline bool is_mpq(sexpr const & s) { return s.kind() == sexpr_kind::MPQ; } inline std::string const & to_string(sexpr const & s) { return s.get_string(); } inline int to_int(sexpr const & s) { return s.get_int(); } diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp index a4f02564e..6cdbeaf29 100644 --- a/src/tests/util/name.cpp +++ b/src/tests/util/name.cpp @@ -21,7 +21,7 @@ static void tst1() { 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(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(n, 1) < name(n, 2)); diff --git a/src/util/name.cpp b/src/util/name.cpp index cb56d0013..109cb43fc 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -133,11 +133,11 @@ name & name::operator=(name && other) { return *this; } -name::kind name::get_kind() const { +name_kind name::kind() const { if (m_imp == nullptr) - return kind::ANONYMOUS; + return name_kind::ANONYMOUS; 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 { diff --git a/src/util/name.h b/src/util/name.h index 42405e1ec..9b00f0de7 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -10,6 +10,7 @@ Author: Leonardo de Moura namespace lean { constexpr char const * default_name_separator = "::"; +enum class name_kind { ANONYMOUS, STRING, NUMERAL }; /** \brief Hierarchical names. @@ -20,7 +21,6 @@ class name { imp * m_imp; explicit name(imp * p); public: - enum class kind { ANONYMOUS, STRING, NUMERAL }; name(); explicit name(char const * name); 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; } - kind get_kind() const; - bool is_anonymous() const { return get_kind() == kind::ANONYMOUS; } - bool is_string() const { return get_kind() == kind::STRING; } - bool is_numeral() const { return get_kind() == kind::NUMERAL; } + name_kind kind() const; + bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; } + bool is_string() const { return kind() == name_kind::STRING; } + bool is_numeral() const { return kind() == name_kind::NUMERAL; } unsigned get_numeral() const; char const * get_string() const; bool is_atomic() const;