From a50398f837761bda56db45d5fa9970b2a1fa93d0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 26 Mar 2017 19:30:45 +0200 Subject: [PATCH] fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error --- src/kernel/kernel_exception.cpp | 5 +++++ src/kernel/kernel_exception.h | 14 ++++++++++++++ src/kernel/type_checker.cpp | 4 +--- src/library/tactic/eval.cpp | 19 ++++++++++++++++--- .../type_error_at_eval_expr.lean.expected.out | 4 +--- 5 files changed, 37 insertions(+), 9 deletions(-) diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index 8248ef1a19..56ea6d6087 100644 --- a/src/kernel/kernel_exception.cpp +++ b/src/kernel/kernel_exception.cpp @@ -9,10 +9,15 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "kernel/scope_pos_info_provider.h" #include "kernel/kernel_exception.h" +#include "kernel/error_msgs.h" namespace lean { format kernel_exception::pp(formatter const &) const { return format(what()); } +format definition_type_mismatch_exception::pp(formatter const & fmt) const { + return pp_def_type_mismatch(fmt, m_decl.get_name(), m_decl.get_type(), m_given_type, true); +} + class generic_kernel_exception : public kernel_exception { protected: optional m_pos; diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 49ec168fe3..9d1379004b 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include "kernel/environment.h" #include "kernel/ext_exception.h" +#include "kernel/scope_pos_info_provider.h" namespace lean { class environment; @@ -24,6 +25,19 @@ public: virtual void rethrow() const override { throw *this; } }; +class definition_type_mismatch_exception : public kernel_exception { + declaration m_decl; + expr m_given_type; +public: + definition_type_mismatch_exception(environment const & env, declaration const & decl, expr const & given_type): + kernel_exception(env), m_decl(decl), m_given_type(given_type) {} + expr const & get_given_type() const { return m_given_type; } + virtual optional get_pos() const override { return get_pos_info(m_decl.get_value()); } + virtual format pp(formatter const & fmt) const override; + virtual throwable * clone() const override { return new definition_type_mismatch_exception(m_env, m_decl, m_given_type); } + virtual void rethrow() const override { throw *this; } +}; + [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m = none_expr()); [[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, optional const & m = none_expr()); [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 43e2a14c6f..9fa315a430 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -735,9 +735,7 @@ static void check_definition(environment const & env, declaration const & d, typ check_no_mlocal(env, d.get_name(), d.get_value(), false); expr val_type = checker.check(d.get_value(), d.get_univ_params()); if (!checker.is_def_eq(val_type, d.get_type())) { - throw_kernel_exception(env, d.get_value(), [=](formatter const &fmt) { - return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true); - }); + throw definition_type_mismatch_exception(env, d, val_type); } } diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp index 9296f77e03..e15a1b6886 100644 --- a/src/library/tactic/eval.cpp +++ b/src/library/tactic/eval.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "util/fresh_name.h" #include "kernel/type_checker.h" #include "kernel/kernel_exception.h" +#include "kernel/error_msgs.h" #include "library/vm/vm.h" #include "library/vm/vm_expr.h" #include "library/compiler/vm_compiler.h" @@ -29,13 +30,25 @@ static vm_obj eval(expr const & A, expr a, tactic_state const & s) { vm_state & S = get_vm_state(); environment aux_env = S.env(); name eval_aux_name = mk_tagged_fresh_name("_eval_expr"); - /* We use nested_exception_without_pos to make sure old position information nested in 'a' is used - in type error messages. */ try { auto cd = check(aux_env, mk_definition(aux_env, eval_aux_name, {}, A, a, true, false)); aux_env = aux_env.add(cd); + } catch (definition_type_mismatch_exception & ex) { + expr given_type = ex.get_given_type(); + return tactic::mk_exception([=]() { + io_state_stream ios = tout(); + formatter fmt = ios.get_formatter(); + + format expected_fmt, given_fmt; + std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, A, given_type); + return format("type error at eval_expr, argument has type '") + given_fmt + + compose(line(), format("but is expected to have type")) + + expected_fmt; + }, s); } catch (kernel_exception & ex) { - return tactic::mk_exception(nested_exception_without_pos("eval_expr failed due to type error", ex), s); + /* We use nested_exception_without_pos to make sure old position information nested in 'a' is not used + in type error messages. */ + return tactic::mk_exception(nested_exception_without_pos("eval_expr failed", ex), s); } try { aux_env = vm_compile(aux_env, aux_env.get(eval_aux_name)); diff --git a/tests/lean/type_error_at_eval_expr.lean.expected.out b/tests/lean/type_error_at_eval_expr.lean.expected.out index aff914bac0..e6205d2cba 100644 --- a/tests/lean/type_error_at_eval_expr.lean.expected.out +++ b/tests/lean/type_error_at_eval_expr.lean.expected.out @@ -1,6 +1,4 @@ -type_error_at_eval_expr.lean:3:0: error: eval_expr failed due to type error -nested exception message: -type mismatch at definition '_eval_expr.16.500', has type +type_error_at_eval_expr.lean:3:0: error: type error at eval_expr, argument has type ' list ℕ but is expected to have type ℕ