From 8fa171cb92ad5ebcdbdc19acad554f1789ad5d34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2014 16:47:41 -0700 Subject: [PATCH] refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument --- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/placeholder_elaborator.cpp | 2 +- src/frontends/lean/proof_qed_elaborator.cpp | 2 +- src/library/unifier.cpp | 10 ++++++---- src/library/unifier.h | 4 ++-- 5 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 323d54a29..e1d0384ea 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -816,7 +816,7 @@ expr elaborator::visit(expr const & e, constraint_seq & cs) { unify_result_seq elaborator::solve(constraint_seq const & cs) { buffer tmp; cs.linearize(tmp); - return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), m_unifier_config); + return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), substitution(), m_unifier_config); } void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) { diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 7aad2c9c9..b8de44c76 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -230,7 +230,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const unifier_config new_cfg(cfg); new_cfg.m_discard = false; new_cfg.m_use_exceptions = false; - unify_result_seq seq1 = unify(env, 1, &c, ngen, new_cfg); + unify_result_seq seq1 = unify(env, 1, &c, ngen, substitution(), new_cfg); unify_result_seq seq2 = filter(seq1, [=](pair const & p) { substitution new_s = p.first; expr result = new_s.instantiate(new_meta); diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp index 08d91bfd8..c1706facf 100644 --- a/src/frontends/lean/proof_qed_elaborator.cpp +++ b/src/frontends/lean/proof_qed_elaborator.cpp @@ -38,7 +38,7 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons unifier_config new_cfg(cfg); new_cfg.m_discard = false; - unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, new_cfg); + unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg); auto p = seq.pull(); lean_assert(p); substitution new_s = p->first.first; diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 736489e05..0b252a251 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -2148,8 +2148,8 @@ unify_result_seq unify(std::shared_ptr u) { } unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - unifier_config const & cfg) { - return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), cfg)); + substitution const & s, unifier_config const & cfg) { + return unify(std::make_shared(env, num_cs, cs, ngen, s, cfg)); } unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, @@ -2295,8 +2295,10 @@ static int unify(lua_State * L) { } else { buffer cs; to_constraint_buffer(L, 2, cs); - if (nargs == 4) - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), unifier_config(to_options(L, 4))); + if (nargs == 5) + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4), unifier_config(to_options(L, 5))); + else if (nargs == 4) + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_substitution(L, 4)); else r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3)); } diff --git a/src/library/unifier.h b/src/library/unifier.h index 6c31c74b4..6fbdf59ee 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -48,9 +48,9 @@ struct unifier_config { typedef lazy_list> unify_result_seq; unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - unifier_config const & c = unifier_config()); -unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque, substitution const & s = substitution(), unifier_config const & c = unifier_config()); +unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, + bool relax_main_opaque, substitution const & s = substitution(), unifier_config const & c = unifier_config()); /** The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance,