max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/aux_definition): add helper functions for creating auxiliary definitions

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-22 17:31:29 -07:00
parent d8447b4c53
commit 3de9509644
3 changed files with 194 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/CMakeLists.txt
View file

@ -15,6 +15,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
inductive.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
aux_definition.cpp
# Legacy -- The following files will be eventually deleted
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp

167
src/library/aux_definition.cpp Normal file
View file

@ -0,0 +1,167 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "kernel/type_checker.h"
#include "kernel/replace_fn.h"
#include "library/locals.h"
#include "library/module.h"
#include "library/trace.h"
#include "library/aux_definition.h"
namespace lean {
struct mk_aux_definition_fn {
type_context & m_ctx;
name m_prefix;
unsigned m_next_idx;
name_set m_found_univ_params;
name_map<level> m_univ_meta_to_param;
name_map<level> m_univ_meta_to_param_inv;
name_set m_found_local;
name_map<expr> m_meta_to_param;
name_map<expr> m_meta_to_param_inv;
buffer<name> m_level_params;
buffer<expr> m_params;
mk_aux_definition_fn(type_context & ctx):
m_ctx(ctx),
m_prefix("_aux_param"),
m_next_idx(0) {}
level collect(level const & l) {
return replace(l, [&](level const & l) {
if (is_meta(l)) {
name const & id = meta_id(l);
if (auto r = m_univ_meta_to_param.find(id)) {
return some_level(*r);
} else {
name n = m_prefix.append_after(m_next_idx);
m_next_idx++;
level new_r = mk_param_univ(n);
m_univ_meta_to_param.insert(id, new_r);
m_univ_meta_to_param_inv.insert(n, l);
m_level_params.push_back(n);
return some_level(new_r);
}
} else if (is_param(l)) {
name const & id = param_id(l);
if (!m_found_univ_params.contains(id)) {
m_found_univ_params.insert(id);
m_level_params.push_back(id);
}
}
return none_level();
});
}
levels collect(levels const & ls) {
bool modified = false;
buffer<level> r;
for (level const & l : ls) {
level new_l = collect(l);
if (new_l != l) modified = true;
r.push_back(new_l);
}
if (!modified)
return ls;
else
return to_list(r);
}
expr collect(expr const & e) {
return replace(e, [&](expr const & e, unsigned) {
if (is_metavar(e)) {
name const & id = mlocal_name(e);
if (auto r = m_meta_to_param.find(id)) {
return some_expr(*r);
} else {
expr type = m_ctx.infer(e);
expr x = m_ctx.push_local("_x", type);
m_meta_to_param.insert(id, x);
m_meta_to_param_inv.insert(mlocal_name(x), e);
m_params.push_back(x);
return some_expr(x);
}
} else if (is_local(e)) {
name const & id = mlocal_name(e);
if (!m_found_local.contains(id)) {
m_found_local.insert(id);
m_params.push_back(e);
}
} else if (is_sort(e)) {
return some_expr(update_sort(e, collect(sort_level(e))));
} else if (is_constant(e)) {
return some_expr(update_constant(e, collect(const_levels(e))));
}
return none_expr();
});
}
/* Collect (and sort) dependencies of collected parameters */
void collect_and_normalize_dependencies(buffer<expr> & norm_params) {
name_map<expr> new_types;
for (unsigned i = 0; i < m_params.size(); i++) {
expr x = m_params[i];
expr new_type = collect(m_ctx.instantiate_mvars(m_ctx.infer(x)));
new_types.insert(mlocal_name(x), new_type);
}
local_context const & lctx = m_ctx.lctx();
std::sort(m_params.begin(), m_params.end(), [&](expr const & l1, expr const & l2) {
return lctx.get_local_decl(l1)->get_idx() < lctx.get_local_decl(l2)->get_idx();
});
for (unsigned i = 0; i < m_params.size(); i++) {
expr x = m_params[i];
expr type = *new_types.find(mlocal_name(x));
expr new_type = replace_locals(type, i, m_params.data(), norm_params.data());
expr new_param = m_ctx.push_local(local_pp_name(x), new_type, local_info(x));
norm_params.push_back(new_param);
}
}
pair<environment, expr> operator()(name const & c, expr const & type, expr const & value) {
expr new_type = collect(m_ctx.instantiate_mvars(type));
expr new_value = collect(m_ctx.instantiate_mvars(value));
buffer<expr> norm_params;
collect_and_normalize_dependencies(norm_params);
new_type = replace_locals(new_type, m_params, norm_params);
new_value = replace_locals(new_value, m_params, norm_params);
expr def_type = m_ctx.mk_pi(norm_params, new_type);
expr def_value = m_ctx.mk_lambda(norm_params, new_value);
bool use_conv_opt = true;
environment const & env = m_ctx.env();
declaration d = mk_definition_inferring_trusted(env, c, to_list(m_level_params), def_type, def_value, use_conv_opt);
environment new_env = module::add(env, check(env, d));
buffer<level> ls;
for (name const & n : m_level_params) {
if (level const * l = m_univ_meta_to_param_inv.find(n))
ls.push_back(*l);
else
ls.push_back(mk_param_univ(n));
}
buffer<expr> ps;
for (expr const & x : m_params) {
if (expr const * m = m_meta_to_param_inv.find(mlocal_name(x)))
ps.push_back(*m);
else
ps.push_back(x);
}
expr r = mk_app(mk_constant(c, to_list(ls)), ps);
return mk_pair(new_env, r);
}
};
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & type, expr const & value) {
aux_type_context ctx(env, options(), mctx, lctx, transparency_mode::All);
return mk_aux_definition_fn(ctx.get())(c, type, value);
}
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & value) {
aux_type_context ctx(env, options(), mctx, lctx, transparency_mode::All);
expr type = ctx->infer(value);
return mk_aux_definition_fn(ctx.get())(c, type, value);
}
}

26
src/library/aux_definition.h Normal file
View file

@ -0,0 +1,26 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/type_context.h"
namespace lean {
/** \brief Create an auxiliary definition with name `c` where `type` and `value` may contain local constants and
meta-variables. This function collects all dependencies (universe parameters, universe metavariables,
local constants and metavariables). The result is the updated environment and an expression of the form
(c.{l_1 ... l_n} a_1 ... a_m)
where l_i's and a_j's are the collected dependencies.
The function also computes whether the new definition should be tagged as trusted or not.
The updated environment is an extension of ctx.env() */
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & type, expr const & value);
/** \brief Similar to mk_aux_definition, but the type of value is inferred using ctx. */
pair<environment, expr> mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx,
name const & c, expr const & value);
}