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

fix(library/tactic/class_instance_synth): discard partial solutions even when option class.unique_instances = true is used

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-12 10:13:16 -07:00
parent 47a350d888
commit b38c943086
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/tactic/class_instance_synth.cpp
View file

@ -375,11 +375,18 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
}; };
unify_result_seq seq1 = unify(env, 1, &c, ngen, substitution(), 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);
// We only keep complete solutions (modulo universe metavariables)
return !has_expr_metavar_relaxed(result);
});
if (get_class_unique_class_instances(C->m_ios.get_options())) { if (get_class_unique_class_instances(C->m_ios.get_options())) {
optional<expr> solution; optional<expr> solution;
substitution subst; substitution subst;
constraints cnstrs; constraints cnstrs;
for_each(seq1, [&](pair<substitution, constraints> const & p) { for_each(seq2, [&](pair<substitution, constraints> const & p) {
subst = p.first; subst = p.first;
cnstrs = p.second; cnstrs = p.second;
expr next_solution = subst.instantiate(new_meta); expr next_solution = subst.instantiate(new_meta);
@ -403,12 +410,6 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
return lazy_list<constraints>(to_cnstrs_fn(subst, cnstrs)); return lazy_list<constraints>(to_cnstrs_fn(subst, cnstrs));
} }
} else { } else {
unify_result_seq seq2 = filter(seq1, [=](pair<substitution, constraints> const & p) {
substitution new_s = p.first;
expr result = new_s.instantiate(new_meta);
// We only keep complete solutions (modulo universe metavariables)
return !has_expr_metavar_relaxed(result);
});
if (try_multiple_instances(env, *cls_name_it)) { if (try_multiple_instances(env, *cls_name_it)) {
lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) { lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
return to_cnstrs_fn(p.first, p.second); return to_cnstrs_fn(p.first, p.second);