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

refactor(library/tc_multigraph): improve tc_multigraph API

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-01 16:01:40 -07:00
parent 765865ed41
commit fe26c37fcb
3 changed files with 26 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/class.cpp
View file

@ -309,15 +309,15 @@ environment add_trans_instance(environment const & env, name const & n, unsigned
pair<name, name> src_tgt = get_source_target(env, *tc, n);
class_state const & s = class_ext::get_state(env);
tc_multigraph g = s.m_mgraph;
pair<environment, list<name>> new_env_insts = g.add(env, src_tgt.first, n, src_tgt.second);
pair<environment, list<tc_edge>> 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<name, name> 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;
}

26
src/library/tc_multigraph.cpp
View file

@ -87,8 +87,8 @@ struct add_edge_fn {
return env_e.second;
}
pair<environment, list<name>> operator()(name const & src, name const & edge, name const & tgt) {
buffer<std::tuple<name, name, name>> new_edges;
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)) {
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<std::tuple<name, name, name>> new_back_edges;
buffer<tc_edge> new_back_edges;
new_back_edges.append(new_edges);
if (auto succs = m_graph.m_successors.find(tgt)) {
for (pair<name, name> 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<name> 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<environment, list<name>> tc_multigraph::add(environment const & env, name const & src, name const & e, name const & tgt) {
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);
}

11
src/library/tc_multigraph.h
View file

@ -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<environment, list<name>> 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<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;