fix(library/tc_multigraph): typos
This commit is contained in:
parent
ee0d919c6f
commit
6872761c67
3 changed files with 11 additions and 8 deletions
|
@ -14,6 +14,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
|
||||||
local_context.cpp choice_iterator.cpp pp_options.cpp
|
local_context.cpp choice_iterator.cpp pp_options.cpp
|
||||||
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
|
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
|
||||||
relation_manager.cpp export.cpp user_recursors.cpp
|
relation_manager.cpp export.cpp user_recursors.cpp
|
||||||
class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp)
|
class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp
|
||||||
|
tc_multigraph.cpp)
|
||||||
|
|
||||||
target_link_libraries(library ${LEAN_LIBS})
|
target_link_libraries(library ${LEAN_LIBS})
|
||||||
|
|
|
@ -4,15 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
Author: Leonardo de Moura
|
||||||
*/
|
*/
|
||||||
|
#include "kernel/type_checker.h"
|
||||||
#include "library/tc_multigraph.h"
|
#include "library/tc_multigraph.h"
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
pair<environment, list<name>> tc_multigraph::add(environment const & env, name const & e, unsigned num_args) {
|
pair<environment, list<name>> tc_multigraph::add(environment const & env, name const & /* e */, unsigned /* num_args */) {
|
||||||
// TODO(Leo)
|
// TODO(Leo)
|
||||||
return mk_pair(env, list<name>());
|
return mk_pair(env, list<name>());
|
||||||
}
|
}
|
||||||
pair<environment, list<name>> tc_multigraph::add(environment const & env, name const & e) {
|
pair<environment, list<name>> tc_multigraph::add(environment const & env, name const & e) {
|
||||||
|
declaration const & d = env.get(e);
|
||||||
|
return add(env, e, get_arity(d.get_type()));
|
||||||
}
|
}
|
||||||
void tc_multigraph::erase(name const & e) {
|
void tc_multigraph::erase(name const & e) {
|
||||||
auto src = m_edges.find(e);
|
auto src = m_edges.find(e);
|
||||||
|
@ -31,14 +33,14 @@ void tc_multigraph::erase(name const & e) {
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
lean_assert(!tgt.is_anonymous());
|
lean_assert(!tgt.is_anonymous());
|
||||||
m_successors.insert(src, new_succ_lst);
|
m_successors.insert(*src, new_succ_lst);
|
||||||
if (std::all_of(new_succs.begin(), new_succs.end(), [&](pair<name, name> const & p) {
|
if (std::all_of(new_succ_lst.begin(), new_succ_lst.end(), [&](pair<name, name> const & p) {
|
||||||
return p.second != tgt;
|
return p.second != tgt;
|
||||||
})) {
|
})) {
|
||||||
// e is the last edge from src to tgt
|
// e is the last edge from src to tgt
|
||||||
auto pred_lst = m_predecessors.find(tgt);
|
auto pred_lst = m_predecessors.find(tgt);
|
||||||
lean_assert(pred_list);
|
lean_assert(pred_list);
|
||||||
list<name> new_pred_lst = filter(*pred_lst, [&](name const & n) { return n != src; });
|
list<name> new_pred_lst = filter(*pred_lst, [&](name const & n) { return n != *src; });
|
||||||
m_predecessors.insert(tgt, new_pred_lst);
|
m_predecessors.insert(tgt, new_pred_lst);
|
||||||
}
|
}
|
||||||
m_edges.erase(e);
|
m_edges.erase(e);
|
||||||
|
|
|
@ -20,7 +20,7 @@ public:
|
||||||
bool is_node(name const & c) const;
|
bool is_node(name const & c) const;
|
||||||
list<pair<name, name>> get_successors(name const & c) const;
|
list<pair<name, name>> get_successors(name const & c) const;
|
||||||
list<name> get_predecessors(name const & c) const;
|
list<name> get_predecessors(name const & c) const;
|
||||||
static bool is_fun_sink(name const & c) const;
|
static bool is_fun_sink(name const & c);
|
||||||
static bool is_sort_sink(name const & c) const;
|
static bool is_sort_sink(name const & c);
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue