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

Add kernel_exceptions. The idea is to avoid expression formatting in the kernel. It also allows different frontends to display the error messages is a different way.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-16 12:51:12 -07:00
parent 1038f7346e
commit c41b3dc4d8
9 changed files with 237 additions and 197 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/CMakeLists.txt
View file

@ -1,6 +1,5 @@
add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
normalize.cpp context.cpp level.cpp object.cpp environment.cpp
type_check.cpp builtin.cpp expr_formatter.cpp expr_locator.cpp
occurs.cpp)
type_check.cpp builtin.cpp expr_formatter.cpp occurs.cpp)
target_link_libraries(kernel ${LEAN_LIBS})

105
src/kernel/environment.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <atomic>
#include <sstream>
#include <unordered_map>
#include "kernel_exception.h"
#include "environment.h"
#include "safe_arith.h"
#include "type_check.h"
@ -50,7 +51,6 @@ struct environment::imp {
object_dictionary m_object_dictionary;
// Expression formatter && locator
std::shared_ptr<expr_formatter> m_formatter;
std::shared_ptr<expr_locator> m_locator;
expr_formatter & get_formatter() {
if (m_formatter) {
@ -62,16 +62,6 @@ struct environment::imp {
}
}
expr_locator & get_locator() {
if (m_locator) {
return *m_locator;
} else {
// root environments always have a locator.
lean_assert(has_parent());
return m_parent->get_locator();
}
}
/**
\brief Return true iff this environment has children.
@ -125,9 +115,9 @@ struct environment::imp {
}
/** \brief Add a new universe variable */
level add_var(name const & n) {
level add_var(name const & n, environment const & env) {
if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; }))
throw exception("invalid universe variable declaration, it has already been declared");
throw already_declared_universe_exception(env, n);
level r(n);
m_uvars.push_back(r);
return r;
@ -175,12 +165,12 @@ struct environment::imp {
}
/** \brief Add a new universe variable with constraint n >= l */
level add_uvar(name const & n, level const & l) {
level add_uvar(name const & n, level const & l, environment const & env) {
if (has_parent())
throw exception("invalid universe declaration, universe variables can only be declared in top-level environments");
throw kernel_exception(env, "invalid universe declaration, universe variables can only be declared in top-level environments");
if (has_children())
throw exception("invalid universe declaration, environment has children environments");
level r = add_var(n);
throw read_only_environment_exception(env);
level r = add_var(n, env);
add_constraints(r, l, 0);
m_objects.push_back(new uvar_declaration(n, l));
return r;
@ -191,18 +181,15 @@ struct environment::imp {
exception if the environment and its ancestors do not
contain a universe variable named \c n.
*/
level get_uvar(name const & n) const {
level get_uvar(name const & n, environment const & env) const {
if (has_parent()) {
return m_parent->get_uvar(n);
return m_parent->get_uvar(n, env);
} else {
auto it = std::find_if(m_uvars.begin(), m_uvars.end(), [&](level const & l) { return uvar_name(l) == n; });
if (it == m_uvars.end()) {
std::ostringstream s;
s << "unknown universe variable '" << n << "'";
throw exception (s.str());
} else {
if (it == m_uvars.end())
throw unknown_universe_variable_exception(env, n);
else
return *it;
}
}
}
@ -223,26 +210,18 @@ struct environment::imp {
}
}
/** \brief Throw exception if environment has children. */
void check_no_children() {
if (has_children())
throw exception("invalid object declaration, environment has children environments");
}
/** \brief Throw exception if environment or its ancestors already have an object with the given name. */
void check_name_core(name const & n) {
void check_name_core(name const & n, environment const & env) {
if (has_parent())
m_parent->check_name_core(n);
if (m_object_dictionary.find(n) != m_object_dictionary.end()) {
std::ostringstream s;
s << "environment already contains an object with name '" << n << "'";
throw exception (s.str());
}
m_parent->check_name_core(n, env);
if (m_object_dictionary.find(n) != m_object_dictionary.end())
throw already_declared_object_exception(env, n);
}
void check_name(name const & n) {
check_no_children();
check_name_core(n);
void check_name(name const & n, environment const & env) {
if (has_children())
throw read_only_environment_exception(env);
check_name_core(n, env);
}
/**
@ -255,18 +234,13 @@ struct environment::imp {
void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
infer_universe(t, env);
expr v_t = infer_type(v, env);
if (!is_convertible(t, v_t, env)) {
std::ostringstream buffer;
buffer << "type mismatch when defining '" << n << "'\n"
<< "expected type:\n" << t << "\n"
<< "given type:\n" << v_t;
throw exception(buffer.str());
}
if (!is_convertible(t, v_t, env))
throw def_type_mismatch_exception(env, n, t, v, v_t);
}
/** \brief Throw exception if it is not a valid new definition */
void check_new_definition(name const & n, expr const & t, expr const & v, environment const & env) {
check_name(n);
check_name(n, env);
check_type(n, t, v, env);
}
@ -287,7 +261,7 @@ struct environment::imp {
The type of the new definition is the type of \c v.
*/
void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
check_name(n);
check_name(n, env);
expr v_t = infer_type(v, env);
register_named_object(new definition(n, v_t, v, opaque));
}
@ -300,14 +274,14 @@ struct environment::imp {
/** \brief Add new axiom. */
void add_axiom(name const & n, expr const & t, environment const & env) {
check_name(n);
check_name(n, env);
infer_universe(t, env);
register_named_object(new axiom(n, t));
}
/** \brief Add new variable. */
void add_var(name const & n, expr const & t, environment const & env) {
check_name(n);
check_name(n, env);
infer_universe(t, env);
register_named_object(new variable(n, t));
}
@ -329,15 +303,12 @@ struct environment::imp {
}
}
named_object const & get_object(name const & n) const {
named_object const & get_object(name const & n, environment const & env) const {
named_object const * ptr = get_object_ptr(n);
if (ptr) {
if (ptr)
return *ptr;
} else {
std::ostringstream s;
s << "unknown object '" << n << "'";
throw exception (s.str());
}
else
throw unknown_object_exception(env, n);
}
unsigned get_num_objects(bool local) const {
@ -373,7 +344,6 @@ struct environment::imp {
m_num_children(0) {
init_uvars();
m_formatter = mk_simple_expr_formatter();
m_locator = mk_dummy_expr_locator();
}
explicit imp(std::shared_ptr<imp> const & parent):
@ -413,15 +383,6 @@ expr_formatter & environment::get_formatter() const {
return m_imp->get_formatter();
}
void environment::set_locator(std::shared_ptr<expr_locator> const & locator) {
lean_assert(locator);
m_imp->m_locator = locator;
}
expr_locator & environment::get_locator() const {
return m_imp->get_locator();
}
environment environment::mk_child() const {
return environment(new imp(m_imp));
}
@ -440,7 +401,7 @@ environment environment::parent() const {
}
level environment::add_uvar(name const & n, level const & l) {
return m_imp->add_uvar(n, l);
return m_imp->add_uvar(n, l, *this);
}
bool environment::is_ge(level const & l1, level const & l2) const {
@ -452,7 +413,7 @@ void environment::display_uvars(std::ostream & out) const {
}
level environment::get_uvar(name const & n) const {
return m_imp->get_uvar(n);
return m_imp->get_uvar(n, *this);
}
void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
@ -480,7 +441,7 @@ void environment::add_anonymous_object(anonymous_object * o) {
}
named_object const & environment::get_object(name const & n) const {
return m_imp->get_object(n);
return m_imp->get_object(n, *this);
}
named_object const * environment::get_object_ptr(name const & n) const {

7
src/kernel/environment.h
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "object.h"
#include "level.h"
#include "expr_formatter.h"
#include "expr_locator.h"
namespace lean {
/**
@ -36,12 +35,6 @@ public:
/** \brief Return expression formatter. */
expr_formatter & get_formatter() const;
/** \brief Set expression locator. */
void set_locator(std::shared_ptr<expr_locator> const & locator);
/** \brief Return expression locator. */
expr_locator & get_locator() const;
// =======================================
// Parent/Child environment management
/**

35
src/kernel/expr_locator.cpp
View file

@ -1,35 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "expr_locator.h"
#include "exception.h"
namespace lean {
expr_locator::~expr_locator() {}
bool expr_locator::has_location(expr const & e) const { return false; }
std::pair<unsigned, unsigned> expr_locator::get_location(expr const & e) const { lean_unreachable(); return mk_pair(0, 0); }
std::shared_ptr<expr_locator> mk_dummy_expr_locator() {
return std::shared_ptr<expr_locator>(new expr_locator());
}
void throw_exception(expr_locator const & loc, expr const & src, char const * msg) {
if (loc.has_location(src)) {
std::ostringstream s;
auto p = loc.get_location(src);
s << "(line: " << p.first << ", pos: " << p.second << ") " << msg;
throw exception(s.str());
} else {
throw exception(msg);
}
}
void throw_exception(expr_locator const & loc, expr const & src, format const & msg) {
std::ostringstream s;
s << msg;
throw_exception(loc, src, s.str().c_str());
}
}

35
src/kernel/expr_locator.h
View file

@ -1,35 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "expr.h"
namespace lean {
/**
\brief Abstract class that specifies the API to retrieve
expression location (line and position).
*/
class expr_locator {
public:
virtual ~expr_locator();
/** \brief Return true iff the expression has location information associated with it. */
virtual bool has_location(expr const & e) const;
/** \brief Return location (line, pos) associated with expression. \pre has_location() */
virtual std::pair<unsigned, unsigned> get_location(expr const & e) const;
};
/**
\brief Create a expression locator s.t. has_location always return false.
*/
std::shared_ptr<expr_locator> mk_dummy_expr_locator();
/**
\brief Throw an exception with the given msg, and include location
of the given expression (if available).
*/
void throw_exception [[noreturn]] (expr_locator const & loc, expr const & src, char const * msg);
void throw_exception [[noreturn]] (expr_locator const & loc, expr const & src, format const & msg);
}

182
src/kernel/kernel_exception.h Normal file
View file

@ -0,0 +1,182 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "exception.h"
#include "context.h"
#include "environment.h"
namespace lean {
class environment;
/** \brief Base class for all kernel exceptions. */
class kernel_exception : public exception {
protected:
environment m_env;
public:
kernel_exception(environment const & env):m_env(env) {}
kernel_exception(environment const & env, char const * msg):exception(msg), m_env(env) {}
virtual ~kernel_exception() noexcept {}
environment const & get_environment() const { return m_env; }
};
/** \brief Base class for unknown universe or object exceptions. */
class unknown_name_exception : public kernel_exception {
name m_name;
public:
unknown_name_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {}
virtual ~unknown_name_exception() {}
name const & get_name() const { return m_name; }
};
/** \brief Exception used to report that a universe variable is not known in a given environment. */
class unknown_universe_variable_exception : public unknown_name_exception {
public:
unknown_universe_variable_exception(environment const & env, name const & n):unknown_name_exception(env, n) {}
virtual char const * what() const noexcept { return "unknown universe variable"; }
};
/** \brief Exception used to report that an object is not known in a given environment. */
class unknown_object_exception : public unknown_name_exception {
public:
unknown_object_exception(environment const & env, name const & n):unknown_name_exception(env, n) {}
virtual char const * what() const noexcept { return "unknown object"; }
};
/** \brief Base class for already declared universe or object. */
class already_declared_exception : public kernel_exception {
name m_name;
public:
already_declared_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {}
virtual ~already_declared_exception() noexcept {}
name const & get_name() const { return m_name; }
};
/** \brief Exception used to report that a universe variable has already been declared in a given environment. */
class already_declared_universe_exception : public already_declared_exception {
public:
already_declared_universe_exception(environment const & env, name const & n):already_declared_exception(env, n) {}
virtual char const * what() const noexcept { return "invalid universe variable declaration, it has already been declared"; }
};
/** \brief Exception used to report that an object has already been declared in a given environment. */
class already_declared_object_exception : public already_declared_exception {
public:
already_declared_object_exception(environment const & env, name const & n):already_declared_exception(env, n) {}
virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; }
};
/**
\brief Exception used to report that a update has been tried on a
read-only environment.
An environment is read-only if it has "children environments".
*/
class read_only_environment_exception : public kernel_exception {
public:
read_only_environment_exception(environment const & env):kernel_exception(env) {}
virtual char const * what() const noexcept { return "environment cannot be updated because it has children environments"; }
};
/** \brief Base class for type checking related exceptions. */
class type_checker_exception : public kernel_exception {
public:
type_checker_exception(environment const & env):kernel_exception(env) {}
};
/**
\brief Exception used to report an application argument type
mismatch.
Explanation:
In the environment get_environment() and local context
get_context(), the argument get_arg_pos() of the application
get_application() has type get_given_type(), but it is expected to
have type get_expected_type().
*/
class app_type_mismatch_exception : public type_checker_exception {
context m_context;
expr m_app;
unsigned m_arg_pos;
expr m_expected_type;
expr m_given_type;
public:
app_type_mismatch_exception(environment const & env, context const & ctx, expr const & app, unsigned pos, expr const & expected, expr const & given):
type_checker_exception(env), m_context(ctx), m_app(app), m_arg_pos(pos),
m_expected_type(expected), m_given_type(given) {}
virtual ~app_type_mismatch_exception() {}
context const & get_context() const { return m_context; }
expr const & get_application() const { return m_app; }
unsigned get_arg_pos() const { return m_arg_pos; }
expr const & get_expected_type() const { return m_expected_type; }
expr const & get_given_type() const { return m_given_type; }
virtual char const * what() const noexcept { return "application argument type mismatch"; }
};
/**
\brief Exception used to report than an expression that is not a
function is being used as a function.
Explanation:
In the environment get_environment() and local context
get_context(), the expression get_expr() is expected to be a function.
*/
class function_expected_exception : public type_checker_exception {
context m_context;
expr m_expr;
public:
function_expected_exception(environment const & env, context const & ctx, expr const & e):
type_checker_exception(env), m_context(ctx), m_expr(e) {}
virtual ~function_expected_exception() {}
context const & get_context() const { return m_context; }
expr const & get_expr() const { return m_expr; }
virtual char const * what() const noexcept { return "function expected"; }
};
/**
\brief Exception used to report than an expression that is not a
type is being used where a type is expected.
Explanation:
In the environment get_environment() and local context
get_context(), the expression get_expr() is expected to be a type.
*/
class type_expected_exception : public type_checker_exception {
context m_context;
expr m_expr;
public:
type_expected_exception(environment const & env, context const & ctx, expr const & e):
type_checker_exception(env), m_context(ctx), m_expr(e) {}
virtual ~type_expected_exception() {}
context const & get_context() const { return m_context; }
expr const & get_expr() const { return m_expr; }
virtual char const * what() const noexcept { return "type expected"; }
};
/**
\brief Exception used to report a definition type mismatch.
Explanation:
In the environment get_environment(), the declaration with name
get_name(), type get_type() and value get_value() is incorrect
because the value has type get_value_type() and it not matches
the given type get_type().
*/
class def_type_mismatch_exception : public type_checker_exception {
name m_name;
expr m_type;
expr m_value;
expr m_value_type;
public:
def_type_mismatch_exception(environment const & env, name const & n, expr const & type, expr const & val, expr const & val_type):
type_checker_exception(env), m_name(n), m_type(type), m_value(val), m_value_type(val_type) {}
virtual ~def_type_mismatch_exception() {}
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
expr const & get_value() const { return m_value; }
expr const & get_value_type() const { return m_value_type; }
virtual char const * what() const noexcept { return "definition type mismatch"; }
};
}

51
src/kernel/type_check.cpp
View file

@ -5,13 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "type_check.h"
#include "scoped_map.h"
#include "environment.h"
#include "kernel_exception.h"
#include "normalize.h"
#include "instantiate.h"
#include "scoped_map.h"
#include "builtin.h"
#include "free_vars.h"
#include "exception.h"
#include "trace.h"
namespace lean {
@ -58,47 +58,6 @@ struct infer_type_fn {
return lift_free_vars(def.get_domain(), length(c) - length(def_c));
}
expr_formatter & fmt() { return m_env.get_formatter(); }
format nl_indent(format const & f) { return fmt().nest(format{line(), f}); }
void throw_error [[ noreturn ]] (expr const & src, format const & msg) {
throw_exception(m_env.get_locator(), src, msg);
}
/** \brief Include context (if not empty) in the formatted message */
void push_context(format & msg, context const & ctx) {
if (!is_empty(ctx)) {
msg += format{format("in context: "), nl_indent(pp(fmt(), ctx)), line()};
}
}
void throw_type_expected_error [[ noreturn ]] (expr const & t, context const & ctx) {
context ctx2 = sanitize_names(ctx, t);
format msg = format("type expected, ");
push_context(msg, ctx2);
msg += format{format("got:"), nl_indent(fmt()(t, ctx2))};
throw_error(t, msg);
}
void throw_function_expected_error [[ noreturn ]] (expr const & s, context const & ctx) {
context ctx2 = sanitize_names(ctx, s);
format msg = format("function expected, ");
push_context(msg, ctx2);
msg += format{format("got:"), nl_indent(fmt()(s, ctx2))};
throw_error(s, msg);
}
void throw_type_mismatch_error [[ noreturn ]] (expr const & app, unsigned arg_pos,
expr const & expected, expr const & given, context const & ctx) {
context ctx2 = sanitize_names(ctx, {app, expected, given});
format msg = format{format("type mismatch at argument "), format(arg_pos), space(), format("of"),
nl_indent(fmt()(app, ctx2)), line()};
push_context(msg, ctx2);
msg += format{format("expected type:"), nl_indent(fmt()(expected, ctx2)), line(), format("given type:"), nl_indent(fmt()(given, ctx2))};
throw_error(arg(app, arg_pos), msg);
}
level infer_universe(expr const & t, context const & ctx) {
lean_trace("type_check", tout << "infer universe\n" << t << "\n";);
expr u = normalize(infer_type(t, ctx), m_env, ctx);
@ -106,7 +65,7 @@ struct infer_type_fn {
return ty_level(u);
if (u == Bool)
return level();
throw_type_expected_error(t, ctx);
throw type_expected_exception(m_env, ctx, t);
}
expr check_pi(expr const & e, expr const & s, context const & ctx) {
@ -115,7 +74,7 @@ struct infer_type_fn {
expr r = normalize(e, m_env, ctx);
if (is_pi(r))
return r;
throw_function_expected_error(s, ctx);
throw function_expected_exception(m_env, ctx, s);
}
expr infer_pi(expr const & e, context const & ctx) {
@ -153,7 +112,7 @@ struct infer_type_fn {
expr const & c = arg(e, i);
expr c_t = infer_type(c, ctx);
if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx))
throw_type_mismatch_error(e, i, abst_domain(f_t), c_t, ctx);
throw app_type_mismatch_exception(m_env, ctx, e, i, abst_domain(f_t), c_t);
if (closed(abst_body(f_t)))
f_t = abst_body(f_t);
else if (closed(c))

15
src/tests/kernel/environment.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel_exception.h"
#include "environment.h"
#include "type_check.h"
#include "toplevel.h"
@ -192,6 +193,19 @@ static void tst8() {
lean_assert(counter == 6);
}
static void tst9() {
try {
environment env;
env.add_uvar("u1", level());
env.add_uvar("u2", level());
env.add_uvar("u1", level("u2"));
} catch (already_declared_universe_exception & ex) {
std::cout << ex.what() << "\n";
level l = ex.get_environment().get_uvar(ex.get_name());
std::cout << l << "\n";
}
}
int main() {
enable_trace("is_convertible");
tst1();
@ -202,5 +216,6 @@ int main() {
tst6();
tst7();
tst8();
tst9();
return has_violations() ? 1 : 0;
}

1
src/util/exception.h
View file

@ -13,6 +13,7 @@ namespace lean {
class exception : public std::exception {
protected:
std::string m_msg;
exception() {}
public:
exception(char const * msg);
exception(std::string const & msg);