max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): always use approximate is_def_eq in the elaborator

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-14 08:43:01 -07:00
parent 9461595a70
commit 9bb8b0e6ef
3 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -443,12 +443,14 @@ optional<expr> elaborator::mk_coercion(expr const & e, expr const & _e_type, exp
}
}
optional<expr> elaborator::ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref) {
bool elaborator::is_def_eq(expr const & e1, expr const & e2) {
type_context::approximate_scope scope(m_ctx);
return m_ctx.is_def_eq(e1, e2);
}
optional<expr> elaborator::ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref) {
if (is_def_eq(e_type, type))
return some_expr(e);
return mk_coercion(e, e_type, type, ref);
}
@ -1800,7 +1802,8 @@ expr elaborator::visit_suffices_expr(expr const & e, optional<expr> const & expe
expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
flet<unsigned> inc_depth(m_depth, m_depth+1);
trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n";);
trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n";
if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";);
if (is_placeholder(e)) {
return visit_placeholder(e, expected_type);
} else if (is_have_expr(e)) {

2
src/frontends/lean/elaborator.h
View file

@ -99,7 +99,7 @@ private:
expr whnf(expr const & e) { return m_ctx.whnf(e); }
expr try_to_pi(expr const & e) { return m_ctx.try_to_pi(e); }
bool is_def_eq(expr const & e1, expr const & e2) { return m_ctx.is_def_eq(e1, e2); }
bool is_def_eq(expr const & e1, expr const & e2);
bool assign_mvar(expr const & e1, expr const & e2) { lean_assert(is_metavar(e1)); return is_def_eq(e1, e2); }
expr instantiate_mvars(expr const & e);
bool is_uvar_assigned(level const & l) const { return m_ctx.is_assigned(l); }

2
src/library/type_context.cpp
View file

@ -2276,7 +2276,7 @@ bool type_context::is_def_eq(expr const & t, expr const & s) {
bool success = is_def_eq_core(t, s);
lean_trace(name({"type_context", "is_def_eq"}),
tout() << t << " =?= " << s << " ... "
<< (success ? "success" : "failed") << "\n";);
<< (success ? "success" : "failed") << " " << (approximate() ? " (approximate mode)" : "") << "\n";);
if (success) {
S.commit();
return true;