Refactor kernel objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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); }

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<name, named_object *, name_hash, name_eq> object_dictionary;
+    typedef std::unordered_map<name, object, name_hash, name_eq> object_dictionary;
     typedef std::tuple<level, level, int> constraint;
     // Universe variable management
     std::vector<constraint>              m_constraints;
@@ -47,7 +30,7 @@ struct environment::imp {
     std::atomic<unsigned>                m_num_children;
     std::shared_ptr<imp>                 m_parent;
     // Object management
-    std::vector<object*>                 m_objects;
+    std::vector<object>                  m_objects;
     object_dictionary                    m_object_dictionary;
     // Expression formatter && locator
     std::shared_ptr<expr_formatter>      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) {
+    level add_uvar(name const & n, environment const & env) {
-        if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; }))
+        check_name(n, env);
-            throw already_declared_universe_exception(env, n);
         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));
+        register_named_object(mk_var_decl(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);
     }
 
     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) {
+        for (object const & obj : m_objects) {
-            out << obj->pp(env) << "\n";
+            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) {
+void environment::add_neutral_object(neutral_object_cell * o) {
-    m_imp->m_objects.push_back(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);
 }

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;
+    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;
 
     /** \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 {

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"; }
 };
 

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);
             }

src/kernel/object.cpp

@@ -8,60 +8,141 @@ Author: Leonardo de Moura
 #include "environment.h"
 
 namespace lean {
-object::~object() {}
+neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
-void object::display(std::ostream & out, environment const & env) const { out << pp(env); }
+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; }
+   \brief Named kernel objects.
-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) {}
+   \remark All nonneutral objects have names.
-named_object::~named_object() {}
+*/
-bool         named_object::has_name() const      { return true; }
+class named_object_cell : public object_cell {
-name const & named_object::get_name() const      { return m_name; }
+    name m_name;
-bool         named_object::has_type() const      { return true; }
+public:
-expr const & named_object::get_type() const      { return m_type; }
+    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";
+    virtual bool has_name() const          { return true; }
-definition::definition(name const & n, expr const & t, expr const & v, bool opaque):named_object(n, t), m_value(v), m_opaque(opaque) {}
+    virtual name const & get_name() const  { return m_name; }
-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; }
+   \brief Universe variable name declaration.
-expr const & definition::get_value() const     { return m_value; }
+*/
-format       definition::pp(environment const & env) const {
+class uvar_declaration_object_cell : public named_object_cell {
-    expr_formatter & fmt = env.get_formatter();
+    level m_level;
-    return fmt(keyword(), get_name(), get_type(), get_value());
+public:
-}
+    uvar_declaration_object_cell(name const & n, level const & l):
-
+        named_object_cell(object_kind::UVarDeclaration, n), m_level(l) {}
-char const * theorem::g_keyword = "Theorem";
+    virtual ~uvar_declaration_object_cell() {}
-theorem::theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {}
+
-theorem::~theorem() {}
+    virtual bool has_cnstr_level() const   { return true; }
-char const * theorem::keyword() const { return g_keyword; }
+    virtual level get_cnstr_level() const  { return m_level; }
-
+
-fact::fact(name const & n, expr const & t):named_object(n, t) {}
+    bool has_type() const          { return false; }
-fact::~fact() {}
+    expr const & get_type() const  { lean_unreachable(); return expr::null(); }
-bool         fact::is_definition() const { return false; }
+    bool is_definition() const     { return false; }
-bool         fact::is_opaque() const     { lean_unreachable(); return false; }
+    bool is_opaque() const         { lean_unreachable(); return false; }
-expr const & fact::get_value() const     { lean_unreachable(); return expr::null(); }
+    expr const & get_value() const { lean_unreachable(); return expr::null(); }
-format fact::pp(environment const & env) const {
+
-    expr_formatter & fmt = env.get_formatter();
+    virtual char const * keyword() const { return "Universe"; }
-    return fmt(keyword(), get_name(), get_type());
+};
-}
+
-
+/**
-char const * axiom::g_keyword = "Axiom";
+   \brief Named (and typed) kernel objects.
-axiom::axiom(name const & n, expr const & t):fact(n, t) {}
+*/
-axiom::~axiom() {}
+class named_typed_object_cell : public named_object_cell {
-char const * axiom::keyword() const { return g_keyword; }
+    expr m_type;
-
+public:
-char const * variable::g_keyword = "Variable";
+    named_typed_object_cell(object_kind k, name const & n, expr const & t):
-variable::variable(name const & n, expr const & t):fact(n, t) {}
+        named_object_cell(k, n), m_type(t) {}
-variable::~variable() {}
+    virtual ~named_typed_object_cell() {}
-char const * variable::keyword() const { return g_keyword; }
+
+    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;
+}
 }
 

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 };
 
-/**
+class object_cell {
-   \brief Abstract class used to represent kernel objects (i.e.,
+    void dealloc() { delete this; }
-   definitions, theorems, axioms, recursive definitions, etc)
+    MK_LEAN_RC();
-*/
+    object_kind m_kind;
-class object {
-protected:
 public:
-    object() {}
+    object_cell(object_kind k):m_rc(1), m_kind(k) {}
-    object(object const & o) = delete;
+    virtual ~object_cell() {}
-    object & operator=(object const & o) = delete;
+
-    virtual ~object();
+    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 {
+class object {
-    name m_name;
+    object_cell * m_ptr;
-    expr m_type;
+    explicit object(object_cell * ptr):m_ptr(ptr) {}
 public:
-    named_object(name const & n, expr const & t);
+    object():m_ptr(nullptr) {}
-    virtual ~named_object();
+    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;
+    static object const & null();
-    virtual name const & get_name() const;
 
-    virtual bool has_type() const;
+    friend void swap(object & a, object & b) { std::swap(a.m_ptr, b.m_ptr); }
-    virtual expr const & get_type() const;
+
-};
+    void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; }
-
+
-/**
+    object & operator=(object const & s) { LEAN_COPY_REF(object, s); }
-   \brief Non-recursive definitions.
+    object & operator=(object && s) { LEAN_MOVE_REF(object, s); }
-*/
+
-class definition : public named_object {
+    operator bool() const { return m_ptr != nullptr; }
-    expr m_value;
+
-    bool m_opaque; // Opaque definitions are ignored by definitional equality.
+    object_kind kind() const { return m_ptr->kind(); }
-public:
+
-    definition(name const & n, expr const & t, expr const & v, bool opaque);
+    friend object mk_uvar_decl(name const & n, level const & l);
-    virtual ~definition();
+    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);
-    static char const * g_keyword;
+    friend object mk_axiom(name const & n, expr const & t);
-    virtual char const * keyword() const;
+    friend object mk_var_decl(name const & n, expr const & t);
-
+    friend object mk_neutral(neutral_object_cell * c);
-    virtual bool is_definition() const;
+
-    virtual bool is_opaque() const;
+    char const * keyword() const { return m_ptr->keyword(); }
-    virtual expr const & get_value() const;
+    bool has_name() const { return m_ptr->has_name(); }
-
+    name const & get_name() const { return m_ptr->get_name(); }
-    virtual format pp(environment const & env) const;
+    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(); }
-   \brief A theorem is essentially an opaque definition.
+    bool is_definition() const { return m_ptr->is_definition(); }
-*/
+    bool is_opaque() const { return m_ptr->is_opaque(); }
-class theorem : public definition {
+    expr const & get_value() const { return m_ptr->get_value(); }
-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;
 };
+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); }
 }

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";

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() {

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() {