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

Add missing case to elaborator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-06 17:43:08 -07:00
parent 26bf7bcaac
commit edafd519e1
3 changed files with 26 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/lean_elaborator.cpp
View file

@ -232,6 +232,8 @@ class elaborator::imp {
// this can happen if we access a variable out of scope
throw type_expected_exception(m_env, s_ctx, s);
}
} else if (has_assigned_metavar(e)) {
return check_universe(instantiate(e), ctx, s, s_ctx);
}
throw type_expected_exception(m_env, s_ctx, s);
}
@ -735,16 +737,16 @@ class elaborator::imp {
try {
expr t = infer(m_metavars[midx].m_assignment, ctx);
m_metavars[midx].m_type_cnstr = true;
info_ref r = mk_expected_type_info(m_metavars[midx].m_mvar, m_metavars[midx].m_mvar,
info_ref r = mk_expected_type_info(m_metavars[midx].m_mvar, m_metavars[midx].m_assignment,
m_metavars[midx].m_type, t, ctx);
m_constraints.push_back(constraint(m_metavars[midx].m_type, t, ctx, r));
progress = true;
} catch (exception&) {
// std::cout << "Failed to infer type of: ?M" << midx << "\n"
// << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
// << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
expr null_given_type; // failed to infer given type.
throw unification_type_mismatch_exception(*m_owner, ctx, m_metavars[midx].m_mvar, m_metavars[midx].m_mvar,
m_metavars[midx].m_type, null_given_type);
throw unification_type_mismatch_exception(*m_owner, ctx, m_metavars[midx].m_mvar, m_metavars[midx].m_assignment,
instantiate(m_metavars[midx].m_type), null_given_type);
}
}
}

12
tests/lean/elab3.lean Normal file
View file

@ -0,0 +1,12 @@
Variable C : Pi (A B : Type) (H : A = B) (a : A), B
Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
(B a) = (B' (C A A' (D A A' B B' H) a))
Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : A1 -> B1 = A2 -> B2) (a : A1), B1 = B2 :=
fun A1 A2 B1 B2 H a,
R _ _ _ _ H a
Show Environment 1.

8
tests/lean/elab3.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
R A1 A2 (λ a : A1, B1) (λ _ : A2, B2) H a