From aeea8f83c47555f4c6a125e5d010ffe62ff3f006 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jun 2015 16:00:59 -0700 Subject: [PATCH] feat(library/composition_manager): check if existing definition is definitionally equal --- src/library/composition_manager.cpp | 22 ++++++++++++++++++---- src/library/composition_manager.h | 2 +- src/library/init_module.cpp | 3 +++ src/library/tc_multigraph.cpp | 27 +++++++++++++++++++-------- 4 files changed, 41 insertions(+), 13 deletions(-) diff --git a/src/library/composition_manager.cpp b/src/library/composition_manager.cpp index c6f8bef87..ce6ed7d45 100644 --- a/src/library/composition_manager.cpp +++ b/src/library/composition_manager.cpp @@ -34,8 +34,7 @@ static environment update(environment const & env, composition_manager_ext const return env.update(g_ext->m_ext_id, std::make_shared(ext)); } -pair compose(type_checker & tc, name const & g, name const & f, optional const & gf) { - environment const & env = tc.env(); +pair compose(environment const & env, type_checker & tc, name const & g, name const & f, optional const & gf) { composition_manager_ext ext = get_extension(env); if (name const * it = ext.m_cache.find(mk_pair(g, f))) return mk_pair(env, *it); @@ -70,7 +69,22 @@ pair compose(type_checker & tc, name const & g, name const & unsigned idx = 1; // make sure name is unique - while (env.find(new_name)) { + while (true) { + auto it = env.find(new_name); + if (!it) + break; + if (it->is_definition() && it->get_num_univ_params() == f_decl.get_num_univ_params()) { + // check if definitions is definitionally equal to exisiting one + expr it_type = instantiate_type_univ_params(*it, f_ls); + expr it_val = instantiate_value_univ_params(*it, f_ls); + if (tc.is_def_eq(it_type, new_type).first && tc.is_def_eq(it_val, new_val).first) { + // environment already contains a definition that is definitially equal to the new one. + // So, we do not need to create a new one + ext.m_cache.insert(mk_pair(g, f), new_name); + environment new_env = module::add(env, *g_key, [=](environment const &, serializer & s) { s << g << f << new_name; }); + return mk_pair(update(new_env, ext), new_name); + } + } new_name = base_name.append_after(idx); idx++; } @@ -84,7 +98,7 @@ pair compose(type_checker & tc, name const & g, name const & pair compose(environment const & env, name const & g, name const & f, optional const & gf) { type_checker tc(env); - return compose(tc, g, f, gf); + return compose(env, tc, g, f, gf); } static void composition_reader(deserializer & d, shared_environment & senv, diff --git a/src/library/composition_manager.h b/src/library/composition_manager.h index 0f851ec31..4ee4ed3a4 100644 --- a/src/library/composition_manager.h +++ b/src/library/composition_manager.h @@ -13,7 +13,7 @@ namespace lean { If the environment already has a definition with this name, then adds the prefix _idx, where idx is a numeral. The result is a pair (new environment, new constant name). */ -pair compose(type_checker & tc, name const & g, name const & f, optional const & gf = optional()); +pair compose(environment const & env, type_checker & tc, name const & g, name const & f, optional const & gf = optional()); pair compose(environment const & env, name const & g, name const & f, optional const & gf = optional()); void initialize_composition_manager(); void finalize_composition_manager(); diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 5c23e2f3d..afe95b491 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -40,6 +40,7 @@ Author: Leonardo de Moura #include "library/user_recursors.h" #include "library/class_instance_synth.h" #include "library/composition_manager.h" +#include "library/tc_multigraph.h" namespace lean { void initialize_library_module() { @@ -79,9 +80,11 @@ void initialize_library_module() { initialize_user_recursors(); initialize_class_instance_elaborator(); initialize_composition_manager(); + initialize_tc_multigraph(); } void finalize_library_module() { + finalize_tc_multigraph(); finalize_composition_manager(); finalize_class_instance_elaborator(); finalize_user_recursors(); diff --git a/src/library/tc_multigraph.cpp b/src/library/tc_multigraph.cpp index 62d40b23e..93c566d2b 100644 --- a/src/library/tc_multigraph.cpp +++ b/src/library/tc_multigraph.cpp @@ -63,7 +63,7 @@ struct add_edge_fn { name compose(name const & src, name const & e1, name const & e2, name const & tgt) { name n = src + name("to") + tgt; - pair env_e = ::lean::compose(*m_tc, e2, e1, optional(n)); + pair env_e = ::lean::compose(m_env, *m_tc, e2, e1, optional(n)); m_env = env_e.first; return env_e.second; } @@ -117,9 +117,15 @@ struct add_edge_fn { /** \brief Return true iff args contains Var(0), Var(1), ..., Var(args.size() - 1) */ static bool check_var_args(buffer const & args) { + buffer found; + found.resize(args.size(), false); for (unsigned i = 0; i < args.size(); i++) { - if (!is_var(args[i]) || var_idx(args[i]) != i) + if (!is_var(args[i])) return false; + unsigned idx = var_idx(args[i]); + if (idx >= args.size() || found[idx]) + return false; + found[idx] = true; } return true; } @@ -149,16 +155,19 @@ pair tc_multigraph::validate(environment const & env, name const & e declaration const & d = env.get(e); expr type = d.get_type(); for (unsigned i = 0; i < num_args; i++) { - if (!is_pi(type)) + if (!is_pi(type)) { throw_ex(m_kind, e); + } type = binding_body(type); } - if (!is_pi(type)) + if (!is_pi(type)) { throw_ex(m_kind, e); + } buffer args; expr const & C = get_app_args(binding_domain(type), args); - if (!is_constant(C) || !check_levels(const_levels(C), d.get_univ_params()) || !check_var_args(args)) + if (!is_constant(C) || !check_levels(const_levels(C), d.get_univ_params()) || !check_var_args(args)) { throw_ex(m_kind, e); + } name src = const_name(C); type = binding_body(type); name tgt; @@ -168,13 +177,15 @@ pair tc_multigraph::validate(environment const & env, name const & e tgt = *g_fun_sink; } else { expr const & D = get_app_fn(type); - if (is_constant(D)) + if (is_constant(D)) { tgt = const_name(D); - else + } else { throw_ex(m_kind, e); + } } - if (src == tgt) + if (src == tgt) { throw_ex(m_kind, e); + } return mk_pair(src, tgt); }