From edc8af7bb3f76f20961f33e50e7f32783f496cfe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 May 2014 11:11:19 -0700 Subject: [PATCH] refactor(kernel): reduce code duplication Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 42 ++++++++++------------------------------ src/kernel/expr.cpp | 38 ++++++++++++++++++++++++------------ src/kernel/expr.h | 12 +++++++++++- 3 files changed, 47 insertions(+), 45 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 71aa908ee..682f21b76 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -123,12 +123,8 @@ struct default_converter : public converter { break; case expr_kind::App: { buffer args; - expr const * it = &e; - while (is_app(*it)) { - args.push_back(app_arg(*it)); - it = &(app_fn(*it)); - } - expr f = whnf_core(*it, c); + expr f0 = get_app_rev_args(e, args); + expr f = whnf_core(f0, c); if (is_lambda(f)) { unsigned m = 1; unsigned num_args = args.size(); @@ -139,7 +135,7 @@ struct default_converter : public converter { lean_assert(m <= num_args); r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c); } else { - r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data()); + r = is_eqp(f, f0) ? e : mk_rev_app(f, args.size(), args.data()); } break; }} @@ -197,21 +193,14 @@ struct default_converter : public converter { */ expr unfold_names(expr const & e, unsigned w) { if (is_app(e)) { - expr const * it = &e; - while (is_app(*it)) { - it = &(app_fn(*it)); - } - expr f = unfold_name_core(*it, w); - if (is_eqp(f, *it)) { + expr f0 = get_app_fn(e); + expr f = unfold_name_core(f0, w); + if (is_eqp(f, f0)) { return e; } else { buffer args; - expr const * it = &e; - while (is_app(*it)) { - args.push_back(app_arg(*it)); - it = &(app_fn(*it)); - } - return mk_rev_app(f, args.size(), args.data()); + get_app_rev_args(e, args); + return mk_rev_app(f, args); } } else { return unfold_name_core(e, w); @@ -232,17 +221,7 @@ struct default_converter : public converter { \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one to be expanded. */ - optional is_delta(expr const & e) { - if (is_app(e)) { - expr const * it = &e; - while (is_app(*it)) { - it = &(app_fn(*it)); - } - return is_delta_core(*it); - } else { - return is_delta_core(e); - } - } + optional is_delta(expr const & e) { return is_delta_core(get_app_fn(e)); } /** \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with @@ -365,8 +344,7 @@ struct default_converter : public converter { /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */ bool is_app_of(expr t, name const & f_name) { - while (is_app(t)) - t = app_fn(t); + t = get_app_fn(t); return is_constant(t) && const_name(t) == f_name; } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 3f02f5bd8..ef3950a40 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -82,11 +82,7 @@ void expr_cell::set_tag(tag t) { } bool is_meta(expr const & e) { - expr const * it = &e; - while (is_app(*it)) { - it = &(app_fn(*it)); - } - return is_metavar(*it); + return is_metavar(get_app_fn(e)); } // Expr variables @@ -323,14 +319,32 @@ expr mk_app_vars(expr const & f, unsigned n) { return r; } -expr get_app_args(expr const & e, buffer & args) { - if (is_app(e)) { - expr r = get_app_args(app_fn(e), args); - args.push_back(app_arg(e)); - return r; - } else { - return e; +expr const & get_app_args(expr const & e, buffer & args) { + lean_assert(args.empty()); + expr const * it = &e; + while (is_app(*it)) { + args.push_back(app_arg(*it)); + it = &(app_fn(*it)); } + std::reverse(args.begin(), args.end()); + return *it; +} + +expr const & get_app_rev_args(expr const & e, buffer & args) { + expr const * it = &e; + while (is_app(*it)) { + args.push_back(app_arg(*it)); + it = &(app_fn(*it)); + } + return *it; +} + +expr const & get_app_fn(expr const & e) { + expr const * it = &e; + while (is_app(*it)) { + it = &(app_fn(*it)); + } + return *it; } static name g_default_var_name("a"); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 875b31f98..03a116323 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -597,7 +597,17 @@ inline bool has_free_var_ge(expr const & e, unsigned low) { return get_free_var_ It returns the f. */ -expr get_app_args(expr const & e, buffer & args); +expr const & get_app_args(expr const & e, buffer & args); +/** + \brief Similar to \c get_app_args, but arguments are stored in reverse order in \c args. + If e is of the form (...(f a1) ... an), then the procedure stores [an, ..., a1] in \c args. +*/ +expr const & get_app_rev_args(expr const & e, buffer & args); +/** + \brief Given of the form (...(f a1) ... an), return \c f. If \c e is not an application, + then return \c e. +*/ +expr const & get_app_fn(expr const & e); // =======================================