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

Fix elaborator for let-expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-31 14:24:07 -07:00
parent 4a28a64685
commit 64788320f2
2 changed files with 16 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
examples/ex15.lean
View file

@ -1,4 +1,3 @@
Variable N : Type Variable N : Type
Variable h : N -> N -> N Variable h : N -> N -> N
@ -45,3 +44,15 @@ Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧
Set lean::pp::implicit false Set lean::pp::implicit false
Show Environment 1 Show Environment 1
Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
DisjCases H
(fun H1 : _,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
in CongrH AeqC (Symm AeqC))
(fun H1 : _,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
in CongrH AeqC (Symm AeqC))
Set lean::pp::implicit false
Show Environment 1

6
src/library/elaborator.cpp
View file

@ -211,7 +211,7 @@ class elaborator::imp {
} }
case expr_kind::Let: { case expr_kind::Let: {
expr lt = infer(let_value(e), ctx); expr lt = infer(let_value(e), ctx);
return infer(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); return lower_free_vars_mmv(infer(let_body(e), extend(ctx, let_name(e), lt, let_value(e))), 1, 1);
}} }}
lean_unreachable(); lean_unreachable();
return expr(); return expr();
@ -462,7 +462,8 @@ class elaborator::imp {
m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast<unsigned>(-1))); m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast<unsigned>(-1)));
progress = true; progress = true;
} catch (exception&) { } catch (exception&) {
// std::cout << "Failed to infer: " << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n"; // std::cout << "Failed to infer type of: ?M" << midx << "\n"
// << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
throw unification_type_mismatch_exception(*m_owner, m_metavars[midx].m_ctx, m_metavars[midx].m_mvar); throw unification_type_mismatch_exception(*m_owner, m_metavars[midx].m_ctx, m_metavars[midx].m_mvar);
} }
} }
@ -524,6 +525,7 @@ public:
} }
expr operator()(expr const & e, elaborator const & elb) { expr operator()(expr const & e, elaborator const & elb) {
// std::cout << "ELABORATIMG: " << e << "\n";
m_owner = &elb; m_owner = &elb;
unsigned num_meta = m_metavars.size(); unsigned num_meta = m_metavars.size();
m_add_constraints = true; m_add_constraints = true;