Remove duplicate code

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

src/kernel/expr.h

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "mpz.h"
 #include "level.h"
 #include "hash.h"
+#include "buffer.h"
 
 namespace lean {
 /* =======================================
@@ -334,4 +335,33 @@ struct args {
 */
 expr copy(expr const & e);
 // =======================================
+
+// =======================================
+// Update
+template<typename F> expr update_app(expr const & e, F f) {
+    buffer<expr> new_args;
+    bool modified = false;
+    for (expr const & a : args(e)) {
+        new_args.push_back(f(a));
+        if (!eqp(a, new_args.back()))
+            modified = true;
+    }
+    if (modified)
+        return app(new_args.size(), new_args.data());
+    else
+        return e;
+}
+template<typename F> expr update_abst(expr const & e, F f) {
+    expr const & old_t = abst_type(e);
+    expr const & old_b = abst_body(e);
+    std::pair<expr, expr> p = f(old_t, old_b);
+    if (!eqp(p.first, old_t) || !eqp(p.second, old_b)) {
+        name const & n = abst_name(e);
+        return is_pi(e) ? pi(n, p.first, p.second) : lambda(n, p.first, p.second);
+    }
+    else {
+        return e;
+    }
+}
+// =======================================
 }

src/kernel/max_sharing.cpp

@@ -36,39 +36,15 @@ struct max_sharing_fn::imp {
             cache(a);
             return a;
         case expr_kind::App: {
-            buffer<expr> new_args;
+            expr r = update_app(a, [=](expr const & c){ return apply(c); });
-            bool modified = false;
-            for (expr const & old_arg : args(a)) {
-                new_args.push_back(apply(old_arg));
-                if (!eqp(old_arg, new_args.back()))
-                    modified = true;
-            }
-            if (!modified) {
-                cache(a);
-                return a;
-            }
-            else {
-                expr r = app(new_args.size(), new_args.data());
             cache(r);
             return r;
         }
-        }
         case expr_kind::Lambda:
         case expr_kind::Pi: {
-            expr const & old_t = abst_type(a);
+            expr r = update_abst(a, [=](expr const & t, expr const & b) { return std::make_pair(apply(t), apply(b)); });
-            expr const & old_b = abst_body(a);
-            expr t = apply(old_t);
-            expr b = apply(old_b);
-            if (!eqp(t, old_t) || !eqp(b, old_b)) {
-                name const & n     = abst_name(a);
-                expr r = is_pi(a) ? pi(n, t, b) : lambda(n, t, b);
             cache(r);
             return r;
-            }
-            else {
-                cache(a);
-                return a;
-            }
         }}
         lean_unreachable();
         return a;

src/kernel/replace.h

@@ -39,35 +39,14 @@ class replace_fn {
             switch (e.kind()) {
             case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var:
                 break;
-            case expr_kind::App: {
+            case expr_kind::App:
-                buffer<expr> new_args;
+                r = update_app(e, [=](expr const & c) { return apply(c, offset); });
-                bool modified = false;
-                for (expr const & a : args(e)) {
-                    new_args.push_back(apply(a, offset));
-                    if (!eqp(a, new_args.back()))
-                        modified = true;
-                }
-                if (modified)
-                    r = app(new_args.size(), new_args.data());
-                else
-                    r = e;
                 break;
-            }
             case expr_kind::Lambda:
-            case expr_kind::Pi: {
+            case expr_kind::Pi:
-                expr const & old_t = abst_type(e);
+                r = update_abst(e, [=](expr const & t, expr const & b) { return std::make_pair(apply(t, offset), apply(b, offset+1)); });
-                expr const & old_b = abst_body(e);
-                expr t = apply(old_t, offset);
-                expr b = apply(old_b, offset+1);
-                if (!eqp(t, old_t) || !eqp(b, old_b)) {
-                    name const & n = abst_name(e);
-                    r = is_pi(e) ? pi(n, t, b) : lambda(n, t, b);
-                }
-                else {
-                    r = e;
-                }
                 break;
-            }}
+            }
         }
 
         if (sh)