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

refactor(kernel): environment, kernel object and exceptions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-18 22:55:00 -08:00
parent 3c8ccdd33d
commit b5f0f28009
8 changed files with 146 additions and 531 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/CMakeLists.txt
View file

@ -1,9 +1,10 @@
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
# normalizer.cpp object.cpp environment.cpp object.cpp environment.cpp
# normalizer.cpp
# type_checker.cpp kernel.cpp metavar.cpp # type_checker.cpp kernel.cpp metavar.cpp
# justification.cpp unification_constraint.cpp kernel_exception.cpp # justification.cpp unification_constraint.cpp
# type_checker_justification.cpp pos_info_provider.cpp # type_checker_justification.cpp pos_info_provider.cpp
# replace_visitor.cpp update_expr.cpp io_state.cpp # replace_visitor.cpp update_expr.cpp io_state.cpp
# universe_constraints.cpp # universe_constraints.cpp

300
src/kernel/environment.cpp
View file

@ -22,10 +22,8 @@ Author: Leonardo de Moura
#include "kernel/kernel_exception.h" #include "kernel/kernel_exception.h"
#include "kernel/environment.h" #include "kernel/environment.h"
#include "kernel/threadsafe_environment.h" #include "kernel/threadsafe_environment.h"
#include "kernel/type_checker.h" // #include "kernel/type_checker.h"
#include "kernel/normalizer.h" // #include "kernel/normalizer.h"
#include "kernel/universe_constraints.h"
#include "kernel/kernel.h"
#include "version.h" #include "version.h"
namespace lean { namespace lean {
@ -182,7 +180,7 @@ unsigned environment_cell::get_max_weight(expr const & e) {
} }
return true; return true;
}; };
for_each_fn<decltype(proc)> visitor(proc); for_each_fn visitor(proc);
visitor(e); visitor(e);
return w; return w;
} }
@ -192,12 +190,12 @@ void environment_cell::check_name_core(name const & n) {
if (has_parent()) if (has_parent())
m_parent->check_name_core(n); m_parent->check_name_core(n);
if (m_object_dictionary.find(n) != m_object_dictionary.end()) if (m_object_dictionary.find(n) != m_object_dictionary.end())
throw already_declared_exception(env(), n); throw_already_declared(env(), n);
} }
void environment_cell::check_name(name const & n) { void environment_cell::check_name(name const & n) {
if (has_children()) if (has_children())
throw read_only_environment_exception(env()); throw_read_only_environment(env());
check_name_core(n); check_name_core(n);
} }
@ -229,177 +227,17 @@ object environment_cell::get_object(name const & n) const {
if (obj) { if (obj) {
return *obj; return *obj;
} else { } else {
throw unknown_object_exception(env(), n); throw_unknown_object(env(), n);
} }
} }
class universes {
public:
std::vector<level> m_uvars;
universe_constraints m_constraints;
};
universes & environment_cell::get_rw_universes() {
if (!m_universes) {
lean_assert(has_parent());
m_universes.reset(new universes(m_parent->get_rw_universes()));
}
return *m_universes;
}
universes const & environment_cell::get_ro_universes() const {
if (m_universes) {
return *m_universes;
} else {
lean_assert(has_parent());
return m_parent->get_ro_universes();
}
}
universe_constraints & environment_cell::get_rw_ucs() {
return get_rw_universes().m_constraints;
}
universe_constraints const & environment_cell::get_ro_ucs() const {
return get_ro_universes().m_constraints;
}
optional<int> environment_cell::get_universe_distance(name const & u1, name const & u2) const {
return get_ro_ucs().get_distance(u1, u2);
}
/** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */
bool environment_cell::is_ge(level const & l1, level const & l2, int k) const {
if (l1 == l2)
return k <= 0;
switch (kind(l2)) {
case level_kind::UVar:
switch (kind(l1)) {
case level_kind::UVar: return get_ro_ucs().is_implied(uvar_name(l1), uvar_name(l2), k);
case level_kind::Lift: return is_ge(lift_of(l1), l2, safe_sub(k, lift_offset(l1)));
case level_kind::Max: return std::any_of(max_begin_levels(l1), max_end_levels(l1), [&](level const & l) { return is_ge(l, l2, k); });
}
case level_kind::Lift: return is_ge(l1, lift_of(l2), safe_add(k, lift_offset(l2)));
case level_kind::Max: return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); });
}
lean_unreachable(); // LCOV_EXCL_LINE
}
/** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */
bool environment_cell::is_ge(level const & l1, level const & l2) const {
return is_ge(l1, l2, 0);
}
/** \brief Add a new universe variable */
level environment_cell::add_uvar_core(name const & n) {
check_name(n);
universes & u = get_rw_universes();
u.m_constraints.add_var(n);
level r(n);
u.m_uvars.push_back(r);
return r;
}
/** /**
\brief Add all basic constraints implied by n >= l + k The kernel should *not* accept expressions containing Local or Meta.
Reason: they may introduce unsoundness.
A basic constraint is a constraint of the form u >= v + k
where u and v are universe variables.
*/ */
void environment_cell::add_constraints(name const & n, level const & l, int k) { void environment_cell::check_no_mlocal(expr const & e) {
switch (kind(l)) { if (find(e, [](expr const & a, unsigned) { return is_mlocal(a); }))
case level_kind::UVar: get_rw_ucs().add_constraint(n, uvar_name(l), k); return; throw_kernel_exception(env(), "expression has metavariable and/or local constants, this is a bug in one of Lean tactics and/or solvers"); // LCOV_EXCL_LINE
case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return;
case level_kind::Max: std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
/**
\brief Check if n >= l + k is consistent with the existing constraints.
*/
void environment_cell::check_consistency(name const & n, level const & l, int k) const {
switch (kind(l)) {
case level_kind::UVar:
if (l == ty_level(TypeU))
throw kernel_exception(env(), sstream() << "invalid universe constraint: " << n << " >= " << l << " + " << k
<< ", several modules in Lean assume that " << l << " is the maximal universe");
if (!get_ro_ucs().is_consistent(n, uvar_name(l), k))
throw kernel_exception(env(), sstream() << "universe constraint inconsistency: " << n << " >= " << l << " + " << k);
if (get_ro_ucs().overflows(n, uvar_name(l), k))
throw kernel_exception(env(), sstream() << "universe constraint produces an integer overflow: " << n << " >= " << l << " + " << k);
return;
case level_kind::Lift: check_consistency(n, lift_of(l), safe_add(k, lift_offset(l))); return;
case level_kind::Max: std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { check_consistency(n, l1, k); }); return;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
/** \brief Add a new universe variable with constraint n >= l */
level environment_cell::add_uvar_cnstr(name const & n, level const & l) {
if (has_children())
throw read_only_environment_exception(env());
level r;
auto const & uvs = get_ro_universes().m_uvars;
auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
bool new_universe;
check_consistency(n, l, 0);
if (it == uvs.end()) {
r = add_uvar_core(n);
new_universe = true;
} else {
// universe n already exists, we must check consistency of the new constraint.
r = *it;
new_universe = false;
}
m_objects.push_back(mk_uvar_cnstr(n, l));
add_constraints(n, l, 0);
name const & Uname = uvar_name(ty_level(TypeU));
if (new_universe && n != Uname && !is_ge(ty_level(TypeU), r, 1)) {
// In Lean, U is the maximal universe, several Lean modules assume that,
// and the kernel axioms are all with respect to U.
// So, we force all other universes to smaller than U
add_uvar_cnstr(Uname, r+1);
}
return r;
}
/**
\brief Return the universe variable with given name. Throw an
exception if the environment and its ancestors do not
contain a universe variable named \c n.
*/
level environment_cell::get_uvar(name const & n) const {
auto const & uvs = get_ro_universes().m_uvars;
auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
if (it == uvs.end())
throw unknown_universe_variable_exception(env(), n);
else
return *it;
}
/**
\brief Initialize the set of universe variables with bottom
*/
void environment_cell::init_uvars() {
m_universes.reset(new universes());
universes & u = get_rw_universes();
level bottom;
u.m_uvars.push_back(bottom);
u.m_constraints.add_var(uvar_name(bottom));
}
/**
The kernel should *not* accept expressions containing cached types.
Reason: Cached types may introduce unsoundness.
For example, in the environment env, the constant x may have type T.
Now suppose we are trying to add a new definition D that contains x,
and x is associated with a cached type T'. The cached type may allow
us to accept a definition that is type incorrect with respect to env.
*/
void environment_cell::check_no_cached_type(expr const & e) {
if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); }))
throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); // LCOV_EXCL_LINE
} }
/** /**
@ -407,12 +245,21 @@ void environment_cell::check_no_cached_type(expr const & e) {
v is not convertible to \c t. v is not convertible to \c t.
*/ */
void environment_cell::check_type(name const & n, expr const & t, expr const & v) { void environment_cell::check_type(name const & n, expr const & t, expr const & v) {
#if 0
if (m_type_check) { if (m_type_check) {
m_type_checker->check_type(t); m_type_checker->check_type(t);
expr v_t = m_type_checker->check(v); expr v_t = m_type_checker->check(v);
if (!m_type_checker->is_convertible(v_t, t)) if (!m_type_checker->is_convertible(v_t, t))
throw def_type_mismatch_exception(env(), n, t, v, v_t); throw def_type_mismatch_exception(env(), n, t, v, v_t);
} }
#endif
}
void environment_cell::check_type(expr const & t) {
#if 0
if (m_type_check)
m_type_checker->check_type(t);
#endif
} }
/** \brief Throw exception if it is not a valid new definition */ /** \brief Throw exception if it is not a valid new definition */
@ -421,34 +268,10 @@ void environment_cell::check_new_definition(name const & n, expr const & t, expr
check_type(n, t, v); check_type(n, t, v);
} }
/** \brief Add a new builtin value to this environment */
void environment_cell::add_builtin(expr const & v) {
if (!is_value(v))
throw invalid_builtin_value_declaration(env(), v); // LCOV_EXCL_LINE
name const & n = to_value(v).get_name();
check_name(n);
name const & u = to_value(v).get_unicode_name();
check_name(u);
register_named_object(mk_builtin(v));
if (u != n) {
auxiliary_section([&]() {
add_definition(u, to_value(v).get_type(), mk_constant(n), false);
});
}
}
/** \brief Add a new builtin value set to this environment */
void environment_cell::add_builtin_set(expr const & r) {
if (!is_value(r))
throw invalid_builtin_value_declaration(env(), r); // LCOV_EXCL_LINE
check_name(to_value(r).get_name());
register_named_object(mk_builtin_set(r));
}
/** \brief Add new definition. */ /** \brief Add new definition. */
void environment_cell::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { void environment_cell::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
check_no_cached_type(t); check_no_mlocal(t);
check_no_cached_type(v); check_no_mlocal(v);
check_new_definition(n, t, v); check_new_definition(n, t, v);
unsigned w = get_max_weight(v) + 1; unsigned w = get_max_weight(v) + 1;
register_named_object(mk_definition(n, t, v, w)); register_named_object(mk_definition(n, t, v, w));
@ -461,13 +284,15 @@ void environment_cell::add_definition(name const & n, expr const & t, expr const
The type of the new definition is the type of \c v. The type of the new definition is the type of \c v.
*/ */
void environment_cell::add_definition(name const & n, expr const & v, bool opaque) { void environment_cell::add_definition(name const & n, expr const & v, bool opaque) {
check_no_cached_type(v); check_no_mlocal(v);
check_name(n); check_name(n);
expr v_t; expr v_t;
#if 0
if (m_type_check) if (m_type_check)
v_t = m_type_checker->check(v); v_t = m_type_checker->check(v);
else else
v_t = m_type_checker->infer_type(v); v_t = m_type_checker->infer_type(v);
#endif
unsigned w = get_max_weight(v) + 1; unsigned w = get_max_weight(v) + 1;
register_named_object(mk_definition(n, v_t, v, w)); register_named_object(mk_definition(n, v_t, v, w));
if (opaque) if (opaque)
@ -476,8 +301,8 @@ void environment_cell::add_definition(name const & n, expr const & v, bool opaqu
/** \brief Add new theorem. */ /** \brief Add new theorem. */
void environment_cell::add_theorem(name const & n, expr const & t, expr const & v) { void environment_cell::add_theorem(name const & n, expr const & t, expr const & v) {
check_no_cached_type(t); check_no_mlocal(t);
check_no_cached_type(v); check_no_mlocal(v);
check_new_definition(n, t, v); check_new_definition(n, t, v);
register_named_object(mk_theorem(n, t, v)); register_named_object(mk_theorem(n, t, v));
} }
@ -485,26 +310,24 @@ void environment_cell::add_theorem(name const & n, expr const & t, expr const &
void environment_cell::set_opaque(name const & n, bool opaque) { void environment_cell::set_opaque(name const & n, bool opaque) {
auto obj = find_object(n); auto obj = find_object(n);
if (!obj || !obj->is_definition()) if (!obj || !obj->is_definition())
throw kernel_exception(env(), sstream() << "set_opaque failed, '" << n << "' is not a definition"); throw_kernel_exception(env(), sstream() << "set_opaque failed, '" << n << "' is not a definition");
obj->set_opaque(opaque); obj->set_opaque(opaque);
add_neutral_object(new set_opaque_command(n, opaque)); add_neutral_object(new set_opaque_command(n, opaque));
} }
/** \brief Add new axiom. */ /** \brief Add new axiom. */
void environment_cell::add_axiom(name const & n, expr const & t) { void environment_cell::add_axiom(name const & n, expr const & t) {
check_no_cached_type(t); check_no_mlocal(t);
check_name(n); check_name(n);
if (m_type_check) check_type(t);
m_type_checker->check_type(t);
register_named_object(mk_axiom(n, t)); register_named_object(mk_axiom(n, t));
} }
/** \brief Add new variable. */ /** \brief Add new variable. */
void environment_cell::add_var(name const & n, expr const & t) { void environment_cell::add_var(name const & n, expr const & t) {
check_no_cached_type(t); check_no_mlocal(t);
check_name(n); check_name(n);
if (m_type_check) check_type(t);
m_type_checker->check_type(t);
register_named_object(mk_var_decl(n, t)); register_named_object(mk_var_decl(n, t));
} }
@ -532,20 +355,36 @@ object const & environment_cell::get_object(unsigned i, bool local) const {
} }
} }
expr environment_cell::type_check(expr const & e, context const & ctx) const { expr environment_cell::type_check(expr const & e) const {
#if 0
return m_type_checker->check(e, ctx); return m_type_checker->check(e, ctx);
#else
return e;
#endif
} }
expr environment_cell::infer_type(expr const & e, context const & ctx) const { expr environment_cell::infer_type(expr const & e) const {
#if 0
return m_type_checker->infer_type(e, ctx); return m_type_checker->infer_type(e, ctx);
#else
return e;
#endif
} }
expr environment_cell::normalize(expr const & e, context const & ctx, bool unfold_opaque) const { expr environment_cell::normalize(expr const & e) const {
#if 0
return m_type_checker->get_normalizer()(e, ctx, unfold_opaque); return m_type_checker->get_normalizer()(e, ctx, unfold_opaque);
#else
return e;
#endif
} }
bool environment_cell::is_proposition(expr const & e, context const & ctx) const { bool environment_cell::is_proposition(expr const & e) const {
#if 0
return m_type_checker->is_proposition(e, ctx); return m_type_checker->is_proposition(e, ctx);
#else
return false;
#endif
} }
bool environment_cell::already_imported(name const & n) const { bool environment_cell::already_imported(name const & n) const {
@ -561,7 +400,7 @@ bool environment_cell::mark_imported_core(name n) {
if (already_imported(n)) { if (already_imported(n)) {
return false; return false;
} else if (has_children()) { } else if (has_children()) {
throw read_only_environment_exception(env()); throw_read_only_environment(env());
} else { } else {
m_imported_modules.insert(n); m_imported_modules.insert(n);
return true; return true;
@ -618,12 +457,12 @@ bool environment_cell::load_core(std::string const & fname, io_state const & ios
if (!mod_name || mark_imported_core(fname)) { if (!mod_name || mark_imported_core(fname)) {
std::ifstream in(fname, std::ifstream::binary); std::ifstream in(fname, std::ifstream::binary);
if (!in.good()) if (!in.good())
throw exception(sstream() << "failed to open file '" << fname << "'"); throw_kernel_exception(env(), sstream() << "failed to open file '" << fname << "'");
deserializer d(in); deserializer d(in);
std::string header; std::string header;
d >> header; d >> header;
if (header != g_olean_header) if (header != g_olean_header)
throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file"); throw_kernel_exception(env(), sstream() << "file '" << fname << "' does not seem to be a valid object Lean file");
unsigned major, minor; unsigned major, minor;
// Perhaps we should enforce the right version number // Perhaps we should enforce the right version number
d >> major >> minor; d >> major >> minor;
@ -672,7 +511,6 @@ environment_cell::environment_cell():
m_num_children(0) { m_num_children(0) {
m_trust_imported = false; m_trust_imported = false;
m_type_check = true; m_type_check = true;
init_uvars();
} }
environment_cell::environment_cell(std::shared_ptr<environment_cell> const & parent): environment_cell::environment_cell(std::shared_ptr<environment_cell> const & parent):
@ -691,14 +529,18 @@ environment_cell::~environment_cell() {
environment::environment(): environment::environment():
m_ptr(std::make_shared<environment_cell>()) { m_ptr(std::make_shared<environment_cell>()) {
m_ptr->m_this = m_ptr; m_ptr->m_this = m_ptr;
#if 0
m_ptr->m_type_checker.reset(new type_checker(*this)); m_ptr->m_type_checker.reset(new type_checker(*this));
#endif
} }
// used when creating a new child environment // used when creating a new child environment
environment::environment(std::shared_ptr<environment_cell> const & parent, bool): environment::environment(std::shared_ptr<environment_cell> const & parent, bool):
m_ptr(std::make_shared<environment_cell>(parent)) { m_ptr(std::make_shared<environment_cell>(parent)) {
m_ptr->m_this = m_ptr; m_ptr->m_this = m_ptr;
#if 0
m_ptr->m_type_checker.reset(new type_checker(*this)); m_ptr->m_type_checker.reset(new type_checker(*this));
#endif
} }
// used when creating a reference to the parent environment // used when creating a reference to the parent environment
@ -712,7 +554,7 @@ ro_environment::ro_environment(environment const & env):
ro_environment::ro_environment(weak_ref const & r) { ro_environment::ro_environment(weak_ref const & r) {
if (r.expired()) if (r.expired())
throw exception("weak reference to environment object has expired (i.e., the environment has been deleted)"); throw_kernel_exception(*this, "weak reference to environment object has expired (i.e., the environment has been deleted)");
m_ptr = r.lock(); m_ptr = r.lock();
} }
@ -750,26 +592,4 @@ read_write_shared_environment::read_write_shared_environment(environment const &
m_lock(m_env.m_ptr->m_mutex) { m_lock(m_env.m_ptr->m_mutex) {
} }
read_write_shared_environment::~read_write_shared_environment() {} read_write_shared_environment::~read_write_shared_environment() {}
static std::unique_ptr<name_map<std::pair<mk_builtin_fn, bool>>> g_available_builtins;
name_map<std::pair<mk_builtin_fn, bool>> & get_available_builtins() {
if (!g_available_builtins)
g_available_builtins.reset(new name_map<std::pair<mk_builtin_fn, bool>>());
return *g_available_builtins;
}
void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) {
auto & bs = get_available_builtins();
if (bs.find(n) != bs.end())
throw exception("invalid builtin object, system already has a builtin object with the given name"); // LCOV_EXCL_LINE
bs[n] = mk_pair(mk, is_builtin_set);
}
optional<std::pair<expr, bool>> get_builtin(name const & n) {
auto it = get_available_builtins().find(n);
if (it != get_available_builtins().end())
return optional<std::pair<expr, bool>>(it->second.first(), it->second.second);
else
return optional<std::pair<expr, bool>>();
}
} }

103
src/kernel/environment.h
View file

@ -14,7 +14,6 @@ Author: Leonardo de Moura
#include "util/lua.h" #include "util/lua.h"
#include "util/shared_mutex.h" #include "util/shared_mutex.h"
#include "util/name_map.h" #include "util/name_map.h"
#include "kernel/context.h"
#include "kernel/object.h" #include "kernel/object.h"
#include "kernel/level.h" #include "kernel/level.h"
@ -23,8 +22,6 @@ class environment;
class ro_environment; class ro_environment;
class type_checker; class type_checker;
class environment_extension; class environment_extension;
class universe_constraints;
class universes;
/** \brief Implementation of the Lean environment. */ /** \brief Implementation of the Lean environment. */
class environment_cell { class environment_cell {
@ -35,15 +32,14 @@ class environment_cell {
typedef name_map<object> object_dictionary; typedef name_map<object> object_dictionary;
typedef std::tuple<level, level, int> constraint; typedef std::tuple<level, level, int> constraint;
std::weak_ptr<environment_cell> m_this; std::weak_ptr<environment_cell> m_this;
// Universe variable management
std::unique_ptr<universes> m_universes;
// Children environment management // Children environment management
atomic<unsigned> m_num_children; atomic<unsigned> m_num_children;
std::shared_ptr<environment_cell> m_parent; std::shared_ptr<environment_cell> m_parent;
// Object management // Object management
std::vector<object> m_objects; std::vector<object> m_objects;
object_dictionary m_object_dictionary; object_dictionary m_object_dictionary;
std::unique_ptr<type_checker> m_type_checker;
// std::unique_ptr<type_checker> m_type_checker;
std::set<name> m_imported_modules; // set of imported files and builtin modules std::set<name> m_imported_modules; // set of imported files and builtin modules
bool m_trust_imported; // if true, then imported modules are not type checked. bool m_trust_imported; // if true, then imported modules are not type checked.
bool m_type_check; // auxiliary flag used to implement m_trust_imported. bool m_type_check; // auxiliary flag used to implement m_trust_imported.
@ -69,18 +65,9 @@ class environment_cell {
void register_named_object(object const & new_obj); void register_named_object(object const & new_obj);
optional<object> get_object_core(name const & n) const; optional<object> get_object_core(name const & n) const;
universes & get_rw_universes(); void check_no_mlocal(expr const & e);
universes const & get_ro_universes() const;
universe_constraints & get_rw_ucs();
universe_constraints const & get_ro_ucs() const;
level add_uvar_core(name const & n);
bool is_ge(level const & l1, level const & l2, int k) const;
void check_consistency(name const & n, level const & l, int k) const;
void add_constraints(name const & n, level const & l, int k);
void init_uvars();
void check_no_cached_type(expr const & e);
void check_type(name const & n, expr const & t, expr const & v); void check_type(name const & n, expr const & t, expr const & v);
void check_type(expr const & t);
void check_new_definition(name const & n, expr const & t, expr const & v); void check_new_definition(name const & n, expr const & t, expr const & v);
bool mark_imported_core(name n); bool mark_imported_core(name n);
@ -111,60 +98,9 @@ public:
*/ */
environment mk_child() const; environment mk_child() const;
// =======================================
// Universe variables
/**
\brief Add a new universe variable constraint of the form <tt>n >= l</tt>.
Return the level of \c n.
\remark An exception is thrown if a universe inconsistency is detected.
*/
level add_uvar_cnstr(name const & n, level const & l);
level add_uvar_cnstr(name const & n) { return add_uvar_cnstr(n, level()); }
/**
\brief Return true iff the constraint l1 >= l2 is implied by the constraints
in the environment.
*/
bool is_ge(level const & l1, level const & l2) const;
/**
\brief Return the (minimal) distance between two universes.
That is, the biggest \c k s.t. <tt>u1 >= u2 + k</tt>.
Return none if there is no such \c k.
*/
optional<int> get_universe_distance(name const & u1, name const & u2) const;
/**
\brief Return universal variable with the given name.
Throw an exception if variable is not defined in this environment.
*/
level get_uvar(name const & n) const;
// =======================================
// ======================================= // =======================================
// Environment Objects // Environment Objects
/**
\brief Add builtin value to the environment.
\pre is_value(v)
*/
void add_builtin(expr const & v);
/**
\brief Add a builtin value set to the environment.
The set is registered by providing a representative of the set.
Each builtin set of values is implemented by a C++ class.
The environment will only accept object of the same class of
the representative. This functionality is used to support
infinite set of builtin values such as the natural numbers.
\pre is_value(r);
*/
void add_builtin_set(expr const & r);
/** /**
\brief Add a new definition n : t := v. \brief Add a new definition n : t := v.
It throws an exception if v does not have type t. It throws an exception if v does not have type t.
@ -218,22 +154,22 @@ public:
/** /**
\brief Type check the given expression, and return the type of \c e in the given context and this environment. \brief Type check the given expression, and return the type of \c e in the given context and this environment.
*/ */
expr type_check(expr const & e, context const & ctx = context()) const; expr type_check(expr const & e) const;
/** /**
\brief Return the type of \c e in the given context and this environment. \brief Return the type of \c e in the given context and this environment.
*/ */
expr infer_type(expr const & e, context const & ctx = context()) const; expr infer_type(expr const & e) const;
/** /**
\brief Normalize \c e in the given context and this environment. \brief Normalize \c e in the given context and this environment.
*/ */
expr normalize(expr const & e, context const & ctx = context(), bool unfold_opaque = false) const; expr normalize(expr const & e) const;
/** /**
\brief Return true iff \c e is a proposition. \brief Return true iff \c e is a proposition.
*/ */
bool is_proposition(expr const & e, context const & ctx = context()) const; bool is_proposition(expr const & e) const;
/** /**
\brief Low-level function for accessing objects. Consider using iterators. \brief Low-level function for accessing objects. Consider using iterators.
@ -421,34 +357,17 @@ bool is_end_import(object const & obj);
*/ */
optional<std::string> get_imported_module(object const & obj); optional<std::string> get_imported_module(object const & obj);
typedef std::function<expr()> mk_builtin_fn;
/** /**
\brief Register a builtin or builtin-set that is available to be added to \brief Return true iff \c obj is a set_opaque command mark.
a Lean environment.
*/
void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set);
struct register_builtin_fn {
register_builtin_fn(name const & n, mk_builtin_fn mk, bool is_builtin_set = false) {
register_builtin(n, mk, is_builtin_set);
}
};
/**
\brief Return a builtin/builtin-set associated with the name \c n.
Return none if there is no builtin associated the given name.
*/
optional<std::pair<expr, bool>> get_builtin(name const & n);
/**
\brief Return true iff \c obj is a SetOpaque command mark.
*/ */
bool is_set_opaque(object const & obj); bool is_set_opaque(object const & obj);
/** /**
\brief Return the identifier of a SetOpaque command. \brief Return the identifier of a set_opaque command.
\pre is_set_opaque(obj) \pre is_set_opaque(obj)
*/ */
name const & get_set_opaque_id(object const & obj); name const & get_set_opaque_id(object const & obj);
/** /**
\brief Return the flag of a SetOpaque command. \brief Return the flag of a set_opaque command.
\pre is_set_opaque(obj) \pre is_set_opaque(obj)
*/ */
bool get_set_opaque_flag(object const & obj); bool get_set_opaque_flag(object const & obj);

2
src/kernel/formatter.h
View file

@ -56,4 +56,6 @@ std::ostream & operator<<(std::ostream & out, expr const & e);
\brief Create a simple formatter object based on operator<< \brief Create a simple formatter object based on operator<<
*/ */
formatter mk_simple_formatter(); formatter mk_simple_formatter();
typedef std::function<format(formatter const &, options const &)> pp_fn;
} }

60
src/kernel/kernel_exception.cpp
View file

@ -5,21 +5,68 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include <vector> #include <vector>
#include <string>
#include "util/sstream.h"
#include "kernel/kernel_exception.h" #include "kernel/kernel_exception.h"
namespace lean { namespace lean {
format kernel_exception::pp(formatter const &, options const &) const { format kernel_exception::pp(formatter const &, options const &) const { return format(what()); }
return format(what());
class generic_kernel_exception : public kernel_exception {
protected:
optional<expr> m_main_expr;
pp_fn m_pp_fn;
public:
generic_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn):
kernel_exception(env, msg),
m_main_expr(m),
m_pp_fn(fn) {}
virtual ~generic_kernel_exception() noexcept {}
virtual optional<expr> get_main_expr() const { return m_main_expr; }
virtual format pp(formatter const & fmt, options const & opts) const { return m_pp_fn(fmt, opts); }
virtual exception * clone() const { return new generic_kernel_exception(m_env, m_msg.c_str(), m_main_expr, m_pp_fn); }
virtual void rethrow() const { throw *this; }
};
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m) {
std::string msg_str = msg;
throw generic_kernel_exception(env, msg, m, [=](formatter const &, options const &) { return format(msg); });
} }
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm, optional<expr> const & m) {
throw_kernel_exception(env, strm.str().c_str(), m);
}
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, pp_fn const & fn,
optional<expr> const & m) {
throw generic_kernel_exception(env, msg, m, fn);
}
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional<expr> const & m) {
throw generic_kernel_exception(env, "kernel exception", m, fn);
}
[[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n) {
throw_kernel_exception(env, sstream() << "unknown object '" << n << "'");
}
[[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n) {
throw_kernel_exception(env, sstream() << "invalid object declaration, environment already has an object named '" << n << "'");
}
[[ noreturn ]] void throw_read_only_environment(ro_environment const & env) {
throw_kernel_exception(env, "environment cannot be updated because it has children environments");
}
#if 0
format unknown_name_exception::pp(formatter const &, options const &) const { format unknown_name_exception::pp(formatter const &, options const &) const {
return format{format(what()), format(" '"), format(get_name()), format("'")}; return format{format(what()), format(" '"), format(get_name()), format("'")};
} }
format already_declared_exception::pp(formatter const &, options const &) const {
return format{format("invalid object declaration, environment already has an object named '"), format(get_name()), format("'")};
}
format has_no_type_exception::pp(formatter const &, options const &) const { format has_no_type_exception::pp(formatter const &, options const &) const {
return format{format("object '"), format(const_name(m_const)), format("' has no type associated with it")}; return format{format("object '"), format(const_name(m_const)), format("' has no type associated with it")};
} }
@ -107,4 +154,5 @@ format def_type_mismatch_exception::pp(formatter const & fmt, options const & op
r += nest(indent, compose(line(), fmt(ctx, get_value_type(), false, opts))); r += nest(indent, compose(line(), fmt(ctx, get_value_type(), false, opts)));
return r; return r;
} }
#endif
} }

95
src/kernel/kernel_exception.h
View file

@ -34,65 +34,20 @@ public:
virtual void rethrow() const { throw *this; } virtual void rethrow() const { throw *this; }
}; };
/** \brief Base class for unknown universe or object exceptions. */ [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m = none_expr());
class unknown_name_exception : public kernel_exception { [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm,
protected: optional<expr> const & m = none_expr());
name m_name; [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg,
public: pp_fn const & fn, optional<expr> const & m = none_expr());
unknown_name_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {} [[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional<expr> const & m = none_expr());
virtual ~unknown_name_exception() {}
name const & get_name() const { return m_name; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new unknown_name_exception(m_env, m_name); }
virtual void rethrow() const { throw *this; }
};
/** \brief Exception used to report that a universe variable is not known in a given environment. */ [[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n);
class unknown_universe_variable_exception : public unknown_name_exception { [[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n);
public: [[ noreturn ]] void throw_read_only_environment(ro_environment const & env);
unknown_universe_variable_exception(ro_environment const & env, name const & n):unknown_name_exception(env, n) {}
virtual char const * what() const noexcept { return "unknown universe variable"; }
virtual exception * clone() const { return new unknown_universe_variable_exception(m_env, m_name); }
virtual void rethrow() const { throw *this; }
};
/** \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(ro_environment const & env, name const & n):unknown_name_exception(env, n) {}
virtual char const * what() const noexcept { return "unknown object"; }
virtual exception * clone() const { return new unknown_object_exception(m_env, m_name); }
virtual void rethrow() const { throw *this; }
};
/** \brief Base class for already declared object. */
class already_declared_exception : public kernel_exception {
protected:
name m_name;
public:
already_declared_exception(ro_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; }
virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object with the given name"; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new already_declared_exception(m_env, m_name); }
virtual void rethrow() const { throw *this; }
};
/**
\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(ro_environment const & env):kernel_exception(env) {}
virtual char const * what() const noexcept { return "environment cannot be updated because it has children environments"; }
virtual exception * clone() const { return new read_only_environment_exception(m_env); }
virtual void rethrow() const { throw *this; }
};
#if 0
/** \brief Base class for type checking related exceptions. */ /** \brief Base class for type checking related exceptions. */
class type_checker_exception : public kernel_exception { class type_checker_exception : public kernel_exception {
public: public:
@ -266,35 +221,6 @@ public:
virtual void rethrow() const { throw *this; } virtual void rethrow() const { throw *this; }
}; };
/**
\brief Invalid builtin value declaration.
*/
class invalid_builtin_value_declaration : public kernel_exception {
expr m_expr;
public:
invalid_builtin_value_declaration(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_declaration() {}
virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
virtual exception * clone() const { return new invalid_builtin_value_declaration(m_env, m_expr); }
virtual void rethrow() const { throw *this; }
};
/**
\brief Exception used to report that a builtin value is not
declared in the environment.
*/
class invalid_builtin_value_reference : public kernel_exception {
expr m_expr;
public:
invalid_builtin_value_reference(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_reference() {}
virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
virtual exception * clone() const { return new invalid_builtin_value_reference(m_env, m_expr); }
virtual void rethrow() const { throw *this; }
};
/** /**
\brief Unexpected metavariable occurrence \brief Unexpected metavariable occurrence
*/ */
@ -308,4 +234,5 @@ public:
virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); } virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); }
virtual void rethrow() const { throw *this; } virtual void rethrow() const { throw *this; }
}; };
#endif
} }

87
src/kernel/object.cpp
View file

@ -46,86 +46,6 @@ public:
virtual name get_name() const { return m_name; } virtual name get_name() const { return m_name; }
}; };
/**
\brief Universe variable constraint.
*/
class uvar_constraint_object_cell : public named_object_cell {
level m_level;
public:
uvar_constraint_object_cell(name const & n, level const & l):
named_object_cell(object_kind::UVarConstraint, n), m_level(l) {}
virtual ~uvar_constraint_object_cell() {}
virtual bool has_cnstr_level() const { return true; }
virtual level get_cnstr_level() const { return m_level; }
virtual char const * keyword() const { return "universe"; }
virtual void write(serializer & s) const { s << "universe" << get_name() << m_level; }
};
static void read_uvar_cnstr(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d);
level lvl = read_level(d);
env->add_uvar_cnstr(n, lvl);
}
static object_cell::register_deserializer_fn uvar_ds("universe", read_uvar_cnstr);
/**
\brief Builtin object.
*/
class builtin_object_cell : public object_cell {
expr m_value;
bool m_opaque;
public:
builtin_object_cell(expr const & v):
object_cell(object_kind::Builtin), m_value(v), m_opaque(false) { lean_assert(is_value(v)); }
virtual ~builtin_object_cell() {}
virtual bool has_name() const { return true; }
virtual name get_name() const { return to_value(m_value).get_name(); }
virtual bool has_type() const { return true; }
virtual expr get_type() const { return to_value(m_value).get_type(); }
virtual bool is_definition() const { return true; }
virtual bool is_opaque() const { return m_opaque; }
virtual void set_opaque(bool f) { m_opaque = f; }
virtual expr get_value() const { return m_value; }
virtual char const * keyword() const { return "builtin"; }
virtual bool is_builtin() const { return true; }
virtual void write(serializer & s) const { s << "builtin" << m_value; }
};
static void read_builtin(environment const & env, io_state const &, deserializer & d) {
expr v = read_expr(d);
env->add_builtin(v);
}
static object_cell::register_deserializer_fn builtin_ds("builtin", read_builtin);
/**
\brief Base class for capturing a set of builtin objects such as
a) the natural numbers 0, 1, 2, ...
b) the integers 0, -1, 1, -2, 2, ...
c) the reals
d) ...
This object represents an infinite set of declarations.
This is just a markup to sign that an environment depends on a
particular builtin set of values.
*/
class builtin_set_object_cell : public object_cell {
// The representative is only used to test if a builtin value
// is in the same C++ class of the representative.
expr m_representative;
public:
builtin_set_object_cell(expr const & r):object_cell(object_kind::BuiltinSet), m_representative(r) { lean_assert(is_value(r)); }
virtual ~builtin_set_object_cell() {}
virtual bool has_name() const { return true; }
virtual name get_name() const { return to_value(m_representative).get_name(); }
virtual bool is_builtin_set() const { return true; }
virtual bool in_builtin_set(expr const & v) const { return is_value(v) && typeid(to_value(v)) == typeid(to_value(m_representative)); }
virtual char const * keyword() const { return "builtinset"; }
virtual void write(serializer & s) const { s << "builtinset" << m_representative; }
};
static void read_builtin_set(environment const & env, io_state const &, deserializer & d) {
env->add_builtin_set(read_expr(d));
}
static object_cell::register_deserializer_fn builtin_set_ds("builtinset", read_builtin_set);
/** /**
\brief Named (and typed) kernel objects. \brief Named (and typed) kernel objects.
*/ */
@ -233,11 +153,10 @@ static void read_theorem(environment const & env, io_state const &, deserializer
} }
static object_cell::register_deserializer_fn theorem_ds("th", read_theorem); static object_cell::register_deserializer_fn theorem_ds("th", read_theorem);
object mk_uvar_cnstr(name const & n, level const & l) { return object(new uvar_constraint_object_cell(n, l)); } object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) {
object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) { return object(new definition_object_cell(n, t, v, weight)); } return object(new definition_object_cell(n, t, v, weight));
}
object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); } object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); } object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); } object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); }
object mk_builtin(expr const & v) { return object(new builtin_object_cell(v)); }
object mk_builtin_set(expr const & r) { return object(new builtin_set_object_cell(r)); }
} }

