max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-29 14:49:56 -07:00
parent 0169989411
commit 29f79d71e3
3 changed files with 1 additions and 216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/CMakeLists.txt
View file

@ -9,7 +9,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp pp_options.cpp
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
composition_manager.cpp noncomputable.cpp
aux_recursors.cpp norm_num.cpp trace.cpp
attribute_manager.cpp error_handling.cpp unification_hint.cpp
local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp

177
src/library/tc_multigraph.cpp
View file

@ -1,177 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sstream.h"
#include "library/tc_multigraph.h"
#include "library/old_type_checker.h"
#include "library/composition_manager.h"
#include "library/old_util.h"
namespace lean {
struct add_edge_fn {
environment m_env;
old_type_checker_ptr m_tc;
tc_multigraph & m_graph;
add_edge_fn(environment const & env, tc_multigraph & g):
m_env(env), m_tc(new old_type_checker(env)), m_graph(g) {}
// Return true iff the types of constants c1 and c2 are equal.
bool is_def_eq(name const & c1, name const & c2) {
if (c1 == c2)
return true;
declaration const & d1 = m_env.get(c1);
declaration const & d2 = m_env.get(c2);
if (d1.get_num_univ_params() != d2.get_num_univ_params())
return false;
return m_tc->is_def_eq(d1.get_type(), d2.get_type()).first;
}
// Erase edges that are definitionally equal to edge
void erase_def_eqs(name const & src, name const & edge, name const & tgt) {
buffer<name> to_delete;
for (auto const & p : m_graph.get_successors(src)) {
if (p.second == tgt) {
if (is_def_eq(p.first, edge))
to_delete.push_back(p.first);
}
}
for (name const & e : to_delete)
m_graph.erase(e);
}
template<typename Val>
static void insert_maplist(name_map<list<Val>> & m, name const & k, Val const & v) {
if (auto it = m.find(k)) {
m.insert(k, cons(v, filter(*it, [&](Val const & v2) { return v2 != v; })));
} else {
m.insert(k, list<Val>(v));
}
}
void add_core(name const & src, name const & edge, name const & tgt) {
erase_def_eqs(src, edge, tgt);
insert_maplist(m_graph.m_successors, src, mk_pair(edge, tgt));
insert_maplist(m_graph.m_predecessors, tgt, src);
m_graph.m_edges.insert(edge, src);
}
name compose(name const & base_name, name const & e1, name const & e2) {
pair<environment, name> env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional<name>(base_name));
m_env = env_e.first;
return env_e.second;
}
pair<environment, list<tc_edge>> operator()(name const & src, name const & edge, name const & tgt) {
buffer<tc_edge> new_edges;
if (auto preds = m_graph.m_predecessors.find(src)) {
name base_name = edge.append_before("_trans_to_");
for (name const & pred : *preds) {
if (pred == tgt)
continue; // avoid loops
if (auto pred_succ = m_graph.m_successors.find(pred)) {
for (pair<name, name> const & p : *pred_succ) {
if (p.second != src)
continue;
name new_e = compose(base_name, p.first, edge);
new_edges.emplace_back(pred, new_e, tgt);
}
}
}
}
m_tc.reset(new old_type_checker(m_env)); // update to reflect new constants in the environment
buffer<tc_edge> new_back_edges;
new_back_edges.append(new_edges);
if (auto succs = m_graph.m_successors.find(tgt)) {
name base_name = edge.append_before("_trans_of_");
for (pair<name, name> const & p : *succs) {
if (src == p.second)
continue; // avoid loops
name new_e = compose(base_name, edge, p.first);
new_edges.emplace_back(src, new_e, p.second);
for (auto const & back_edge : new_back_edges) {
if (back_edge.m_from != p.second)
continue;
name new_e = compose(base_name, back_edge.m_cnst, p.first);
new_edges.emplace_back(back_edge.m_from, new_e, p.second);
}
}
}
return mk_pair(m_env, to_list(new_edges));
}
};
pair<environment, list<tc_edge>> tc_multigraph::add(environment const & env, name const & src, name const & e, name const & tgt) {
return add_edge_fn(env, *this)(src, e, tgt);
}
void tc_multigraph::add1(environment const & env, name const & src, name const & e, name const & tgt) {
return add_edge_fn(env, *this).add_core(src, e, tgt);
}
void tc_multigraph::erase(name const & e) {
auto src = m_edges.find(e);
if (!src)
return;
auto succ_lst = m_successors.find(*src);
lean_assert(succ_lst);
name tgt;
list<pair<name, name>> new_succ_lst = filter(*succ_lst, [&](pair<name, name> const & p) {
if (p.first == e) {
lean_assert(tgt.is_anonymous());
tgt = p.second;
return false;
} else {
return true;
}
});
lean_assert(!tgt.is_anonymous());
m_successors.insert(*src, new_succ_lst);
if (std::all_of(new_succ_lst.begin(), new_succ_lst.end(), [&](pair<name, name> const & p) {
return p.second != tgt;
})) {
// e is the last edge from src to tgt
auto pred_lst = m_predecessors.find(tgt);
lean_assert(pred_lst);
list<name> new_pred_lst = filter(*pred_lst, [&](name const & n) { return n != *src; });
if (new_pred_lst)
m_predecessors.insert(tgt, new_pred_lst);
else
m_predecessors.erase(tgt);
}
m_edges.erase(e);
}
bool tc_multigraph::is_edge(name const & e) const {
return m_edges.contains(e);
}
bool tc_multigraph::is_node(name const & c) const {
return m_successors.contains(c) || m_predecessors.contains(c);
}
list<pair<name, name>> tc_multigraph::get_successors(name const & c) const {
if (auto r = m_successors.find(c))
return *r;
else
return list<pair<name, name>>();
}
list<name> tc_multigraph::get_predecessors(name const & c) const {
if (auto r = m_predecessors.find(c))
return *r;
else
return list<name>();
}
void tc_multigraph::for_each(std::function<void(name const &, name const &, name const &)> const & fn) const {
m_successors.for_each([&](name const & from, list<pair<name, name>> const & succs) {
for (pair<name, name> const & p : succs) {
fn(from, p.first, p.second);
}
});
}
}

38
src/library/tc_multigraph.h
View file

@ -1,38 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/environment.h"
namespace lean {
struct tc_edge {
name m_from;
name m_cnst; // constant representing the edge in the environment
name m_to;
tc_edge(name const & from, name const & e, name const & to):
m_from(from), m_cnst(e), m_to(to) {}
};
/** \brief Transitive closed multigraph */
class tc_multigraph {
name m_kind;
name_map<list<pair<name, name>>> m_successors;
name_map<list<name>> m_predecessors;
name_map<name> m_edges;
pair<name, name> validate(environment const & env, name const & e, unsigned num_args);
friend struct add_edge_fn;
public:
tc_multigraph(name const & kind):m_kind(kind) {}
/** \brief Add a new edge, and return updated environment, and list of transitive edges added to the graph. */
pair<environment, list<tc_edge>> add(environment const & env, name const & src, name const & e, name const & tgt);
void add1(environment const & env, name const & src, name const & e, name const & tgt);
void erase(name const & e);
bool is_edge(name const & e) const;
bool is_node(name const & c) const;
list<pair<name, name>> get_successors(name const & c) const;
list<name> get_predecessors(name const & c) const;
void for_each(std::function<void(name const &, name const &, name const &)> const & fn) const;
};
}