Add functions for 'updating expressions'. The new functions are used to simplify the elaborator.

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

src/library/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
-  state.cpp metavar.cpp elaborator.cpp)
+  state.cpp metavar.cpp elaborator.cpp update_expr.cpp)
 target_link_libraries(library ${LEAN_LIBS})

src/library/elaborator.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "builtin.h"
 #include "free_vars.h"
 #include "for_each.h"
+#include "update_expr.h"
 #include "replace.h"
 #include "flet.h"
 #include "elaborator_exception.h"
@@ -96,6 +97,12 @@ class elaborator::imp {
 
     volatile bool       m_interrupted;
 
+    void add_trace(expr const & old_e, expr const & new_e) {
+        if (!is_eqp(old_e, new_e)) {
+            m_trace[new_e] = old_e;
+        }
+    }
+
     expr mk_metavar(context const & ctx) {
         unsigned midx = m_metavars.size();
         expr r = ::lean::mk_metavar(midx);
@@ -317,49 +324,33 @@ class elaborator::imp {
         case expr_kind::Eq: {
             auto lhs_p = process(eq_lhs(e), ctx);
             auto rhs_p = process(eq_rhs(e), ctx);
-            if (is_eqp(lhs_p.first, eq_lhs(e)) && is_eqp(rhs_p.first, eq_rhs(e))) {
-                return expr_pair(e, mk_bool_type());
-            } else {
-                expr new_e = mk_eq(lhs_p.first, rhs_p.first);
-                m_trace[new_e] = e;
-                return expr_pair(new_e, mk_bool_type());
-            }
+            expr new_e = update_eq(e, lhs_p.first, rhs_p.first);
+            add_trace(e, new_e);
+            return expr_pair(new_e, mk_bool_type());
         }
         case expr_kind::Pi: {
             auto d_p = process(abst_domain(e), ctx);
             auto b_p = process(abst_body(e), extend(ctx, abst_name(e), d_p.first));
             expr t   = mk_type(max(check_universe(d_p.second, ctx, e, ctx), check_universe(b_p.second, ctx, e, ctx)));
-            if (is_eqp(d_p.first, abst_domain(e)) && is_eqp(b_p.first, abst_body(e))) {
-                return expr_pair(e, t);
-            } else {
-                expr new_e = mk_pi(abst_name(e), d_p.first, b_p.first);
-                m_trace[new_e] = e;
-                return expr_pair(new_e, t);
-            }
+            expr new_e = update_pi(e, d_p.first, b_p.first);
+            add_trace(e, new_e);
+            return expr_pair(new_e, t);
         }
         case expr_kind::Lambda: {
             auto d_p = process(abst_domain(e), ctx);
             auto b_p = process(abst_body(e), extend(ctx, abst_name(e), d_p.first));
             expr t   = mk_pi(abst_name(e), d_p.first, b_p.second);
-            if (is_eqp(d_p.first, abst_domain(e)) && is_eqp(b_p.first, abst_body(e))) {
-                return expr_pair(e, t);
-            } else {
-                expr new_e = mk_lambda(abst_name(e), d_p.first, b_p.first);
-                m_trace[new_e] = e;
-                return expr_pair(new_e, t);
-            }
+            expr new_e = update_lambda(e, d_p.first, b_p.first);
+            add_trace(e, new_e);
+            return expr_pair(new_e, t);
         }
         case expr_kind::Let: {
             auto v_p = process(let_value(e), ctx);
             auto b_p = process(let_body(e), extend(ctx, let_name(e), v_p.second, v_p.first));
             expr t   = lower_free_vars_mmv(b_p.second, 1, 1);
-            if (is_eqp(v_p.first, let_value(e)) && is_eqp(b_p.first, let_body(e))) {
-                return expr_pair(e, t);
-            } else {
-                expr new_e = mk_let(let_name(e), v_p.first, b_p.first);
-                m_trace[new_e] = e;
-                return expr_pair(new_e, t);
-            }
+            expr new_e = update_let(e, v_p.first, b_p.first);
+            add_trace(e, new_e);
+            return expr_pair(new_e, t);
         }}
         lean_unreachable();
         return expr_pair(expr(), expr());
@@ -588,9 +579,7 @@ class elaborator::imp {
         };
 
         auto tracer = [&](expr const & old_e, expr const & new_e) {
-            if (!is_eqp(new_e, old_e)) {
-                m_trace[new_e] = old_e;
-            }
+            add_trace(old_e, new_e);
         };
 
         replace_fn<decltype(proc), decltype(tracer)> replacer(proc, tracer);

src/library/metavar.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "for_each.h"
 #include "environment.h"
 #include "occurs.h"
+#include "update_expr.h"
 #include "printer.h"
 
 namespace lean {
@@ -337,12 +338,8 @@ expr head_reduce_mmv(expr const & e, environment const & env, name_set const * d
         return r;
     } else if (is_app(e) && is_constant(arg(e, 0))) {
         expr def = get_def_value(const_name(arg(e, 0)), env, defs);
-        if (def) {
-            buffer<expr> new_args;
-            new_args.push_back(def);
-            new_args.append(num_args(e)-1, &arg(e,1));
-            return mk_app(new_args.size(), new_args.data());
-        }
+        if (def)
+            return update_app(e, 0, def);
     } else if (is_let(e)) {
         return instantiate_free_var_mmv(let_body(e), 0, let_value(e));
     } else if (is_constant(e)) {

src/library/update_expr.cpp

@@ -0,0 +1,54 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "update_expr.h"
+#include "buffer.h"
+
+namespace lean {
+expr update_app(expr const & app, unsigned i, expr const & new_arg) {
+    if (is_eqp(arg(app, i), new_arg)) {
+        return app;
+    } else {
+        buffer<expr> new_args;
+        unsigned num = num_args(app);
+        for (unsigned j = 0; j < num; j++) {
+            if (i == j)
+                new_args.push_back(new_arg);
+            else
+                new_args.push_back(arg(app, j));
+        }
+        return mk_app(new_args.size(), new_args.data());
+    }
+}
+
+expr update_lambda(expr const & lambda, expr const & d, expr const & b) {
+    if (is_eqp(abst_domain(lambda), d) && is_eqp(abst_body(lambda), b))
+        return lambda;
+    else
+        return mk_lambda(abst_name(lambda), d, b);
+}
+
+expr update_pi(expr const & pi, expr const & d, expr const & b) {
+    if (is_eqp(abst_domain(pi), d) && is_eqp(abst_body(pi), b))
+        return pi;
+    else
+        return mk_pi(abst_name(pi), d, b);
+}
+
+expr update_let(expr const & let, expr const & v, expr const & b) {
+    if (is_eqp(let_value(let), v) && is_eqp(let_body(let), b))
+        return let;
+    else
+        return mk_let(let_name(let), v, b);
+}
+
+expr update_eq(expr const & eq, expr const & l, expr const & r) {
+    if (is_eqp(eq_lhs(eq), l) && is_eqp(eq_rhs(eq), r))
+        return eq;
+    else
+        return mk_eq(l, r);
+}
+}

src/library/update_expr.h

@@ -0,0 +1,41 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "expr.h"
+
+namespace lean {
+/**
+   \brief Return an application equal to \c app but argument \c i has been replaced with \c new_arg.
+
+   \remark Return \c app if <tt>is_eqp(new_arg, app[i])</tt>.
+*/
+expr update_app(expr const & app, unsigned i, expr const & new_arg);
+/**
+   \brief Return a lambda expression based on \c lambda with domain \c d and \c body b.
+
+   \remark Return \c lambda if the given domain and body are (pointer) equal to the ones in \c lambda.
+*/
+expr update_lambda(expr const & lambda, expr const & d, expr const & b);
+/**
+   \brief Return a pi expression based on \c pi with domain \c d and \c body b.
+
+   \remark Return \c pi if the given domain and body are (pointer) equal to the ones in \c pi.
+*/
+expr update_pi(expr const & pi, expr const & d, expr const & b);
+/**
+   \brief Return a let expression based on \c let with value \c v and \c body b.
+
+   \remark Return \c let if the given value and body are (pointer) equal to the ones in \c let.
+*/
+expr update_let(expr const & let, expr const & v, expr const & b);
+/**
+   \brief Return a new equality with lhs \c l and rhs \c r.
+
+   \remark Return \c eq if the given lhs and rhs are (pointer) equal to the ones in \c eq.
+*/
+expr update_eq(expr const & eq, expr const & l, expr const & r);
+}