23
src/kernel/object.h
View file

@ -18,7 +18,7 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
class io_state; class io_state;
class object; class object;
enum class object_kind { UVarConstraint, Definition, Postulate, Builtin, BuiltinSet, Neutral }; enum class object_kind { Definition, Postulate, Neutral };
class object_cell { class object_cell {
protected: protected:
@ -45,11 +45,6 @@ public:
/** \brief Return object name. \pre has_name() */ /** \brief Return object name. \pre has_name() */
virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE
/** \brief Has constraint level associated with it (for universal variables). */
virtual bool has_cnstr_level() const { return false; }
/** \brief Return the constraint level associated with the object. */
virtual level get_cnstr_level() const { lean_unreachable(); } // LCOV_EXCL_LINE
/** \brief Return true iff object has a type. */ /** \brief Return true iff object has a type. */
virtual bool has_type() const { return false; } virtual bool has_type() const { return false; }
/** \brief Return object type. \pre has_type() */ /** \brief Return object type. \pre has_type() */
@ -63,13 +58,9 @@ public:
virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE
virtual bool is_axiom() const { return false; } virtual bool is_axiom() const { return false; }
virtual bool is_builtin() const { return false; }
virtual bool is_builtin_set() const { return false; }
virtual bool is_theorem() const { return false; } virtual bool is_theorem() const { return false; }
virtual bool is_var_decl() const { return false; } virtual bool is_var_decl() const { return false; }
virtual bool in_builtin_set(expr const &) const { return false; }
virtual unsigned get_weight() const { return 0; } virtual unsigned get_weight() const { return 0; }
virtual void write(serializer & ) const = 0; virtual void write(serializer & ) const = 0;
@ -111,21 +102,16 @@ public:
object_kind kind() const { return m_ptr->kind(); } object_kind kind() const { return m_ptr->kind(); }
friend object mk_uvar_cnstr(name const & n, level const & l);
friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight); friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
friend object mk_theorem(name const & n, expr const & t, expr const & v); friend object mk_theorem(name const & n, expr const & t, expr const & v);
friend object mk_axiom(name const & n, expr const & t); friend object mk_axiom(name const & n, expr const & t);
friend object mk_var_decl(name const & n, expr const & t); friend object mk_var_decl(name const & n, expr const & t);
friend object mk_neutral(neutral_object_cell * c); friend object mk_neutral(neutral_object_cell * c);
friend object mk_builtin(expr const & v);
friend object mk_builtin_set(expr const & r);
char const * keyword() const { return m_ptr->keyword(); } char const * keyword() const { return m_ptr->keyword(); }
bool has_name() const { return m_ptr->has_name(); } bool has_name() const { return m_ptr->has_name(); }
name get_name() const { return m_ptr->get_name(); } name get_name() const { return m_ptr->get_name(); }
bool has_type() const { return m_ptr->has_type(); } bool has_type() const { return m_ptr->has_type(); }
bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); }
level get_cnstr_level() const { return m_ptr->get_cnstr_level(); }
expr get_type() const { return m_ptr->get_type(); } expr get_type() const { return m_ptr->get_type(); }
bool is_definition() const { return m_ptr->is_definition(); } bool is_definition() const { return m_ptr->is_definition(); }
bool is_opaque() const { return m_ptr->is_opaque(); } bool is_opaque() const { return m_ptr->is_opaque(); }
@ -135,12 +121,8 @@ public:
bool is_axiom() const { return m_ptr->is_axiom(); } bool is_axiom() const { return m_ptr->is_axiom(); }
bool is_theorem() const { return m_ptr->is_theorem(); } bool is_theorem() const { return m_ptr->is_theorem(); }
bool is_var_decl() const { return m_ptr->is_var_decl(); } bool is_var_decl() const { return m_ptr->is_var_decl(); }
bool is_builtin() const { return m_ptr->is_builtin(); }
bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }
void write(serializer & s) const { m_ptr->write(s); } void write(serializer & s) const { m_ptr->write(s); }
object_cell const * cell() const { return m_ptr; } object_cell const * cell() const { return m_ptr; }
}; };
@ -148,9 +130,6 @@ inline optional<object> none_object() { return optional<object>(); }
inline optional<object> some_object(object const & o) { return optional<object>(o); } inline optional<object> some_object(object const & o) { return optional<object>(o); }
inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(o)); } inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(o)); }
object mk_uvar_cnstr(name const & n, level const & l);
object mk_builtin(expr const & v);
object mk_builtin_set(expr const & r);
object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight); object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
object mk_theorem(name const & n, expr const & t, expr const & v); object mk_theorem(name const & n, expr const & t, expr const & v);
object mk_axiom(name const & n, expr const & t); object mk_axiom(name const & n, expr const & t);