From fe26c37fcb373a5fbd938d4e44026faa9b0c36c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jul 2015 16:01:40 -0700 Subject: [PATCH] refactor(library/tc_multigraph): improve tc_multigraph API --- src/library/class.cpp | 16 ++++++++-------- src/library/tc_multigraph.cpp | 26 ++++++++------------------ src/library/tc_multigraph.h | 11 ++++++++++- 3 files changed, 26 insertions(+), 27 deletions(-) diff --git a/src/library/class.cpp b/src/library/class.cpp index 9ff85f1e7..d31aa93ef 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -309,15 +309,15 @@ environment add_trans_instance(environment const & env, name const & n, unsigned pair src_tgt = get_source_target(env, *tc, n); class_state const & s = class_ext::get_state(env); tc_multigraph g = s.m_mgraph; - pair> new_env_insts = g.add(env, src_tgt.first, n, src_tgt.second); + pair> new_env_insts = g.add(env, src_tgt.first, n, src_tgt.second); environment new_env = new_env_insts.first; - new_env = class_ext::add_entry(new_env, get_dummy_ios(), class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), persistent); - tc = mk_type_checker(new_env, name_generator()); - for (name const & tn : new_env_insts.second) { - pair d_src_tgt = get_source_target(new_env, *tc, tn); - new_env = class_ext::add_entry(new_env, get_dummy_ios(), class_entry::mk_derived_trans_inst(d_src_tgt.first, d_src_tgt.second, tn), persistent); - new_env = set_reducible(new_env, tn, reducible_status::Reducible, persistent); - new_env = add_protected(new_env, tn); + new_env = class_ext::add_entry(new_env, get_dummy_ios(), + class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), persistent); + for (tc_edge const & edge : new_env_insts.second) { + new_env = class_ext::add_entry(new_env, get_dummy_ios(), + class_entry::mk_derived_trans_inst(edge.m_from, edge.m_to, edge.m_cnst), persistent); + new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, persistent); + new_env = add_protected(new_env, edge.m_cnst); } return new_env; } diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp index 563f69381..6b31eb727 100644 --- a/src/library/tc_multigraph.cpp +++ b/src/library/tc_multigraph.cpp @@ -87,8 +87,8 @@ struct add_edge_fn { return env_e.second; } - pair> operator()(name const & src, name const & edge, name const & tgt) { - buffer> new_edges; + pair> operator()(name const & src, name const & edge, name const & tgt) { + buffer new_edges; if (auto preds = m_graph.m_predecessors.find(src)) { for (name const & pred : *preds) { if (pred == tgt) @@ -104,7 +104,7 @@ struct add_edge_fn { } } m_tc.reset(new type_checker(m_env)); // update to reflect new constants in the environment - buffer> new_back_edges; + buffer new_back_edges; new_back_edges.append(new_edges); if (auto succs = m_graph.m_successors.find(tgt)) { for (pair const & p : *succs) { @@ -113,28 +113,18 @@ struct add_edge_fn { name new_e = compose(src, edge, p.first, p.second); new_edges.emplace_back(src, new_e, p.second); for (auto const & back_edge : new_back_edges) { - name bsrc, bedge, btgt; - std::tie(bsrc, bedge, btgt) = back_edge; - if (bsrc != p.second) + if (back_edge.m_from != p.second) continue; - name new_e = compose(bsrc, bedge, p.first, p.second); - new_edges.emplace_back(bsrc, new_e, p.second); + name new_e = compose(back_edge.m_from, back_edge.m_cnst, p.first, p.second); + new_edges.emplace_back(back_edge.m_from, new_e, p.second); } } } - buffer new_cnsts; - add_core(src, edge, tgt); - for (auto const & new_edge : new_edges) { - name nsrc, nedge, ntgt; - std::tie(nsrc, nedge, ntgt) = new_edge; - add_core(nsrc, nedge, ntgt); - new_cnsts.push_back(nedge); - } - return mk_pair(m_env, to_list(new_cnsts)); + 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) { +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); } diff --git a/src/library/tc_multigraph.h b/src/library/tc_multigraph.h index ce79d7fdc..63cd041fd 100644 --- a/src/library/tc_multigraph.h +++ b/src/library/tc_multigraph.h @@ -7,6 +7,14 @@ 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; @@ -17,7 +25,8 @@ class tc_multigraph { friend struct add_edge_fn; public: tc_multigraph(name const & kind):m_kind(kind) {} - pair> add(environment const & env, name const & src, name const & e, name const & tgt); + /** \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;