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

style(util/sexpr): name convetion for enumeration types

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-13 11:50:00 -08:00
parent 450128e28b
commit e2efce6b62
4 changed files with 58 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/bindings/lua/sexpr.cpp
View file

@ -219,15 +219,15 @@ void open_sexpr(lua_State * L) {
SET_GLOBAL_FUN(sexpr_pred, "is_sexpr"); SET_GLOBAL_FUN(sexpr_pred, "is_sexpr");
lua_newtable(L); lua_newtable(L);
SET_ENUM("Nil", sexpr_kind::NIL); SET_ENUM("Nil", sexpr_kind::Nil);
SET_ENUM("String", sexpr_kind::STRING); SET_ENUM("String", sexpr_kind::String);
SET_ENUM("Bool", sexpr_kind::BOOL); SET_ENUM("Bool", sexpr_kind::Bool);
SET_ENUM("Int", sexpr_kind::INT); SET_ENUM("Int", sexpr_kind::Int);
SET_ENUM("Double", sexpr_kind::DOUBLE); SET_ENUM("Double", sexpr_kind::Double);
SET_ENUM("Name", sexpr_kind::NAME); SET_ENUM("Name", sexpr_kind::Name);
SET_ENUM("MPZ", sexpr_kind::MPZ); SET_ENUM("MPZ", sexpr_kind::MPZ);
SET_ENUM("MPQ", sexpr_kind::MPQ); SET_ENUM("MPQ", sexpr_kind::MPQ);
SET_ENUM("Cons", sexpr_kind::CONS); SET_ENUM("Cons", sexpr_kind::Cons);
lua_setglobal(L, "sexpr_kind"); lua_setglobal(L, "sexpr_kind");
} }
} }

14
src/util/sexpr/format.cpp
View file

@ -400,19 +400,19 @@ format pp(name const & n) {
struct sexpr_pp_fn { struct sexpr_pp_fn {
format apply(sexpr const & s) { format apply(sexpr const & s) {
switch (s.kind()) { switch (s.kind()) {
case sexpr_kind::NIL: return format("nil"); case sexpr_kind::Nil: return format("nil");
case sexpr_kind::STRING: { case sexpr_kind::String: {
std::ostringstream ss; std::ostringstream ss;
ss << "\"" << escaped(to_string(s).c_str()) << "\""; ss << "\"" << escaped(to_string(s).c_str()) << "\"";
return format(ss.str()); return format(ss.str());
} }
case sexpr_kind::BOOL: return format(to_bool(s) ? "true" : "false"); case sexpr_kind::Bool: return format(to_bool(s) ? "true" : "false");
case sexpr_kind::INT: return format(to_int(s)); case sexpr_kind::Int: return format(to_int(s));
case sexpr_kind::DOUBLE: return format(to_double(s)); case sexpr_kind::Double: return format(to_double(s));
case sexpr_kind::NAME: return pp(to_name(s)); case sexpr_kind::Name: return pp(to_name(s));
case sexpr_kind::MPZ: return format(to_mpz(s)); case sexpr_kind::MPZ: return format(to_mpz(s));
case sexpr_kind::MPQ: return format(to_mpq(s)); case sexpr_kind::MPQ: return format(to_mpq(s));
case sexpr_kind::CONS: { case sexpr_kind::Cons: {
sexpr const * curr = &s; sexpr const * curr = &s;
format r; format r;
while (true) { while (true) {

72
src/util/sexpr/sexpr.cpp
View file

@ -29,10 +29,10 @@ struct sexpr_cell {
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_str(strlen(v), v, 13)), sexpr_cell(sexpr_kind::String, hash_str(strlen(v), 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_str(v.size(), v.c_str(), 13)), sexpr_cell(sexpr_kind::String, hash_str(v.size(), v.c_str(), 13)),
m_value(v) {} m_value(v) {}
}; };
@ -40,7 +40,7 @@ struct sexpr_string : public sexpr_cell {
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) {}
}; };
@ -48,7 +48,7 @@ struct sexpr_int : public sexpr_cell {
struct sexpr_bool : public sexpr_cell { struct sexpr_bool : public sexpr_cell {
bool m_value; bool m_value;
sexpr_bool(bool v): sexpr_bool(bool v):
sexpr_cell(sexpr_kind::BOOL, v), sexpr_cell(sexpr_kind::Bool, v),
m_value(v) {} m_value(v) {}
}; };
@ -56,7 +56,7 @@ struct sexpr_bool : public sexpr_cell {
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) {}
}; };
@ -64,7 +64,7 @@ struct sexpr_double : public sexpr_cell {
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) {}
}; };
@ -89,22 +89,22 @@ 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(); // LCOV_EXCL_LINE case sexpr_kind::Nil: lean_unreachable(); // LCOV_EXCL_LINE
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::BOOL: delete static_cast<sexpr_bool*>(this); break; case sexpr_kind::Bool: delete static_cast<sexpr_bool*>(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;
} }
} }
@ -129,7 +129,7 @@ sexpr::~sexpr() {
m_ptr->dec_ref(); 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<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; }
@ -183,15 +183,15 @@ bool operator==(sexpr const & a, sexpr const & b) {
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::BOOL: return to_bool(a) == to_bool(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::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);
} }
lean_unreachable(); // LCOV_EXCL_LINE lean_unreachable(); // LCOV_EXCL_LINE
} }
@ -208,15 +208,15 @@ 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::BOOL: return to_bool(a) == to_bool(b) ? 0 : (!to_bool(a) && to_bool(b) ? -1 : 1); 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::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;
@ -227,15 +227,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.kind()) { switch (s.kind()) {
case sexpr_kind::NIL: out << "nil"; break; case sexpr_kind::Nil: out << "nil"; break;
case sexpr_kind::STRING: out << "\"" << escaped(to_string(s).c_str()) << "\""; 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::Bool: out << (to_bool(s) ? "true" : "false"); 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) {

16
src/util/sexpr/sexpr.h
View file

@ -15,7 +15,7 @@ class mpq;
class mpz; class mpz;
struct sexpr_cell; 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. \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); } 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). */ /** \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. */ /** \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_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.kind() == sexpr_kind::String; }
inline bool is_bool(sexpr const & s) { return s.kind() == sexpr_kind::BOOL; } 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_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_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_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_mpz(sexpr const & s) { return s.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.kind() == sexpr_kind::MPQ; }