From 498b2f681ef7b68f60aecb29b6efe95da123a715 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Oct 2014 14:44:58 -0700 Subject: [PATCH] feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution --- src/frontends/lean/CMakeLists.txt | 3 ++- src/frontends/lean/elaborator.cpp | 5 ++-- src/frontends/lean/elaborator_exception.cpp | 26 +++++++++++++++++++ src/frontends/lean/elaborator_exception.h | 16 ++++++++++++ src/frontends/lean/placeholder_elaborator.cpp | 12 +++++++-- 5 files changed, 56 insertions(+), 6 deletions(-) create mode 100644 src/frontends/lean/elaborator_exception.cpp create mode 100644 src/frontends/lean/elaborator_exception.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 8d1509d00..81dbdebd6 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,7 +7,8 @@ begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp -proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp) +proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp +elaborator_exception.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7531ce0d4..f5afb88eb 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -46,6 +46,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_tactic.h" #include "frontends/lean/pp_options.h" #include "frontends/lean/begin_end_ext.h" +#include "frontends/lean/elaborator_exception.h" namespace lean { /** \brief 'Choice' expressions (choice e_1 ... e_n) are mapped into a metavariable \c ?m @@ -1212,9 +1213,7 @@ static expr translate_local_name(environment const & env, list const & ctx if (local_pp_name(local) == local_name) return copy(local); } - // TODO(Leo): we should create an elaborator exception. - // Using kernel_exception here is just a dirty hack. - throw_kernel_exception(env, sstream() << "unknown identifier '" << local_name << "'", src); + throw_elaborator_exception(env, sstream() << "unknown identifier '" << local_name << "'", src); } /** \brief Translated local constants (and undefined constants) occurring in \c e into diff --git a/src/frontends/lean/elaborator_exception.cpp b/src/frontends/lean/elaborator_exception.cpp new file mode 100644 index 000000000..f78efac45 --- /dev/null +++ b/src/frontends/lean/elaborator_exception.cpp @@ -0,0 +1,26 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/kernel_exception.h" +#include "frontends/lean/elaborator_exception.h" + +namespace lean { +[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m) { + throw_kernel_exception(env, msg, m); +} + +[[ noreturn ]] void throw_elaborator_exception(environment const & env, sstream const & strm, expr const & m) { + throw_kernel_exception(env, strm, m); +} + +[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn) { + throw_kernel_exception(env, msg, m, fn); +} + +[[ noreturn ]] void throw_elaborator_exception(environment const & env, expr const & m, pp_fn const & fn) { + throw_kernel_exception(env, m, fn); +} +} diff --git a/src/frontends/lean/elaborator_exception.h b/src/frontends/lean/elaborator_exception.h new file mode 100644 index 000000000..d6d6233b9 --- /dev/null +++ b/src/frontends/lean/elaborator_exception.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" +#include "kernel/formatter.h" + +namespace lean { +[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m); +[[ noreturn ]] void throw_elaborator_exception(environment const & env, sstream const & strm, expr const & m); +[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn); +[[ noreturn ]] void throw_elaborator_exception(environment const & env, expr const & m, pp_fn const & fn); +} diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 7d4ddec85..b5cec43f9 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" +#include "kernel/error_msgs.h" #include "library/unifier.h" #include "library/reducible.h" #include "library/metavar_closure.h" @@ -18,6 +19,7 @@ Author: Leonardo de Moura #include "frontends/lean/class.h" #include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" +#include "frontends/lean/elaborator_exception.h" #ifndef LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES #define LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES false @@ -279,8 +281,14 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const cnstrs = p.second; expr next_solution = subst.instantiate(new_meta); if (solution) { - // TODO(Leo): more informative error message - throw exception("ambiguous class-instance resolution, there is more than one solution"); + throw_elaborator_exception(env, m, [=](formatter const & fmt) { + format r = format("ambiguous class-instance resolution, " + "there is more than one solution"); + r += pp_indent_expr(fmt, *solution); + r += compose(line(), format("and")); + r += pp_indent_expr(fmt, next_solution); + return r; + }); } else { solution = next_solution; }