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

refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-07 16:47:41 -07:00
parent 826166c257
commit 8fa171cb92
5 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -816,7 +816,7 @@ expr elaborator::visit(expr const & e, constraint_seq & cs) {
unify_result_seq elaborator::solve(constraint_seq const & cs) {
buffer<constraint> 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) {

2
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -230,7 +230,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> 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<substitution, constraints> const & p) {
substitution new_s = p.first;
expr result = new_s.instantiate(new_meta);

2
src/frontends/lean/proof_qed_elaborator.cpp
View file

@ -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;

10
src/library/unifier.cpp
View file

@ -2148,8 +2148,8 @@ unify_result_seq unify(std::shared_ptr<unifier_fn> 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<unifier_fn>(env, num_cs, cs, ngen, substitution(), cfg));
substitution const & s, unifier_config const & cfg) {
return unify(std::make_shared<unifier_fn>(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<constraint> 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));
}

4
src/library/unifier.h
View file

@ -48,9 +48,9 @@ struct unifier_config {
typedef lazy_list<pair<substitution, constraints>> 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,