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

chore(library/blast): style

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-28 08:52:24 -08:00
parent f679ce0da9
commit 89a5d00714
4 changed files with 19 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/blast/discr_tree.cpp
View file

@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include <vector>
#include "util/rb_map.h"
#include "util/memory_pool.h"
#include "library/blast/trace.h"
@ -26,6 +28,10 @@ struct discr_tree::node_cmp {
int operator()(node const & n1, node const & n2) const;
};
void discr_tree::swap(node & n1, node & n2) {
std::swap(n1.m_ptr, n2.m_ptr);
}
struct discr_tree::edge {
edge_kind m_kind;
bool m_fn;
@ -246,7 +252,7 @@ void discr_tree::insert_erase(expr const & k, expr const & v, bool ins) {
lean_trace("discr_tree", tout() << "\n"; trace(););
}
bool discr_tree::find_atom(node const & n, edge const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) {
bool discr_tree::find_atom(node const & n, edge const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) { // NOLINT
if (auto child = n.m_ptr->m_children.find(e)) {
return find(*child, todo, fn);
} else {
@ -254,7 +260,7 @@ bool discr_tree::find_atom(node const & n, edge const & e, list<pair<expr, bool>
}
}
bool discr_tree::find_star(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) {
bool discr_tree::find_star(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) { // NOLINT
bool cont = true;
n.m_ptr->m_skip.for_each([&](node const & skip_child) {
if (cont && !find(skip_child, todo, fn))
@ -270,7 +276,7 @@ bool discr_tree::find_star(node const & n, list<pair<expr, bool>> todo, std::fun
return cont;
}
bool discr_tree::find_app(node const & n, expr const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) {
bool discr_tree::find_app(node const & n, expr const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) { // NOLINT
lean_assert(is_app(e));
buffer<expr> args;
expr const & f = get_app_args(e, args);
@ -296,7 +302,7 @@ bool discr_tree::find_app(node const & n, expr const & e, list<pair<expr, bool>>
}
}
bool discr_tree::find(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) {
bool discr_tree::find(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn) { // NOLINT
if (!todo) {
bool cont = true;
n.m_ptr->m_values.for_each([&](expr const & v) {
@ -330,7 +336,7 @@ bool discr_tree::find(node const & n, list<pair<expr, bool>> todo, std::function
lean_unreachable();
}
void discr_tree::find(expr const & e, std::function<bool(expr const &)> const & fn) const {
void discr_tree::find(expr const & e, std::function<bool(expr const &)> const & fn) const { // NOLINT
if (m_root)
find(m_root, to_list(mk_pair(e, false)), fn);
}

13
src/library/blast/discr_tree.h
View file

@ -48,9 +48,8 @@ private:
bool is_shared() const;
node steal() { node r; swap(r, *this); return r; }
void trace(optional<edge> const & e, unsigned depth, bool disj) const;
friend void swap(node & n1, node & n2) { std::swap(n1.m_ptr, n2.m_ptr); }
};
static void swap(node & n1, node & n2);
static node ensure_unshared(node && n);
static node insert_erase_atom(node && n, edge const & e, buffer<pair<expr, bool>> & todo, expr const & v, buffer<pair<node, node>> & skip, bool ins);
static node insert_erase_star(node && n, buffer<pair<expr, bool>> & todo, expr const & v, buffer<pair<node, node>> & skip, bool ins);
@ -59,10 +58,10 @@ private:
static node insert_erase(node && n, bool is_root, buffer<pair<expr, bool>> & todo, expr const & v, buffer<pair<node, node>> & skip, bool ins);
void insert_erase(expr const & k, expr const & v, bool ins);
static bool find_atom(node const & n, edge const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn);
static bool find_star(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn);
static bool find_app(node const & n, expr const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn);
static bool find(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn);
static bool find_atom(node const & n, edge const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn); // NOLINT
static bool find_star(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn); // NOLINT
static bool find_app(node const & n, expr const & e, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn); // NOLINT
static bool find(node const & n, list<pair<expr, bool>> todo, std::function<bool(expr const &)> const & fn); // NOLINT
node m_root;
public:
@ -71,7 +70,7 @@ public:
void erase(expr const & k, expr const & v) { insert_erase(k, v, false); }
void erase(expr const & k) { erase(k, k); }
void find(expr const & e, std::function<bool(expr const &)> const & fn) const;
void find(expr const & e, std::function<bool(expr const &)> const & fn) const; // NOLINT
void collect(expr const & e, buffer<expr> & r) const;
void trace() const;

2
src/library/blast/state.cpp
View file

@ -807,7 +807,7 @@ void state::remove_from_indices(hypothesis const & h, hypothesis_idx hidx) {
m_branch.m_hyp_index.erase(get_key_for(h.get_type()), h.get_self());
}
void state::find_hypotheses(expr const & e, std::function<bool(hypothesis_idx)> const & fn) const {
void state::find_hypotheses(expr const & e, std::function<bool(hypothesis_idx)> const & fn) const { // NOLINT
m_branch.m_hyp_index.find(get_key_for(e), [&](expr const & h) { return fn(href_index(h)); });
}

2
src/library/blast/state.h
View file

@ -321,7 +321,7 @@ public:
optional<hypothesis_idx> contains_hypothesis(expr const & type) const;
/** \brief Find hypotheses whose type may unify with \c e or its negation */
void find_hypotheses(expr const & e, std::function<bool(hypothesis_idx)> const & fn) const;
void find_hypotheses(expr const & e, std::function<bool(hypothesis_idx)> const & fn) const; // NOLINT
/************************
Abstracting hypotheses