From f3202772483fdb0eebfeb2ec9125f48c4da035c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Apr 2014 12:48:21 -0700 Subject: [PATCH] feat(kernel/definition): add mk_definition procedure that automatically computes the weight Signed-off-by: Leonardo de Moura --- src/kernel/definition.cpp | 14 ++++++++++++++ src/kernel/definition.h | 6 +++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/kernel/definition.cpp b/src/kernel/definition.cpp index 1227a1b63..3b4e3ff94 100644 --- a/src/kernel/definition.cpp +++ b/src/kernel/definition.cpp @@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/definition.h" +#include "kernel/environment.h" +#include "kernel/for_each_fn.h" namespace lean { static serializer & operator<<(serializer & s, param_names const & ps) { return write_list(s, ps); } @@ -91,6 +93,18 @@ void definition::write(serializer & s) const { m_ptr->write(s); } definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) { return definition(new definition::cell(n, params, cs, t, false, v, opaque, weight, mod_idx, use_conv_opt)); } +definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt) { + unsigned w = 0; + for_each(v, [&](expr const & e, unsigned) { + if (is_constant(e)) { + auto d = env.find(const_name(e)); + if (d && d->get_weight() > w) + w = d->get_weight(); + } + return true; + }); + return mk_definition(n, params, cs, t, v, opaque, w+1, mod_idx, use_conv_opt); +} definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v) { return definition(new definition::cell(n, params, cs, t, true, v, true, 0, 0, false)); } diff --git a/src/kernel/definition.h b/src/kernel/definition.h index c1800b7b7..a52dd106c 100644 --- a/src/kernel/definition.h +++ b/src/kernel/definition.h @@ -68,7 +68,10 @@ public: module_idx get_module_idx() const; bool use_conv_opt() const; - friend definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt); + friend definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, + expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt); + friend definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, + unsigned weight, module_idx mod_idx, bool use_conv_opt); friend definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v); friend definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); friend definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); @@ -81,6 +84,7 @@ inline optional some_definition(definition const & o) { return optio inline optional some_definition(definition && o) { return optional(std::forward(o)); } definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true); +definition mk_definition(environment const & env, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true); definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v); definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);