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

feat(src/library/type_context): add support for preserving macros at type_context whnf

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-02 18:18:11 -07:00
parent 39429251c6
commit 24e4dbe353
2 changed files with 21 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/type_context.cpp
View file

@ -155,7 +155,10 @@ bool type_context::is_opaque(declaration const & d) const {
optional<expr> type_context::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, *m_ext_ctx);
if (should_unfold_macro(m))
return macro_def(m).expand(m, *m_ext_ctx);
else
return none_expr();
}
optional<expr> type_context::reduce_projection(expr const & e) {
@ -1887,6 +1890,15 @@ expr normalizer::normalize_app(expr const & e) {
}
}
expr normalizer::normalize_macro(expr const & e) {
// This method is invoked for macros that are not unfolded at whnf because
// the predicate should_unfold_macro(e) returned false
buffer<expr> new_args;
for (unsigned i = 0; i < macro_num_args(e); i++)
new_args.push_back(normalize(macro_arg(e, i)));
return update_macro(e, new_args.size(), new_args.data());
}
expr normalizer::normalize(expr e) {
check_system("normalize");
if (!should_normalize(e))
@ -1894,8 +1906,10 @@ expr normalizer::normalize(expr e) {
e = m_ctx.whnf(e);
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro:
case expr_kind::Meta: case expr_kind::Local:
return e;
case expr_kind::Macro:
return normalize_macro(e);
case expr_kind::Lambda: {
e = normalize_binding(e);
if (m_use_eta)

5
src/library/type_context.h
View file

@ -319,6 +319,10 @@ public:
\remark This class always treats projections and theorems as opaque. */
virtual bool is_extra_opaque(name const & n) const = 0;
/** \brief This method is invoked when a term is being put in weak-head-normal-form.
It is used to decide whether a macro should be unfolded or not. */
virtual bool should_unfold_macro(expr const &) const { return true; }
/** \brief Create a temporary local constant */
expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()) {
return m_local_gen->mk_tmp_local(type, bi);
@ -572,6 +576,7 @@ class normalizer {
buffer<unsigned> const & idxs, buffer<expr> & args, bool is_rec);
optional<expr> unfold_recursor_major(expr const & f, unsigned idx, buffer<expr> & args);
expr normalize_app(expr const & e);
expr normalize_macro(expr const & e);
expr normalize(expr e);
public: