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

refactor(util/trie): modify interface to avoid the creation of many temporary optional values and inc/dec reference counters

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-05 12:40:31 -07:00
parent 38f471b390
commit 5b898aa3ed
3 changed files with 99 additions and 100 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/library/token_set.cpp
View file

@ -7,18 +7,24 @@ Author: Leonardo de Moura
#include "library/token_set.h" #include "library/token_set.h"
namespace lean { namespace lean {
token_set token_set::add_command_token(char const * token) const { return token_set(insert(m_tokens, token, info(token))); } token_set add_command_token(token_set const & s, char const * token) {
token_set token_set::add_token(char const * token, unsigned prec) const { return token_set(insert(m_tokens, token, info(token, prec))); } return insert(s, token, token_info(token));
token_set token_set::add_token(char const * token, char const * val, unsigned prec) const {
return token_set(insert(m_tokens, token, info(val, prec)));
} }
token_set token_set::merge(token_set const & s) const { return token_set(::lean::merge(m_tokens, s.m_tokens)); } token_set add_token(token_set const & s, char const * token, unsigned prec) {
optional<token_set> token_set::find(char c) const { return insert(s, token, token_info(token, prec));
auto r = m_tokens.find(c); }
return r ? optional<token_set>(token_set(*r)) : optional<token_set>(); token_set add_token(token_set const & s, char const * token, char const * val, unsigned prec) {
return insert(s, token, token_info(val, prec));
}
token_set merge(token_set const & s1, token_set const & s2) {
return merge(s1, s2);
}
token_set const * find(token_set const & s, char c) {
return s.find(c);
}
token_info const * value_of(token_set const & s) {
return s.value();
} }
optional<token_set::info> token_set::value() const { return m_tokens.value(); }
static char const * g_lambda_unicode = "\u03BB"; static char const * g_lambda_unicode = "\u03BB";
static char const * g_pi_unicode = "\u03A0"; static char const * g_pi_unicode = "\u03A0";
static char const * g_forall_unicode = "\u2200"; static char const * g_forall_unicode = "\u2200";
@ -28,20 +34,20 @@ static char const * g_arrow_unicode = "\u2192";
class init_token_set_fn { class init_token_set_fn {
public: public:
token_set m_token_set; token_set m_token_set;
init_token_set_fn():m_token_set(true) { init_token_set_fn() {
char const * builtin[] = {"fun", "forall", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}", char const * builtin[] = {"fun", "forall", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}",
".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->", 0}; ".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->", 0};
char const ** it = builtin; char const ** it = builtin;
while (*it) { while (*it) {
m_token_set = m_token_set.add_token(*it); m_token_set = add_token(m_token_set, *it);
it++; it++;
} }
m_token_set = m_token_set.add_token(g_lambda_unicode, "fun"); m_token_set = add_token(m_token_set, g_lambda_unicode, "fun");
m_token_set = m_token_set.add_token(g_forall_unicode, "forall"); m_token_set = add_token(m_token_set, g_forall_unicode, "forall");
m_token_set = m_token_set.add_token(g_pi_unicode, "forall"); m_token_set = add_token(m_token_set, g_pi_unicode, "forall");
m_token_set = m_token_set.add_token(g_arrow_unicode, "->"); m_token_set = add_token(m_token_set, g_arrow_unicode, "->");
} }
}; };
static init_token_set_fn g_init; static init_token_set_fn g_init;
token_set::token_set():token_set(g_init.m_token_set) {} token_set mk_default_token_set() { return g_init.m_token_set; }
} }

38
src/library/token_set.h
View file

@ -8,34 +8,28 @@ Author: Leonardo de Moura
#include <utility> #include <utility>
#include <string> #include <string>
#include "util/trie.h" #include "util/trie.h"
#include "util/name.h"
namespace lean { namespace lean {
class token_info {
/** \brief Set of tokens and their precedences. This information is used by the scanner. */
class token_set {
class info {
bool m_command; bool m_command;
std::string m_value; name m_value;
unsigned m_precedence; unsigned m_precedence;
public: public:
info():m_command(true) {} token_info():m_command(true) {}
info(char const * val):m_command(true), m_value(val), m_precedence(0) {} token_info(char const * val):m_command(true), m_value(val), m_precedence(0) {}
info(char const * val, unsigned prec):m_command(false), m_value(val), m_precedence(prec) {} token_info(char const * val, unsigned prec):m_command(false), m_value(val), m_precedence(prec) {}
bool is_command() const { return m_command; } bool is_command() const { return m_command; }
std::string const & value() const { return m_value; } name const & value() const { return m_value; }
unsigned precedence() const { return m_precedence; } unsigned precedence() const { return m_precedence; }
}; };
ctrie<info> m_tokens;
explicit token_set(ctrie<info> const & t):m_tokens(t) {} typedef ctrie<token_info> token_set;
friend class init_token_set_fn; token_set mk_default_token_set();
token_set(bool) {} // NOLINT token_set add_command_token(token_set const & s, char const * token);
public: token_set add_token(token_set const & s, char const * token, unsigned prec = 0);
token_set(); token_set add_token(token_set const & s, char const * token, char const * val, unsigned prec = 0);
token_set add_command_token(char const * token) const; token_set merge(token_set const & s1, token_set const & s2);
token_set add_token(char const * token, unsigned prec = 0) const; token_set const * find(token_set const & s, char c);
token_set add_token(char const * token, char const * val, unsigned prec = 0) const; token_info const * value_of(token_set const & s);
token_set merge(token_set const & s) const;
optional<token_set> find(char c) const;
optional<info> value() const;
};
} }

