From 83d38674c953054ea59d0f60449ea1a2fc83b52d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 27 Jul 2014 09:41:25 -0700 Subject: [PATCH] feat(kernel/error_msgs): improve cryptic type mismatch error messages where the types may seem identical because key information is being suppressed Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 3 ++ src/frontends/lean/pp.cpp | 14 +++++-- src/frontends/lean/pp.h | 7 ++-- src/frontends/lean/pp_options.cpp | 12 ++++++ src/frontends/lean/pp_options.h | 1 + src/kernel/error_msgs.cpp | 68 +++++++++++++++++++++++++++---- src/kernel/error_msgs.h | 16 ++++++++ src/kernel/formatter.cpp | 2 +- src/kernel/formatter.h | 7 ++-- src/util/sexpr/format.cpp | 8 ++++ src/util/sexpr/format.h | 3 ++ 11 files changed, 124 insertions(+), 17 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 1adbae19a..b2bb1341f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" +#include "kernel/error_msgs.h" #include "library/parser_nested_exception.h" #include "library/aliases.h" #include "library/private.h" @@ -34,6 +35,7 @@ Author: Leonardo de Moura #include "frontends/lean/parser_bindings.h" #include "frontends/lean/notation_cmd.h" #include "frontends/lean/elaborator.h" +#include "frontends/lean/pp_options.h" #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true @@ -1043,6 +1045,7 @@ void parser::parse_imports() { bool parser::parse_commands() { // We disable hash-consing while parsing to make sure the pos-info are correct. scoped_expr_caching disable(false); + scoped_set_distinguishing_pp_options set(get_distinguishing_pp_options()); try { bool done = false; parse_imports(); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 087276d4f..ba6570b66 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -99,7 +99,8 @@ expr pretty_fn::purify(expr const & e) { }); } -void pretty_fn::set_options(options const & o) { +void pretty_fn::set_options_core(options const & o) { + m_options = o; m_indent = get_pp_indent(o); m_max_depth = get_pp_max_depth(o); m_max_steps = get_pp_max_steps(o); @@ -112,6 +113,12 @@ void pretty_fn::set_options(options const & o) { m_private_names = get_pp_private_names(o); } +void pretty_fn::set_options(options const & o) { + if (is_eqp(o, m_options)) + return; + set_options_core(o); +} + format pretty_fn::pp_level(level const & l) { return ::lean::pp(l, m_unicode, m_indent); } @@ -411,7 +418,7 @@ auto pretty_fn::pp(expr const & e) -> result { pretty_fn::pretty_fn(environment const & env, options const & o): m_env(env), m_tc(env) { - set_options(o); + set_options_core(o); m_meta_prefix = "M"; m_next_meta_idx = 1; } @@ -424,7 +431,8 @@ format pretty_fn::operator()(expr const & e) { formatter_factory mk_pretty_formatter_factory() { return [](environment const & env, options const & o) { // NOLINT auto fn_ptr = std::make_shared(env, o); - return formatter(o, [=](expr const & e) { + return formatter(o, [=](expr const & e, options const & new_o) { + fn_ptr->set_options(new_o); return (*fn_ptr)(e); }); }; diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 0e2f81a08..0fe3f35e8 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -29,6 +29,7 @@ private: name_map m_purify_local_table; name_set m_purify_used_locals; // cached configuration + options m_options; unsigned m_indent; unsigned m_max_depth; unsigned m_max_steps; @@ -40,8 +41,6 @@ private: bool m_full_names; bool m_private_names; - void set_options(options const & o); - unsigned max_bp() const { return std::numeric_limits::max(); } name mk_metavar_name(name const & m); name mk_local_name(name const & n, name const & suggested); @@ -69,11 +68,13 @@ private: result pp_have(expr const & e); result pp_show(expr const & e); result pp_macro(expr const & e); + void set_options_core(options const & o); public: pretty_fn(environment const & env, options const & o); result pp(expr const & e); - + void set_options(options const & o); + options const & get_options() const { return m_options; } format operator()(expr const & e); }; diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 8d3d395d7..2831ed21e 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -48,6 +48,18 @@ static name g_pp_universes {"pp", "universes"}; static name g_pp_full_names {"pp", "full_names"}; static name g_pp_private_names {"pp", "private_names"}; +list const & get_distinguishing_pp_options() { + static options g_universes_true(g_pp_universes, true); + static options g_implicit_true(g_pp_implicit, true); + static options g_coercion_true(g_pp_coercion, true); + static options g_notation_false(g_pp_notation, false); + static options g_implicit_coercion = join(g_coercion_true, g_implicit_true); + static options g_implicit_notation = join(g_notation_false, g_implicit_true); + static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercion_true, g_notation_false)); + static list g_distinguishing_pp_options({g_universes_true, g_implicit_true, g_coercion_true, g_implicit_coercion, g_implicit_notation, g_all}); + return g_distinguishing_pp_options; +} + RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(pretty printer) maximum expression depth, after that it will use ellipsis"); RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index f0a0569b8..6c09e5cb1 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -15,4 +15,5 @@ bool get_pp_coercion(options const & opts); bool get_pp_universes(options const & opts); bool get_pp_full_names(options const & opts); bool get_pp_private_names(options const & opts); +list const & get_distinguishing_pp_options(); } diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 22e28a8e7..b6b00cf3e 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/error_msgs.h" namespace lean { @@ -19,35 +20,88 @@ format pp_function_expected(formatter const & fmt, expr const & e) { return compose(format("function expected at"), pp_indent_expr(fmt, e)); } +MK_THREAD_LOCAL_GET_DEF(list, get_distinguishing_pp_options) + +list set_distinguishing_pp_options(list const & opts) { + list r = get_distinguishing_pp_options(); + get_distinguishing_pp_options() = opts; + return r; +} + +static std::tuple pp_until_different(formatter const & fmt, expr const & e1, expr const & e2, list extra) { + formatter fmt1 = fmt; + while (true) { + format r1 = pp_indent_expr(fmt1, e1); + format r2 = pp_indent_expr(fmt1, e2); + if (!format_pp_eq(r1, r2, fmt1.get_options())) + return mk_pair(r1, r2); + if (!extra) + return mk_pair(pp_indent_expr(fmt, e1), pp_indent_expr(fmt, e2)); + options o = join(head(extra), fmt.get_options()); + fmt1 = fmt.update_options(o); + extra = tail(extra); + } +} + +std::tuple pp_until_different(formatter const & fmt, expr const & e1, expr const & e2) { + return pp_until_different(fmt, e1, e2, get_distinguishing_pp_options()); +} + format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & expected_type, expr const & given_type) { format r; + format expected_fmt, given_fmt; + std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type); r += format("type mismatch at application"); r += pp_indent_expr(fmt, app); r += compose(line(), format("expected type:")); - r += pp_indent_expr(fmt, expected_type); + r += expected_fmt; r += compose(line(), format("given type:")); - r += pp_indent_expr(fmt, given_type); + r += given_fmt; return r; } format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type) { + format expected_fmt, given_fmt; + std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type); format r("type mismatch at definition '"); r += format(n); r += format("', expected type"); - r += pp_indent_expr(fmt, expected_type); + r += expected_fmt; r += compose(line(), format("given type:")); - r += pp_indent_expr(fmt, given_type); + r += given_fmt; return r; } format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type) { + format expected_fmt, given_fmt; + std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type); format r("type mismatch, expected type:"); - r += ::lean::pp_indent_expr(fmt, expected_type); + r += expected_fmt; r += compose(line(), format("given type:")); - r += ::lean::pp_indent_expr(fmt, given_type); + r += given_fmt; return r; } +static format pp_until_meta_visible(formatter const & fmt, expr const & e, list extra) { + formatter fmt1 = fmt; + while (true) { + format r = pp_indent_expr(fmt1, e); + std::ostringstream out; + out << mk_pair(r, fmt1.get_options()); + if (out.str().find("?M") != std::string::npos) + return r; + if (!extra) + return pp_indent_expr(fmt, e); + options o = join(head(extra), fmt.get_options()); + fmt1 = fmt.update_options(o); + extra = tail(extra); + } +} + +format pp_until_meta_visible(formatter const & fmt, expr const & e) { + return pp_until_meta_visible(fmt, e, get_distinguishing_pp_options()); +} + format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type) { format r("failed to add declaration '"); r += format(n); @@ -57,7 +111,7 @@ format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & else r += format("value"); r += format(" has metavariables"); - r += pp_indent_expr(fmt, e); + r += pp_until_meta_visible(fmt, e); return r; } } diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index 16daac504..866023db2 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -15,4 +15,20 @@ format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type); format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type); format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type); + +/** \brief Set a list extra configuration options that are used to try to distinguish error such as given/expected type mismatch + This is a trick used to avoid cryptic error messages when to types seem identical because the pretty printer is suppressing + universes and/or implicit arguments. The error messages will keep using these extra options until it finds one that + can distinguish given/expected type. The extra options do not override user provided options. + + \remark This is a thread local information. + \remark Consider using #scoped_set_distinguishing_pp_options +*/ +list set_distinguishing_pp_options(list const & opts); +struct scoped_set_distinguishing_pp_options { + list m_old; + scoped_set_distinguishing_pp_options(list const & os):m_old(set_distinguishing_pp_options(os)) {} + ~scoped_set_distinguishing_pp_options() { set_distinguishing_pp_options(m_old); } +}; +std::tuple pp_until_different(formatter const & fmt, expr const & e1, expr const & e2); } diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index c90ca258b..d377b48fc 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -246,7 +246,7 @@ std::ostream & operator<<(std::ostream & out, expr const & e) { formatter_factory mk_simple_formatter_factory() { return [](environment const & env, options const & o) { // NOLINT - return formatter(o, [=](expr const & e) { + return formatter(o, [=](expr const & e, options const &) { std::ostringstream s; print_expr_fn pr(s, env.prop_proof_irrel()); pr(e); diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index e9279b71b..0507ac59e 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -28,12 +28,13 @@ std::pair binding_body_fresh(expr const & b, bool preserve_type = fa std::pair let_body_fresh(expr const & l, bool preserve_type = false); class formatter { - std::function m_fn; + std::function m_fn; options m_options; public: - formatter(options const & o, std::function const & fn):m_fn(fn), m_options(o) {} - format operator()(expr const & e) const { return m_fn(e); } + formatter(options const & o, std::function const & fn):m_fn(fn), m_options(o) {} + format operator()(expr const & e) const { return m_fn(e, m_options); } options const & get_options() const { return m_options; } + formatter update_options(options const & o) const { return formatter(o, m_fn); } }; typedef std::function formatter_factory; diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 15573937f..ed62ac299 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -350,6 +350,14 @@ std::ostream & operator<<(std::ostream & out, std::pair