From 707cf45a26e11d716192f436fef67e729a008b2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Feb 2017 20:20:27 -0800 Subject: [PATCH] refactor(library/type_context): rename whnf_pred => whnf_head_pred --- src/library/class.cpp | 2 +- src/library/compiler/preprocess.cpp | 4 ++-- src/library/equations_compiler/elim_match.cpp | 6 +++--- src/library/equations_compiler/structural_rec.cpp | 2 +- src/library/equations_compiler/util.cpp | 2 +- src/library/inductive_compiler/nested.cpp | 2 +- src/library/tactic/induction_tactic.cpp | 2 +- src/library/type_context.cpp | 2 +- src/library/type_context.h | 2 +- 9 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/library/class.cpp b/src/library/class.cpp index cdb89c88b1..f7a6f6b243 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -184,7 +184,7 @@ environment add_instance_core(environment const & env, name const & n, unsigned class_state S = class_ext::get_state(env); type_context::tmp_locals locals(ctx); while (true) { - type = ctx.whnf_pred(type, [&](expr const & e) { + type = ctx.whnf_head_pred(type, [&](expr const & e) { expr const & fn = get_app_fn(e); return !is_constant(fn) || !S.m_instances.contains(const_name(fn)); }); if (!is_pi(type)) diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 3e5481b49f..17ae5ff0bb 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -110,7 +110,7 @@ class expand_aux_fn : public compiler_step_visitor { return visit(copy_tag(e, expr(*r))); } } - expr new_e = copy_tag(e, ctx().whnf_pred(e, [&](expr const &) { return false; })); + expr new_e = copy_tag(e, ctx().whnf_head_pred(e, [&](expr const &) { return false; })); if (is_eqp(new_e, e)) return compiler_step_visitor::visit_app(new_e); else @@ -119,7 +119,7 @@ class expand_aux_fn : public compiler_step_visitor { case recursor_kind::CasesOn: return visit_cases_on(e); case recursor_kind::Aux: - return compiler_step_visitor::visit(copy_tag(e, ctx().whnf_pred(e, [&](expr const & e) { return is_aux_recursor(e); }))); + return compiler_step_visitor::visit(copy_tag(e, ctx().whnf_head_pred(e, [&](expr const & e) { return is_aux_recursor(e); }))); } lean_unreachable(); } diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 289ce46701..b0d5732991 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -327,7 +327,7 @@ struct elim_match_fn { if (is_inaccessible(e)) { return e; } else { - return ctx.whnf_pred(e, [&](expr const & e) { + return ctx.whnf_head_pred(e, [&](expr const & e) { return !is_constructor_app(e) && !is_value(ctx, e) && !is_transport_app(e); }); } @@ -335,14 +335,14 @@ struct elim_match_fn { /* Normalize until head is constructor */ expr whnf_constructor(type_context & ctx, expr const & e) { - return ctx.whnf_pred(e, [&](expr const & e) { + return ctx.whnf_head_pred(e, [&](expr const & e) { return !is_constructor_app(e); }); } /* Normalize until head is an inductive datatype */ expr whnf_inductive(type_context & ctx, expr const & e) { - return ctx.whnf_pred(e, [&](expr const & e) { + return ctx.whnf_head_pred(e, [&](expr const & e) { return !is_inductive_app(e); }); } diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index 34fb5c7881..a881e9834f 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -553,7 +553,7 @@ struct structural_rec_fn { expr whnf_upto_below(type_context & ctx, name const & I_name, expr const & below_type) { name below_name(I_name, "below"); name ibelow_name(I_name, "ibelow"); - return ctx.whnf_pred(below_type, [&](expr const & e) { + return ctx.whnf_head_pred(below_type, [&](expr const & e) { expr const & fn = get_app_fn(e); return !is_constant(fn) || (const_name(fn) != below_name && const_name(fn) != ibelow_name); }); diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index e539f2a849..8f569f7477 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -329,7 +329,7 @@ static environment add_equation_lemma(environment const & env, options const & o } static expr whnf_ite(type_context & ctx, expr const & e) { - return ctx.whnf_pred(e, [&](expr const & e) { + return ctx.whnf_head_pred(e, [&](expr const & e) { expr const & fn = get_app_fn(e); return !is_constant(fn, get_ite_name()); }); diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 7915fa7b69..2ce80ae8e3 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -211,7 +211,7 @@ class add_nested_inductive_decl_fn { // Helpers expr safe_whnf(type_context & tctx, expr const & e) { - expr r = tctx.whnf_pred(e, [&](expr const & t) { + expr r = tctx.whnf_head_pred(e, [&](expr const & t) { expr fn = get_app_fn(t); if (!is_constant(fn)) return true; diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index f6bae67786..996ee4d68f 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -80,7 +80,7 @@ static void throw_invalid_major_premise_type(unsigned arg_idx, expr const & H_ty static expr whnf_until(type_context & ctx, name const & n, expr const & e) { type_context::transparency_scope scope(ctx, transparency_mode::All); - return ctx.whnf_pred(e, [&](expr const & t) { + return ctx.whnf_head_pred(e, [&](expr const & t) { expr fn = get_app_fn(t); if (is_constant(fn) && const_name(fn) == n) return false; diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index f459071efc..200a918d31 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -774,7 +774,7 @@ expr type_context::whnf(expr const & e) { } } -expr type_context::whnf_pred(expr const & e, std::function const & pred) { // NOLINT +expr type_context::whnf_head_pred(expr const & e, std::function const & pred) { // NOLINT flet const *>set_unfold_pred(m_unfold_pred, &pred); // NOLINT expr t = e; while (true) { diff --git a/src/library/type_context.h b/src/library/type_context.h index 1bb7ef9256..ee6cc78596 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -369,7 +369,7 @@ public: /** Similar to whnf, but invokes the given predicate before unfolding constant symbols in the head. If pred(e') is false, then the method will not unfold definition in the head of e', and will return e'. This method is useful when we want to normalize the expression until we get a particular symbol as the head symbol. */ - expr whnf_pred(expr const & e, std::function const & pred); // NOLINT + expr whnf_head_pred(expr const & e, std::function const & pred); // NOLINT optional reduce_aux_recursor(expr const & e); optional reduce_projection(expr const & e); optional norm_ext(expr const & e) { return env().norm_ext()(e, *this); }