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

refactor(kernel/environment): simplified (functional) environment object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-18 14:21:49 -07:00
parent 234abb1238
commit 582352d647
5 changed files with 226 additions and 932 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -1,7 +1,7 @@
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
definition.cpp replace_visitor.cpp definition.cpp replace_visitor.cpp environment.cpp
justification.cpp pos_info_provider.cpp metavar.cpp justification.cpp pos_info_provider.cpp metavar.cpp
constraint.cpp type_checker.cpp error_msgs.cpp constraint.cpp type_checker.cpp error_msgs.cpp
) )

667
src/kernel/environment.cpp
View file

@ -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. Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include <cstdlib> #include <limits>
#include <algorithm>
#include <vector>
#include <tuple>
#include <fstream>
#include <string>
#include <utility>
#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 "kernel/environment.h" #include "kernel/environment.h"
#include "kernel/threadsafe_environment.h" #include "kernel/kernel_exception.h"
// #include "kernel/type_checker.h"
// #include "kernel/normalizer.h"
#include "version.h"
namespace lean { namespace lean {
class set_opaque_command : public neutral_object_cell { /**
name m_obj_name; \brief "Do nothing" normalizer extension.
bool m_opaque; */
class noop_normalizer_extension : public normalizer_extension {
public: public:
set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {} virtual optional<std::pair<expr, constraints>> operator()(expr const &, environment const &, type_checker &) const {
virtual ~set_opaque_command() {} return optional<std::pair<expr, constraints>>();
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<set_opaque_command const *>(obj.cell());
}
name const & get_set_opaque_id(object const & obj) {
lean_assert(is_set_opaque(obj));
return static_cast<set_opaque_command const *>(obj.cell())->get_obj_name();
}
bool get_set_opaque_flag(object const & obj) {
lean_assert(is_set_opaque(obj));
return static_cast<set_opaque_command const *>(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<import_command const*>(obj.cell());
}
optional<std::string> get_imported_module(object const & obj) {
if (is_begin_import(obj)) {
return optional<std::string>(static_cast<import_command const*>(obj.cell())->get_module());
} else {
return optional<std::string>();
} }
};
environment_header::environment_header(bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension const> 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<normalizer_extension>(new noop_normalizer_extension()))
{}
environment::environment(bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension> ext):
m_header(std::make_shared<environment_header>(proof_irrel, eta, std::move(ext))),
m_extensions(std::make_shared<environment_extensions const>())
{}
optional<definition> 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) { definition environment::get(name const & n) const {
return dynamic_cast<begin_import_mark const*>(obj.cell()); definition const * r = m_definitions.find(n);
if (!r)
throw_unknown_declaration(*this, n);
return *r;
} }
bool is_end_import(object const & obj) { [[ noreturn ]] void throw_incompatible_environment(environment const & env) {
return dynamic_cast<end_import_mark const*>(obj.cell()); throw_kernel_exception(env, "invalid declaration, it was checked/certified in an incompatible environment");
} }
class extension_factory { environment environment::add(certified_definition const & d) const {
std::vector<environment_cell::mk_extension> m_makers; if (d.get_header().get() != m_header.get())
mutex m_makers_mutex; 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<std::shared_ptr<environment_extension const>> m_exts;
mutex m_mutex;
public: public:
unsigned register_extension(environment_cell::mk_extension mk) { unsigned register_extension(std::shared_ptr<environment_extension const> const & ext) {
lock_guard<mutex> lock(m_makers_mutex); lock_guard<mutex> lock(m_mutex);
unsigned r = m_makers.size(); unsigned r = m_exts.size();
m_makers.push_back(mk); m_exts.push_back(ext);
return r; return r;
} }
std::unique_ptr<environment_extension> mk(unsigned extid) { bool has_ext(unsigned extid) const { return extid < m_exts.size(); }
lock_guard<mutex> lock(m_makers_mutex);
return m_makers[extid](); environment_extension const & get_initial(unsigned extid) {
lock_guard<mutex> lock(m_mutex);
return *(m_exts[extid].get());
} }
}; };
static std::unique_ptr<extension_factory> g_extension_factory; static std::unique_ptr<extension_manager> g_extension_manager;
static extension_factory & get_extension_factory() {
if (!g_extension_factory) static extension_manager & get_extension_manager() {
g_extension_factory.reset(new extension_factory()); if (!g_extension_manager)
return *g_extension_factory; g_extension_manager.reset(new extension_manager());
return *g_extension_manager;
} }
unsigned environment_cell::register_extension(mk_extension mk) { unsigned environment::register_extension(std::shared_ptr<environment_extension const> const & initial) {
return get_extension_factory().register_extension(mk); return get_extension_manager().register_extension(initial);
} }
environment environment_cell::env() const { [[ noreturn ]] void throw_invalid_extension(environment const & env) {
lean_assert(!m_this.expired()); // it is not possible to expire since it is a reference to this object throw_kernel_exception(env, "invalid environment extension identifier");
lean_assert(this == m_this.lock().get());
return environment(m_this.lock());
} }
environment environment_cell::parent() const { environment_extension const & environment::get_extension(unsigned id) const {
lean_assert(has_parent()); if (id >= get_extension_manager().has_ext(id))
return environment(m_parent); 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 { environment environment::update(unsigned id, std::shared_ptr<environment_extension const> const & ext) const {
return environment(m_this.lock(), true); if (id >= get_extension_manager().has_ext(id))
throw_invalid_extension(*this);
auto new_exts = std::make_shared<environment_extensions>(*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<environment_extension> 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<environment_cell *>(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<object> 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<object> 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<object> 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<void()> 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<import_command const*>(obj.cell())) {
if (num_imports == 0)
obj.write(s);
num_imports++;
} else if (dynamic_cast<end_import_mark const*>(obj.cell())) {
lean_assert(num_imports > 0);
num_imports--;
} else if (dynamic_cast<begin_import_mark const*>(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<std::string> 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<bool> set(m_type_check, !m_trust_imported);
return load_core(realpath(find_file(fname, {".olean"}).c_str()), ios, optional<std::string>(fname));
}
void environment_cell::load(std::string const & fname, io_state const & ios) {
load_core(fname, ios, optional<std::string>());
}
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<environment_cell> 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<environment_cell>()) {
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<environment_cell> const & parent, bool):
m_ptr(std::make_shared<environment_cell>(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<environment_cell> 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<environment_cell*>(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() {}
} }

438
src/kernel/environment.h
View file

@ -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. Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include <iostream>
#include <memory>
#include <vector>
#include <set>
#include <string>
#include <utility> #include <utility>
#include "util/lua.h" #include <memory>
#include "util/shared_mutex.h" #include "util/rc.h"
#include "util/name_map.h" #include "util/optional.h"
#include "kernel/object.h" #include "util/rb_map.h"
#include "kernel/level.h" #include "kernel/expr.h"
#include "kernel/constraint.h"
#include "kernel/definition.h"
namespace lean { namespace lean {
class environment;
class ro_environment;
class type_checker; class type_checker;
class environment_extension; class environment;
class certified_definition;
/** \brief Implementation of the Lean environment. */ /**
class environment_cell { \brief The Lean kernel can be instantiated with different normalization extensions.
friend class environment; Each extension is part of the trusted code base. The extensions allow us to support
friend class read_write_shared_environment; different flavors of the core type theory. We will use these extensions to implement
friend class read_only_shared_environment; inductive datatype (ala Coq), HIT, record types, etc.
// Remark: only named objects are stored in the dictionary. */
typedef name_map<object> object_dictionary; class normalizer_extension {
typedef std::tuple<level, level, int> constraint; public:
std::weak_ptr<environment_cell> m_this; virtual optional<std::pair<expr, constraints>> operator()(expr const & t, environment const & env, type_checker & tc) const;
// Children environment management };
atomic<unsigned> m_num_children;
std::shared_ptr<environment_cell> m_parent;
// Object management
std::vector<object> m_objects;
object_dictionary m_object_dictionary;
// std::unique_ptr<type_checker> m_type_checker; /**
std::set<name> m_imported_modules; // set of imported files and builtin modules \brief The header of an environment is created when we create the empty environment.
bool m_trust_imported; // if true, then imported modules are not type checked. Moreover if environment B is an extension of environment A, then A and B share the same header.
bool m_type_check; // auxiliary flag used to implement m_trust_imported. */
std::vector<std::unique_ptr<environment_extension>> m_extensions; class environment_header {
friend class environment_extension; 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<normalizer_extension const> m_norm_ext;
void dealloc();
public:
environment_header(bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension const> 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 class environment_extension {
// in the external APIs public:
shared_mutex m_mutex; virtual ~environment_extension();
};
environment env() const; typedef std::vector<std::shared_ptr<environment_extension const>> 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); 1- By providing a normalizer_extension when creating an empty environment.
environment_extension const & get_extension_core(unsigned extid) const; 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<environment_header const> header;
typedef rb_map<name, definition, name_quick_cmp> definitions;
typedef std::shared_ptr<environment_extensions const> extensions;
unsigned get_max_weight(expr const & e); header m_header;
void check_name_core(name const & n); definitions m_definitions;
void check_name(name const & n); extensions m_extensions;
void check_level_cnstrs(param_names const & ps, level_cnstrs const & ls); environment(header const & h, definitions const & d, extensions const & ext);
void register_named_object(object const & new_obj);
optional<object> 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<std::string> 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);
public: public:
environment_cell(); environment(bool proof_irrel = true, bool eta = true);
environment_cell(std::shared_ptr<environment_cell> const & parent); environment(bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension> ext);
~environment_cell(); ~environment();
/** \brief Return true iff this environment has children environments. */ std::shared_ptr<environment_header const> get_header() const { return m_header; }
bool has_children() const { return m_num_children > 0; }
/** \brief Return true iff this environment has a parent environment */ /** \brief Return true iff the environment assumes proof irrelevance */
bool has_parent() const { return m_parent != nullptr; } 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<definition> 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. \brief Extends the current environment with the given (certified) definition
\pre has_parent() 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 \brief Replace the axiom with name <tt>t.get_definition().get_name()</tt> with the theorem t.get_definition().
all children environments are deleted. 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 <tt>t.get_definition().get_name()</tt>
*/ */
environment mk_child() const; environment replace(certified_definition const & t) 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<object> 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<bool>(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<environment_cell const> m_env;
unsigned m_idx;
bool m_local;
friend class environment_cell;
object_iterator(std::shared_ptr<environment_cell const> && 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); }
// =======================================
/** /**
\brief Register an environment extension. Every environment \brief Register an environment extension. Every environment
object will contain this extension. The funciton mk creates a object may contain this extension. The argument \c initial is
new instance of the extension. The extension object can be the initial value for the new extensions. The extension object
retrieved using the token (unsigned integer) returned by this can be retrieved using the given token (unsigned integer) returned
method. by this method.
\remark The extension objects are created on demand. \remark The extension objects are created on demand.
\see get_extension \see get_extension
*/ */
typedef std::unique_ptr<environment_extension> (*mk_extension)(); static unsigned register_extension(std::shared_ptr<environment_extension const> const & initial);
static unsigned register_extension(mk_extension mk);
/** /** \brief Return the extension with the given id. */
\brief Retrieve the extension associated with the token \c extid. environment_extension const & get_extension(unsigned extid) const;
The token is the value returned by \c register_extension.
*/
template<typename Ext>
Ext const & get_extension(unsigned extid) const {
environment_extension const & ext = get_extension_core(extid);
lean_assert(dynamic_cast<Ext const *>(&ext) != nullptr);
return static_cast<Ext const &>(ext);
}
template<typename Ext> /** \brief Update the environment extension with the given id. */
Ext & get_extension(unsigned extid) { environment update(unsigned extid, std::shared_ptr<environment_extension const> const & ext) const;
environment_extension & ext = get_extension_core(extid);
lean_assert(dynamic_cast<Ext*>(&ext) != nullptr);
return static_cast<Ext&>(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<void()> fn);
}; };
/** /**
\brief Frontend can store data in environment extensions. \brief A certified definition is one that has been type checked.
Each extension is associated with a unique token/id. Only the type_checker class can create certified definitions.
This token allows the frontend to retrieve/store an extension object
in the environment
*/ */
class environment_extension { class certified_definition {
friend class environment_cell; friend class type_checker;
environment_cell * m_env; std::shared_ptr<environment_header const> m_header;
unsigned m_extid; // extension id definition m_definition;
environment_extension const * get_parent_core() const; certified_definition(std::shared_ptr<environment_header const> const & h, definition const & d);
public: public:
environment_extension(); certified_definition(certified_definition const & c);
virtual ~environment_extension(); std::shared_ptr<environment_header const> const & get_header() const { return m_header; }
/** definition const & get_definition() const { return m_definition; }
\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<typename Ext> Ext const * get_parent() const {
environment_extension const * ext = get_parent_core();
lean_assert(!ext || dynamic_cast<Ext const *>(ext) != nullptr);
return static_cast<Ext const *>(ext);
}
}; };
/**
\brief Reference to environment
*/
class environment {
friend class ro_environment;
friend class environment_cell;
friend class read_write_shared_environment;
std::shared_ptr<environment_cell> m_ptr;
environment(std::shared_ptr<environment_cell> const & parent, bool);
environment(std::shared_ptr<environment_cell> 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<environment_cell const> m_ptr;
ro_environment(std::shared_ptr<environment_cell const> 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<environment_cell>(m_ptr)); }
public:
typedef std::weak_ptr<environment_cell const> 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<std::string> 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);
} }

24
src/kernel/kernel_exception.cpp
View file

@ -17,7 +17,7 @@ protected:
optional<expr> m_main_expr; optional<expr> m_main_expr;
pp_fn m_pp_fn; pp_fn m_pp_fn;
public: public:
generic_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn): generic_kernel_exception(environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn):
kernel_exception(env, msg), kernel_exception(env, msg),
m_main_expr(m), m_main_expr(m),
m_pp_fn(fn) {} m_pp_fn(fn) {}
@ -28,40 +28,36 @@ public:
virtual void rethrow() const { throw *this; } virtual void rethrow() const { throw *this; }
}; };
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m) { [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m) {
std::string msg_str = msg; std::string msg_str = msg;
throw generic_kernel_exception(env, msg, m, [=](formatter const &, options const &) { return format(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) { [[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, optional<expr> const & m) {
throw_kernel_exception(env, strm.str().c_str(), m); throw_kernel_exception(env, strm.str().c_str(), m);
} }
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn) { [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn) {
throw generic_kernel_exception(env, msg, m, fn); throw generic_kernel_exception(env, msg, m, fn);
} }
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional<expr> const & m, pp_fn const & fn) { [[ noreturn ]] void throw_kernel_exception(environment const & env, optional<expr> const & m, pp_fn const & fn) {
throw generic_kernel_exception(env, "kernel exception", m, 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); 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); throw_kernel_exception(env, some_expr(m), fn);
} }
[[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n) { [[ noreturn ]] void throw_unknown_declaration(environment const & env, name const & n) {
throw_kernel_exception(env, sstream() << "unknown object '" << 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 << "'"); 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");
}
} }

27
src/kernel/kernel_exception.h
View file

@ -17,13 +17,13 @@ class environment;
/** \brief Base class for all kernel exceptions. */ /** \brief Base class for all kernel exceptions. */
class kernel_exception : public exception { class kernel_exception : public exception {
protected: protected:
ro_environment m_env; environment m_env;
public: public:
kernel_exception(ro_environment const & env):m_env(env) {} kernel_exception(environment const & env):m_env(env) {}
kernel_exception(ro_environment const & env, char const * msg):exception(msg), m_env(env) {} kernel_exception(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, sstream const & strm):exception(strm), m_env(env) {}
virtual ~kernel_exception() noexcept {} 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. \brief Return a reference (if available) to the main expression associated with this exception.
This information is used to provide better error messages. This information is used to provide better error messages.
@ -34,14 +34,13 @@ public:
virtual void rethrow() const { throw *this; } virtual void rethrow() const { throw *this; }
}; };
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m = none_expr()); [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m = none_expr());
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm, [[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm,
optional<expr> const & m = none_expr()); optional<expr> const & m = none_expr());
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn); [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn);
[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, optional<expr> const & m, pp_fn const & fn); [[ noreturn ]] void throw_kernel_exception(environment const & env, optional<expr> const & m, pp_fn const & fn);
[[ noreturn ]] void throw_kernel_exception(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);
[[ 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);
[[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n); [[ noreturn ]] void throw_unknown_declaration(environment const & env, name const & n);
[[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n); [[ noreturn ]] void throw_already_declared(environment const & env, name const & n);
[[ noreturn ]] void throw_read_only_environment(ro_environment const & env);
} }