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

feat(library/elaborator): use equality constraints instead of convertability constraints on definitions

Browse source 
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-30 14:13:17 -08:00
parent 8c1f6b9055
commit b45ab9dc30
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/frontend_elaborator.cpp
View file

@ -469,8 +469,8 @@ public:
if (has_metavar(new_e) || has_metavar(new_t)) {
m_type_checker.check(new_t, context(), m_menv, m_ucs);
expr new_e_t = m_type_checker.check(new_e, context(), m_menv, m_ucs);
m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t,
mk_def_type_match_justification(context(), n, e)));
m_ucs.push_back(mk_eq_constraint(context(), new_e_t, new_t,
mk_def_type_match_justification(context(), n, e)));
// for (auto c : m_ucs) {
// formatter fmt = mk_simple_formatter();
// std::cout << c.pp(fmt, options(), nullptr, false) << "\n";

2
src/library/elaborator/elaborator.cpp
View file

@ -414,7 +414,7 @@ class elaborator::imp {
expr tv = m_type_inferer(v, ctx, menv, ucs);
push_active(ucs);
justification new_jst(new typeof_mvar_justification(ctx, m, menv->get_type(m), tv, jst));
push_active(mk_convertible_constraint(ctx, tv, menv->get_type(m), new_jst));
push_active(mk_eq_constraint(ctx, tv, menv->get_type(m), new_jst));
}
m_state.m_recently_assigned.insert(metavar_name(m));
return true;

2
tests/lean/elab1.lean.expected.out
View file

@ -34,7 +34,7 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
Assumed: b
Assumed: H
Failed to solve
⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≺ b
⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≈ b
elab1.lean:18:18: Type of definition 't1' must be convertible to expected type.
Failed to solve
⊢ @eq ?M::6 b b ≺ @eq ?M::1 a b