From 29f79d71e381200a9cab98bbcd470b5d00de497e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Jul 2016 14:49:56 -0700 Subject: [PATCH] chore(library): remove dead code --- src/library/CMakeLists.txt | 2 +- src/library/tc_multigraph.cpp | 177 ---------------------------------- src/library/tc_multigraph.h | 38 -------- 3 files changed, 1 insertion(+), 216 deletions(-) delete mode 100644 src/library/tc_multigraph.cpp delete mode 100644 src/library/tc_multigraph.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 0e20297f78..6bcb4a8dbc 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -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 diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp deleted file mode 100644 index bd31db4a20..0000000000 --- a/src/library/tc_multigraph.cpp +++ /dev/null @@ -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 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 - static void insert_maplist(name_map> & 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(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 env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional(base_name)); - m_env = env_e.first; - return env_e.second; - } - - pair> operator()(name const & src, name const & edge, name const & tgt) { - buffer 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 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 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 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> 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> new_succ_lst = filter(*succ_lst, [&](pair 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 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 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> tc_multigraph::get_successors(name const & c) const { - if (auto r = m_successors.find(c)) - return *r; - else - return list>(); -} - -list tc_multigraph::get_predecessors(name const & c) const { - if (auto r = m_predecessors.find(c)) - return *r; - else - return list(); -} - -void tc_multigraph::for_each(std::function const & fn) const { - m_successors.for_each([&](name const & from, list> const & succs) { - for (pair const & p : succs) { - fn(from, p.first, p.second); - } - }); -} -} diff --git a/src/library/tc_multigraph.h b/src/library/tc_multigraph.h deleted file mode 100644 index 53b6f7551e..0000000000 --- a/src/library/tc_multigraph.h +++ /dev/null @@ -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>> m_successors; - name_map> m_predecessors; - name_map m_edges; - pair 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> 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> get_successors(name const & c) const; - list get_predecessors(name const & c) const; - void for_each(std::function const & fn) const; -}; -}