michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/definition): add mk_definition procedure that automatically computes the weight

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-28 12:48:21 -07:00
parent 6c3a796119
commit f320277248
2 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/definition.cpp
View file

@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include "kernel/definition.h" #include "kernel/definition.h"
#include "kernel/environment.h"
#include "kernel/for_each_fn.h"
namespace lean { namespace lean {
static serializer & operator<<(serializer & s, param_names const & ps) { return write_list<name>(s, ps); } static serializer & operator<<(serializer & s, param_names const & ps) { return write_list<name>(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) { 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)); 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) { 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)); return definition(new definition::cell(n, params, cs, t, true, v, true, 0, 0, false));
} }

6
src/kernel/definition.h
View file

@ -68,7 +68,10 @@ public:
module_idx get_module_idx() const; module_idx get_module_idx() const;
bool use_conv_opt() 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_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_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); 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<definition> some_definition(definition const & o) { return optio
inline optional<definition> some_definition(definition && o) { return optional<definition>(std::forward<definition>(o)); } inline optional<definition> some_definition(definition && o) { return optional<definition>(std::forward<definition>(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(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_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_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); definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);