From b5f0f280091cade538027e217280c26a93bbfb22 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Feb 2014 22:55:00 -0800 Subject: [PATCH] refactor(kernel): environment, kernel object and exceptions Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 7 +- src/kernel/environment.cpp | 300 +++++++------------------------- src/kernel/environment.h | 103 ++--------- src/kernel/formatter.h | 2 + src/kernel/kernel_exception.cpp | 60 ++++++- src/kernel/kernel_exception.h | 95 ++-------- src/kernel/object.cpp | 87 +-------- src/kernel/object.h | 23 +-- 8 files changed, 146 insertions(+), 531 deletions(-) diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 4f8ef15aa..24367962c 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,9 +1,10 @@ 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 -instantiate.cpp context.cpp formatter.cpp max_sharing.cpp -# normalizer.cpp object.cpp environment.cpp +instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp +object.cpp environment.cpp +# normalizer.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 # replace_visitor.cpp update_expr.cpp io_state.cpp # universe_constraints.cpp diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 465f2ed43..2b3f006cd 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -22,10 +22,8 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/environment.h" #include "kernel/threadsafe_environment.h" -#include "kernel/type_checker.h" -#include "kernel/normalizer.h" -#include "kernel/universe_constraints.h" -#include "kernel/kernel.h" +// #include "kernel/type_checker.h" +// #include "kernel/normalizer.h" #include "version.h" namespace lean { @@ -182,7 +180,7 @@ unsigned environment_cell::get_max_weight(expr const & e) { } return true; }; - for_each_fn visitor(proc); + for_each_fn visitor(proc); visitor(e); return w; } @@ -192,12 +190,12 @@ void environment_cell::check_name_core(name const & n) { if (has_parent()) m_parent->check_name_core(n); 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) { if (has_children()) - throw read_only_environment_exception(env()); + throw_read_only_environment(env()); check_name_core(n); } @@ -229,177 +227,17 @@ object environment_cell::get_object(name const & n) const { if (obj) { return *obj; } else { - throw unknown_object_exception(env(), n); + throw_unknown_object(env(), n); } } -class universes { -public: - std::vector 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 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 - - A basic constraint is a constraint of the form u >= v + k - where u and v are universe variables. + The kernel should *not* accept expressions containing Local or Meta. + Reason: they may introduce unsoundness. */ -void environment_cell::add_constraints(name const & n, level const & l, int k) { - switch (kind(l)) { - case level_kind::UVar: get_rw_ucs().add_constraint(n, uvar_name(l), k); return; - 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 +void environment_cell::check_no_mlocal(expr const & e) { + if (find(e, [](expr const & a, unsigned) { return is_mlocal(a); })) + 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 } /** @@ -407,12 +245,21 @@ void environment_cell::check_no_cached_type(expr const & e) { v is not convertible to \c t. */ void environment_cell::check_type(name const & n, expr const & t, expr const & v) { +#if 0 if (m_type_check) { m_type_checker->check_type(t); expr v_t = m_type_checker->check(v); if (!m_type_checker->is_convertible(v_t, 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 */ @@ -421,34 +268,10 @@ void environment_cell::check_new_definition(name const & n, expr const & t, expr 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. */ void environment_cell::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - check_no_cached_type(t); - check_no_cached_type(v); + check_no_mlocal(t); + check_no_mlocal(v); check_new_definition(n, t, v); unsigned w = get_max_weight(v) + 1; 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. */ 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); expr v_t; +#if 0 if (m_type_check) v_t = m_type_checker->check(v); else v_t = m_type_checker->infer_type(v); +#endif unsigned w = get_max_weight(v) + 1; register_named_object(mk_definition(n, v_t, v, w)); if (opaque) @@ -476,8 +301,8 @@ void environment_cell::add_definition(name const & n, expr const & v, bool opaqu /** \brief Add new theorem. */ void environment_cell::add_theorem(name const & n, expr const & t, expr const & v) { - check_no_cached_type(t); - check_no_cached_type(v); + check_no_mlocal(t); + check_no_mlocal(v); check_new_definition(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) { auto obj = find_object(n); 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); add_neutral_object(new set_opaque_command(n, opaque)); } /** \brief Add new axiom. */ void environment_cell::add_axiom(name const & n, expr const & t) { - check_no_cached_type(t); + check_no_mlocal(t); check_name(n); - if (m_type_check) - m_type_checker->check_type(t); + check_type(t); register_named_object(mk_axiom(n, t)); } /** \brief Add new variable. */ void environment_cell::add_var(name const & n, expr const & t) { - check_no_cached_type(t); + check_no_mlocal(t); check_name(n); - if (m_type_check) - m_type_checker->check_type(t); + check_type(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); +#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); +#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); +#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); +#else + return false; +#endif } 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)) { return false; } else if (has_children()) { - throw read_only_environment_exception(env()); + throw_read_only_environment(env()); } else { m_imported_modules.insert(n); 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)) { std::ifstream in(fname, std::ifstream::binary); if (!in.good()) - throw exception(sstream() << "failed to open file '" << fname << "'"); + throw_kernel_exception(env(), sstream() << "failed to open file '" << fname << "'"); deserializer d(in); std::string header; d >> 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; // Perhaps we should enforce the right version number d >> major >> minor; @@ -672,7 +511,6 @@ environment_cell::environment_cell(): m_num_children(0) { m_trust_imported = false; m_type_check = true; - init_uvars(); } environment_cell::environment_cell(std::shared_ptr const & parent): @@ -691,14 +529,18 @@ environment_cell::~environment_cell() { environment::environment(): m_ptr(std::make_shared()) { m_ptr->m_this = m_ptr; +#if 0 m_ptr->m_type_checker.reset(new type_checker(*this)); +#endif } // used when creating a new child environment environment::environment(std::shared_ptr const & parent, bool): m_ptr(std::make_shared(parent)) { m_ptr->m_this = m_ptr; +#if 0 m_ptr->m_type_checker.reset(new type_checker(*this)); +#endif } // 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) { 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(); } @@ -750,26 +592,4 @@ read_write_shared_environment::read_write_shared_environment(environment const & m_lock(m_env.m_ptr->m_mutex) { } read_write_shared_environment::~read_write_shared_environment() {} - -static std::unique_ptr>> g_available_builtins; -name_map> & get_available_builtins() { - if (!g_available_builtins) - g_available_builtins.reset(new name_map>()); - 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> get_builtin(name const & n) { - auto it = get_available_builtins().find(n); - if (it != get_available_builtins().end()) - return optional>(it->second.first(), it->second.second); - else - return optional>(); -} } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 4dad4418b..9cf1e8e36 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "util/lua.h" #include "util/shared_mutex.h" #include "util/name_map.h" -#include "kernel/context.h" #include "kernel/object.h" #include "kernel/level.h" @@ -23,8 +22,6 @@ class environment; class ro_environment; class type_checker; class environment_extension; -class universe_constraints; -class universes; /** \brief Implementation of the Lean environment. */ class environment_cell { @@ -35,15 +32,14 @@ class environment_cell { typedef name_map object_dictionary; typedef std::tuple constraint; std::weak_ptr m_this; - // Universe variable management - std::unique_ptr m_universes; // Children environment management atomic m_num_children; std::shared_ptr m_parent; // Object management std::vector m_objects; object_dictionary m_object_dictionary; - std::unique_ptr m_type_checker; + + // std::unique_ptr m_type_checker; std::set 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_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); optional get_object_core(name const & n) const; - universes & get_rw_universes(); - 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_no_mlocal(expr const & e); 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); bool mark_imported_core(name n); @@ -111,60 +98,9 @@ public: */ environment mk_child() const; - // ======================================= - // Universe variables - /** - \brief Add a new universe variable constraint of the form n >= l. - 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. u1 >= u2 + k. - Return none if there is no such \c k. - */ - optional 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 - /** - \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. 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. */ - 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. */ - 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. */ - 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. */ - 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. @@ -421,34 +357,17 @@ bool is_end_import(object const & obj); */ optional get_imported_module(object const & obj); -typedef std::function mk_builtin_fn; /** - \brief Register a builtin or builtin-set that is available to be added to - 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> get_builtin(name const & n); - -/** - \brief Return true iff \c obj is a SetOpaque command mark. + \brief Return true iff \c obj is a set_opaque command mark. */ 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) */ 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) */ bool get_set_opaque_flag(object const & obj); diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index af6be062a..44c9f7358 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -56,4 +56,6 @@ std::ostream & operator<<(std::ostream & out, expr const & e); \brief Create a simple formatter object based on operator<< */ formatter mk_simple_formatter(); + +typedef std::function pp_fn; } diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index 3a31ac54c..08d5b50ae 100644 --- a/src/kernel/kernel_exception.cpp +++ b/src/kernel/kernel_exception.cpp @@ -5,21 +5,68 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include +#include "util/sstream.h" #include "kernel/kernel_exception.h" namespace lean { -format kernel_exception::pp(formatter const &, options const &) const { - return format(what()); +format kernel_exception::pp(formatter const &, options const &) const { return format(what()); } + +class generic_kernel_exception : public kernel_exception { +protected: + optional m_main_expr; + pp_fn m_pp_fn; +public: + generic_kernel_exception(ro_environment const & env, char const * msg, optional 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 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 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 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 const & m) { + throw generic_kernel_exception(env, msg, m, fn); +} + +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional 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 { 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 { 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))); return r; } +#endif } diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 23507b85d..fe487c41c 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -34,65 +34,20 @@ public: virtual void rethrow() const { throw *this; } }; -/** \brief Base class for unknown universe or object exceptions. */ -class unknown_name_exception : public kernel_exception { -protected: - name m_name; -public: - unknown_name_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {} - 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; } -}; +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional const & m = none_expr()); +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm, + optional const & m = none_expr()); +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, + pp_fn const & fn, optional const & m = none_expr()); +[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional const & m = none_expr()); -/** \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(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; } -}; +[[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n); +[[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n); +[[ noreturn ]] void throw_read_only_environment(ro_environment const & env); -/** \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. */ class type_checker_exception : public kernel_exception { public: @@ -266,35 +221,6 @@ public: 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 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 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 */ @@ -308,4 +234,5 @@ public: virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); } virtual void rethrow() const { throw *this; } }; +#endif } diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 9987b7788..e0f04c407 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -46,86 +46,6 @@ public: 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. */ @@ -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); -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) { return object(new definition_object_cell(n, t, v, 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)); +} 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_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)); } } diff --git a/src/kernel/object.h b/src/kernel/object.h index c33c8fca6..a907ded39 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -18,7 +18,7 @@ Author: Leonardo de Moura namespace lean { class io_state; class object; -enum class object_kind { UVarConstraint, Definition, Postulate, Builtin, BuiltinSet, Neutral }; +enum class object_kind { Definition, Postulate, Neutral }; class object_cell { protected: @@ -45,11 +45,6 @@ public: /** \brief Return object name. \pre has_name() */ 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. */ virtual bool has_type() const { return false; } /** \brief Return object type. \pre has_type() */ @@ -63,13 +58,9 @@ public: virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE 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_var_decl() const { return false; } - virtual bool in_builtin_set(expr const &) const { return false; } - virtual unsigned get_weight() const { return 0; } virtual void write(serializer & ) const = 0; @@ -111,21 +102,16 @@ public: 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_theorem(name const & n, expr const & t, expr const & v); friend object mk_axiom(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_builtin(expr const & v); - friend object mk_builtin_set(expr const & r); char const * keyword() const { return m_ptr->keyword(); } bool has_name() const { return m_ptr->has_name(); } name get_name() const { return m_ptr->get_name(); } 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(); } bool is_definition() const { return m_ptr->is_definition(); } 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_theorem() const { return m_ptr->is_theorem(); } 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); } - object_cell const * cell() const { return m_ptr; } }; @@ -148,9 +130,6 @@ inline optional none_object() { return optional(); } inline optional some_object(object const & o) { return optional(o); } inline optional some_object(object && o) { return optional(std::forward(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_theorem(name const & n, expr const & t, expr const & v); object mk_axiom(name const & n, expr const & t);