diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index cb6d35893..b4fd1897d 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,7 +1,7 @@ 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 -definition.cpp replace_visitor.cpp +definition.cpp replace_visitor.cpp environment.cpp justification.cpp pos_info_provider.cpp metavar.cpp constraint.cpp type_checker.cpp error_msgs.cpp ) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 0f8b68f44..9443df1c1 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -1,601 +1,132 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include -#include -#include -#include -#include -#include -#include -#include "util/thread.h" -#include "util/safe_arith.h" -#include "util/realpath.h" -#include "util/sstream.h" -#include "util/lean_path.h" -#include "util/flet.h" -#include "kernel/for_each_fn.h" -#include "kernel/find_fn.h" -#include "kernel/kernel_exception.h" +#include #include "kernel/environment.h" -#include "kernel/threadsafe_environment.h" -// #include "kernel/type_checker.h" -// #include "kernel/normalizer.h" -#include "version.h" +#include "kernel/kernel_exception.h" namespace lean { -class set_opaque_command : public neutral_object_cell { - name m_obj_name; - bool m_opaque; +/** + \brief "Do nothing" normalizer extension. +*/ +class noop_normalizer_extension : public normalizer_extension { public: - set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {} - virtual ~set_opaque_command() {} - virtual char const * keyword() const { return "set_opaque"; } - virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; } - name const & get_obj_name() const { return m_obj_name; } - bool get_flag() const { return m_opaque; } -}; -static void read_set_opaque(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - bool o = d.read_bool(); - env->set_opaque(n, o); -} -static object_cell::register_deserializer_fn set_opaque_ds("Opa", read_set_opaque); - -bool is_set_opaque(object const & obj) { - return dynamic_cast(obj.cell()); -} - -name const & get_set_opaque_id(object const & obj) { - lean_assert(is_set_opaque(obj)); - return static_cast(obj.cell())->get_obj_name(); -} - -bool get_set_opaque_flag(object const & obj) { - lean_assert(is_set_opaque(obj)); - return static_cast(obj.cell())->get_flag(); -} - -class import_command : public neutral_object_cell { - std::string m_mod_name; -public: - import_command(std::string const & n):m_mod_name(n) {} - virtual ~import_command() {} - virtual char const * keyword() const { return "import"; } - virtual void write(serializer & s) const { s << "import" << m_mod_name; } - std::string const & get_module() const { return m_mod_name; } -}; -static void read_import(environment const & env, io_state const & ios, deserializer & d) { - std::string n = d.read_string(); - env->import(n, ios); -} -static object_cell::register_deserializer_fn import_ds("import", read_import); - -class end_import_mark : public neutral_object_cell { -public: - end_import_mark() {} - virtual ~end_import_mark() {} - virtual char const * keyword() const { return "EndImport"; } - virtual void write(serializer &) const {} -}; - -// For Importing builtin modules -class begin_import_mark : public neutral_object_cell { -public: - begin_import_mark() {} - virtual ~begin_import_mark() {} - virtual char const * keyword() const { return "BeginImport"; } - virtual void write(serializer &) const {} -}; - -bool is_begin_import(object const & obj) { - return dynamic_cast(obj.cell()); -} - -optional get_imported_module(object const & obj) { - if (is_begin_import(obj)) { - return optional(static_cast(obj.cell())->get_module()); - } else { - return optional(); + virtual optional> operator()(expr const &, environment const &, type_checker &) const { + return optional>(); } +}; + +environment_header::environment_header(bool proof_irrel, bool eta, std::unique_ptr ext): + m_proof_irrel(proof_irrel), m_eta(eta), m_norm_ext(std::move(ext)) {} + +environment_extension::~environment_extension() {} + +environment::environment(header const & h, definitions const & d, extensions const & exts): + m_header(h), m_definitions(d), m_extensions(exts) {} + +environment::environment(bool proof_irrel, bool eta): + environment(proof_irrel, eta, std::unique_ptr(new noop_normalizer_extension())) +{} + +environment::environment(bool proof_irrel, bool eta, std::unique_ptr ext): + m_header(std::make_shared(proof_irrel, eta, std::move(ext))), + m_extensions(std::make_shared()) +{} + +optional environment::find(name const & n) const { + definition const * r = m_definitions.find(n); + return r ? some_definition(*r) : none_definition(); } -bool is_begin_builtin_import(object const & obj) { - return dynamic_cast(obj.cell()); +definition environment::get(name const & n) const { + definition const * r = m_definitions.find(n); + if (!r) + throw_unknown_declaration(*this, n); + return *r; } -bool is_end_import(object const & obj) { - return dynamic_cast(obj.cell()); +[[ noreturn ]] void throw_incompatible_environment(environment const & env) { + throw_kernel_exception(env, "invalid declaration, it was checked/certified in an incompatible environment"); } -class extension_factory { - std::vector m_makers; - mutex m_makers_mutex; +environment environment::add(certified_definition const & d) const { + if (d.get_header().get() != m_header.get()) + throw_incompatible_environment(*this); + name const & n = d.get_definition().get_name(); + if (find(n)) + throw_already_declared(*this, n); + return environment(m_header, insert(m_definitions, n, d.get_definition()), m_extensions); +} + +environment environment::replace(certified_definition const & t) const { + if (t.get_header().get() != m_header.get()) + throw_incompatible_environment(*this); + name const & n = t.get_definition().get_name(); + auto ax = find(n); + if (!ax) + throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the environment does not have an axiom with the given name"); + if (!ax->is_axiom()) + throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the current declaration in the environment is not an axiom"); + if (!t.get_definition().is_theorem()) + throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the new declaration is not a theorem"); + if (ax->get_type() != t.get_definition().get_type()) + throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same type"); + return environment(m_header, insert(m_definitions, n, t.get_definition()), m_extensions); +} + +class extension_manager { + std::vector> m_exts; + mutex m_mutex; public: - unsigned register_extension(environment_cell::mk_extension mk) { - lock_guard lock(m_makers_mutex); - unsigned r = m_makers.size(); - m_makers.push_back(mk); + unsigned register_extension(std::shared_ptr const & ext) { + lock_guard lock(m_mutex); + unsigned r = m_exts.size(); + m_exts.push_back(ext); return r; } - std::unique_ptr mk(unsigned extid) { - lock_guard lock(m_makers_mutex); - return m_makers[extid](); + bool has_ext(unsigned extid) const { return extid < m_exts.size(); } + + environment_extension const & get_initial(unsigned extid) { + lock_guard lock(m_mutex); + return *(m_exts[extid].get()); } }; -static std::unique_ptr g_extension_factory; -static extension_factory & get_extension_factory() { - if (!g_extension_factory) - g_extension_factory.reset(new extension_factory()); - return *g_extension_factory; +static std::unique_ptr g_extension_manager; + +static extension_manager & get_extension_manager() { + if (!g_extension_manager) + g_extension_manager.reset(new extension_manager()); + return *g_extension_manager; } -unsigned environment_cell::register_extension(mk_extension mk) { - return get_extension_factory().register_extension(mk); +unsigned environment::register_extension(std::shared_ptr const & initial) { + return get_extension_manager().register_extension(initial); } -environment environment_cell::env() const { - lean_assert(!m_this.expired()); // it is not possible to expire since it is a reference to this object - lean_assert(this == m_this.lock().get()); - return environment(m_this.lock()); +[[ noreturn ]] void throw_invalid_extension(environment const & env) { + throw_kernel_exception(env, "invalid environment extension identifier"); } -environment environment_cell::parent() const { - lean_assert(has_parent()); - return environment(m_parent); +environment_extension const & environment::get_extension(unsigned id) const { + if (id >= get_extension_manager().has_ext(id)) + throw_invalid_extension(*this); + if (id < m_extensions->size() || !(*m_extensions)[id]) + return get_extension_manager().get_initial(id); + return *((*m_extensions)[id].get()); } -environment environment_cell::mk_child() const { - return environment(m_this.lock(), true); +environment environment::update(unsigned id, std::shared_ptr const & ext) const { + if (id >= get_extension_manager().has_ext(id)) + throw_invalid_extension(*this); + auto new_exts = std::make_shared(*m_extensions); + if (id >= new_exts->size()) + new_exts->resize(id+1); + (*new_exts)[id] = ext; + return environment(m_header, m_definitions, new_exts); } - -environment_extension & environment_cell::get_extension_core(unsigned extid) { - if (extid >= m_extensions.size()) - m_extensions.resize(extid+1); - if (!m_extensions[extid]) { - std::unique_ptr ext = get_extension_factory().mk(extid); - ext->m_extid = extid; - ext->m_env = this; - m_extensions[extid].swap(ext); - } - return *(m_extensions[extid].get()); -} - -environment_extension const & environment_cell::get_extension_core(unsigned extid) const { - return const_cast(this)->get_extension_core(extid); -} - -unsigned environment_cell::get_max_weight(expr const & e) { - unsigned w = 0; - auto proc = [&](expr const & c, unsigned) { - if (is_constant(c)) { - optional obj = get_object_core(const_name(c)); - if (obj) - w = std::max(w, obj->get_weight()); - } - return true; - }; - for_each_fn visitor(proc); - visitor(e); - return w; -} - -/** \brief Throw exception if environment or its ancestors already have an object with the given name. */ -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(env(), n); -} - -void environment_cell::check_name(name const & n) { - if (has_children()) - throw_read_only_environment(env()); - check_name_core(n); -} - -void environment_cell::check_level_cnstrs(param_names const & ps, level_cnstrs const & ls) { - if (has_meta(ls) > 0) - throw_kernel_exception(env(), "invalid level constraint, it contains level placeholders (aka meta-parameters that must be synthesized by Lean's elaborator"); - if (auto it = get_undef_param(ls, ps)) - throw_kernel_exception(env(), "invalid level constraints, it contains undefined parameters"); -} - -/** \brief Store new named object inside internal data-structures */ -void environment_cell::register_named_object(object const & new_obj) { - m_objects.push_back(new_obj); - m_object_dictionary.insert(std::make_pair(new_obj.get_name(), new_obj)); -} - -/** - \brief Return the object named \c n in the environment or its - ancestors. Return null object if there is no object with the - given name. -*/ -optional environment_cell::get_object_core(name const & n) const { - auto it = m_object_dictionary.find(n); - if (it == m_object_dictionary.end()) { - if (has_parent()) - return m_parent->get_object_core(n); - else - return none_object(); - } else { - return some_object(it->second); - } -} - -object environment_cell::get_object(name const & n) const { - optional obj = get_object_core(n); - if (obj) { - return *obj; - } else { - throw_unknown_object(env(), n); - } -} - -/** - The kernel should *not* accept expressions containing Local or Meta. - Reason: they may introduce unsoundness. -*/ -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 -} - -/** - \brief Throw an exception if \c t is not a type or type of \c - 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 */ -void environment_cell::check_new_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) { - check_name(n); - check_level_cnstrs(ps, cs); - check_type(n, t, v); -} - -/** \brief Add new definition. */ -void environment_cell::add_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) { - check_no_mlocal(t); - check_no_mlocal(v); - check_new_definition(n, ps, cs, t, v); - unsigned w = get_max_weight(v) + 1; - register_named_object(mk_definition(n, ps, cs, t, v, w)); -} - -/** - \brief Add new definition. - The type of the new definition is the type of \c v. -*/ -void environment_cell::add_definition(name const & n, expr const & 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, param_names(), level_cnstrs(), v_t, v, w)); -} - -/** \brief Add new theorem. */ -void environment_cell::add_theorem(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) { - check_no_mlocal(t); - check_no_mlocal(v); - check_new_definition(n, ps, cs, t, v); - register_named_object(mk_theorem(n, ps, cs, t, v)); -} - -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"); - 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, param_names const & ps, level_cnstrs const & cs, expr const & t) { - check_no_mlocal(t); - check_name(n); - check_level_cnstrs(ps, cs); - check_type(t); - register_named_object(mk_axiom(n, ps, cs, t)); -} - -/** \brief Add new variable. */ -void environment_cell::add_var(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) { - check_no_mlocal(t); - check_name(n); - check_level_cnstrs(ps, cs); - check_type(t); - register_named_object(mk_var_decl(n, ps, cs, t)); -} - -void environment_cell::add_neutral_object(neutral_object_cell * o) { - m_objects.push_back(mk_neutral(o)); -} - -unsigned environment_cell::get_num_objects(bool local) const { - if (local || !has_parent()) { - return m_objects.size(); - } else { - return m_objects.size() + m_parent->get_num_objects(false); - } -} - -object const & environment_cell::get_object(unsigned i, bool local) const { - if (local || !has_parent()) { - return m_objects[i]; - } else { - unsigned num_parent_objects = m_parent->get_num_objects(false); - if (i >= num_parent_objects) - return m_objects[i - num_parent_objects]; - else - return m_parent->get_object(i, false); - } -} - -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) const { -#if 0 - return m_type_checker->infer_type(e, ctx); -#else - return e; -#endif -} - -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) const { -#if 0 - return m_type_checker->is_proposition(e, ctx); -#else - return false; -#endif -} - -bool environment_cell::already_imported(name const & n) const { - if (m_imported_modules.find(n) != m_imported_modules.end()) - return true; - else if (has_parent()) - return m_parent->already_imported(n); - else - return false; -} - -bool environment_cell::mark_imported_core(name n) { - if (already_imported(n)) { - return false; - } else if (has_children()) { - throw_read_only_environment(env()); - } else { - m_imported_modules.insert(n); - return true; - } -} - -bool environment_cell::mark_imported(char const * fname) { - return mark_imported_core(name(realpath(fname))); -} - -void environment_cell::auxiliary_section(std::function fn) { - add_neutral_object(new begin_import_mark()); - try { - fn(); - add_neutral_object(new end_import_mark()); - } catch (...) { - add_neutral_object(new end_import_mark()); - throw; - } -} - -void environment_cell::set_trusted_imported(bool flag) { - m_trust_imported = flag; -} - -static char const * g_olean_header = "oleanfile"; -static char const * g_olean_end_file = "EndFile"; -void environment_cell::export_objects(std::string const & fname) { - std::ofstream out(fname, std::ofstream::binary); - serializer s(out); - s << g_olean_header << LEAN_VERSION_MAJOR << LEAN_VERSION_MINOR; - auto it = begin_objects(); - auto end = end_objects(); - unsigned num_imports = 0; - for (; it != end; ++it) { - object const & obj = *it; - if (dynamic_cast(obj.cell())) { - if (num_imports == 0) - obj.write(s); - num_imports++; - } else if (dynamic_cast(obj.cell())) { - lean_assert(num_imports > 0); - num_imports--; - } else if (dynamic_cast(obj.cell())) { - num_imports++; - } else if (num_imports == 0) { - obj.write(s); - } - } - s << g_olean_end_file; -} - -bool environment_cell::load_core(std::string const & fname, io_state const & ios, optional const & mod_name) { - if (!mod_name || mark_imported_core(fname)) { - std::ifstream in(fname, std::ifstream::binary); - if (!in.good()) - throw_kernel_exception(env(), sstream() << "failed to open file '" << fname << "'"); - deserializer d(in); - std::string header; - d >> header; - if (header != g_olean_header) - 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; - try { - if (mod_name) - add_neutral_object(new import_command(*mod_name)); - while (true) { - std::string k; - d >> k; - if (k == g_olean_end_file) { - if (mod_name) - add_neutral_object(new end_import_mark()); - return true; - } - read_object(env(), ios, k, d); - } - } catch (...) { - if (mod_name) - add_neutral_object(new end_import_mark()); - throw; - } - } else { - return false; - } -} - -bool environment_cell::import(std::string const & fname, io_state const & ios) { - flet set(m_type_check, !m_trust_imported); - return load_core(realpath(find_file(fname, {".olean"}).c_str()), ios, optional(fname)); -} - -void environment_cell::load(std::string const & fname, io_state const & ios) { - load_core(fname, ios, optional()); -} - -bool environment_cell::imported(std::string const & n) const { - try { - return already_imported(name(realpath(find_file(n, {".olean"}).c_str()))); - } catch (...) { - // module named n does not even exist - return false; - } -} - -environment_cell::environment_cell(): - m_num_children(0) { - m_trust_imported = false; - m_type_check = true; -} - -environment_cell::environment_cell(std::shared_ptr const & parent): - m_num_children(0), - m_parent(parent) { - m_trust_imported = false; - m_type_check = true; - parent->inc_children(); -} - -environment_cell::~environment_cell() { - if (m_parent) - m_parent->dec_children(); -} - -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 -environment::environment(std::shared_ptr const & ptr): - m_ptr(ptr) { -} - -ro_environment::ro_environment(environment const & env): - m_ptr(env.m_ptr) { -} - -ro_environment::ro_environment(weak_ref const & r) { - if (r.expired()) - throw_kernel_exception(*this, "weak reference to environment object has expired (i.e., the environment has been deleted)"); - m_ptr = r.lock(); -} - -environment_extension::environment_extension(): - m_env(nullptr), - m_extid(0) { -} - -environment_extension::~environment_extension() { -} - -environment_extension const * environment_extension::get_parent_core() const { - if (m_env == nullptr) - return nullptr; - environment_cell * parent = m_env->m_parent.get(); - while (parent) { - if (m_extid < parent->m_extensions.size()) { - environment_extension * ext = parent->m_extensions[m_extid].get(); - if (ext) - return ext; - } - parent = parent->m_parent.get(); - } - return nullptr; -} - -read_only_shared_environment::read_only_shared_environment(ro_environment const & env): - m_env(env), - m_lock(const_cast(m_env.m_ptr.get())->m_mutex) { -} -read_only_shared_environment::~read_only_shared_environment() {} - -read_write_shared_environment::read_write_shared_environment(environment const & env): - m_env(env), - m_lock(m_env.m_ptr->m_mutex) { -} -read_write_shared_environment::~read_write_shared_environment() {} } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 9fb83c5b0..516a2601b 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -1,379 +1,147 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include -#include -#include -#include -#include #include -#include "util/lua.h" -#include "util/shared_mutex.h" -#include "util/name_map.h" -#include "kernel/object.h" -#include "kernel/level.h" +#include +#include "util/rc.h" +#include "util/optional.h" +#include "util/rb_map.h" +#include "kernel/expr.h" +#include "kernel/constraint.h" +#include "kernel/definition.h" namespace lean { -class environment; -class ro_environment; class type_checker; -class environment_extension; +class environment; +class certified_definition; -/** \brief Implementation of the Lean environment. */ -class environment_cell { - friend class environment; - friend class read_write_shared_environment; - friend class read_only_shared_environment; - // Remark: only named objects are stored in the dictionary. - typedef name_map object_dictionary; - typedef std::tuple constraint; - std::weak_ptr m_this; - // Children environment management - atomic m_num_children; - std::shared_ptr m_parent; - // Object management - std::vector m_objects; - object_dictionary m_object_dictionary; +/** + \brief The Lean kernel can be instantiated with different normalization extensions. + Each extension is part of the trusted code base. The extensions allow us to support + different flavors of the core type theory. We will use these extensions to implement + inductive datatype (ala Coq), HIT, record types, etc. +*/ +class normalizer_extension { +public: + virtual optional> operator()(expr const & t, environment const & env, type_checker & tc) const; +}; - // 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. - std::vector> m_extensions; - friend class environment_extension; +/** + \brief The header of an environment is created when we create the empty environment. + Moreover if environment B is an extension of environment A, then A and B share the same header. +*/ +class environment_header { + bool m_proof_irrel; //!< true if the kernel assumes proof irrelevance + bool m_eta; //!< true if the kernel uses eta-reduction in convertability checks + std::unique_ptr m_norm_ext; + void dealloc(); +public: + environment_header(bool proof_irrel, bool eta, std::unique_ptr ext); + bool proof_irrel() const { return m_proof_irrel; } + bool eta() const { return m_eta; } + normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); } +}; - // This mutex is only used to implement threadsafe environment objects - // in the external APIs - shared_mutex m_mutex; +class environment_extension { +public: + virtual ~environment_extension(); +}; - environment env() const; +typedef std::vector> environment_extensions; - void inc_children() { m_num_children++; } - void dec_children() { m_num_children--; } +/** + \brief Lean core environment. An environment object can be extended/customized in different ways: - environment_extension & get_extension_core(unsigned extid); - environment_extension const & get_extension_core(unsigned extid) const; + 1- By providing a normalizer_extension when creating an empty environment. + 2- By setting the proof_irrel and eta flags when creating an empty environment. + 3- By attaching additional data as environment::extensions. The additional data can be added + at any time. They contain information used by the automation (e.g., rewriting sets, unification hints, etc). +*/ +class environment { + typedef std::shared_ptr header; + typedef rb_map definitions; + typedef std::shared_ptr extensions; - unsigned get_max_weight(expr const & e); - void check_name_core(name const & n); - void check_name(name const & n); + header m_header; + definitions m_definitions; + extensions m_extensions; - void check_level_cnstrs(param_names const & ps, level_cnstrs const & ls); - - void register_named_object(object const & new_obj); - optional get_object_core(name const & n) const; - - 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, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v); - - bool mark_imported_core(name n); - bool load_core(std::string const & fname, io_state const & ios, optional const & mod_name); - bool already_imported(name const & n) const; - /** \brief Return true iff the given file was not already marked as imported. It will also mark the file as imported. */ - bool mark_imported(char const * fname); + environment(header const & h, definitions const & d, extensions const & ext); public: - environment_cell(); - environment_cell(std::shared_ptr const & parent); - ~environment_cell(); + environment(bool proof_irrel = true, bool eta = true); + environment(bool proof_irrel, bool eta, std::unique_ptr ext); + ~environment(); - /** \brief Return true iff this environment has children environments. */ - bool has_children() const { return m_num_children > 0; } - /** \brief Return true iff this environment has a parent environment */ - bool has_parent() const { return m_parent != nullptr; } + std::shared_ptr get_header() const { return m_header; } + + /** \brief Return true iff the environment assumes proof irrelevance */ + bool proof_irrel() const { return m_header->proof_irrel(); } + + /** \brief Return true iff the environment assumes Eta-reduction */ + bool eta() const { return m_header->eta(); } + + /** \brief Return reference to the normalizer extension associatied with this environment. */ + normalizer_extension const & norm_ext() const { return m_header->norm_ext(); } + + /** \brief Return definition with name \c n (if it is defined in this environment). */ + optional find(name const & n) const; + + /** \brief Return definition with name \c n. Throws and exception if definition does not exist in this environment. */ + definition get(name const & n) const; /** - \brief Return parent environment of this environment. - \pre has_parent() + \brief Extends the current environment with the given (certified) definition + This method throws an exception if: + - The definition was certified in an environment which is not an ancestor of this one. + - The environment already contains a definition with the given name. */ - environment parent() const; + environment add(certified_definition const & d) const; /** - \brief Create a child environment. This environment will only allow "read-only" operations until - all children environments are deleted. + \brief Replace the axiom with name t.get_definition().get_name() with the theorem t.get_definition(). + This method throws an exception if: + - The theorem was certified in an environment which is not an ancestor of this one. + - The environment does not contain an axiom named t.get_definition().get_name() */ - environment mk_child() const; - - // ======================================= - // Environment Objects - - /** - \brief Add a new definition n : t := v. - It throws an exception if v does not have type t. - It throws an exception if there is already an object with the given name. - */ - void add_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v); - void add_theorem(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v); - void add_definition(name const & n, expr const & t, expr const & v) { add_definition(n, param_names(), level_cnstrs(), t, v); } - void add_theorem(name const & n, expr const & t, expr const & v) { add_theorem(n, param_names(), level_cnstrs(), t, v); } - - /** - \brief Add a new definition n : infer_type(v) := v. - It throws an exception if there is already an object with the given name. - */ - void add_definition(name const & n, expr const & v); - - /** - \brief Set the given definition as opaque (or not) - - \remark It throws an error if \c n is not a definition. - */ - void set_opaque(name const & n, bool opaque); - - /** - \brief Add a new fact (Axiom or Fact) to the environment. - It throws an exception if there is already an object with the given name. - */ - void add_axiom(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t); - void add_var(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t); - void add_axiom(name const & n, expr const & t) { add_axiom(n, param_names(), level_cnstrs(), t); } - void add_var(name const & n, expr const & t) { add_var(n, param_names(), level_cnstrs(), t); }; - - /** - \brief Register the given unanymous object in this environment. - The environment assume the object ownership. - */ - void add_neutral_object(neutral_object_cell * o); - - /** - \brief Return the object with the given name. - It throws an exception if the environment does not have an object with the given name. - */ - object get_object(name const & n) const; - - /** - \brief Find a given object in the environment. Return the null - object if there is no object with the given name. - */ - optional find_object(name const & n) const { return get_object_core(n); } - - /** \brief Return true iff the environment has an object with the given name */ - bool has_object(name const & n) const { return static_cast(find_object(n)); } - - /** - \brief Type check the given expression, and return the type of \c e in this environment. - */ - expr type_check(expr const & e) const; - - /** - \brief Return the type of \c e in this environment. - */ - expr infer_type(expr const & e) const; - - /** - \brief Normalize \c e in this environment. - */ - expr normalize(expr const & e) const; - - /** - \brief Return true iff \c e is a proposition. - */ - bool is_proposition(expr const & e) const; - - /** - \brief Low-level function for accessing objects. Consider using iterators. - */ - unsigned get_num_objects(bool local) const; - /** - \brief Low-level function for accessing objects. Consider using iterators. - */ - object const & get_object(unsigned i, bool local) const; - - /** \brief Iterator for Lean environment objects. */ - class object_iterator { - std::shared_ptr m_env; - unsigned m_idx; - bool m_local; - friend class environment_cell; - object_iterator(std::shared_ptr && env, unsigned idx, bool local):m_env(env), m_idx(idx), m_local(local) {} - public: - object_iterator(object_iterator const & s):m_env(s.m_env), m_idx(s.m_idx), m_local(s.m_local) {} - object_iterator & operator++() { ++m_idx; return *this; } - object_iterator operator++(int) { object_iterator tmp(*this); operator++(); return tmp; } - object_iterator & operator--() { --m_idx; return *this; } - object_iterator operator--(int) { object_iterator tmp(*this); operator--(); return tmp; } - bool operator==(object_iterator const & s) const { lean_assert(m_env.get() == s.m_env.get()); return m_idx == s.m_idx; } - bool operator!=(object_iterator const & s) const { return !operator==(s); } - object const & operator*() { return m_env->get_object(m_idx, m_local); } - object const * operator->() { return &(m_env->get_object(m_idx, m_local)); } - }; - - /** - \brief Return an iterator to the beginning of the sequence of - objects stored in this environment. - - \remark The objects in this environment and ancestor - environments are considered - */ - object_iterator begin_objects() const { return object_iterator(m_this.lock(), 0, false); } - - /** - \brief Return an iterator to the end of the sequence of - objects stored in this environment. - - \remark The objects in this environment and ancestor - environments are considered - */ - object_iterator end_objects() const { return object_iterator(m_this.lock(), get_num_objects(false), false); } - - /** - \brief Return an iterator to the beginning of the sequence of - objects stored in this environment (objects in ancestor - environments are ingored). - */ - object_iterator begin_local_objects() const { return object_iterator(m_this.lock(), 0, true); } - - /** - \brief Return an iterator to the end of the sequence of - objects stored in this environment (objects in ancestor - environments are ingored). - */ - object_iterator end_local_objects() const { return object_iterator(m_this.lock(), get_num_objects(true), true); } - // ======================================= + environment replace(certified_definition const & t) const; /** \brief Register an environment extension. Every environment - object will contain this extension. The funciton mk creates a - new instance of the extension. The extension object can be - retrieved using the token (unsigned integer) returned by this - method. + object may contain this extension. The argument \c initial is + the initial value for the new extensions. The extension object + can be retrieved using the given token (unsigned integer) returned + by this method. \remark The extension objects are created on demand. \see get_extension */ - typedef std::unique_ptr (*mk_extension)(); - static unsigned register_extension(mk_extension mk); + static unsigned register_extension(std::shared_ptr const & initial); - /** - \brief Retrieve the extension associated with the token \c extid. - The token is the value returned by \c register_extension. - */ - template - Ext const & get_extension(unsigned extid) const { - environment_extension const & ext = get_extension_core(extid); - lean_assert(dynamic_cast(&ext) != nullptr); - return static_cast(ext); - } + /** \brief Return the extension with the given id. */ + environment_extension const & get_extension(unsigned extid) const; - template - Ext & get_extension(unsigned extid) { - environment_extension & ext = get_extension_core(extid); - lean_assert(dynamic_cast(&ext) != nullptr); - return static_cast(ext); - } - - void export_objects(std::string const & fname); - bool import(std::string const & fname, io_state const & ios); - void load(std::string const & fname, io_state const & ios); - /** \brief Return true iff module \c n has already been imported */ - bool imported(std::string const & n) const; - - /** - \brief When trusted_imported flag is true, the environment will - not type check imported modules. - */ - void set_trusted_imported(bool flag); - - /** - \brief Execute function \c fn. Any object created by \c fn - is not exported by the environment. - */ - void auxiliary_section(std::function fn); + /** \brief Update the environment extension with the given id. */ + environment update(unsigned extid, std::shared_ptr const & ext) const; }; /** - \brief Frontend can store data in environment extensions. - Each extension is associated with a unique token/id. - This token allows the frontend to retrieve/store an extension object - in the environment + \brief A certified definition is one that has been type checked. + Only the type_checker class can create certified definitions. */ -class environment_extension { - friend class environment_cell; - environment_cell * m_env; - unsigned m_extid; // extension id - environment_extension const * get_parent_core() const; +class certified_definition { + friend class type_checker; + std::shared_ptr m_header; + definition m_definition; + certified_definition(std::shared_ptr const & h, definition const & d); public: - environment_extension(); - virtual ~environment_extension(); - /** - \brief Return a constant reference for a parent extension, - and a nullptr if there is no parent/ancestor, or if the - parent/ancestor has an extension. - */ - template Ext const * get_parent() const { - environment_extension const * ext = get_parent_core(); - lean_assert(!ext || dynamic_cast(ext) != nullptr); - return static_cast(ext); - } + certified_definition(certified_definition const & c); + std::shared_ptr const & get_header() const { return m_header; } + definition const & get_definition() const { return m_definition; } }; - -/** - \brief Reference to environment -*/ -class environment { - friend class ro_environment; - friend class environment_cell; - friend class read_write_shared_environment; - std::shared_ptr m_ptr; - environment(std::shared_ptr const & parent, bool); - environment(std::shared_ptr const & ptr); -public: - environment(); - environment_cell * operator->() const { return m_ptr.get(); } - environment_cell & operator*() const { return *(m_ptr.get()); } -}; - -/** - \brief Read-only reference to environment. -*/ -class ro_environment { - friend class environment_cell; - friend class read_only_shared_environment; - std::shared_ptr m_ptr; - ro_environment(std::shared_ptr const & p):m_ptr(p) {} - friend int push_environment(lua_State * L, ro_environment const & env); - environment cast_to_environment() const { return environment(std::const_pointer_cast(m_ptr)); } -public: - typedef std::weak_ptr weak_ref; - ro_environment(environment const & env); - ro_environment(weak_ref const & env); - explicit operator weak_ref() const { return weak_ref(m_ptr); } - weak_ref to_weak_ref() const { return weak_ref(m_ptr); } - environment_cell const * operator->() const { return m_ptr.get(); } - environment_cell const & operator*() const { return *(m_ptr.get()); } -}; - -/** \brief Return true iff the given object marks the begin of the of a sequence of imported objects. */ -bool is_begin_import(object const & obj); -/** \brief Return true iff the given object marks the begin of the of a sequence of builtin imported objects. */ -bool is_begin_builtin_import(object const & obj); -/** \brief Return true iff the given object marks the end of the of a sequence of imported objects. */ -bool is_end_import(object const & obj); -/** - \brief Return the module imported by the given import object. - Return none if \c obj is not an import object. -*/ -optional get_imported_module(object const & obj); - -/** - \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 set_opaque command. - \pre is_set_opaque(obj) -*/ -name const & get_set_opaque_id(object const & obj); -/** - \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/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index 502c58547..96bbe8ba5 100644 --- a/src/kernel/kernel_exception.cpp +++ b/src/kernel/kernel_exception.cpp @@ -17,7 +17,7 @@ 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): + generic_kernel_exception(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) {} @@ -28,40 +28,36 @@ public: virtual void rethrow() const { throw *this; } }; -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional const & m) { +[[ noreturn ]] void throw_kernel_exception(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) { +[[ noreturn ]] void throw_kernel_exception(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, optional const & m, pp_fn const & fn) { +[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m, pp_fn const & fn) { throw generic_kernel_exception(env, msg, m, fn); } -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional const & m, pp_fn const & fn) { +[[ noreturn ]] void throw_kernel_exception(environment const & env, optional const & m, pp_fn const & fn) { throw generic_kernel_exception(env, "kernel exception", m, fn); } -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, expr const & m, pp_fn const & fn) { +[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn) { throw_kernel_exception(env, msg, some_expr(m), fn); } -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, expr const & m, pp_fn const & fn) { +[[ noreturn ]] void throw_kernel_exception(environment const & env, expr const & m, pp_fn const & fn) { throw_kernel_exception(env, some_expr(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_unknown_declaration(environment const & env, name const & n) { + throw_kernel_exception(env, sstream() << "unknown declaration '" << n << "'"); } -[[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n) { +[[ noreturn ]] void throw_already_declared(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"); -} } diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index e594f31d9..961504390 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -17,13 +17,13 @@ class environment; /** \brief Base class for all kernel exceptions. */ class kernel_exception : public exception { protected: - ro_environment m_env; + environment m_env; public: - kernel_exception(ro_environment const & env):m_env(env) {} - kernel_exception(ro_environment const & env, char const * msg):exception(msg), m_env(env) {} - kernel_exception(ro_environment const & env, sstream const & strm):exception(strm), m_env(env) {} + kernel_exception(environment const & env):m_env(env) {} + kernel_exception(environment const & env, char const * msg):exception(msg), m_env(env) {} + kernel_exception(environment const & env, sstream const & strm):exception(strm), m_env(env) {} virtual ~kernel_exception() noexcept {} - ro_environment const & get_environment() const { return m_env; } + environment const & get_environment() const { return m_env; } /** \brief Return a reference (if available) to the main expression associated with this exception. This information is used to provide better error messages. @@ -34,14 +34,13 @@ public: 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, +[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m = none_expr()); +[[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, optional const & m = none_expr()); -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional const & m, pp_fn const & fn); -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional const & m, pp_fn const & fn); -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, expr const & m, pp_fn const & fn); -[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, expr const & m, pp_fn const & fn); -[[ 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); +[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m, pp_fn const & fn); +[[ noreturn ]] void throw_kernel_exception(environment const & env, optional const & m, pp_fn const & fn); +[[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn); +[[ noreturn ]] void throw_kernel_exception(environment const & env, expr const & m, pp_fn const & fn); +[[ noreturn ]] void throw_unknown_declaration(environment const & env, name const & n); +[[ noreturn ]] void throw_already_declared(environment const & env, name const & n); }