From 00ac867ddfb473e8fd2ff687ec027356d4290392 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 19 May 2017 14:57:14 +0200 Subject: [PATCH] feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys --- src/frontends/lean/definition_cmds.cpp | 4 +- src/frontends/lean/elaborator.cpp | 41 ++++++++++++++------ src/frontends/lean/elaborator.h | 6 ++- src/frontends/lean/parser.cpp | 4 +- src/frontends/lean/parser.h | 2 +- src/frontends/lean/pp.cpp | 2 + src/library/sorry.cpp | 42 +++++++++++---------- src/library/sorry.h | 11 +++++- src/library/tactic/elaborator_exception.cpp | 1 + src/library/tactic/elaborator_exception.h | 12 +++++- 10 files changed, 84 insertions(+), 41 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 15e814e81b..6db6727f8e 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -710,7 +710,7 @@ static expr elaborate_proof( /* Remark: we need the catch to be able to produce correct line information */ message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, ERROR) .set_exception(ex).report(); - return mk_sorry(final_type); + return mk_sorry(final_type, true); } } @@ -878,7 +878,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif // Even though we catch exceptions during elaboration, there can still be other exceptions, // e.g. when adding a declaration to the environment. try { - auto res = process(p.mk_sorry(header_pos)); + auto res = process(p.mk_sorry(header_pos, true)); p.mk_message(header_pos, ERROR).set_exception(ex).report(); return res; } catch (...) {} diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 76e22a5070..8f479801d1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -201,6 +201,9 @@ bool elaborator::try_report(std::exception const & ex) { } bool elaborator::try_report(std::exception const & ex, optional const & ref) { + if (auto elab_ex = dynamic_cast(&ex)) { + if (elab_ex->is_ignored()) return true; + } if (!m_recover_from_errors) return false; auto pip = get_pos_info_provider(); @@ -220,9 +223,18 @@ void elaborator::report_or_throw(elaborator_exception const & ex) { throw elaborator_exception(ex); } -expr elaborator::mk_sorry(optional const & expected_type, expr const & ref) { +bool elaborator::has_synth_sorry(std::initializer_list && es) { + for (auto & e : es) { + if (has_synthetic_sorry(instantiate_mvars(e))) { + return true; + } + } + return false; +} + +expr elaborator::mk_sorry(optional const & expected_type, expr const & ref, bool synthetic) { auto sorry_type = expected_type ? *expected_type : mk_type_metavar(ref); - return copy_tag(ref, mk_sorry(sorry_type)); + return copy_tag(ref, mk_sorry(sorry_type, synthetic)); } expr elaborator::recoverable_error(optional const & expected_type, expr const & ref, elaborator_exception const & ex) { @@ -274,7 +286,8 @@ expr elaborator::mk_instance_core(local_context const & lctx, expr const & C, ex new_lctx = erase_inaccessible_annotations(new_lctx); tactic_state s = ::lean::mk_tactic_state_for(m_env, m_opts, m_decl_name, mctx, new_lctx, C); return recoverable_error(some_expr(C), ref, elaborator_exception( - ref, format("failed to synthesize type class instance for") + line() + s.pp())); + ref, format("failed to synthesize type class instance for") + line() + s.pp()) + .ignore_if(has_synth_sorry({C}))); } return *inst; } @@ -1058,7 +1071,8 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< if (!is_def_eq(new_arg_type, d)) { new_args.push_back(new_arg); throw elaborator_exception(ref, mk_app_type_mismatch_error(mk_app(fn, new_args), - new_arg, new_arg_type, d)); + new_arg, new_arg_type, d)) + .ignore_if(has_synth_sorry({new_arg_type, d})); } } else if (is_explicit(bi)) { expr arg_ref = args[j]; @@ -1346,7 +1360,8 @@ void elaborator::first_pass(expr const & fn, buffer const & args, tmp_args.push_back(new_arg); format msg = mk_app_type_mismatch_error(mk_app(fn, tmp_args), new_arg, new_arg_type, arg_expected_type); - throw elaborator_exception(ref, msg); + throw elaborator_exception(ref, msg). + ignore_if(has_synth_sorry({new_arg_type, arg_expected_type})); } new_arg = *new_new_arg; } else { @@ -1382,7 +1397,8 @@ void elaborator::first_pass(expr const & fn, buffer const & args, throw elaborator_exception(ref, format("type mismatch") + pp_indent(pp_fn, e) + line() + format("has type") + std::get<1>(pp_data) + line() + format("but is expected to have type") + - std::get<2>(pp_data)); + std::get<2>(pp_data)) + .ignore_if(has_synth_sorry({type, expected_type, e})); } } @@ -1422,7 +1438,8 @@ expr elaborator::second_pass(expr const & fn, buffer const & args, tmp_args.push_back(new_arg); format msg = mk_app_type_mismatch_error(mk_app(fn, tmp_args), new_arg, new_arg_type, info.args_expected_types[i]); - throw elaborator_exception(ref, msg); + throw elaborator_exception(ref, msg). + ignore_if(has_synth_sorry({new_arg_type, info.args_expected_types[i]})); } if (!is_def_eq(info.args_mvars[i], *new_new_arg)) { buffer tmp_args; @@ -1430,7 +1447,8 @@ expr elaborator::second_pass(expr const & fn, buffer const & args, tmp_args.push_back(new_arg); format msg = mk_app_arg_mismatch_error(mk_app(fn, tmp_args), new_arg, info.args_mvars[i]); - throw elaborator_exception(ref, msg); + throw elaborator_exception(ref, msg). + ignore_if(has_synth_sorry({new_arg, instantiate_mvars(info.args_mvars[i])})); } return *new_new_arg; } else { @@ -1517,7 +1535,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer< new_args.push_back(new_arg); format msg = mk_app_type_mismatch_error(mk_app(fn, new_args.size(), new_args.data()), new_arg, new_arg_type, d); - throw elaborator_exception(ref, msg); + throw elaborator_exception(ref, msg).ignore_if(has_synth_sorry({new_arg_type, d})); } i++; } else { @@ -2890,7 +2908,7 @@ expr elaborator::visit_macro(expr const & e, optional const & expected_typ implicit arguments. */ return visit_base_app_core(new_e, arg_mask::Default, buffer(), true, expected_type, e); } else if (is_sorry(e)) { - return mk_sorry(expected_type, e); + return mk_sorry(expected_type, e, is_synthetic_sorry(e)); } else if (is_structure_instance(e)) { return visit_structure_instance(e, expected_type); } else if (is_frozen_name(e)) { @@ -3364,8 +3382,9 @@ void elaborator::ensure_no_unassigned_metavars(expr & e) { if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) { tactic_state s = mk_tactic_state_for(e); if (m_recover_from_errors) { - report_error(s, "context:", "don't know how to synthesize placeholder", e); auto ty = m_ctx.mctx().get_metavar_decl(e).get_type(); + if (!has_synth_sorry(ty)) + report_error(s, "context:", "don't know how to synthesize placeholder", e); m_ctx.assign(e, copy_tag(e, mk_sorry(ty))); ensure_no_unassigned_metavars(ty); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index f05ec9ea37..603f10732a 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -155,8 +155,10 @@ private: bool try_report(std::exception const & ex); bool try_report(std::exception const & ex, optional const & ref); void report_or_throw(elaborator_exception const & ex); - expr mk_sorry(expr const & type) { return ::lean::mk_sorry(type); } - expr mk_sorry(optional const & expected_type, expr const & ref); + bool has_synth_sorry(expr const & e) { return has_synth_sorry({e}); } + bool has_synth_sorry(std::initializer_list && es); + expr mk_sorry(expr const & type, bool synthetic = true) { return ::lean::mk_sorry(type, synthetic); } + expr mk_sorry(optional const & expected_type, expr const & ref, bool synthetic = true); expr recoverable_error(optional const & expected_type, expr const & ref, elaborator_exception const & ex); template expr recover_expr_from_exception(optional const & expected_type, expr const & ref, Fn &&); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 5efadc649a..2f4f20f594 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -223,8 +223,8 @@ void parser::scan() { m_curr = m_scanner.scan(m_env); } -expr parser::mk_sorry(pos_info const & p) { - return save_pos(::lean::mk_sorry(mk_Prop()), p); +expr parser::mk_sorry(pos_info const & p, bool synthetic) { + return save_pos(::lean::mk_sorry(mk_Prop(), synthetic), p); } void parser::updt_options() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 2ee67c701d..a2cc786e6a 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -489,7 +489,7 @@ public: /* Elaborate \c e as a type using the given metavariable context, and using m_local_decls as the local context */ pair elaborate_type(name const & decl_name, metavar_context & mctx, expr const & e); - expr mk_sorry(pos_info const & p); + expr mk_sorry(pos_info const & p, bool synthetic = false); /** return true iff profiling is enabled */ bool profiling() const { return m_profile; } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 06a5224e9c..1b284ae7b2 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1162,6 +1162,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result { return pp(get_annotation_arg(e)); } else if (is_rec_fn_macro(e)) { return format("[") + format(get_rec_fn_name(e)) + format("]"); + } else if (is_synthetic_sorry(e)) { + return m_unicode ? format("⁇") : format("??"); } else if (is_sorry(e)) { return format("sorry"); } else { diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp index 300a1ce209..457b4538d8 100644 --- a/src/library/sorry.cpp +++ b/src/library/sorry.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "library/sorry.h" #include +#include #include "kernel/type_checker.h" #include "kernel/environment.h" #include "library/module.h" @@ -14,11 +15,16 @@ Author: Leonardo de Moura namespace lean { static name * g_sorry_name = nullptr; -static macro_definition * g_sorry = nullptr; static std::string * g_sorry_opcode = nullptr; class sorry_macro_cell : public macro_definition_cell { + bool m_synthetic; + public: + sorry_macro_cell(bool synthetic) : m_synthetic(synthetic) {} + + bool is_synthetic() const { return m_synthetic; } + virtual name get_name() const override { return *g_sorry_name; } unsigned int trust_level() const override { return 1; } @@ -36,47 +42,43 @@ public: virtual void write(serializer & s) const override { s.write_string(*g_sorry_opcode); + s.write_bool(m_synthetic); } }; void initialize_sorry() { g_sorry_name = new name{"sorry"}; g_sorry_opcode = new std::string("Sorry"); - g_sorry = new macro_definition(new sorry_macro_cell); register_macro_deserializer(*g_sorry_opcode, - [] (deserializer &, unsigned num, expr const * args) { + [] (deserializer & d, unsigned num, expr const * args) { if (num != 1) throw corrupted_stream_exception(); - return mk_sorry(args[0]); + bool synthetic = d.read_bool(); + return mk_sorry(args[0], synthetic); }); } void finalize_sorry() { - delete g_sorry; delete g_sorry_opcode; delete g_sorry_name; } -expr mk_sorry(expr const & ty) { - return mk_macro(*g_sorry, 1, &ty); +expr mk_sorry(expr const & ty, bool synthetic) { + return mk_macro(macro_definition(new sorry_macro_cell(synthetic)), 1, &ty); } bool is_sorry(expr const & e) { - return is_macro(e) && macro_num_args(e) == 1 && macro_def(e) == *g_sorry; + return is_macro(e) && macro_num_args(e) == 1 && dynamic_cast(macro_def(e).raw()); +} +bool is_synthetic_sorry(expr const & e) { + return is_sorry(e) && static_cast(macro_def(e).raw())->is_synthetic(); +} + +bool has_synthetic_sorry(expr const & ex) { + return !!find(ex, [] (expr const & e, unsigned) { return is_synthetic_sorry(e); }); } bool has_sorry(expr const & ex) { - bool found_sorry = false; - for_each(ex, [&] (expr const & e, unsigned) { - if (found_sorry) return false; - - if (is_sorry(e)) { - found_sorry = true; - return false; - } - - return true; - }); - return found_sorry; + return !!find(ex, [] (expr const & e, unsigned) { return is_sorry(e); }); } bool has_sorry(declaration const & decl) { diff --git a/src/library/sorry.h b/src/library/sorry.h index 2fde78f2a2..bc546e2f95 100644 --- a/src/library/sorry.h +++ b/src/library/sorry.h @@ -12,11 +12,18 @@ namespace lean { bool has_sorry(environment const & env); bool has_sorry(expr const &); bool has_sorry(declaration const &); +bool has_synthetic_sorry(expr const &); -/** \brief Returns the sorry macro with the specified type. */ -expr mk_sorry(expr const & ty); +/** \brief Returns the sorry macro with the specified type. + * \param synthetic Synthetic macros are created by parser and + * elaborator during error recovery. Non-synthetic macros are + * entered by the user using the `sorry` keyword. + */ +expr mk_sorry(expr const & ty, bool synthetic = false); /** \brief Return true iff \c e is a sorry macro. */ bool is_sorry(expr const & e); +/** \brief Return true iff \c e is a synthetic sorry macro */ +bool is_synthetic_sorry(expr const & e); /** \brief Type of the sorry macro. */ expr const & sorry_type(expr const & sry); void initialize_sorry(); diff --git a/src/library/tactic/elaborator_exception.cpp b/src/library/tactic/elaborator_exception.cpp index 598d44a38c..de4f0d99e7 100644 --- a/src/library/tactic/elaborator_exception.cpp +++ b/src/library/tactic/elaborator_exception.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/scope_pos_info_provider.h" #include "library/tactic/elaborator_exception.h" diff --git a/src/library/tactic/elaborator_exception.h b/src/library/tactic/elaborator_exception.h index a516a21560..9bd13f15e2 100644 --- a/src/library/tactic/elaborator_exception.h +++ b/src/library/tactic/elaborator_exception.h @@ -11,12 +11,18 @@ Author: Leonardo de Moura namespace lean { class elaborator_exception : public formatted_exception { +protected: + bool m_ignore = false; // We ignore exceptions that mention synthetic sorrys. public: elaborator_exception(optional const & p, format const & fmt):formatted_exception(p, fmt) {} elaborator_exception(optional const & e, format const & fmt):formatted_exception(e, fmt) {} elaborator_exception(expr const & e, format const & fmt):formatted_exception(e, fmt) {} elaborator_exception(expr const & e, sstream const & strm):formatted_exception(e, format(strm.str())) {} elaborator_exception(expr const & e, char const * msg):formatted_exception(e, format(msg)) {} + + elaborator_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); } + bool is_ignored() const { return m_ignore; } + virtual throwable * clone() const override; virtual void rethrow() const override { throw *this; } }; @@ -31,6 +37,7 @@ public: virtual throwable * clone() const override { return new failed_to_synthesize_placeholder_exception(m_mvar, m_state); } + failed_to_synthesize_placeholder_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); } virtual void rethrow() const override { throw *this; } expr const & get_mvar() const { return m_mvar; } tactic_state const & get_tactic_state() const { return m_state; } @@ -45,9 +52,12 @@ class nested_elaborator_exception : public elaborator_exception { public: nested_elaborator_exception(optional const & p, elaborator_exception const & ex, format const & fmt): elaborator_exception(p, fmt), - m_exception(static_cast(ex.clone())) {} + m_exception(static_cast(ex.clone())) { + m_ignore = ex.is_ignored(); + } nested_elaborator_exception(expr const & ref, elaborator_exception const & ex, format const & fmt): nested_elaborator_exception(get_pos_info(ref), ex, fmt) {} + nested_elaborator_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); } virtual void rethrow() const override { throw *this; } virtual throwable * clone() const override; virtual optional get_pos() const override;