chore(library/attribute_manager): remove dead code

This commit is contained in:
Leonardo de Moura 2019-01-24 13:36:05 -08:00
parent f5f6a7f85e
commit 8ac423768c
2 changed files with 0 additions and 49 deletions

View file

@ -15,7 +15,6 @@ Author: Leonardo de Moura
namespace lean {
template class typed_attribute<indices_attribute_data>;
template class typed_attribute<key_value_data>;
static name_map<attribute_ptr> * g_system_attributes = nullptr;
static user_attribute_ext * g_user_attribute_ext = nullptr;

View file

@ -205,57 +205,9 @@ struct indices_attribute_data : public attr_data {
}
};
struct key_value_data : public attr_data {
// generalize: name_map<std::string> m_pairs;
std::string m_symbol;
std::string m_library;
virtual unsigned hash() const override {
// unsigned h = 0;
// // This isn't right ..., well maybe? I don't really know.
// // Rust's Hash trait is super good at this.
// m_pairs.for_each([&] (name const & n, std::string const & value) {
// h += n.hash();
// // h += ::lean::hash_str(value, h);
// });
return 0;
}
void write(serializer & s) const {
s << m_symbol;
s << m_library;
}
void read(deserializer & d) {
std::string m_symbol, m_library;
d >> m_symbol;
d >> m_library;
}
void parse(abstract_parser & p) override {
std::cout << "in extern parser" << std::endl;
std::string n = p.parse_string_lit();
std::string l = p.parse_string_lit();
std::cout << "link symbol: " << n << std::endl;
std::cout << "library symbol: " << l << std::endl;
this->m_symbol = n;
this->m_library = l;
}
virtual void print(std::ostream & out) override {
out << "external";
// for (auto p : m_idxs) {
// out << " " << p + 1;
// }
}
};
/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
typedef typed_attribute<indices_attribute_data> indices_attribute;
/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
typedef typed_attribute<key_value_data> key_value_attribute;
class user_attribute_ext {
public:
virtual ~user_attribute_ext() {}