From 519a290f320c6a84c1c182ad9f736e0352d466af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 Aug 2013 15:09:26 -0700 Subject: [PATCH] Refactor kernel objects Signed-off-by: Leonardo de Moura --- src/frontend/frontend.cpp | 4 +- src/kernel/environment.cpp | 165 +++++++++++---------------- src/kernel/environment.h | 15 +-- src/kernel/kernel_exception.h | 15 +-- src/kernel/normalize.cpp | 2 +- src/kernel/object.cpp | 185 ++++++++++++++++++++++--------- src/kernel/object.h | 173 +++++++++++------------------ src/tests/kernel/environment.cpp | 12 +- src/tests/kernel/level.cpp | 4 +- src/tests/kernel/type_check.cpp | 2 +- 10 files changed, 281 insertions(+), 296 deletions(-) diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index 749cc7cfe..fa305036b 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -18,7 +18,7 @@ namespace lean { \brief Create object for tracking notation/operator declarations. This object is mainly used for pretty printing. */ -class notation_declaration : public anonymous_object { +class notation_declaration : public neutral_object_cell { operator_info m_op; name m_name; public: @@ -183,7 +183,7 @@ struct frontend::imp { remove_bindings(old_op); register_new_op(new_op, n, led); } - m_env.add_anonymous_object(new notation_declaration(new_op, n)); + m_env.add_neutral_object(new notation_declaration(new_op, n)); } void add_infixl(name const & opn, unsigned p, name const & n) { add_op(infixl(opn, p), n, true); } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 20c7416ee..84c757c14 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -17,28 +17,11 @@ Author: Leonardo de Moura #include "debug.h" namespace lean { -/** - \brief Create object for tracking universe variable declarations. - This object is mainly used for pretty printing. -*/ -class uvar_declaration : public anonymous_object { - name m_name; - level m_level; -public: - uvar_declaration(name const & n, level const & l):m_name(n), m_level(l) {} - virtual ~uvar_declaration() {} - static char const * g_keyword; - virtual char const * keyword() const { return g_keyword; } - virtual format pp(environment const &) const { - return format{highlight_command(format(keyword())), space(), format(m_name), space(), format("\u2265"), space(), ::lean::pp(m_level)}; - } -}; -char const * uvar_declaration::g_keyword = "Universe"; /** \brief Implementation of the Lean environment. */ struct environment::imp { // Remark: only named objects are stored in the dictionary. - typedef std::unordered_map object_dictionary; + typedef std::unordered_map object_dictionary; typedef std::tuple constraint; // Universe variable management std::vector m_constraints; @@ -47,7 +30,7 @@ struct environment::imp { std::atomic m_num_children; std::shared_ptr m_parent; // Object management - std::vector m_objects; + std::vector m_objects; object_dictionary m_object_dictionary; // Expression formatter && locator std::shared_ptr m_formatter; @@ -75,6 +58,51 @@ struct environment::imp { /** \brief Return true iff this environment has a parent environment */ bool has_parent() const { return m_parent != nullptr; } + /** \brief Throw exception if environment or its ancestors already have an object with the given name. */ + void check_name_core(name const & n, environment const & env) { + if (has_parent()) + m_parent->check_name_core(n, env); + if (m_object_dictionary.find(n) != m_object_dictionary.end()) + throw already_declared_exception(env, n); + } + + void check_name(name const & n, environment const & env) { + if (has_children()) + throw read_only_environment_exception(env); + check_name_core(n, env); + } + + /** \brief Store new named object inside internal data-structures */ + void 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. + */ + object const & 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 object::null(); + } else { + return it->second; + } + } + + object const & get_object(name const & n, environment const & env) const { + object const & obj = get_object_core(n); + if (obj) + return obj; + else + throw unknown_object_exception(env, n); + } + /** \brief Return true if u >= v + k is implied by constraints \pre is_uvar(u) && is_uvar(v) @@ -115,9 +143,8 @@ struct environment::imp { } /** \brief Add a new universe variable */ - level add_var(name const & n, environment const & env) { - if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; })) - throw already_declared_universe_exception(env, n); + level add_uvar(name const & n, environment const & env) { + check_name(n, env); level r(n); m_uvars.push_back(r); return r; @@ -170,9 +197,9 @@ struct environment::imp { throw kernel_exception(env, "invalid universe declaration, universe variables can only be declared in top-level environments"); if (has_children()) throw read_only_environment_exception(env); - level r = add_var(n, env); + level r = add_uvar(n, env); add_constraints(r, l, 0); - m_objects.push_back(new uvar_declaration(n, l)); + register_named_object(mk_uvar_decl(n, l)); return r; } @@ -200,30 +227,6 @@ struct environment::imp { m_uvars.push_back(level()); } - /** \brief Display universe variable constraints */ - void display_uvars(std::ostream & out) const { - for (constraint const & c : m_constraints) { - out << uvar_name(std::get<0>(c)) << " >= " << uvar_name(std::get<1>(c)); - if (std::get<2>(c) >= 0) - out << " + " << std::get<2>(c); - out << "\n"; - } - } - - /** \brief Throw exception if environment or its ancestors already have an object with the given name. */ - void check_name_core(name const & n, environment const & env) { - if (has_parent()) - m_parent->check_name_core(n, env); - if (m_object_dictionary.find(n) != m_object_dictionary.end()) - throw already_declared_object_exception(env, n); - } - - void check_name(name const & n, environment const & env) { - if (has_children()) - throw read_only_environment_exception(env); - check_name_core(n, env); - } - /** \brief Throw an exception if \c t is not a type or type of \c v is not convertible to \c t. @@ -244,16 +247,10 @@ struct environment::imp { check_type(n, t, v, env); } - /** \brief Store new named object inside internal data-structures */ - void register_named_object(named_object * new_obj) { - m_objects.push_back(new_obj); - m_object_dictionary.insert(std::make_pair(new_obj->get_name(), new_obj)); - } - /** \brief Add new definition. */ void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) { check_new_definition(n, t, v, env); - register_named_object(new definition(n, t, v, opaque)); + register_named_object(mk_definition(n, t, v, opaque)); } /** @@ -263,52 +260,27 @@ struct environment::imp { void add_definition(name const & n, expr const & v, bool opaque, environment const & env) { check_name(n, env); expr v_t = infer_type(v, env); - register_named_object(new definition(n, v_t, v, opaque)); + register_named_object(mk_definition(n, v_t, v, opaque)); } /** \brief Add new theorem. */ void add_theorem(name const & n, expr const & t, expr const & v, environment const & env) { check_new_definition(n, t, v, env); - register_named_object(new theorem(n, t, v)); + register_named_object(mk_theorem(n, t, v)); } /** \brief Add new axiom. */ void add_axiom(name const & n, expr const & t, environment const & env) { check_name(n, env); infer_universe(t, env); - register_named_object(new axiom(n, t)); + register_named_object(mk_axiom(n, t)); } /** \brief Add new variable. */ void add_var(name const & n, expr const & t, environment const & env) { check_name(n, env); 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); - if (it == m_object_dictionary.end()) { - if (has_parent()) - return m_parent->get_object_ptr(n); - else - return nullptr; - } else { - return it->second; - } - } - - named_object const & get_object(name const & n, environment const & env) const { - named_object const * ptr = get_object_ptr(n); - if (ptr) - return *ptr; - else - throw unknown_object_exception(env, n); + register_named_object(mk_var_decl(n, t)); } unsigned get_num_objects(bool local) const { @@ -321,11 +293,11 @@ struct environment::imp { object const & get_object(unsigned i, bool local) const { if (local || !has_parent()) { - return *(m_objects[i]); + 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]); + return m_objects[i - num_parent_objects]; else return m_parent->get_object(i, false); } @@ -335,8 +307,10 @@ struct environment::imp { void display(std::ostream & out, environment const & env) const { if (has_parent()) m_parent->display(out, env); - for (object const * obj : m_objects) { - out << obj->pp(env) << "\n"; + for (object const & obj : m_objects) { + if (obj.has_name()) { + out << obj.keyword() << " " << obj.get_name() << "\n"; + } } } @@ -355,7 +329,6 @@ struct environment::imp { ~imp() { if (m_parent) m_parent->dec_children(); - std::for_each(m_objects.begin(), m_objects.end(), [](object * obj) { delete obj; }); } }; @@ -408,10 +381,6 @@ bool environment::is_ge(level const & l1, level const & l2) const { return m_imp->is_ge(l1, l2); } -void environment::display_uvars(std::ostream & out) const { - m_imp->display_uvars(out); -} - level environment::get_uvar(name const & n) const { return m_imp->get_uvar(n, *this); } @@ -436,18 +405,14 @@ void environment::add_var(name const & n, expr const & t) { m_imp->add_var(n, t, *this); } -void environment::add_anonymous_object(anonymous_object * o) { - m_imp->m_objects.push_back(o); +void environment::add_neutral_object(neutral_object_cell * o) { + m_imp->m_objects.push_back(mk_neutral(o)); } -named_object const & environment::get_object(name const & n) const { +object const & environment::get_object(name const & n) const { return m_imp->get_object(n, *this); } -named_object const * environment::get_object_ptr(name const & n) const { - return m_imp->get_object_ptr(n); -} - unsigned environment::get_num_objects(bool local) const { return m_imp->get_num_objects(local); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 705b7b2ac..2226346fe 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -73,9 +73,6 @@ public: */ bool is_ge(level const & l1, level const & l2) const; - /** \brief Display universal variables, and their constraints */ - void display_uvars(std::ostream & out) const; - /** \brief Return universal variable with the given name. Throw an exception if variable is not defined in this environment. @@ -112,22 +109,16 @@ public: \brief Register the given unanymous object in this environment. The environment assume the object ownership. */ - void add_anonymous_object(anonymous_object * o); + 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. */ - named_object const & get_object(name const & n) const; - - /** - \brief Return the object with the given name. - Return nullptr if there is no object with the given name. - */ - named_object const * get_object_ptr(name const & n) const; + object const & get_object(name const & n) const; /** \brief Return true iff the environment has an object with the given name */ - bool has_object(name const & n) const { return get_object_ptr(n) != nullptr; } + bool has_object(name const & n) const { return get_object(n); } /** \brief Iterator for Lean environment objects. */ class object_iterator { diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 093256569..b69a4df08 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -45,26 +45,13 @@ public: virtual char const * what() const noexcept { return "unknown object"; } }; -/** \brief Base class for already declared universe or object. */ +/** \brief Base class for already declared object. */ class already_declared_exception : public kernel_exception { name m_name; public: already_declared_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {} virtual ~already_declared_exception() noexcept {} name const & get_name() const { return m_name; } -}; - -/** \brief Exception used to report that a universe variable has already been declared in a given environment. */ -class already_declared_universe_exception : public already_declared_exception { -public: - already_declared_universe_exception(environment const & env, name const & n):already_declared_exception(env, n) {} - virtual char const * what() const noexcept { return "invalid universe variable declaration, it has already been declared"; } -}; - -/** \brief Exception used to report that an object has already been declared in a given environment. */ -class already_declared_object_exception : public already_declared_exception { -public: - already_declared_object_exception(environment const & env, name const & n):already_declared_exception(env, n) {} virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; } }; diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp index 0c8b03792..ad0280673 100644 --- a/src/kernel/normalize.cpp +++ b/src/kernel/normalize.cpp @@ -147,7 +147,7 @@ class normalize_fn { r = lookup(s, var_idx(a), k); break; case expr_kind::Constant: { - named_object const & obj = m_env.get_object(const_name(a)); + object const & obj = m_env.get_object(const_name(a)); if (obj.is_definition() && !obj.is_opaque()) { r = normalize(obj.get_value(), value_stack(), 0); } diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 24049e681..b9d3c0326 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -8,60 +8,141 @@ Author: Leonardo de Moura #include "environment.h" namespace lean { -object::~object() {} -void object::display(std::ostream & out, environment const & env) const { out << pp(env); } +neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {} +neutral_object_cell::~neutral_object_cell() {} +bool neutral_object_cell::has_name() const { return false; } +name const & neutral_object_cell::get_name() const { lean_unreachable(); return name::anonymous(); } +bool neutral_object_cell::has_cnstr_level() const { return false; } +level neutral_object_cell::get_cnstr_level() const { lean_unreachable(); return level(); } +bool neutral_object_cell::has_type() const { return false; } +expr const & neutral_object_cell::get_type() const { lean_unreachable(); return expr::null(); } +bool neutral_object_cell::is_definition() const { return false; } +bool neutral_object_cell::is_opaque() const { lean_unreachable(); return false; } +expr const & neutral_object_cell::get_value() const { lean_unreachable(); return expr::null(); } -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(); } +/** + \brief Named kernel objects. -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; } + \remark All nonneutral objects have names. +*/ +class named_object_cell : public object_cell { + name m_name; +public: + named_object_cell(object_kind k, name const & n):object_cell(k), m_name(n) {} + virtual ~named_object_cell() {} -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 { - expr_formatter & fmt = env.get_formatter(); - return fmt(keyword(), get_name(), get_type(), get_value()); -} - -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 { - expr_formatter & fmt = env.get_formatter(); - return fmt(keyword(), get_name(), get_type()); -} - -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; } + virtual bool has_name() const { return true; } + virtual name const & get_name() const { return m_name; } +}; + +/** + \brief Universe variable name declaration. +*/ +class uvar_declaration_object_cell : public named_object_cell { + level m_level; +public: + uvar_declaration_object_cell(name const & n, level const & l): + named_object_cell(object_kind::UVarDeclaration, n), m_level(l) {} + virtual ~uvar_declaration_object_cell() {} + + virtual bool has_cnstr_level() const { return true; } + virtual level get_cnstr_level() const { return m_level; } + + bool has_type() const { return false; } + expr const & get_type() const { lean_unreachable(); return expr::null(); } + bool is_definition() const { return false; } + bool is_opaque() const { lean_unreachable(); return false; } + expr const & get_value() const { lean_unreachable(); return expr::null(); } + + virtual char const * keyword() const { return "Universe"; } +}; + +/** + \brief Named (and typed) kernel objects. +*/ +class named_typed_object_cell : public named_object_cell { + expr m_type; +public: + named_typed_object_cell(object_kind k, name const & n, expr const & t): + named_object_cell(k, n), m_type(t) {} + virtual ~named_typed_object_cell() {} + + virtual bool has_type() const { return true; } + virtual expr const & get_type() const { return m_type; } + + virtual bool has_cnstr_level() const { return false; } + virtual level get_cnstr_level() const { lean_unreachable(); return level(); } +}; + +/** + \brief Base class for Axioms and Variable declarations. +*/ +class postulate_object_cell : public named_typed_object_cell { +public: + postulate_object_cell(name const & n, expr const & t): + named_typed_object_cell(object_kind::Postulate, n, t) {} + + bool is_definition() const { return false; } + bool is_opaque() const { lean_unreachable(); return false; } + expr const & get_value() const { lean_unreachable(); return expr::null(); } +}; + +/** + \brief Axioms +*/ +class axiom_object_cell : public postulate_object_cell { +public: + axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {} + virtual char const * keyword() const { return "Axiom"; } +}; + +/** + \brief Variable (aka constant) declaration +*/ +class variable_decl_object_cell : public postulate_object_cell { +public: + variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {} + virtual char const * keyword() const { return "Variable"; } +}; + +/** + \brief Base class for definitions: theorems and definitions. +*/ +class definition_object_cell : public named_typed_object_cell { + expr m_value; + bool m_opaque; +public: + definition_object_cell(name const & n, expr const & t, expr const & v, bool opaque): + named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque) {} + virtual ~definition_object_cell() {} + + bool is_definition() const { return true; } + bool is_opaque() const { return m_opaque; } + expr const & get_value() const { return m_value; } + virtual char const * keyword() const { return "Definition"; } +}; + +/** + \brief Theorems +*/ +class theorem_object_cell : public definition_object_cell { +public: + theorem_object_cell(name const & n, expr const & t, expr const & v): + definition_object_cell(n, t, v, true) {} + virtual char const * keyword() const { return "Definition"; } +}; + +object mk_uvar_decl(name const & n, level const & l) { return object(new uvar_declaration_object_cell(n, l)); } +object mk_definition(name const & n, expr const & t, expr const & v, bool opaque) { return object(new definition_object_cell(n, t, v, opaque)); } +object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); } +object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); } +object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); } + +static object g_null_object; + +object const & object::null() { + lean_assert(!g_null_object); + return g_null_object; +} } diff --git a/src/kernel/object.h b/src/kernel/object.h index 45a0c91b3..74d0da826 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "expr.h" +#include "rc.h" /* Kernel objects. @@ -14,19 +15,17 @@ Author: Leonardo de Moura frontend may need to create new objects for bookkeeping. */ namespace lean { -class environment; +enum class object_kind { UVarDeclaration, Definition, Postulate, Neutral }; -/** - \brief Abstract class used to represent kernel objects (i.e., - definitions, theorems, axioms, recursive definitions, etc) -*/ -class object { -protected: +class object_cell { + void dealloc() { delete this; } + MK_LEAN_RC(); + object_kind m_kind; public: - object() {} - object(object const & o) = delete; - object & operator=(object const & o) = delete; - virtual ~object(); + object_cell(object_kind k):m_rc(1), m_kind(k) {} + virtual ~object_cell() {} + + object_kind kind() const { return m_kind; } /** \brief Return the keyword used to define this object in a Lean @@ -34,44 +33,44 @@ public: */ 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 Has constraint level associated with it (for universal variables). */ + virtual bool has_cnstr_level() const = 0; + /** \brief Return the constraint level associated with the object. */ + virtual level get_cnstr_level() 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. + \brief Neutral objects are mainly used for bookkeeping in + kernel frontends. */ -class anonymous_object : public object { +class neutral_object_cell : public object_cell { public: - virtual ~anonymous_object(); + neutral_object_cell(); + virtual ~neutral_object_cell(); virtual bool has_name() const; virtual name const & get_name() const; + virtual bool has_cnstr_level() const; + virtual level get_cnstr_level() const; + virtual bool has_type() const; virtual expr const & get_type() const; @@ -81,91 +80,53 @@ public: }; /** - \brief Named (and typed) kernel objects. + \brief Environment objects: definitions, theorems, axioms, universe + variable declarations, etc. */ -class named_object : public object { - name m_name; - expr m_type; +class object { + object_cell * m_ptr; + explicit object(object_cell * ptr):m_ptr(ptr) {} public: - named_object(name const & n, expr const & t); - virtual ~named_object(); + object():m_ptr(nullptr) {} + object(object const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + object(object && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~object() { if (m_ptr) m_ptr->dec_ref(); } - virtual bool has_name() const; - virtual name const & get_name() const; + static object const & null(); - 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; + friend void swap(object & a, object & b) { std::swap(a.m_ptr, b.m_ptr); } + + void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; } + + object & operator=(object const & s) { LEAN_COPY_REF(object, s); } + object & operator=(object && s) { LEAN_MOVE_REF(object, s); } + + operator bool() const { return m_ptr != nullptr; } + + object_kind kind() const { return m_ptr->kind(); } + + friend object mk_uvar_decl(name const & n, level const & l); + friend object mk_definition(name const & n, expr const & t, expr const & v, bool opaque); + friend object mk_theorem(name const & n, expr const & t, expr const & v); + friend object mk_axiom(name const & n, expr const & t); + friend object mk_var_decl(name const & n, expr const & t); + friend object mk_neutral(neutral_object_cell * c); + + char const * keyword() const { return m_ptr->keyword(); } + bool has_name() const { return m_ptr->has_name(); } + name const & get_name() const { return m_ptr->get_name(); } + bool has_type() const { return m_ptr->has_type(); } + bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); } + level get_cnstr_level() const { return m_ptr->get_cnstr_level(); } + expr const & get_type() const { return m_ptr->get_type(); } + bool is_definition() const { return m_ptr->is_definition(); } + bool is_opaque() const { return m_ptr->is_opaque(); } + expr const & get_value() const { return m_ptr->get_value(); } }; +object mk_uvar_decl(name const & n, level const & l); +object mk_definition(name const & n, expr const & t, expr const & v, bool opaque); +object mk_theorem(name const & n, expr const & t, expr const & v); +object mk_axiom(name const & n, expr const & t); +object mk_var_decl(name const & n, expr const & t); +inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); } } diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 877ec68df..7273c1c64 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -41,7 +41,7 @@ static void tst1() { std::cout << "tst1 checkpoint" << std::endl; level o = env.add_uvar("o", w + 1); lean_assert(!env.has_children()); - env.display_uvars(std::cout); + std::cout << env; } static environment mk_child() { @@ -55,7 +55,7 @@ static void tst2() { lean_assert(child.has_parent()); lean_assert(!child.has_children()); environment parent = child.parent(); - parent.display_uvars(std::cout); + std::cout << parent; lean_assert(parent.has_children()); std::cout << "uvar: " << child.get_uvar("u") << "\n"; } @@ -179,17 +179,17 @@ static void tst8() { env2.add_var("d", Type()); env2.add_var("e", Type()); unsigned counter = 0; - std::for_each(env2.begin_local_objects(), env2.end_local_objects(), [&](object const & obj) { std::cout << obj.pp(env2) << "\n"; counter++; }); + std::for_each(env2.begin_local_objects(), env2.end_local_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); lean_assert(counter == 3); std::cout << "=======================\n"; counter = 0; - std::for_each(env2.begin_objects(), env2.end_objects(), [&](object const & obj) { std::cout << obj.pp(env2) << "\n"; counter++; }); + std::for_each(env2.begin_objects(), env2.end_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); lean_assert(counter == 5); environment env3 = env2.mk_child(); env3.add_var("f", Type() >> Type()); std::cout << "=======================\n"; counter = 0; - std::for_each(env3.begin_objects(), env3.end_objects(), [&](object const & obj) { std::cout << obj.pp(env3) << "\n"; counter++; }); + std::for_each(env3.begin_objects(), env3.end_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); lean_assert(counter == 6); } @@ -199,7 +199,7 @@ static void tst9() { env.add_uvar("u1", level()); env.add_uvar("u2", level()); env.add_uvar("u1", level("u2")); - } catch (already_declared_universe_exception & ex) { + } catch (already_declared_exception & ex) { std::cout << ex.what() << "\n"; level l = ex.get_environment().get_uvar(ex.get_name()); std::cout << l << "\n"; diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index af367a621..9f51fe7c2 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -19,7 +19,7 @@ static void tst1() { std::cout << pp(max(l1 + 8, max(l2 + 2, l3 + 20))) << "\n"; std::cout << pp(level()) << "\n"; std::cout << pp(level()+1) << "\n"; - env.display_uvars(std::cout); + std::cout << env; lean_assert(env.is_ge(l4 + 10, l3 + 30)); lean_assert(!env.is_ge(l4 + 9, l3 + 30)); } @@ -74,7 +74,7 @@ static void tst4() { lean_assert(env.is_ge(max(l6, l5), max(l2+3, l1+1))); lean_assert(!env.is_ge(max(l6, l5), max(l2, l1+1)+3)); lean_assert(env.is_ge(max(l6+1, l5), max(l2, l1+1)+3)); - env.display_uvars(std::cout); + std::cout << env; } static void tst5() { diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp index c44a2698a..cfe20e91a 100644 --- a/src/tests/kernel/type_check.cpp +++ b/src/tests/kernel/type_check.cpp @@ -181,7 +181,7 @@ static void tst10() { expr prop = Eq(t1, t2); expr proof = Refl(Int, t1); env.add_theorem("simp_eq", prop, proof); - std::cout << env.get_object("simp_eq").pp(env) << "\n"; + std::cout << env.get_object("simp_eq").get_name() << "\n"; } static void tst11() {