From 078380567124c988ce0b167f931ab89cd07592ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Oct 2013 14:50:08 -0700 Subject: [PATCH] feat(kernel): add weight to kernel definitions Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 22 +++++++++++++++++++--- src/kernel/object.cpp | 20 +++++++++++--------- src/kernel/object.h | 7 +++++-- src/tests/kernel/environment.cpp | 17 +++++++++++++++++ 4 files changed, 52 insertions(+), 14 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 7cce8e1cf..4aa220cc2 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -9,13 +9,13 @@ Author: Leonardo de Moura #include #include #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 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. */ diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 8139bdd5f..9bd6c14f4 100644 --- a/src/kernel/object.cpp +++ b/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)); } diff --git a/src/kernel/object.h b/src/kernel/object.h index d03ef1183..3daf7fdf0 100644 --- a/src/kernel/object.h +++ b/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); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 79d7e38c0..f9254a993 100644 --- a/src/tests/kernel/environment.cpp +++ b/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; }