feat(kernel): add weight to kernel definitions

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

src/kernel/environment.cpp

@@ -9,13 +9,13 @@ Author: Leonardo de Moura
 #include <atomic>
 #include <unordered_map>
 #include "util/safe_arith.h"
+#include "kernel/for_each.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/normalizer.h"
 
 namespace lean {
-
 /** \brief Implementation of the Lean environment. */
 struct environment::imp {
     // Remark: only named objects are stored in the dictionary.
@@ -32,6 +32,20 @@ struct environment::imp {
     object_dictionary                    m_object_dictionary;
     type_checker                         m_type_checker;
 
+    unsigned get_max_weight(expr const & e) {
+        unsigned w = 0;
+        auto proc = [&](expr const & c, unsigned) {
+            if (is_constant(c)) {
+                object const & obj = get_object_core(const_name(c));
+                if (obj)
+                    w = std::max(w, obj.get_weight());
+            }
+        };
+        for_each_fn<decltype(proc)> visitor(proc);
+        visitor(e);
+        return w;
+    }
+
     /**
        \brief Return true iff this environment has children.
 
@@ -258,7 +272,8 @@ struct environment::imp {
     /** \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(mk_definition(n, t, v, opaque));
+        unsigned w = get_max_weight(v) + 1;
+        register_named_object(mk_definition(n, t, v, opaque, w));
     }
 
     /**
@@ -268,7 +283,8 @@ struct environment::imp {
     void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
         check_name(n, env);
         expr v_t = m_type_checker.infer_type(v);
-        register_named_object(mk_definition(n, v_t, v, opaque));
+        unsigned w = get_max_weight(v) + 1;
+        register_named_object(mk_definition(n, v_t, v, opaque, w));
     }
 
     /** \brief Add new theorem. */

src/kernel/object.cpp

@@ -131,17 +131,19 @@ public:
    \brief Base class for definitions: theorems and definitions.
 */
 class definition_object_cell : public named_typed_object_cell {
-    expr m_value;
-    bool m_opaque;
+    expr     m_value;
+    bool     m_opaque;
+    unsigned m_weight;
 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) {}
+    definition_object_cell(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight):
+        named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque), m_weight(weight) {}
     virtual ~definition_object_cell() {}
 
-    virtual bool is_definition() const     { return true; }
-    virtual bool is_opaque() const         { return m_opaque; }
-    virtual expr get_value() const { return m_value; }
+    virtual bool is_definition() const   { return true; }
+    virtual bool is_opaque() const       { return m_opaque; }
+    virtual expr get_value() const       { return m_value; }
     virtual char const * keyword() const { return "Definition"; }
+    virtual unsigned get_weight() const  { return m_weight; }
 };
 
 /**
@@ -150,13 +152,13 @@ public:
 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) {}
+        definition_object_cell(n, t, v, true, 0) {}
     virtual char const * keyword() const { return "Theorem"; }
     virtual bool is_theorem() const { return true; }
 };
 
 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_definition(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight) { return object(new definition_object_cell(n, t, v, opaque, weight)); }
 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)); }

src/kernel/object.h

@@ -62,6 +62,8 @@ public:
     virtual bool is_var_decl() const { return false; }
 
     virtual bool in_builtin_set(expr const &) const { return false; }
+
+    virtual unsigned get_weight() const { return 0; }
 };
 
 /**
@@ -101,7 +103,7 @@ public:
     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_definition(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight);
     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);
@@ -119,6 +121,7 @@ public:
     bool is_definition() const { return m_ptr->is_definition(); }
     bool is_opaque() const { return m_ptr->is_opaque(); }
     expr get_value() const { return m_ptr->get_value(); }
+    unsigned get_weight() const { return m_ptr->get_weight(); }
 
     bool is_axiom() const { return m_ptr->is_axiom(); }
     bool is_theorem() const { return m_ptr->is_theorem(); }
@@ -132,7 +135,7 @@ public:
 object mk_uvar_decl(name const & n, level const & l);
 object mk_builtin(expr const & v);
 object mk_builtin_set(expr const & r);
-object mk_definition(name const & n, expr const & t, expr const & v, bool opaque);
+object mk_definition(name const & n, expr const & t, expr const & v, bool opaque, unsigned weight);
 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);

src/tests/kernel/environment.cpp

@@ -207,6 +207,22 @@ static void tst9() {
     }
 }
 
+static void tst10() {
+    environment env;
+    import_all(env);
+    env.add_definition("a", Int, iVal(1));
+    lean_assert(env.get_object("a").get_weight() == 1);
+    expr a = Const("a");
+    expr b = Const("b");
+    expr c = Const("c");
+    env.add_definition("b", Int, iAdd(a, a));
+    lean_assert(env.get_object("b").get_weight() == 2);
+    env.add_definition("c", Int, iAdd(a, b));
+    lean_assert(env.get_object("c").get_weight() == 3);
+    env.add_definition("d", Int, iAdd(b, b));
+    lean_assert(env.get_object("d").get_weight() == 3);
+}
+
 int main() {
     enable_trace("is_convertible");
     tst1();
@@ -218,5 +234,6 @@ int main() {
     tst7();
     tst8();
     tst9();
+    tst10();
     return has_violations() ? 1 : 0;
 }