refactor(kernel): reduce code duplication

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/converter.cpp

@@ -123,12 +123,8 @@ struct default_converter : public converter {
             break;
         case expr_kind::App: {
             buffer<expr> args;
-            expr const * it = &e;
+            expr f0 = get_app_rev_args(e, args);
-            while (is_app(*it)) {
+            expr f = whnf_core(f0, c);
-                args.push_back(app_arg(*it));
-                it = &(app_fn(*it));
-            }
-            expr f = whnf_core(*it, 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;
+            expr f0 = get_app_fn(e);
-            while (is_app(*it)) {
+            expr f  = unfold_name_core(f0, w);
-                it = &(app_fn(*it));
+            if (is_eqp(f, f0)) {
-            }
-            expr f = unfold_name_core(*it, w);
-            if (is_eqp(f, *it)) {
                 return e;
             } else {
                 buffer<expr> args;
-                expr const * it = &e;
+                get_app_rev_args(e, args);
-                while (is_app(*it)) {
+                return mk_rev_app(f, args);
-                    args.push_back(app_arg(*it));
-                    it = &(app_fn(*it));
-                }
-                return mk_rev_app(f, args.size(), args.data());
             }
         } 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<definition> is_delta(expr const & e) {
+    optional<definition> is_delta(expr const & e) { return is_delta_core(get_app_fn(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);
-        }
-    }
 
     /**
         \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 = get_app_fn(t);
-            t = app_fn(t);
         return is_constant(t) && const_name(t) == f_name;
     }
 

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;
+    return is_metavar(get_app_fn(e));
-    while (is_app(*it)) {
-        it = &(app_fn(*it));
-    }
-    return is_metavar(*it);
 }
 
 // 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<expr> & args) {
+expr const & get_app_args(expr const & e, buffer<expr> & args) {
-    if (is_app(e)) {
+    lean_assert(args.empty());
-        expr r = get_app_args(app_fn(e), args);
+    expr const * it = &e;
-        args.push_back(app_arg(e));
+    while (is_app(*it)) {
-        return r;
+        args.push_back(app_arg(*it));
-    } else {
+        it = &(app_fn(*it));
-        return e;
     }
+    std::reverse(args.begin(), args.end());
+    return *it;
+}
+
+expr const & get_app_rev_args(expr const & e, buffer<expr> & 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");

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<expr> & args);
+expr const & get_app_args(expr const & e, buffer<expr> & args);
+/**
+   \brief Similar to \c get_app_args, but arguments are stored in reverse order in \c args.
+   If e is of the form <tt>(...(f a1) ... an)</tt>, then the procedure stores [an, ..., a1] in \c args.
+*/
+expr const & get_app_rev_args(expr const & e, buffer<expr> & args);
+/**
+   \brief Given of the form <tt>(...(f a1) ... an)</tt>, return \c f. If \c e is not an application,
+   then return \c e.
+*/
+expr const & get_app_fn(expr const & e);
 // =======================================