From bd0e9d958df9222dd5436640f34222412d7bcb53 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jun 2015 12:23:24 -0700 Subject: [PATCH] feat(library/tc_multigraph): shorter names for transitive edges see issue #666 --- src/library/tc_multigraph.cpp | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp index 93c566d2b..b1296b21b 100644 --- a/src/library/tc_multigraph.cpp +++ b/src/library/tc_multigraph.cpp @@ -61,8 +61,29 @@ struct add_edge_fn { m_graph.m_edges.insert(edge, src); } + + static name compose_name_core(name const & src, name const & tgt) { + return src + name("to") + tgt; + } + + static name compose_name(name const & p, name const & src, name const & tgt) { + if (is_prefix_of(p, tgt)) + return compose_name_core(src, tgt.replace_prefix(p, name())); + else if (p.is_atomic()) + return compose_name_core(src, tgt); + else + return compose_name(p.get_prefix(), src, tgt); + } + + static name compose_name(name const & src, name const & tgt) { + if (src.is_atomic()) + return compose_name_core(src, tgt); + else + return compose_name(src.get_prefix(), src, tgt); + } + name compose(name const & src, name const & e1, name const & e2, name const & tgt) { - name n = src + name("to") + tgt; + name n = compose_name(src, tgt); pair env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional(n)); m_env = env_e.first; return env_e.second;