max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/type_context,frontends/lean/elaborator): add class_exception (for max depth reached), ignore them during coercion resolution (just add a trace message)

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-01 08:51:09 -08:00
parent 6320168c90
commit a44a975388
3 changed files with 22 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/frontends/lean/elaborator.cpp
View file

@ -434,7 +434,15 @@ optional<expr> elaborator::mk_coercion_core(expr const & e, expr const & e_type,
"('set_option trace.app_builder true' for more information)");
return none_expr();
}
optional<expr> inst = m_ctx.mk_class_instance_at(m_ctx.lctx(), has_coe_t);
optional<expr> inst;
try {
inst = m_ctx.mk_class_instance_at(m_ctx.lctx(), has_coe_t);
} catch (class_exception &) {
trace_coercion_failure(e_type, type, ref,
"failed to synthesize class instance for 'has_coe_t' "
"('set_option trace.class_instances true' for more information)");
return none_expr();
}
if (!inst) {
trace_coercion_failure(e_type, type, ref,
"failed to synthesize 'has_coe_t' type class instance "
@ -452,8 +460,12 @@ optional<expr> elaborator::mk_coercion_core(expr const & e, expr const & e_type,
}
bool elaborator::is_monad(expr const & e) {
expr m = mk_app(m_ctx, get_monad_name(), e);
return static_cast<bool>(m_ctx.mk_class_instance(m));
try {
expr m = mk_app(m_ctx, get_monad_name(), e);
return static_cast<bool>(m_ctx.mk_class_instance(m));
} catch (class_exception &) {
return false;
}
}
/*

2
src/library/type_context.cpp
View file

@ -2959,7 +2959,7 @@ optional<name> type_context::is_class(expr const & type) {
return is_full_class(type);
}
[[ noreturn ]] static void throw_class_exception(expr const & m, char const * msg) { throw generic_exception(m, msg); }
[[ noreturn ]] static void throw_class_exception(expr const & m, char const * msg) { throw class_exception(m, msg); }
struct instance_synthesizer {
struct stack_entry {

6
src/library/type_context.h
View file

@ -17,8 +17,14 @@ Author: Leonardo de Moura
#include "library/projection.h"
#include "library/metavar_context.h"
#include "library/expr_pair_maps.h"
#include "library/exception.h"
namespace lean {
class class_exception : public generic_exception {
public:
class_exception(expr const & m, char const * msg):generic_exception(m, msg) {}
};
enum class transparency_mode { All, Semireducible, Reducible, None };
/* \brief Cached information for type_context. */