113
src/util/trie.h
View file

@ -14,24 +14,10 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
template<typename Key, typename Val, typename KeyCMP> template<typename Key, typename Val, typename KeyCMP>
class trie : public KeyCMP { class trie : public KeyCMP {
struct cell; friend struct cell;
struct node {
cell * m_ptr;
node():m_ptr(new cell()) { m_ptr->inc_ref(); }
node(cell * ptr):m_ptr(ptr) { if (m_ptr) ptr->inc_ref(); }
node(node const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
node(node && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~node() { if (m_ptr) m_ptr->dec_ref(); }
node & operator=(node const & n) { LEAN_COPY_REF(n); }
node & operator=(node&& n) { LEAN_MOVE_REF(n); }
cell * operator->() const { lean_assert(m_ptr); return m_ptr; }
bool is_shared() const { return m_ptr && m_ptr->get_rc() > 1; }
friend void swap(node & n1, node & n2) { std::swap(n1.m_ptr, n2.m_ptr); }
node steal() { node r; swap(r, *this); return r; }
};
struct cell { struct cell {
rb_map<Key, node, KeyCMP> m_children; rb_map<Key, trie, KeyCMP> m_children;
optional<Val> m_value; optional<Val> m_value;
MK_LEAN_RC(); MK_LEAN_RC();
void dealloc() { delete this; } void dealloc() { delete this; }
@ -40,27 +26,29 @@ class trie : public KeyCMP {
cell(cell const & s):m_children(s.m_children), m_value(s.m_value), m_rc(0) {} cell(cell const & s):m_children(s.m_children), m_value(s.m_value), m_rc(0) {}
}; };
static node ensure_unshared(node && n) { static trie ensure_unshared(trie && n) {
if (n.is_shared()) if (n.is_shared())
return node(new cell(*n.m_ptr)); return trie(new cell(*n.m_ptr));
else else
return n; return n;
} }
template<typename It> template<typename It>
static node insert(node && n, It const & begin, It const & end, Val const & v) { static trie insert(trie && n, It const & begin, It const & end, Val const & v) {
node h = ensure_unshared(n.steal()); trie h = ensure_unshared(n.steal());
if (!h.m_ptr)
h = trie(new cell());
if (begin == end) { if (begin == end) {
h->m_value = v; h->m_value = v;
return h; return h;
} else { } else {
Key k = *begin; Key k = *begin;
node const * c = h->m_children.find(k); trie const * c = h->m_children.find(k);
It it(begin); it++; It it(begin); it++;
if (c == nullptr) { if (c == nullptr) {
h->m_children.insert(k, insert(node(), it, end, v)); h->m_children.insert(k, insert(trie(), it, end, v));
} else { } else {
node n(*c); trie n(*c);
h->m_children.erase(k); h->m_children.erase(k);
h->m_children.insert(k, insert(n.steal(), it, end, v)); h->m_children.insert(k, insert(n.steal(), it, end, v));
} }
@ -68,15 +56,15 @@ class trie : public KeyCMP {
} }
} }
static node merge(node && t1, node const & t2) { static trie merge(trie && t1, trie const & t2) {
node new_t1 = ensure_unshared(t1.steal()); trie new_t1 = ensure_unshared(t1.steal());
new_t1->m_value = t2->m_value; new_t1->m_value = t2->m_value;
t2->m_children.for_each([&](Key const & k, node const & c2) { t2->m_children.for_each([&](Key const & k, trie const & c2) {
node const * c1 = new_t1->m_children.find(k); trie const * c1 = new_t1->m_children.find(k);
if (c1 == nullptr) { if (c1 == nullptr) {
new_t1->m_children.insert(k, c2); new_t1->m_children.insert(k, c2);
} else { } else {
node n1(*c1); trie n1(*c1);
new_t1->m_children.erase(k); new_t1->m_children.erase(k);
new_t1->m_children.insert(k, merge(n1.steal(), c2)); new_t1->m_children.insert(k, merge(n1.steal(), c2));
} }
@ -85,63 +73,74 @@ class trie : public KeyCMP {
} }
template<typename F> template<typename F>
static void for_each(F && f, node const & n, buffer<Key> & prefix) { static void for_each(F && f, trie const & n, buffer<Key> & prefix) {
if (n->m_value) { if (n->m_value) {
f(prefix.size(), prefix.data(), *(n->m_value)); f(prefix.size(), prefix.data(), *(n->m_value));
} }
n->m_children.for_each([&](Key const & k, node const & c) { n->m_children.for_each([&](Key const & k, trie const & c) {
prefix.push_back(k); prefix.push_back(k);
for_each(f, c, prefix); for_each(f, c, prefix);
prefix.pop_back(); prefix.pop_back();
}); });
} }
node m_root; cell * m_ptr;
trie(node const & n):m_root(n) {} cell * operator->() const { lean_assert(m_ptr); return m_ptr; }
public:
trie() {}
trie(trie const & s):m_root(s.m_root) {}
trie(trie && s):m_root(s.m_root) {}
trie & operator=(trie const & s) { m_root = s.m_root; return *this; } trie(cell * ptr):m_ptr(ptr) { if (m_ptr) ptr->inc_ref(); }
trie & operator=(trie && s) { m_root = s.m_root; return *this; } trie steal() { trie r; swap(r, *this); return r; }
public:
trie():m_ptr(nullptr) {}
trie(trie const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
trie(trie && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~trie() { if (m_ptr) m_ptr->dec_ref(); }
trie & operator=(trie const & n) { LEAN_COPY_REF(n); }
trie & operator=(trie&& n) { LEAN_MOVE_REF(n); }
bool is_shared() const { return m_ptr && m_ptr->get_rc() > 1; }
friend void swap(trie & n1, trie & n2) { std::swap(n1.m_ptr, n2.m_ptr); }
template<typename It> template<typename It>
optional<Val> find(It const & begin, It const & end) const { Val const * find(It const & begin, It const & end) const {
node const * n = &m_root; if (!m_ptr)
return nullptr;
cell const * c = m_ptr;
for (It it = begin; it != end; ++it) { for (It it = begin; it != end; ++it) {
n = (*n)->m_children.find(*it); trie const * n = c->m_children.find(*it);
if (!n) if (!n)
return optional<Val>(); return nullptr;
c = n->m_ptr;
} }
return (*n)->m_value; if (c->m_value)
return &c->m_value.value();
else
return nullptr;
} }
template<typename It> template<typename It>
void insert(It const & begin, It const & end, Val const & v) { void insert(It const & begin, It const & end, Val const & v) {
m_root = insert(m_root.steal(), begin, end, v); *this = insert(steal(), begin, end, v);
} }
optional<trie> find(Key const & k) const { trie const * find(Key const & k) const {
node const * c = m_root->m_children.find(k); return m_ptr ? m_ptr->m_children.find(k) : nullptr;
if (c) }
return optional<trie>(trie(*c));
Val const * value() const {
if (m_ptr && m_ptr->m_value)
return &m_ptr->m_value.value();
else else
return optional<trie>(); return nullptr;
}
optional<Val> value() const {
return m_root->m_value;
} }
void merge(trie const & t) { void merge(trie const & t) {
m_root = merge(m_root.steal(), t.m_root); *this = merge(steal(), t);
} }
template<typename F> template<typename F>
void for_each(F && f) const { void for_each(F && f) const {
buffer<Key> prefix; buffer<Key> prefix;
for_each(f, m_root, prefix); for_each(f, *this, prefix);
} }
// for debugging purposes // for debugging purposes
@ -176,10 +175,10 @@ inline ctrie<Val> insert(ctrie<Val> const & t, char const * str, Val const & v)
} }
template<typename Val> template<typename Val>
optional<Val> find(ctrie<Val> const & t, std::string const & str) { return t.find(str.begin(), str.end()); } Val const * find(ctrie<Val> const & t, std::string const & str) { return t.find(str.begin(), str.end()); }
template<typename Val> template<typename Val>
optional<Val> find(ctrie<Val> const & t, char const * str) { return t.find(str, str + strlen(str)); } Val const * find(ctrie<Val> const & t, char const * str) { return t.find(str, str + strlen(str)); }
template<typename Val> template<typename Val>
inline ctrie<Val> merge(ctrie<Val> const & t1, ctrie<Val> const & t2) { inline ctrie<Val> merge(ctrie<Val> const & t1, ctrie<Val> const & t2) {