From 8840b3725887c72cf281224fa52df397fe52b86e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Sep 2013 11:02:00 -0700 Subject: [PATCH] Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_elaborator.cpp | 8 ++-- src/frontends/lean/lean_frontend.cpp | 10 +++-- src/frontends/lean/lean_frontend.h | 2 +- src/kernel/kernel_exception.h | 1 + src/kernel/type_checker.cpp | 3 +- src/library/kernel_exception_formatter.cpp | 7 +-- tests/lean/let4.lean | 51 ++++++++++++++++++++++ tests/lean/let4.lean.expected.out | 20 +++++++++ 8 files changed, 89 insertions(+), 13 deletions(-) create mode 100644 tests/lean/let4.lean create mode 100644 tests/lean/let4.lean.expected.out diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 8a2581249..8a512658a 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -262,7 +262,7 @@ class elaborator::imp { if (!has_metavar(expected) && !has_metavar(given)) { if (is_convertible(expected, given, ctx)) { // compatible - } else if (m_frontend.get_coercion(given, expected)) { + } else if (m_frontend.get_coercion(given, expected, ctx)) { // compatible if using coercion num_coercions++; } else { @@ -381,7 +381,7 @@ class elaborator::imp { m_constraints.push_back(constraint(expected, given, ctx, r)); } else { if (!is_convertible(expected, given, ctx)) { - expr coercion = m_frontend.get_coercion(given, expected); + expr coercion = m_frontend.get_coercion(given, expected, ctx); if (coercion) { modified = true; args[i] = mk_app(coercion, args[i]); @@ -437,7 +437,7 @@ class elaborator::imp { m_constraints.push_back(constraint(expected, given, ctx, r)); } else { if (!is_convertible(expected, given, ctx)) { - expr coercion = m_frontend.get_coercion(given, expected); + expr coercion = m_frontend.get_coercion(given, expected, ctx); if (coercion) { v_p.first = mk_app(coercion, v_p.first); } else { @@ -447,7 +447,7 @@ class elaborator::imp { } } auto b_p = process(let_body(e), extend(ctx, let_name(e), t_p.first ? t_p.first : v_p.second, v_p.first)); - expr t = lower_free_vars_mmv(b_p.second, 1, 1); + expr t = instantiate_free_var_mmv(b_p.second, 0, v_p.first); expr new_e = update_let(e, t_p.first, v_p.first, b_p.first); add_trace(e, new_e); return expr_pair(new_e, t); diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index 25b2aa219..941518ed1 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -324,9 +324,9 @@ struct frontend::imp { return expr(); } - expr get_coercion(expr const & given_type, expr const & expected_type) { - expr norm_given_type = m_env.normalize(given_type); - expr norm_expected_type = m_env.normalize(expected_type); + expr get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) { + expr norm_given_type = m_env.normalize(given_type, ctx); + expr norm_expected_type = m_env.normalize(expected_type, ctx); return get_coercion_core(norm_given_type, norm_expected_type); } @@ -414,7 +414,9 @@ std::vector const & frontend::get_implicit_arguments(name const & n) const name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); } void frontend::add_coercion(expr const & f) { m_imp->add_coercion(f); } -expr frontend::get_coercion(expr const & given_type, expr const & expected_type) const { return m_imp->get_coercion(given_type, expected_type); } +expr frontend::get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const { + return m_imp->get_coercion(given_type, expected_type, ctx); +} bool frontend::is_coercion(expr const & f) const { return m_imp->is_coercion(f); } state const & frontend::get_state() const { return m_imp->m_state; } diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index 7e63bfb4f..741a6eb05 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -168,7 +168,7 @@ public: Return the null expression if there is no coercion from \c given_type to \c expected_type. */ - expr get_coercion(expr const & given_type, expr const & expected_type) const; + expr get_coercion(expr const & given_type, expr const & expected_type, context const & ctx) const; /** \brief Return true iff the given expression is a coercion. That is, it was added using \c add_coercion. diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index e382b0f89..70948afb0 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -175,6 +175,7 @@ public: expr const & get_type() const { return m_type; } expr const & get_value() const { return m_value; } expr const & get_value_type() const { return m_value_type; } + virtual expr const & get_main_expr() const { return m_value; } virtual char const * what() const noexcept { return "definition type mismatch"; } }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index e1b6e83bf..563c64bcc 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -140,7 +140,8 @@ public: } { cache::mk_scope sc(m_cache); - r = lower_free_vars(infer_type(let_body(e), extend(ctx, let_name(e), lt, let_value(e))), 1); + expr t = infer_type(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); + r = instantiate(t, let_value(e)); } break; } diff --git a/src/library/kernel_exception_formatter.cpp b/src/library/kernel_exception_formatter.cpp index ac2abe3ca..c21e4f94b 100644 --- a/src/library/kernel_exception_formatter.cpp +++ b/src/library/kernel_exception_formatter.cpp @@ -88,14 +88,15 @@ format pp(formatter const & fmt, type_expected_exception const & ex, options con } format pp(formatter const & fmt, def_type_mismatch_exception const & ex, options const & opts) { - unsigned indent = get_pp_indent(opts); + unsigned indent = get_pp_indent(opts); + context const & ctx = ex.get_context(); format r; r += format("type mismatch at definition '"); r += format(ex.get_name()); r += format("', expected type"); - r += nest(indent, compose(line(), fmt(ex.get_type(), opts))); + r += nest(indent, compose(line(), fmt(ctx, ex.get_type(), false, opts))); r += compose(line(), format("Given type:")); - r += nest(indent, compose(line(), fmt(ex.get_value_type(), opts))); + r += nest(indent, compose(line(), fmt(ctx, ex.get_value_type(), false, opts))); return r; } diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean new file mode 100644 index 000000000..90c2f77c9 --- /dev/null +++ b/tests/lean/let4.lean @@ -0,0 +1,51 @@ + +Show +let b := true, + a : Int := b +in a + +Variable vector : Type -> Nat -> Type +Variable const {A : Type} (n : Nat) (a : A) : vector A n + +Check +let a := 10, + v1 := const a true, + v2 := v1 +in v2 + +Show +let a := 10, + v1 : vector Bool a := const a true, + v2 : vector Bool a := v1 +in v2 + +Check +let a := 10, + v1 : vector Bool a := const a true, + v2 : vector Bool a := v1 +in v2 + +Check +let a := 10, + v1 : vector Bool a := const a true, + v2 : vector Int a := v1 +in v2 + +Variable foo : (vector Bool 10) -> (vector Int 10) +Coercion foo + +Check +let a := 10, + v1 : vector Bool a := const a true, + v2 : vector Int a := v1 +in v2 + +Set pp::coercion true + +Show +let a := 10, + v1 : vector Bool a := const a true, + v2 : vector Int a := v1 +in v2 + + diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out new file mode 100644 index 000000000..e071a1ccb --- /dev/null +++ b/tests/lean/let4.lean.expected.out @@ -0,0 +1,20 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 4, pos: 15) type mismatch at definition 'a', expected type + ℤ +Given type: + Bool + Assumed: vector + Assumed: const +vector Bool 10 +let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 +vector Bool 10 +Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type + vector ℤ a +Given type: + vector Bool a + Assumed: foo + Coercion foo +vector ℤ 10 + Set: lean::pp::coercion +let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := foo v1 in v2