From 75f4ec5092ccdd706775c7f70830aa38ec5b44ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Sep 2013 15:37:30 -0700 Subject: [PATCH] Add functions for 'updating expressions'. The new functions are used to simplify the elaborator. Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 2 +- src/library/elaborator.cpp | 51 ++++++++++++++--------------------- src/library/metavar.cpp | 9 +++---- src/library/update_expr.cpp | 54 +++++++++++++++++++++++++++++++++++++ src/library/update_expr.h | 41 ++++++++++++++++++++++++++++ 5 files changed, 119 insertions(+), 38 deletions(-) create mode 100644 src/library/update_expr.cpp create mode 100644 src/library/update_expr.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index b16224bd11..ddf0e427f5 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp index 63ec5acdcd..2392bf4d9f 100644 --- a/src/library/elaborator.cpp +++ b/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 replacer(proc, tracer); diff --git a/src/library/metavar.cpp b/src/library/metavar.cpp index 811faca248..8660e07042 100644 --- a/src/library/metavar.cpp +++ b/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 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)) { diff --git a/src/library/update_expr.cpp b/src/library/update_expr.cpp new file mode 100644 index 0000000000..fc19449779 --- /dev/null +++ b/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 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); +} +} diff --git a/src/library/update_expr.h b/src/library/update_expr.h new file mode 100644 index 0000000000..a1112e497a --- /dev/null +++ b/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 is_eqp(new_arg, app[i]). +*/ +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); +}