michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/kernel_exception): add new auxiliary functions for throwing kernel exceptions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 10:37:03 -07:00
parent 3a19d9fee1
commit 84c1cf9600
3 changed files with 21 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/kernel_exception.cpp
View file

@ -37,6 +37,14 @@ public:
throw_kernel_exception(env, strm.str().c_str(), m);
}
[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m) {
throw_kernel_exception(env, msg, some_expr(m));
}
[[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, expr const & m) {
throw_kernel_exception(env, strm, some_expr(m));
}
[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn) {
throw generic_kernel_exception(env, msg, m, fn);
}

5
src/kernel/kernel_exception.h
View file

@ -35,8 +35,9 @@ public:
};
[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m = none_expr());
[[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm,
optional<expr> const & m = none_expr());
[[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, optional<expr> const & m = none_expr());
[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m);
[[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, expr const & m);
[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn);
[[ noreturn ]] void throw_kernel_exception(environment const & env, optional<expr> const & m, pp_fn const & fn);
[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn);

20
src/kernel/type_checker.cpp
View file

@ -263,11 +263,11 @@ struct type_checker::imp {
});
}
void check_level(level const & l) {
void check_level(level const & l, expr const & s) {
if (auto n1 = get_undef_global(l, m_env))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'");
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
if (auto n2 = get_undef_param(l, m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'");
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
}
/**
@ -291,10 +291,10 @@ struct type_checker::imp {
r = mlocal_type(e);
break;
case expr_kind::Var:
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it");
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
case expr_kind::Sort:
if (!infer_only)
check_level(sort_level(e));
check_level(sort_level(e), e);
r = mk_sort(mk_succ(sort_level(e)));
break;
case expr_kind::Constant: {
@ -306,7 +306,7 @@ struct type_checker::imp {
<< length(ps) << " expected, #" << length(ls) << " provided");
if (!infer_only) {
for (level const & l : ls)
check_level(l);
check_level(l, e);
}
r = instantiate_params(d.get_type(), ps, ls);
break;
@ -319,11 +319,11 @@ struct type_checker::imp {
if (!infer_only && macro_def(e).trust_level() <= m_env.trust_lvl()) {
optional<expr> m = expand_macro(e);
if (!m)
throw_kernel_exception(m_env, "failed to expand macro", some_expr(e));
throw_kernel_exception(m_env, "failed to expand macro", e);
expr t = infer_type_core(*m, infer_only);
delayed_justification jst([=]() { return mk_macro_jst(e); });
if (!is_def_eq(r, t, jst))
throw_kernel_exception(m_env, g_macro_error_msg, some_expr(e));
throw_kernel_exception(m_env, g_macro_error_msg, e);
}
break;
}
@ -416,12 +416,12 @@ expr type_checker::ensure_sort(expr const & t) { return m_ptr->ensure_sort(t, t)
static void check_no_metavar(environment const & env, expr const & e) {
if (has_metavar(e))
throw kernel_exception(env, "failed to add declaration to environment, it contains metavariables");
throw_kernel_exception(env, "failed to add declaration to environment, it contains metavariables", e);
}
static void check_no_local(environment const & env, expr const & e) {
if (has_local(e))
throw kernel_exception(env, "failed to add declaration to environment, it contains local constants");
throw_kernel_exception(env, "failed to add declaration to environment, it contains local constants", e);
}
static void check_no_mlocal(environment const & env, expr const & e) {