From 3de9509644e6112cfbb2d8e2a205e2ff5ed74bcc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Aug 2016 17:31:29 -0700 Subject: [PATCH] feat(library/aux_definition): add helper functions for creating auxiliary definitions --- src/library/CMakeLists.txt | 1 + src/library/aux_definition.cpp | 167 +++++++++++++++++++++++++++++++++ src/library/aux_definition.h | 26 +++++ 3 files changed, 194 insertions(+) create mode 100644 src/library/aux_definition.cpp create mode 100644 src/library/aux_definition.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index fcd80a53f9..a646dafb09 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -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 diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp new file mode 100644 index 0000000000..5ff758b173 --- /dev/null +++ b/src/library/aux_definition.cpp @@ -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 +#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 m_univ_meta_to_param; + name_map m_univ_meta_to_param_inv; + name_set m_found_local; + name_map m_meta_to_param; + name_map m_meta_to_param_inv; + buffer m_level_params; + buffer 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 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 & norm_params) { + name_map 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 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 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 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 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 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 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); +} +} diff --git a/src/library/aux_definition.h b/src/library/aux_definition.h new file mode 100644 index 0000000000..6884db9688 --- /dev/null +++ b/src/library/aux_definition.h @@ -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 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 mk_aux_definition(environment const & env, metavar_context const & mctx, local_context const & lctx, + name const & c, expr const & value); +}