From eb046c11fb46c81e6b3310a3f58ddec81df0a2f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Feb 2014 09:48:28 -0800 Subject: [PATCH] refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable Signed-off-by: Leonardo de Moura --- src/kernel/abstract.cpp | 1 - src/kernel/abstract.h | 15 ++----------- src/kernel/expr.cpp | 32 ++++----------------------- src/kernel/expr.h | 37 +++++++++++++------------------- src/kernel/expr_eq_fn.cpp | 9 -------- src/kernel/expr_eq_fn.h | 1 - src/kernel/for_each_fn.cpp | 3 +-- src/kernel/formatter.cpp | 6 ++---- src/kernel/free_vars.cpp | 12 ----------- src/kernel/max_sharing.cpp | 7 ------ src/kernel/replace_fn.cpp | 11 +++------- src/kernel/replace_visitor.cpp | 11 ++-------- src/kernel/replace_visitor.h | 1 - src/tests/kernel/expr.cpp | 6 +++--- src/tests/kernel/instantiate.cpp | 2 +- 15 files changed, 33 insertions(+), 121 deletions(-) diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index cd4578a08..a5688fe1a 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -49,5 +49,4 @@ expr FName(std::initializer_list> const & MkBinder(Fun); MkBinder(Pi); -MkBinder(Let); } diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h index 8f3f3a048..7f537bc82 100644 --- a/src/kernel/abstract.h +++ b/src/kernel/abstract.h @@ -46,21 +46,10 @@ inline expr Pi(expr const & n, expr const & t, expr const & b) { return mk_pi(co inline expr Pi(std::pair const & p, expr const & b) { return Pi(p.first, p.second, b); } expr Pi(std::initializer_list> const & l, expr const & b); -/** - \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x). -*/ -inline expr Let(name const & x, expr const & v, expr const & b) { return mk_let(x, v, abstract(b, mk_constant(x))); } -inline expr Let(expr const & x, expr const & v, expr const & b) { return mk_let(const_name(x), v, abstract(b, x)); } -inline expr Let(std::pair const & p, expr const & b) { return Let(p.first, p.second, b); } - expr Let(std::initializer_list> const & l, expr const & b); -/** - \brief Similar to Let(x, v, b), but returns v if x == b -*/ -inline expr Let_simp(expr const & x, expr const & v, expr const & b) { return x == b ? v : Let(x, v, b); } /** - \brief Create a Let expression (Let x : t := v in b), the term b is abstracted using abstract(b, x). -*/ +- \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x). +-*/ inline expr Let(name const & x, expr const & t, expr const & v, expr const & b) { return mk_let(x, t, v, abstract(b, mk_constant(x))); } inline expr Let(expr const & x, expr const & t, expr const & v, expr const & b) { return mk_let(const_name(x), t, v, abstract(b, x)); } } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 8b3ecf63b..9808d55aa 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -62,11 +62,6 @@ void expr_cell::dec_ref(expr & e, buffer & todelete) { } } -void expr_cell::dec_ref(optional & c, buffer & todelete) { - if (c) - dec_ref(*c, todelete); -} - optional expr_cell::is_arrow() const { // it is stored in bits 3-4 unsigned r = (m_flags & (8+16)) >> 3; @@ -168,8 +163,8 @@ expr_sort::expr_sort(level const & l): expr_sort::~expr_sort() {} // Expr Let -expr_let::expr_let(name const & n, optional const & t, expr const & v, expr const & b): - expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || ::lean::has_metavar(t), +expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b): + expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), t.has_metavar() || v.has_metavar() || b.has_metavar(), std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1), m_name(n), m_type(t), @@ -321,7 +316,7 @@ expr update_binder(expr const & e, expr const & new_domain, expr const & new_bod return e; } -expr update_let(expr const & e, optional const & new_type, expr const & new_val, expr const & new_body) { +expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body) { if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_val) || !is_eqp(let_body(e), new_body)) return mk_let(let_name(e), new_type, new_val, new_body); else @@ -403,16 +398,6 @@ class expr_serializer : public object_serializer super; max_sharing_fn m_max_sharing_fn; - void write_core(optional const & a) { - serializer & s = get_owner(); - if (a) { - s << true; - write_core(*a); - } else { - s << false; - } - } - void write_core(expr const & a) { auto k = a.kind(); super::write_core(a, static_cast(k), [&]() { @@ -460,15 +445,6 @@ public: class expr_deserializer : public object_deserializer { typedef object_deserializer super; public: - optional read_opt() { - deserializer & d = get_owner(); - if (d.read_bool()) { - return some_expr(read()); - } else { - return none_expr(); - } - } - expr read_binder(expr_kind k) { deserializer & d = get_owner(); name n = read_name(d); @@ -509,7 +485,7 @@ public: return read_binder(k); case expr_kind::Let: { name n = read_name(d); - optional t = read_opt(); + expr t = read(); expr v = read(); return mk_let(n, t, v, read()); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 19555b90a..c722b2f11 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -40,7 +40,7 @@ typedef list levels; | Lambda name expr expr | Pi name expr expr | Sigma name expr expr - | Let name expr? expr expr + | Let name expr expr expr | Macro macro */ @@ -72,7 +72,6 @@ protected: friend class has_free_var_fn; static void dec_ref(expr & c, buffer & todelete); - static void dec_ref(optional & c, buffer & todelete); public: expr_cell(expr_kind k, unsigned h, bool has_mv); expr_kind kind() const { return static_cast(m_kind); } @@ -127,7 +126,7 @@ public: friend expr mk_pair(expr const & f, expr const & s, expr const & t); friend expr mk_proj(bool fst, expr const & p); friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e); - friend expr mk_let(name const & n, optional const & t, expr const & v, expr const & e); + friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e); friend expr mk_macro(macro * m); friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } @@ -252,19 +251,19 @@ public: /** \brief Let expressions */ class expr_let : public expr_composite { - name m_name; - optional m_type; - expr m_value; - expr m_body; + name m_name; + expr m_type; + expr m_value; + expr m_body; friend class expr_cell; void dealloc(buffer & todelete); public: - expr_let(name const & n, optional const & t, expr const & v, expr const & b); + expr_let(name const & n, expr const & t, expr const & v, expr const & b); ~expr_let(); - name const & get_name() const { return m_name; } - optional const & get_type() const { return m_type; } - expr const & get_value() const { return m_value; } - expr const & get_body() const { return m_body; } + name const & get_name() const { return m_name; } + expr const & get_type() const { return m_type; } + expr const & get_value() const { return m_value; } + expr const & get_body() const { return m_body; } }; /** \brief Sort */ @@ -388,11 +387,7 @@ inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); } inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); } inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Sigma, n, t, e); } -inline expr mk_let(name const & n, optional const & t, expr const & v, expr const & e) { - return expr(new expr_let(n, t, v, e)); -} -inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, some_expr(t), v, e); } -inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, none_expr(), v, e); } +inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); } inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); } expr mk_Bool(); @@ -484,7 +479,7 @@ inline expr const & binder_body(expr_cell * e) { return to_binder(e)- inline level const & sort_level(expr_cell * e) { return to_sort(e)->get_level(); } inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); } inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } -inline optional const & let_type(expr_cell * e) { return to_let(e)->get_type(); } +inline expr const & let_type(expr_cell * e) { return to_let(e)->get_type(); } inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } inline name const & mlocal_name(expr_cell * e) { return to_mlocal(e)->get_name(); } inline expr const & mlocal_type(expr_cell * e) { return to_mlocal(e)->get_type(); } @@ -508,16 +503,14 @@ inline expr const & binder_body(expr const & e) { return to_binder(e) inline level const & sort_level(expr const & e) { return to_sort(e)->get_level(); } inline name const & let_name(expr const & e) { return to_let(e)->get_name(); } inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } -inline optional const & let_type(expr const & e) { return to_let(e)->get_type(); } +inline expr const & let_type(expr const & e) { return to_let(e)->get_type(); } inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } inline name const & mlocal_name(expr const & e) { return to_mlocal(e)->get_name(); } inline expr const & mlocal_type(expr const & e) { return to_mlocal(e)->get_type(); } inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; } inline bool has_metavar(expr const & e) { return e.has_metavar(); } -inline bool has_metavar(optional const & e) { return e && has_metavar(*e); } unsigned get_depth(expr const & e); -inline unsigned get_depth(optional const & e) { return e ? get_depth(*e) : 0; } // ======================================= @@ -565,7 +558,7 @@ expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); expr update_proj(expr const & e, expr const & new_arg); expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type); expr update_binder(expr const & e, expr const & new_domain, expr const & new_body); -expr update_let(expr const & e, optional const & new_type, expr const & new_val, expr const & new_body); +expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body); expr update_mlocal(expr const & e, expr const & new_type); // ======================================= diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 153bd237e..c216970a6 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -7,15 +7,6 @@ Author: Leonardo de Moura #include "kernel/expr_eq_fn.h" namespace lean { -bool expr_eq_fn::apply(optional const & a0, optional const & b0) { - if (is_eqp(a0, b0)) - return true; - else if (!a0 || !b0) - return false; - else - return apply(*a0, *b0); -} - bool expr_eq_fn::apply(expr const & a, expr const & b) { check_system("expression equality test"); if (is_eqp(a, b)) return true; diff --git a/src/kernel/expr_eq_fn.h b/src/kernel/expr_eq_fn.h index b96014495..1ecb1e828 100644 --- a/src/kernel/expr_eq_fn.h +++ b/src/kernel/expr_eq_fn.h @@ -16,7 +16,6 @@ namespace lean { */ class expr_eq_fn { std::unique_ptr m_eq_visited; - bool apply(optional const & a0, optional const & b0); bool apply(expr const & a, expr const & b); public: bool operator()(expr const & a, expr const & b) { return apply(a, b); } diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp index 0e4e156e9..2c49d8a9b 100644 --- a/src/kernel/for_each_fn.cpp +++ b/src/kernel/for_each_fn.cpp @@ -67,8 +67,7 @@ void for_each_fn::apply(expr const & e, unsigned offset) { case expr_kind::Let: todo.emplace_back(let_body(e), offset + 1); todo.emplace_back(let_value(e), offset); - if (let_type(e)) - todo.emplace_back(*let_type(e), offset); + todo.emplace_back(let_type(e), offset); goto begin_loop; } } diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index a82ed556e..213dc5cbf 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -117,10 +117,8 @@ struct print_expr_fn { break; case expr_kind::Let: out() << "let " << let_name(a); - if (let_type(a)) { - out() << " : "; - print(*let_type(a), c); - } + out() << " : "; + print(let_type(a), c); out() << " := "; print(let_value(a), c); out() << " in "; diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 19ba801c0..88a95c575 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -22,10 +22,6 @@ class has_free_vars_fn { protected: expr_cell_offset_set m_cached; - bool apply(optional const & e, unsigned offset) { - return e && apply(*e, offset); - } - bool apply(expr const & e, unsigned offset) { // handle easy cases switch (e.kind()) { @@ -113,10 +109,6 @@ class free_var_range_fn { static unsigned dec(unsigned s) { return (s == 0) ? 0 : s - 1; } - unsigned apply(optional const & e) { - return e ? apply(*e) : 0; - } - unsigned apply(expr const & e) { // handle easy cases switch (e.kind()) { @@ -191,10 +183,6 @@ protected: expr_cell_offset_set m_cached; std::unique_ptr m_range_fn; - bool apply(optional const & e, unsigned offset) { - return e && apply(*e, offset); - } - // Return true iff m_low + offset <= vidx bool ge_lower(unsigned vidx, unsigned offset) const { unsigned low1 = m_low + offset; diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp index af3f014de..d95e72a6f 100644 --- a/src/kernel/max_sharing.cpp +++ b/src/kernel/max_sharing.cpp @@ -26,13 +26,6 @@ struct max_sharing_fn::imp { m_cache.insert(a); } - optional apply(optional const & a) { - if (a) - return some_expr(apply(*a)); - else - return a; - } - expr apply(expr const & a) { check_system("max_sharing"); auto r = m_cache.find(a); diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 4971c72a5..a8143c100 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -115,19 +115,14 @@ expr replace_fn::operator()(expr const & e) { pop_rs(2); break; case expr_kind::Let: - if (check_index(f, 0) && let_type(e) && !visit(*let_type(e), offset)) + if (check_index(f, 0) && !visit(let_type(e), offset)) goto begin_loop; if (check_index(f, 1) && !visit(let_value(e), offset)) goto begin_loop; if (check_index(f, 2) && !visit(let_body(e), offset + 1)) goto begin_loop; - if (let_type(e)) { - r = update_let(e, some_expr(rs(-3)), rs(-2), rs(-1)); - pop_rs(3); - } else { - r = update_let(e, none_expr(), rs(-2), rs(-1)); - pop_rs(2); - } + r = update_let(e, rs(-3), rs(-2), rs(-1)); + pop_rs(3); break; } save_result(e, r, offset, f.m_shared); diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index ac52d9ae9..b7e11fc7d 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -46,11 +46,10 @@ expr replace_visitor::visit_pi(expr const & e, context const & ctx) { return vis expr replace_visitor::visit_sigma(expr const & e, context const & ctx) { return visit_binder(e, ctx); } expr replace_visitor::visit_let(expr const & e, context const & ctx) { lean_assert(is_let(e)); - optional new_t = visit(let_type(e), ctx); + expr new_t = visit(let_type(e), ctx); expr new_v = visit(let_value(e), ctx); freset reset(m_cache); - // TODO(Leo): decide what we should do with let-exprs - expr new_b; // = visit(let_body(e), extend(ctx, let_name(e), new_t, new_v)); + expr new_b = visit(let_body(e), extend(ctx, let_name(e), new_t)); return update_let(e, new_t, new_v, new_b); } expr replace_visitor::save_result(expr const & e, expr && r, bool shared) { @@ -87,10 +86,4 @@ expr replace_visitor::visit(expr const & e, context const & ctx) { lean_unreachable(); // LCOV_EXCL_LINE } -optional replace_visitor::visit(optional const & e, context const & ctx) { - if (e) - return some_expr(visit(*e, ctx)); - else - return none_expr(); -} } diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index 53611accb..82682ec47 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -42,7 +42,6 @@ protected: virtual expr visit_sigma(expr const &, context const &); virtual expr visit_let(expr const &, context const &); virtual expr visit(expr const &, context const &); - optional visit(optional const &, context const &); void set_ctx(context const & ctx) { if (!is_eqp(m_ctx, ctx)) { diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 5688a16a7..edeba03b0 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -272,7 +272,7 @@ static void tst13() { } static void tst14() { - expr l = mk_let("a", none_expr(), Const("b"), Var(0)); + expr l = mk_let("a", Bool, Const("b"), Var(0)); check_serializer(l); std::cout << l << "\n"; lean_assert(closed(l)); @@ -295,7 +295,7 @@ static void tst15() { lean_assert(has_metavar(Pi({a, m}, a))); lean_assert(has_metavar(Fun({a, Type}, m))); lean_assert(has_metavar(Fun({a, m}, a))); - lean_assert(!has_metavar(Let({a, Type}, a))); + lean_assert(!has_metavar(Let(a, Type, Bool, a))); lean_assert(!has_metavar(mk_let(name("a"), Type, f(x), f(f(x))))); lean_assert(has_metavar(mk_let(name("a"), m, f(x), f(f(x))))); lean_assert(has_metavar(mk_let(name("a"), Type, f(m), f(f(x))))); @@ -319,7 +319,7 @@ static void tst16() { check_copy(mk_metavar("M", Bool)); check_copy(mk_lambda("x", a, Var(0))); check_copy(mk_pi("x", a, Var(0))); - check_copy(mk_let("x", none_expr(), a, Var(0))); + check_copy(mk_let("x", Bool, a, Var(0))); } static void tst17() { diff --git a/src/tests/kernel/instantiate.cpp b/src/tests/kernel/instantiate.cpp index a42e9d635..7021c08a7 100644 --- a/src/tests/kernel/instantiate.cpp +++ b/src/tests/kernel/instantiate.cpp @@ -36,7 +36,7 @@ static void tst2() { expr a = Const("a"); expr f = Const("f"); expr N = Const("N"); - expr F1 = Let({x, a}, f(x)); + expr F1 = Let(x, N, a, f(x)); lean_assert(head_beta_reduce(F1) == F1); }