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

feat(frontends/lean/elaborator): try coercions after each overload

Browse source 
We try only the easy cases since the more general case is too expensive.

closes #444
This commit is contained in:
Leonardo de Moura 2015-02-24 17:40:14 -08:00
parent 34c36648bb
commit 909ebfc5f1
3 changed files with 32 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/int/order.lean
View file

@ -68,7 +68,7 @@ theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n :=
le.intro (show a + 1 + n = a + succ n, from
calc
a + 1 + n = a + (1 + n) : add.assoc
... = a + (n + 1) : add.comm
... = a + (n + 1) : nat.add.comm
... = a + succ n : rfl)
theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b :=
@ -190,9 +190,9 @@ le.intro
(eq.symm
(calc
a * b = (0 + n) * b : Hn
... = n * b : zero_add
... = n * (0 + m) : Hm
... = n * m : zero_add
... = n * b : nat.zero_add
... = n * (0 + m) : {Hm⁻¹}
... = n * m : nat.zero_add
... = 0 + n * m : zero_add))
theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b :=
@ -202,9 +202,9 @@ lt.intro
(eq.symm
(calc
a * b = (0 + succ n) * b : Hn
... = succ n * b : zero_add
... = succ n * (0 + succ m) : Hm
... = succ n * succ m : zero_add
... = succ n * b : nat.zero_add
... = succ n * (0 + succ m) : {Hm⁻¹}
... = succ n * succ m : nat.zero_add
... = of_nat (succ n * succ m) : mul_of_nat
... = of_nat (succ n * m + succ n) : nat.mul_succ
... = of_nat (succ (succ n * m + n)) : nat.add_succ

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

@ -65,14 +65,14 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
local_context m_context;
local_context m_full_context;
expr m_meta;
expr m_type;
expr m_choice;
unsigned m_idx;
bool m_relax_main_opaque;
choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx,
expr const & meta, expr const & c, bool relax):
m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_meta(meta), m_choice(c),
m_idx(get_num_choices(m_choice)),
m_relax_main_opaque(relax) {
expr const & meta, expr const & type, expr const & c, bool relax):
m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_meta(meta),
m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)), m_relax_main_opaque(relax) {
}
virtual optional<constraints> next() {
@ -85,8 +85,21 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
flet<local_context> set1(m_elab.m_context, m_context);
flet<local_context> set2(m_elab.m_full_context, m_full_context);
pair<expr, constraint_seq> rcs = m_elab.visit(c);
expr r = rcs.first;
constraint_seq cs = mk_eq_cnstr(m_meta, r, justification(), m_relax_main_opaque) + rcs.second;
expr r = rcs.first;
constraint_seq cs = rcs.second;
if (!has_expr_metavar_relaxed(m_type)) {
// we only try coercions here if the m_type and r_type do not contain metavariables.
constraint_seq new_cs = cs;
expr r_type = m_elab.infer_type(r, new_cs);
if (!has_expr_metavar_relaxed(r_type)) {
cs = new_cs;
auto new_rcs = m_elab.ensure_has_type(r, r_type, m_type, justification(),
m_relax_main_opaque);
r = new_rcs.first;
cs += new_rcs.second;
}
}
cs = mk_eq_cnstr(m_meta, r, justification(), m_relax_main_opaque) + cs;
return optional<constraints>(cs.to_list());
} catch (exception &) {}
}
@ -289,9 +302,9 @@ expr elaborator::visit_choice(expr const & e, optional<expr> const & t, constrai
bool relax = m_relax_main_opaque;
local_context ctx = m_context;
local_context full_ctx = m_full_context;
auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */,
auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */,
name_generator const & /* ngen */) {
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, e, relax));
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e, relax));
};
justification j = mk_justification("none of the overloads is applicable", some_expr(e));
cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque);

4
tests/lean/run/444.lean Normal file
View file

@ -0,0 +1,4 @@
open nat
check succ 1
notation 1 := unit
check succ 1