From f82658f21348a6f7afe49db7f538ce1fc81999ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 15:09:24 -0700 Subject: [PATCH] feat(library): add helper functions for 'updating' declarations Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 3 +- src/library/scope.cpp | 11 ++---- src/library/update_declaration.cpp | 56 ++++++++++++++++++++++++++++++ src/library/update_declaration.h | 16 +++++++++ 4 files changed, 77 insertions(+), 9 deletions(-) create mode 100644 src/library/update_declaration.cpp create mode 100644 src/library/update_declaration.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 67944b894..b7041f1a8 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -2,7 +2,8 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp kernel_bindings.cpp io_state_stream.cpp bin_app.cpp resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp - private.cpp placeholder.cpp aliases.cpp scope.cpp) + private.cpp placeholder.cpp aliases.cpp scope.cpp + update_declaration.cpp) # fo_unify.cpp hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/scope.cpp b/src/library/scope.cpp index 6c7015e93..923ead9c5 100644 --- a/src/library/scope.cpp +++ b/src/library/scope.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/scope.h" #include "library/module.h" +#include "library/update_declaration.h" namespace lean { namespace scope { @@ -181,14 +182,8 @@ public: new_type = Pi(new_type, var_deps); new_value = Fun(new_value, var_deps); add_decl_info(d.get_name(), level_deps, var_deps, new_type); - if (d.is_definition()) { - declaration new_d = mk_definition(d.get_name(), new_ls, new_type, new_value, d.is_opaque(), - d.get_weight(), d.get_module_idx(), d.use_conv_opt()); - m_env = add(m_env, check(m_env, new_d)); - } else { - declaration new_d = mk_theorem(d.get_name(), new_ls, new_type, new_value); - m_env = add(m_env, check(m_env, new_d)); - } + declaration new_d = update_declaration(d, new_ls, new_type, new_value); + m_env = add(m_env, check(m_env, new_d)); } }; diff --git a/src/library/update_declaration.cpp b/src/library/update_declaration.cpp new file mode 100644 index 000000000..00f5ebfb8 --- /dev/null +++ b/src/library/update_declaration.cpp @@ -0,0 +1,56 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/update_declaration.h" + +namespace lean { +static declaration update_declaration(declaration d, optional const & ps, + optional const & type, optional const & value) { + level_param_names _ps = ps ? *ps : d.get_params(); + expr _type = type ? *type : d.get_type(); + expr _value; + if (d.is_definition()) { + _value = value ? *value : d.get_value(); + } else { + lean_assert(!value); + } + if (d.is_var_decl()) { + if (is_eqp(d.get_type(), _type) && is_eqp(d.get_params(), _ps)) + return d; + if (d.is_axiom()) + return mk_axiom(d.get_name(), _ps, _type); + else + return mk_var_decl(d.get_name(), _ps, _type); + } else { + if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_params(), _ps)) + return d; + if (d.is_theorem()) + return mk_theorem(d.get_name(), _ps, _type, _value); + else + return mk_definition(d.get_name(), _ps, _type, _value, d.is_opaque(), + d.get_weight(), d.get_module_idx(), d.use_conv_opt()); + } +} + +declaration update_declaration_univ_params(declaration const & d, level_param_names const & ps) { + return update_declaration(d, optional(ps), none_expr(), none_expr()); +} + +declaration update_declaration_type(declaration const & d, expr const & type) { + return update_declaration(d, optional(), some_expr(type), none_expr()); +} + +declaration update_declaration_value(declaration const & d, expr const & value) { + return update_declaration(d, optional(), none_expr(), some_expr(value)); +} + +declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type, expr const & value) { + return update_declaration(d, optional(ps), some_expr(type), some_expr(value)); +} +declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type) { + return update_declaration(d, optional(ps), some_expr(type), none_expr()); +} +} diff --git a/src/library/update_declaration.h b/src/library/update_declaration.h new file mode 100644 index 000000000..438bc8328 --- /dev/null +++ b/src/library/update_declaration.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/declaration.h" +namespace lean { +// Helper function for updating "declaration fields" +declaration update_declaration_univ_params(declaration const & d, level_param_names const & ps); +declaration update_declaration_type(declaration const & d, expr const & type); +declaration update_declaration_value(declaration const & d, expr const & value); +declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type, expr const & value); +declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type); +}