diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp index 4160b3a2c..0a6631fdf 100644 --- a/src/bindings/lua/sexpr.cpp +++ b/src/bindings/lua/sexpr.cpp @@ -219,15 +219,15 @@ void open_sexpr(lua_State * L) { SET_GLOBAL_FUN(sexpr_pred, "is_sexpr"); lua_newtable(L); - SET_ENUM("Nil", sexpr_kind::NIL); - SET_ENUM("String", sexpr_kind::STRING); - SET_ENUM("Bool", sexpr_kind::BOOL); - SET_ENUM("Int", sexpr_kind::INT); - SET_ENUM("Double", sexpr_kind::DOUBLE); - SET_ENUM("Name", sexpr_kind::NAME); + SET_ENUM("Nil", sexpr_kind::Nil); + SET_ENUM("String", sexpr_kind::String); + SET_ENUM("Bool", sexpr_kind::Bool); + SET_ENUM("Int", sexpr_kind::Int); + SET_ENUM("Double", sexpr_kind::Double); + SET_ENUM("Name", sexpr_kind::Name); SET_ENUM("MPZ", sexpr_kind::MPZ); SET_ENUM("MPQ", sexpr_kind::MPQ); - SET_ENUM("Cons", sexpr_kind::CONS); + SET_ENUM("Cons", sexpr_kind::Cons); lua_setglobal(L, "sexpr_kind"); } } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 1c7de30ad..ec21dcb71 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -400,19 +400,19 @@ format pp(name const & n) { struct sexpr_pp_fn { format apply(sexpr const & s) { switch (s.kind()) { - case sexpr_kind::NIL: return format("nil"); - case sexpr_kind::STRING: { + case sexpr_kind::Nil: return format("nil"); + case sexpr_kind::String: { std::ostringstream ss; ss << "\"" << escaped(to_string(s).c_str()) << "\""; return format(ss.str()); } - case sexpr_kind::BOOL: return format(to_bool(s) ? "true" : "false"); - case sexpr_kind::INT: return format(to_int(s)); - case sexpr_kind::DOUBLE: return format(to_double(s)); - case sexpr_kind::NAME: return pp(to_name(s)); + case sexpr_kind::Bool: return format(to_bool(s) ? "true" : "false"); + case sexpr_kind::Int: return format(to_int(s)); + case sexpr_kind::Double: return format(to_double(s)); + case sexpr_kind::Name: return pp(to_name(s)); case sexpr_kind::MPZ: return format(to_mpz(s)); case sexpr_kind::MPQ: return format(to_mpq(s)); - case sexpr_kind::CONS: { + case sexpr_kind::Cons: { sexpr const * curr = &s; format r; while (true) { diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index ac707c660..9cd73d2dc 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -29,10 +29,10 @@ struct sexpr_cell { struct sexpr_string : public sexpr_cell { std::string m_value; sexpr_string(char const * v): - sexpr_cell(sexpr_kind::STRING, hash_str(strlen(v), v, 13)), + sexpr_cell(sexpr_kind::String, hash_str(strlen(v), v, 13)), m_value(v) {} sexpr_string(std::string const & v): - sexpr_cell(sexpr_kind::STRING, hash_str(v.size(), v.c_str(), 13)), + sexpr_cell(sexpr_kind::String, hash_str(v.size(), v.c_str(), 13)), m_value(v) {} }; @@ -40,7 +40,7 @@ struct sexpr_string : public sexpr_cell { 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) {} }; @@ -48,7 +48,7 @@ struct sexpr_int : public sexpr_cell { struct sexpr_bool : public sexpr_cell { bool m_value; sexpr_bool(bool v): - sexpr_cell(sexpr_kind::BOOL, v), + sexpr_cell(sexpr_kind::Bool, v), m_value(v) {} }; @@ -56,7 +56,7 @@ struct sexpr_bool : public sexpr_cell { 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) {} }; @@ -64,7 +64,7 @@ struct sexpr_double : public sexpr_cell { 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) {} }; @@ -89,22 +89,22 @@ 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(); // LCOV_EXCL_LINE - case sexpr_kind::STRING: delete static_cast(this); break; - case sexpr_kind::BOOL: 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::Nil: lean_unreachable(); // LCOV_EXCL_LINE + case sexpr_kind::String: delete static_cast(this); break; + case sexpr_kind::Bool: 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::Cons: delete static_cast(this); break; } } @@ -129,7 +129,7 @@ sexpr::~sexpr() { m_ptr->dec_ref(); } -sexpr_kind sexpr::kind() const { return m_ptr ? m_ptr->m_kind : sexpr_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; } @@ -183,15 +183,15 @@ bool operator==(sexpr const & a, sexpr const & b) { 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::BOOL: return to_bool(a) == to_bool(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::Nil: return true; + case sexpr_kind::String: return to_string(a) == to_string(b); + case sexpr_kind::Bool: return to_bool(a) == to_bool(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::Cons: return head(a) == head(b) && tail(a) == tail(b); } lean_unreachable(); // LCOV_EXCL_LINE } @@ -208,15 +208,15 @@ 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::BOOL: return to_bool(a) == to_bool(b) ? 0 : (!to_bool(a) && to_bool(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::NAME: return cmp(to_name(a), to_name(b)); + 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::Bool: return to_bool(a) == to_bool(b) ? 0 : (!to_bool(a) && to_bool(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::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::Cons: { int r = cmp(head(a), head(b)); if (r != 0) return r; @@ -227,15 +227,15 @@ int cmp(sexpr const & a, sexpr const & b) { std::ostream & operator<<(std::ostream & out, sexpr const & s) { switch (s.kind()) { - case sexpr_kind::NIL: out << "nil"; break; - case sexpr_kind::STRING: out << "\"" << escaped(to_string(s).c_str()) << "\""; break; - case sexpr_kind::BOOL: out << (to_bool(s) ? "true" : "false"); 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::Nil: out << "nil"; break; + case sexpr_kind::String: out << "\"" << escaped(to_string(s).c_str()) << "\""; break; + case sexpr_kind::Bool: out << (to_bool(s) ? "true" : "false"); 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: { + case sexpr_kind::Cons: { out << "("; sexpr const * curr = &s; while (true) { diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h index d2cf8b717..478fecfee 100644 --- a/src/util/sexpr/sexpr.h +++ b/src/util/sexpr/sexpr.h @@ -15,7 +15,7 @@ class mpq; class mpz; struct sexpr_cell; -enum class sexpr_kind { NIL, STRING, BOOL, INT, DOUBLE, NAME, MPZ, MPQ, CONS }; +enum class sexpr_kind { Nil, String, Bool, Int, Double, Name, MPZ, MPQ, Cons }; /** \brief Simple LISP-like S-expressions. @@ -102,14 +102,14 @@ inline sexpr const & car(sexpr const & s) { return head(s); } */ inline sexpr const & cdr(sexpr const & s) { return tail(s); } /** \brief Return true iff \c s is not an atom (i.e., it is not a cons cell). */ -inline bool is_atom(sexpr const & s) { return s.kind() != sexpr_kind::CONS; } +inline bool is_atom(sexpr const & s) { return s.kind() != sexpr_kind::Cons; } /** \brief Return true iff \c s is not a cons cell. */ -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_bool(sexpr const & s) { return s.kind() == sexpr_kind::BOOL; } -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_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_bool(sexpr const & s) { return s.kind() == sexpr_kind::Bool; } +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; }