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

feat(kernel/environment): add is_descendant method

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-21 14:28:50 -07:00
parent bfeb51ce58
commit 6417c79569
2 changed files with 59 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/kernel/environment.cpp
View file

@ -24,8 +24,24 @@ environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, boo
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_id::environment_id():m_trail(0, list<unsigned>()) {}
environment_id::environment_id(environment_id const & ancestor, bool):m_trail(car(ancestor.m_trail) + 1, ancestor.m_trail) {}
bool environment_id::is_descendant(environment_id const & id) const {
list<unsigned> const * it = &m_trail;
while (!is_nil(*it)) {
if (is_eqp(*it, id.m_trail))
return true;
if (car(*it) >= car(id.m_trail))
return false;
it = &cdr(*it);
}
return false;
}
environment::environment(header const & h, environment_id const & ancestor, definitions const & d, extensions const & exts):
m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_extensions(exts) {}
environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta):
environment(trust_lvl, proof_irrel, eta, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
@ -53,16 +69,16 @@ definition environment::get(name const & n) const {
}
environment environment::add(certified_definition const & d) const {
if (d.get_header().get() != m_header.get())
if (!m_id.is_descendant(d.get_id()))
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);
return environment(m_header, m_id, 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())
if (!m_id.is_descendant(t.get_id()))
throw_incompatible_environment(*this);
name const & n = t.get_definition().get_name();
auto ax = find(n);
@ -74,7 +90,7 @@ environment environment::replace(certified_definition const & t) const {
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);
return environment(m_header, m_id, insert(m_definitions, n, t.get_definition()), m_extensions);
}
class extension_manager {
@ -127,6 +143,6 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
if (id >= new_exts->size())
new_exts->resize(id+1);
(*new_exts)[id] = ext;
return environment(m_header, m_definitions, new_exts);
return environment(m_header, m_id, m_definitions, new_exts);
}
}

46
src/kernel/environment.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <memory>
#include "util/rc.h"
#include "util/optional.h"
#include "util/list.h"
#include "util/rb_map.h"
#include "kernel/expr.h"
#include "kernel/constraint.h"
@ -59,6 +60,26 @@ public:
typedef std::vector<std::shared_ptr<environment_extension const>> environment_extensions;
/**
\brief environment identifier that allows us to track descendants of a given environment.
*/
class environment_id {
friend class environment; // Only the environment class can create object of this type.
list<unsigned> m_trail; //!< trail of ancestors. The unsigned value is redundant, it store the depth of the trail.
/**
\brief Create an identifier for an environment that is a direct descendant of the given one.
The bool field is just to make sure this constructor is not confused with a copy constructor
*/
environment_id(environment_id const & ancestor, bool);
/** \brief Create an identifier for an environment without ancestors (e.g., empty environment) */
environment_id();
/** Create an identifier for an environment that is a direct descendant of the given one. */
static environment_id mk_descendant(environment_id const & ancestor) { return environment_id(ancestor, true); }
public:
/** \brief Return true iff this object is a descendant of the given one. */
bool is_descendant(environment_id const & id) const;
};
/**
\brief Lean core environment. An environment object can be extended/customized in different ways:
@ -72,18 +93,23 @@ class environment {
typedef rb_map<name, definition, name_quick_cmp> definitions;
typedef std::shared_ptr<environment_extensions const> extensions;
header m_header;
definitions m_definitions;
extensions m_extensions;
header m_header;
environment_id m_id;
definitions m_definitions;
extensions m_extensions;
environment(header const & h, definitions const & d, extensions const & ext);
environment(header const & h, environment_id const & id, definitions const & d, extensions const & ext);
public:
environment(unsigned trust_lvl = 0, bool proof_irrel = true, bool eta = true);
environment(unsigned trust_lvl, bool proof_irrel, bool eta, std::unique_ptr<normalizer_extension> ext);
~environment();
std::shared_ptr<environment_header const> get_header() const { return m_header; }
/** \brief Return the environment unique identifier. */
environment_id const & get_id() const { return m_id; }
/** \brief Return true iff this environment is a descendant of \c env. */
bool is_descendant(environment const & env) const { return m_id.is_descendant(env.m_id); }
/** \brief Return the trust level of this environment. */
unsigned trust_lvl() const { return m_header->trust_lvl(); }
@ -145,12 +171,12 @@ public:
*/
class certified_definition {
friend class type_checker;
std::shared_ptr<environment_header const> m_header;
definition m_definition;
certified_definition(std::shared_ptr<environment_header const> const & h, definition const & d);
environment_id m_id;
definition m_definition;
certified_definition(environment_id const & id, definition const & d):m_id(id), m_definition(d) {}
public:
certified_definition(certified_definition const & c);
std::shared_ptr<environment_header const> const & get_header() const { return m_header; }
/** \brief Return the id of the environment that was used to type check this definition. */
environment_id const & get_id() const { return m_id; }
definition const & get_definition() const { return m_definition; }
};
}