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

Refactor kernel objects

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-13 15:13:54 -07:00
parent 00c06839a4
commit 11a9cac5d6
11 changed files with 413 additions and 197 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
pp.cpp) object.cpp pp.cpp)
target_link_libraries(kernel ${LEAN_LIBS}) target_link_libraries(kernel ${LEAN_LIBS})

238
src/kernel/environment.cpp
View file

@ -17,51 +17,10 @@ Author: Leonardo de Moura
#include "debug.h" #include "debug.h"
namespace lean { namespace lean {
constexpr unsigned uninit = std::numeric_limits<int>::max();
environment::definition::definition(name const & n, expr const & t, expr const & v, bool opaque):
m_name(n),
m_type(t),
m_value(v),
m_opaque(opaque) {
}
environment::definition::~definition() {
}
void environment::definition::display(std::ostream & out) const {
out << header() << " " << m_name << " : " << m_type << " := " << m_value << "\n";
}
format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); }
constexpr unsigned indentation = 2; // TODO: must be option
format environment::definition::pp(environment const & env) const {
return nest(indentation,
format{pp_object_kind(header()), format(" "), format(m_name), format(" : "), ::lean::pp(m_type, env), format(" :="),
line(), ::lean::pp(m_value), format(".")});
}
environment::fact::fact(name const & n, expr const & t):
m_name(n),
m_type(t) {
}
environment::fact::~fact() {
}
format environment::fact::pp(environment const & env) const {
return nest(indentation,
format{pp_object_kind(header()), format(" "), format(m_name), format(" : "), ::lean::pp(m_type, env), format(".")});
}
void environment::fact::display(std::ostream & out) const {
out << header() << " " << m_name << " : " << m_type << "\n";
}
/** \brief Implementation of the Lean environment. */ /** \brief Implementation of the Lean environment. */
struct environment::imp { struct environment::imp {
typedef std::unordered_map<name, object *, name_hash, name_eq> object_dictionary; // Remark: only named objects are stored in the dictionary.
typedef std::unordered_map<name, named_object *, name_hash, name_eq> object_dictionary;
typedef std::tuple<level, level, int> constraint; typedef std::tuple<level, level, int> constraint;
// Universe variable management // Universe variable management
std::vector<constraint> m_constraints; std::vector<constraint> m_constraints;
@ -73,25 +32,33 @@ struct environment::imp {
std::vector<object*> m_objects; std::vector<object*> m_objects;
object_dictionary m_object_dictionary; object_dictionary m_object_dictionary;
/**
\brief Return true iff this environment has children.
\remark If an environment has children than it cannot be
updated. That is, it is read-only.
*/
bool has_children() const { return m_num_children > 0; } bool has_children() const { return m_num_children > 0; }
void inc_children() { m_num_children++; } void inc_children() { m_num_children++; }
void dec_children() { m_num_children--; } void dec_children() { m_num_children--; }
/** \brief Return true iff this environment has a parent environment */
bool has_parent() const { return m_parent != nullptr; } bool has_parent() const { return m_parent != nullptr; }
/** \brief Return true if l1 >= l2 + k is implied by constraints /**
\pre is_uvar(l1) && is_uvar(l2) \brief Return true if u >= v + k is implied by constraints
*/ \pre is_uvar(u) && is_uvar(v)
bool is_implied(level const & l1, level const & l2, int k) { */
lean_assert(is_uvar(l1) && is_uvar(l2)); bool is_implied(level const & u, level const & v, int k) {
if (l1 == l2) lean_assert(is_uvar(u) && is_uvar(v));
if (u == v)
return k <= 0; return k <= 0;
else else
return std::any_of(m_constraints.begin(), m_constraints.end(), return std::any_of(m_constraints.begin(), m_constraints.end(),
[&](constraint const & c) { return std::get<0>(c) == l1 && std::get<1>(c) == l2 && std::get<2>(c) >= k; }); [&](constraint const & c) { return std::get<0>(c) == u && std::get<1>(c) == v && std::get<2>(c) >= k; });
} }
/** \brief Return true iff l1 >= l2 + k */ /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */
bool is_ge(level const & l1, level const & l2, int k) { bool is_ge(level const & l1, level const & l2, int k) {
if (l1 == l2) if (l1 == l2)
return k == 0; return k == 0;
@ -109,6 +76,7 @@ struct environment::imp {
return false; return false;
} }
/** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */
bool is_ge(level const & l1, level const & l2) { bool is_ge(level const & l1, level const & l2) {
if (has_parent()) if (has_parent())
return m_parent->is_ge(l1, l2); return m_parent->is_ge(l1, l2);
@ -116,6 +84,7 @@ struct environment::imp {
return is_ge(l1, l2, 0); return is_ge(l1, l2, 0);
} }
/** \brief Add a new universe variable */
level add_var(name const & n) { level add_var(name const & n) {
if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; })) if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; }))
throw exception("invalid universe variable declaration, it has already been declared"); throw exception("invalid universe variable declaration, it has already been declared");
@ -124,24 +93,37 @@ struct environment::imp {
return r; return r;
} }
void add_constraint(level const & l1, level const & l2, int d) { /**
if (is_implied(l1, l2, d)) \brief Add basic constraint u >= v + d, and all basic
constraints implied by transitivity.
\pre is_uvar(u) && is_uvar(v)
*/
void add_constraint(level const & u, level const & v, int d) {
lean_assert(is_uvar(u) && is_uvar(v));
if (is_implied(u, v, d))
return; // redundant return; // redundant
buffer<constraint> to_add; buffer<constraint> to_add;
for (constraint const & c : m_constraints) { for (constraint const & c : m_constraints) {
if (std::get<0>(c) == l2) { if (std::get<0>(c) == v) {
level const & l3 = std::get<1>(c); level const & l3 = std::get<1>(c);
int l1_l3_d = safe_add(d, std::get<2>(c)); int u_l3_d = safe_add(d, std::get<2>(c));
if (!is_implied(l1, l3, l1_l3_d)) if (!is_implied(u, l3, u_l3_d))
to_add.push_back(constraint(l1, l3, l1_l3_d)); to_add.push_back(constraint(u, l3, u_l3_d));
} }
} }
m_constraints.push_back(constraint(l1, l2, d)); m_constraints.push_back(constraint(u, v, d));
for (constraint const & c: to_add) { for (constraint const & c: to_add) {
m_constraints.push_back(c); m_constraints.push_back(c);
} }
} }
/**
\brief Add all basic constraints implied by n >= l + k
A basic constraint is a constraint of the form u >= v + k
where u and v are universe variables.
*/
void add_constraints(level const & n, level const & l, int k) { void add_constraints(level const & n, level const & l, int k) {
lean_assert(is_uvar(n)); lean_assert(is_uvar(n));
switch (kind(l)) { switch (kind(l)) {
@ -152,6 +134,7 @@ struct environment::imp {
lean_unreachable(); lean_unreachable();
} }
/** \brief Add a new universe variable with constraint n >= l */
level add_uvar(name const & n, level const & l) { level add_uvar(name const & n, level const & l) {
if (has_parent()) if (has_parent())
throw exception("invalid universe declaration, universe variables can only be declared in top-level environments"); throw exception("invalid universe declaration, universe variables can only be declared in top-level environments");
@ -162,6 +145,11 @@ struct environment::imp {
return r; return r;
} }
/**
\brief Return the universe variable with given name. Throw an
exception if the environment and its ancestors do not
contain a universe variable named \c n.
*/
level get_uvar(name const & n) const { level get_uvar(name const & n) const {
if (has_parent()) { if (has_parent()) {
return m_parent->get_uvar(n); return m_parent->get_uvar(n);
@ -177,10 +165,14 @@ struct environment::imp {
} }
} }
/**
\brief Initialize the set of universe variables with bottom
*/
void init_uvars() { void init_uvars() {
m_uvars.push_back(level()); m_uvars.push_back(level());
} }
/** \brief Display universe variable constraints */
void display_uvars(std::ostream & out) const { void display_uvars(std::ostream & out) const {
for (constraint const & c : m_constraints) { for (constraint const & c : m_constraints) {
out << uvar_name(std::get<0>(c)) << " >= " << uvar_name(std::get<1>(c)); out << uvar_name(std::get<0>(c)) << " >= " << uvar_name(std::get<1>(c));
@ -190,12 +182,16 @@ struct environment::imp {
} }
} }
/** \brief Throw exception if environment has children. */
void check_no_children() { void check_no_children() {
if (has_children()) if (has_children())
throw exception("invalid object declaration, environment has children environments"); throw exception("invalid object declaration, environment has children environments");
} }
void check_name(name const & n) { /** \brief Throw exception if environment or its ancestors already have an object with the given name. */
void 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()) { if (m_object_dictionary.find(n) != m_object_dictionary.end()) {
std::ostringstream s; std::ostringstream s;
s << "environment already contains an object with name '" << n << "'"; s << "environment already contains an object with name '" << n << "'";
@ -203,32 +199,84 @@ struct environment::imp {
} }
} }
void check_add(name const & n) { void check_name(name const & n) {
check_no_children(); check_no_children();
check_name_core(n);
}
/**
\brief Throw an exception if \c t is not a type or type of \c
v is not convertible to \c t.
\remark env is the smart pointer of imp. We need it because
infer_universe and infer_type expect an environment instead of environment::imp.
*/
void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
infer_universe(t, env);
expr v_t = infer_type(v, env);
if (!is_convertible(t, v_t, env)) {
std::ostringstream buffer;
buffer << "type mismatch when defining '" << n << "'\n"
<< "expected type:\n" << t << "\n"
<< "given type:\n" << v_t;
throw exception(buffer.str());
}
}
/** \brief Throw exception if it is not a valid new definition */
void check_new_definition(name const & n, expr const & t, expr const & v, environment const & env) {
check_name(n); check_name(n);
check_type(n, t, v, env);
} }
void add_definition(name const & n, expr const & t, expr const & v, bool opaque) { /** \brief Store new named object inside internal data-structures */
m_objects.push_back(new definition(n, t, v, opaque)); void register_named_object(named_object * new_obj) {
m_object_dictionary.insert(std::make_pair(n, m_objects.back())); m_objects.push_back(new_obj);
m_object_dictionary.insert(std::make_pair(new_obj->get_name(), new_obj));
} }
void add_theorem(name const & n, expr const & t, expr const & v) { /** \brief Add new definition. */
m_objects.push_back(new theorem(n, t, v)); void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) {
m_object_dictionary.insert(std::make_pair(n, m_objects.back())); check_new_definition(n, t, v, env);
register_named_object(new definition(n, t, v, opaque));
} }
void add_axiom(name const & n, expr const & t) { /**
m_objects.push_back(new axiom(n, t)); \brief Add new definition.
m_object_dictionary.insert(std::make_pair(n, m_objects.back())); The type of the new definition is the type of \c v.
*/
void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
check_name(n);
expr v_t = infer_type(v, env);
register_named_object(new definition(n, v_t, v, opaque));
} }
void add_var(name const & n, expr const & t) { /** \brief Add new theorem. */
m_objects.push_back(new variable(n, t)); void add_theorem(name const & n, expr const & t, expr const & v, environment const & env) {
m_object_dictionary.insert(std::make_pair(n, m_objects.back())); check_new_definition(n, t, v, env);
register_named_object(new theorem(n, t, v));
} }
object const * get_object_ptr(name const & n) const { /** \brief Add new axiom. */
void add_axiom(name const & n, expr const & t, environment const & env) {
check_name(n);
infer_universe(t, env);
register_named_object(new axiom(n, t));
}
/** \brief Add new variable. */
void add_var(name const & n, expr const & t, environment const & env) {
check_name(n);
infer_universe(t, env);
register_named_object(new variable(n, t));
}
/**
\brief Return the object named \c n in the environment or its
ancestors. Return nullptr if there is not object with the
given name.
*/
named_object const * get_object_ptr(name const & n) const {
auto it = m_object_dictionary.find(n); auto it = m_object_dictionary.find(n);
if (it == m_object_dictionary.end()) { if (it == m_object_dictionary.end()) {
if (has_parent()) if (has_parent())
@ -240,8 +288,8 @@ struct environment::imp {
} }
} }
object const & get_object(name const & n) const { named_object const & get_object(name const & n) const {
object const * ptr = get_object_ptr(n); named_object const * ptr = get_object_ptr(n);
if (ptr) { if (ptr) {
return *ptr; return *ptr;
} else { } else {
@ -331,55 +379,31 @@ level environment::get_uvar(name const & n) const {
return m_imp->get_uvar(n); return m_imp->get_uvar(n);
} }
void environment::check_type(name const & n, expr const & t, expr const & v) {
infer_universe(t, *this);
expr v_t = infer_type(v, *this);
if (!is_convertible(t, v_t, *this)) {
std::ostringstream buffer;
buffer << "type mismatch when defining '" << n << "'\n"
<< "expected type:\n" << t << "\n"
<< "given type:\n" << v_t;
throw exception(buffer.str());
}
}
void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
m_imp->check_no_children(); m_imp->add_definition(n, t, v, opaque, *this);
m_imp->check_name(n);
check_type(n, t, v);
m_imp->add_definition(n, t, v, opaque);
} }
void environment::add_theorem(name const & n, expr const & t, expr const & v) { void environment::add_theorem(name const & n, expr const & t, expr const & v) {
m_imp->check_no_children(); m_imp->add_theorem(n, t, v, *this);
m_imp->check_name(n);
check_type(n, t, v);
m_imp->add_theorem(n, t, v);
} }
void environment::add_definition(name const & n, expr const & v, bool opaque) { void environment::add_definition(name const & n, expr const & v, bool opaque) {
m_imp->check_add(n); m_imp->add_definition(n, v, opaque, *this);
expr v_t = infer_type(v, *this);
m_imp->add_definition(n, v_t, v, opaque);
} }
void environment::add_axiom(name const & n, expr const & t) { void environment::add_axiom(name const & n, expr const & t) {
m_imp->check_add(n); m_imp->add_axiom(n, t, *this);
infer_universe(t, *this);
m_imp->add_axiom(n, t);
} }
void environment::add_var(name const & n, expr const & t) { void environment::add_var(name const & n, expr const & t) {
m_imp->check_add(n); m_imp->add_var(n, t, *this);
infer_universe(t, *this);
m_imp->add_var(n, t);
} }
environment::object const & environment::get_object(name const & n) const { named_object const & environment::get_object(name const & n) const {
return m_imp->get_object(n); return m_imp->get_object(n);
} }
environment::object const * environment::get_object_ptr(name const & n) const { named_object const * environment::get_object_ptr(name const & n) const {
return m_imp->get_object_ptr(n); return m_imp->get_object_ptr(n);
} }
@ -387,7 +411,7 @@ unsigned environment::get_num_objects() const {
return m_imp->m_objects.size(); return m_imp->m_objects.size();
} }
environment::object const & environment::get_object(unsigned i) const { object const & environment::get_object(unsigned i) const {
return *(m_imp->m_objects[i]); return *(m_imp->m_objects[i]);
} }

88
src/kernel/environment.h
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include <iostream> #include <iostream>
#include <memory> #include <memory>
#include "expr.h" #include "object.h"
#include "level.h" #include "level.h"
namespace lean { namespace lean {
@ -16,8 +16,6 @@ namespace lean {
datatypes, universe variables, et.c datatypes, universe variables, et.c
*/ */
class environment { class environment {
public:
class object;
private: private:
struct imp; struct imp;
std::shared_ptr<imp> m_imp; std::shared_ptr<imp> m_imp;
@ -80,86 +78,6 @@ public:
// ======================================= // =======================================
// Environment Objects // Environment Objects
enum class object_kind { Definition, Theorem, Var, Axiom };
/**
\brief Base class for environment objects
It is just a place holder at this point.
*/
class object {
protected:
public:
object() {}
object(object const & o) = delete;
object & operator=(object const & o) = delete;
virtual ~object() {}
virtual object_kind kind() const = 0;
virtual void display(std::ostream & out) const = 0;
virtual format pp(environment const &) const = 0;
virtual expr const & get_type() const = 0;
virtual char const * header() const = 0;
};
class definition : public object {
name m_name;
expr m_type;
expr m_value;
bool m_opaque;
public:
definition(name const & n, expr const & t, expr const & v, bool opaque);
virtual ~definition();
virtual object_kind kind() const { return object_kind::Definition; }
name const & get_name() const { return m_name; }
virtual expr const & get_type() const { return m_type; }
expr const & get_value() const { return m_value; }
bool is_opaque() const { return m_opaque; }
virtual void display(std::ostream & out) const;
virtual format pp(environment const & env) const;
virtual char const * header() const { return "Definition"; }
};
class theorem : public definition {
public:
theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {}
virtual object_kind kind() const { return object_kind::Theorem; }
virtual char const * header() const { return "Theorem"; }
};
class fact : public object {
protected:
name m_name;
expr m_type;
public:
fact(name const & n, expr const & t);
virtual ~fact();
name const & get_name() const { return m_name; }
virtual expr const & get_type() const { return m_type; }
virtual void display(std::ostream & out) const;
virtual format pp(environment const &) const;
};
class axiom : public fact {
public:
axiom(name const & n, expr const & t):fact(n, t) {}
virtual object_kind kind() const { return object_kind::Axiom; }
virtual char const * header() const { return "Axiom"; }
};
class variable : public fact {
public:
variable(name const & n, expr const & t):fact(n, t) {}
virtual object_kind kind() const { return object_kind::Var; }
virtual char const * header() const { return "Variable"; }
};
friend bool is_definition(object const & o) { return o.kind() == object_kind::Definition; }
friend bool is_axiom(object const & o) { return o.kind() == object_kind::Axiom; }
friend bool is_var(object const & o) { return o.kind() == object_kind::Var; }
friend bool is_fact(object const & o) { return is_axiom(o) || is_var(o); }
friend definition const & to_definition(object const & o) { lean_assert(is_definition(o)); return static_cast<definition const &>(o); }
friend fact const & to_fact(object const & o) { lean_assert(is_fact(o)); return static_cast<fact const &>(o); }
/** /**
\brief Add a new definition n : t := v. \brief Add a new definition n : t := v.
It throws an exception if v does not have type t. It throws an exception if v does not have type t.
@ -187,13 +105,13 @@ public:
\brief Return the object with the given name. \brief Return the object with the given name.
It throws an exception if the environment does not have an object with the given name. It throws an exception if the environment does not have an object with the given name.
*/ */
object const & get_object(name const & n) const; named_object const & get_object(name const & n) const;
/** /**
\brief Return the object with the given name. \brief Return the object with the given name.
Return nullptr if there is no object with the given name. Return nullptr if there is no object with the given name.
*/ */
object const * get_object_ptr(name const & n) const; named_object const * get_object_ptr(name const & n) const;
/** \brief Iterator for Lean environment objects. */ /** \brief Iterator for Lean environment objects. */
class object_iterator { class object_iterator {

7
src/kernel/expr.cpp
View file

@ -19,6 +19,13 @@ unsigned hash_args(unsigned size, expr const * args) {
return hash(size, [&args](unsigned i){ return args[i].hash(); }); return hash(size, [&args](unsigned i){ return args[i].hash(); });
} }
static expr g_null;
expr const & expr::null() {
lean_assert(!g_null);
return g_null;
}
expr_cell::expr_cell(expr_kind k, unsigned h): expr_cell::expr_cell(expr_kind k, unsigned h):
m_kind(static_cast<unsigned>(k)), m_kind(static_cast<unsigned>(k)),
m_flags(0), m_flags(0),

13
src/kernel/expr.h
View file

@ -79,6 +79,8 @@ public:
expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~expr() { if (m_ptr) m_ptr->dec_ref(); } ~expr() { if (m_ptr) m_ptr->dec_ref(); }
static expr const & null();
friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); } friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); }
void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; } void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; }
@ -410,6 +412,17 @@ struct args {
expr copy(expr const & e); expr copy(expr const & e);
// ======================================= // =======================================
// =======================================
// Expression formatter
class expr_formatter {
public:
virtual ~expr_formatter() {}
virtual format operator()(expr const & e) = 0;
virtual options const & get_options() const = 0;
};
// =======================================
// ======================================= // =======================================
// Update // Update
template<typename F> expr update_app(expr const & e, F f) { template<typename F> expr update_app(expr const & e, F f) {

6
src/kernel/normalize.cpp
View file

@ -133,9 +133,9 @@ class normalize_fn {
case expr_kind::Var: case expr_kind::Var:
return lookup(s, var_idx(a), k); return lookup(s, var_idx(a), k);
case expr_kind::Constant: { case expr_kind::Constant: {
environment::object const & obj = m_env.get_object(const_name(a)); named_object const & obj = m_env.get_object(const_name(a));
if (is_definition(obj) && !to_definition(obj).is_opaque()) { if (obj.is_definition() && !obj.is_opaque()) {
return normalize(to_definition(obj).get_value(), value_stack(), 0); return normalize(obj.get_value(), value_stack(), 0);
} }
else { else {
return svalue(a); return svalue(a);

74
src/kernel/object.cpp Normal file
View file

@ -0,0 +1,74 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "object.h"
#include "environment.h"
#include "pp.h" // TODO: move to front-end
namespace lean {
// TODO: delete hardcoded
format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); }
constexpr unsigned indentation = 2; // TODO: must be option
//
object::~object() {}
void object::display(std::ostream & out, environment const & env) const { out << pp(env); }
anonymous_object::~anonymous_object() {}
bool anonymous_object::has_name() const { return false; }
name const & anonymous_object::get_name() const { lean_unreachable(); return name::anonymous(); }
bool anonymous_object::has_type() const { return false; }
expr const & anonymous_object::get_type() const { lean_unreachable(); return expr::null(); }
bool anonymous_object::is_definition() const { return false; }
bool anonymous_object::is_opaque() const { lean_unreachable(); return false; }
expr const & anonymous_object::get_value() const { lean_unreachable(); return expr::null(); }
named_object::named_object(name const & n, expr const & t):m_name(n), m_type(t) {}
named_object::~named_object() {}
bool named_object::has_name() const { return true; }
name const & named_object::get_name() const { return m_name; }
bool named_object::has_type() const { return true; }
expr const & named_object::get_type() const { return m_type; }
char const * definition::g_keyword = "Definition";
definition::definition(name const & n, expr const & t, expr const & v, bool opaque):named_object(n, t), m_value(v), m_opaque(opaque) {}
definition::~definition() {}
char const * definition::keyword() const { return g_keyword; }
bool definition::is_definition() const { return true; }
bool definition::is_opaque() const { return m_opaque; }
expr const & definition::get_value() const { return m_value; }
format definition::pp(environment const & env) const {
return nest(indentation,
format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(" :="),
line(), ::lean::pp(get_value()), format(".")});
}
char const * theorem::g_keyword = "Theorem";
theorem::theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {}
theorem::~theorem() {}
char const * theorem::keyword() const { return g_keyword; }
fact::fact(name const & n, expr const & t):named_object(n, t) {}
fact::~fact() {}
bool fact::is_definition() const { return false; }
bool fact::is_opaque() const { lean_unreachable(); return false; }
expr const & fact::get_value() const { lean_unreachable(); return expr::null(); }
format fact::pp(environment const & env) const {
return nest(indentation,
format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(".")});
}
char const * axiom::g_keyword = "Axiom";
axiom::axiom(name const & n, expr const & t):fact(n, t) {}
axiom::~axiom() {}
char const * axiom::keyword() const { return g_keyword; }
char const * variable::g_keyword = "Variable";
variable::variable(name const & n, expr const & t):fact(n, t) {}
variable::~variable() {}
char const * variable::keyword() const { return g_keyword; }
}

171
src/kernel/object.h Normal file
View file

@ -0,0 +1,171 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "expr.h"
/*
Kernel objects.
We use abstract classes and virtual methods because a kernel
frontend may need to create new objects for bookkeeping.
*/
namespace lean {
class environment;
/**
\brief Abstract class used to represent kernel objects (i.e.,
definitions, theorems, axioms, recursive definitions, etc)
*/
class object {
protected:
public:
object() {}
object(object const & o) = delete;
object & operator=(object const & o) = delete;
virtual ~object();
/**
\brief Return the keyword used to define this object in a Lean
file. The keyword is also used to identify the class of an object.
*/
virtual char const * keyword() const = 0;
/** \brief Pretty print this object. */
virtual format pp(environment const &) const = 0;
/** \brief Display the object in the standard output. */
virtual void display(std::ostream & out, environment const &) const;
/** \brief Return true iff object has a name. */
virtual bool has_name() const = 0;
/** \brief Return object name. \pre has_name() */
virtual name const & get_name() const = 0;
/** \brief Return true iff object has a type. */
virtual bool has_type() const = 0;
/** \brief Return object type. \pre has_type() */
virtual expr const & get_type() const = 0;
/** \brief Return true iff object is a definition */
virtual bool is_definition() const = 0;
/** \brief Return true iff the definition is opaque. \pre is_definition() */
virtual bool is_opaque() const = 0;
/** \brief Return object value. \pre is_definition() */
virtual expr const & get_value() const = 0;
};
/**
\brief Anonymous objects are mainly used for bookkeeping.
*/
class anonymous_object : public object {
public:
virtual ~anonymous_object();
virtual bool has_name() const;
virtual name const & get_name() const;
virtual bool has_type() const;
virtual expr const & get_type() const;
virtual bool is_definition() const;
virtual bool is_opaque() const;
virtual expr const & get_value() const;
};
/**
\brief Named (and typed) kernel objects.
*/
class named_object : public object {
name m_name;
expr m_type;
public:
named_object(name const & n, expr const & t);
virtual ~named_object();
virtual bool has_name() const;
virtual name const & get_name() const;
virtual bool has_type() const;
virtual expr const & get_type() const;
};
/**
\brief Non-recursive definitions.
*/
class definition : public named_object {
expr m_value;
bool m_opaque; // Opaque definitions are ignored by definitional equality.
public:
definition(name const & n, expr const & t, expr const & v, bool opaque);
virtual ~definition();
static char const * g_keyword;
virtual char const * keyword() const;
virtual bool is_definition() const;
virtual bool is_opaque() const;
virtual expr const & get_value() const;
virtual format pp(environment const & env) const;
};
/**
\brief A theorem is essentially an opaque definition.
*/
class theorem : public definition {
public:
theorem(name const & n, expr const & t, expr const & v);
virtual ~theorem();
static char const * g_keyword;
virtual char const * keyword() const;
};
/**
\brief Base class for named objects that are not definitions.
*/
class fact : public named_object {
public:
fact(name const & n, expr const & t);
virtual ~fact();
virtual bool is_definition() const;
virtual bool is_opaque() const;
virtual expr const & get_value() const;
virtual format pp(environment const & env) const;
};
/**
\brief Axioms
*/
class axiom : public fact {
public:
axiom(name const & n, expr const & t);
virtual ~axiom();
static char const * g_keyword;
virtual char const * keyword() const;
};
/**
\brief Variable postulate. It is like an axiom since we are
essentially postulating that a type is inhabited.
*/
class variable : public fact {
public:
variable(name const & n, expr const & t);
virtual ~variable();
static char const * g_keyword;
virtual char const * keyword() const;
};
}

3
src/tests/kernel/environment.cpp
View file

@ -68,6 +68,7 @@ static void tst3() {
std::cout << "expected error: " << ex.what() << "\n"; std::cout << "expected error: " << ex.what() << "\n";
} }
env.add_definition("a", Int, iAdd(iVal(1), iVal(2))); env.add_definition("a", Int, iAdd(iVal(1), iVal(2)));
std::cout << env << "\n";
expr t = iAdd(Const("a"), iVal(1)); expr t = iAdd(Const("a"), iVal(1));
std::cout << t << " --> " << normalize(t, env) << "\n"; std::cout << t << " --> " << normalize(t, env) << "\n";
lean_assert(normalize(t, env) == iVal(4)); lean_assert(normalize(t, env) == iVal(4));
@ -169,7 +170,7 @@ static void tst7() {
int main() { int main() {
enable_trace("is_convertible"); enable_trace("is_convertible");
continue_on_violation(true); // continue_on_violation(true);
tst1(); tst1();
tst2(); tst2();
tst3(); tst3();

7
src/util/name.cpp
View file

@ -140,6 +140,13 @@ name::~name() {
m_ptr->dec_ref(); m_ptr->dec_ref();
} }
static name g_anonymous;
name const & name::anonymous() {
lean_assert(g_anonymous.is_anonymous());
return g_anonymous;
}
name & name::operator=(name const & other) { LEAN_COPY_REF(name, other); } name & name::operator=(name const & other) { LEAN_COPY_REF(name, other); }
name & name::operator=(name && other) { LEAN_MOVE_REF(name, other); } name & name::operator=(name && other) { LEAN_MOVE_REF(name, other); }

1
src/util/name.h
View file

@ -28,6 +28,7 @@ public:
name(name && other); name(name && other);
name(std::initializer_list<char const *> const & l); name(std::initializer_list<char const *> const & l);
~name(); ~name();
static name const & anonymous();
name & operator=(name const & other); name & operator=(name const & other);
name & operator=(name && other); name & operator=(name && other);
friend bool operator==(name const & a, name const & b); friend bool operator==(name const & a, name const & b);