From 3c878ecd01d807ea6e3382809a1b3f4cafad0bb1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 16:40:17 -0800 Subject: [PATCH] feat(kernel): add let-expressions to the kernel The frontend is still using the old "let-expression macros". We will use the new let-expressions to implement the new tactic framework. --- src/api/expr.cpp | 1 + src/api/lean_expr.h | 1 + src/frontends/lean/builtin_exprs.cpp | 3 +- src/frontends/lean/elaborator.cpp | 10 +++++ src/frontends/lean/parser.cpp | 6 +++ src/frontends/lean/pp.cpp | 7 +++- src/kernel/default_converter.cpp | 17 +++++--- src/kernel/equiv_manager.cpp | 6 +++ src/kernel/expr.cpp | 41 +++++++++++++++++-- src/kernel/expr.h | 32 +++++++++++++-- src/kernel/expr_eq_fn.cpp | 7 ++++ src/kernel/for_each_fn.cpp | 5 +++ src/kernel/metavar.cpp | 9 ++++ src/kernel/replace_fn.cpp | 6 +++ src/kernel/type_checker.cpp | 20 +++++++++ src/kernel/type_checker.h | 1 + src/library/abstract_expr_manager.cpp | 6 +++ src/library/blast/congruence_closure.cpp | 3 ++ src/library/blast/discr_tree.cpp | 2 + src/library/blast/forward/ematch.cpp | 3 ++ .../blast/forward/forward_extension.cpp | 3 ++ src/library/blast/forward/pattern.cpp | 3 ++ src/library/blast/simplifier/ceqv.cpp | 3 ++ src/library/blast/simplifier/simplifier.cpp | 3 ++ src/library/class.cpp | 2 +- src/library/deep_copy.cpp | 1 + src/library/defeq_simplifier.cpp | 3 ++ src/library/definition_cache.cpp | 5 +++ src/library/definitional/equations.cpp | 7 ++++ src/library/export.cpp | 4 ++ src/library/expr_lt.cpp | 18 ++++++++ src/library/kernel_serializer.cpp | 10 +++++ src/library/let.cpp | 12 +++--- src/library/let.h | 6 ++- src/library/light_lt_manager.cpp | 6 +++ src/library/locals.cpp | 5 +++ src/library/match.cpp | 3 ++ src/library/max_sharing.cpp | 21 ++++++++-- src/library/normalize.cpp | 3 ++ src/library/print.cpp | 15 ++++++- src/library/replace_visitor.cpp | 8 ++++ src/library/replace_visitor.h | 1 + src/library/type_context.cpp | 14 ++++++- src/library/unfold_macros.cpp | 7 ++++ src/library/unifier.cpp | 1 + src/tests/kernel/expr.cpp | 2 + 46 files changed, 321 insertions(+), 31 deletions(-) diff --git a/src/api/expr.cpp b/src/api/expr.cpp index 8bb1dee7ba..a4fa02b0e9 100644 --- a/src/api/expr.cpp +++ b/src/api/expr.cpp @@ -170,6 +170,7 @@ lean_expr_kind lean_expr_get_kind(lean_expr e) { case expr_kind::App: return LEAN_EXPR_APP; case expr_kind::Lambda: return LEAN_EXPR_LAMBDA; case expr_kind::Pi: return LEAN_EXPR_PI; + case expr_kind::Let: return LEAN_EXPR_LET; case expr_kind::Macro: return LEAN_EXPR_MACRO; } lean_unreachable(); diff --git a/src/api/lean_expr.h b/src/api/lean_expr.h index cec7816e0c..492f25acf3 100644 --- a/src/api/lean_expr.h +++ b/src/api/lean_expr.h @@ -34,6 +34,7 @@ typedef enum { LEAN_EXPR_APP, LEAN_EXPR_LAMBDA, LEAN_EXPR_PI, + LEAN_EXPR_LET, LEAN_EXPR_MACRO, } lean_expr_kind; diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 15bb28b70a..1942ebba90 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -126,7 +126,8 @@ static expr parse_let(parser & p, pos_info const & pos) { v = p.save_pos(mk_let_value(v), id_pos); p.add_local_expr(id, v); expr b = parse_let_body(p, pos); - return p.save_pos(mk_let(id, v, b), pos); + // TODO(Leo): use let-expression after we reimplement elaborator + return p.save_pos(mk_let_macro(id, v, b), pos); } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d10b2570d4..2b91dad261 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1747,6 +1747,9 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) { case expr_kind::Lambda: return visit_lambda(e, cs); case expr_kind::Pi: return visit_pi(e, cs); case expr_kind::App: return visit_app(e, cs); + case expr_kind::Let: + // NOT IMPLEMENTED YET + lean_unreachable(); } lean_unreachable(); // LCOV_EXCL_LINE } @@ -2199,6 +2202,13 @@ static void visit_unassigned_mvars(expr const & e, std::function args; for (unsigned i = 0; i < macro_num_args(e); i++) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 61dcbdd4c6..42b787f10c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -829,7 +829,7 @@ auto pretty_fn::pp_macro(expr const & e) -> result { auto pretty_fn::pp_let(expr e) -> result { buffer> decls; while (true) { - if (!is_let(e)) + if (!is_let_macro(e)) break; name n = get_let_var_name(e); expr v = get_let_value(e); @@ -1263,7 +1263,7 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { if (is_placeholder(e)) return result(*g_placeholder_fmt); if (is_show(e)) return pp_show(e); if (is_have(e)) return pp_have(e); - if (is_let(e)) return pp_let(e); + if (is_let_macro(e)) return pp_let(e); if (is_typed_expr(e)) return pp(get_typed_expr_expr(e)); if (is_let_value(e)) return pp(get_let_value_expr(e)); if (m_num_nat_coe) @@ -1282,6 +1282,9 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result { case expr_kind::Lambda: return pp_lambda(e); case expr_kind::Pi: return pp_pi(e); case expr_kind::Macro: return pp_macro(e); + case expr_kind::Let: + // NOT IMPLEMENTED YET + lean_unreachable(); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 7a78400d66..8086f18c0b 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -68,7 +68,7 @@ expr default_converter::whnf_core(expr const & e) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: return e; - case expr_kind::Macro: case expr_kind::App: + case expr_kind::Macro: case expr_kind::App: case expr_kind::Let: break; } @@ -82,7 +82,7 @@ expr default_converter::whnf_core(expr const & e) { // do the actual work expr r; switch (e.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Macro: @@ -108,7 +108,11 @@ expr default_converter::whnf_core(expr const & e) { r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data())); } break; - }} + } + case expr_kind::Let: + r = whnf_core(instantiate(let_body(e), let_value(e))); + break; + } if (m_memoize) m_whnf_core_cache.insert(mk_pair(e, r)); @@ -190,7 +194,8 @@ pair default_converter::whnf(expr const & e_prime) { switch (e_prime.kind()) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: return to_ecs(e_prime); - case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant: + case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: + case expr_kind::Constant: case expr_kind::Let: break; } @@ -300,8 +305,8 @@ lbool default_converter::quick_is_def_eq(expr const & t, expr const & s, constra return to_lbool(is_def_eq(sort_level(t), sort_level(s), cs)); case expr_kind::Meta: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Var: case expr_kind::Local: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Macro: + case expr_kind::Var: case expr_kind::Local: case expr_kind::App: + case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let: // We do not handle these cases in this method. break; } diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp index 644aaee807..29a024fbac 100644 --- a/src/kernel/equiv_manager.cpp +++ b/src/kernel/equiv_manager.cpp @@ -92,6 +92,12 @@ bool equiv_manager::is_equiv_core(expr const & a, expr const & b) { case expr_kind::Sort: result = sort_level(a) == sort_level(b); break; + case expr_kind::Let: + result = + is_equiv_core(let_type(a), let_type(b)) && + is_equiv_core(let_value(a), let_value(b)) && + is_equiv_core(let_body(a), let_body(b)); + break; case expr_kind::Macro: if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b)) return false; diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 4ecb3401c4..49b17e8c44 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -240,6 +240,29 @@ void expr_sort::dealloc() { get_sort_allocator().recycle(this); } +// Let expressions +DEF_THREAD_MEMORY_POOL(get_let_allocator, sizeof(expr_let)); +expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b, tag g): + expr_composite(expr_kind::Let, + ::lean::hash(::lean::hash(t.hash(), v.hash()), b.hash()), + t.has_expr_metavar() || v.has_expr_metavar() || b.has_expr_metavar(), + t.has_univ_metavar() || v.has_univ_metavar() || b.has_univ_metavar(), + t.has_local() || v.has_local() || b.has_local(), + t.has_param_univ() || v.has_param_univ() || b.has_param_univ(), + inc_weight(add_weight(add_weight(get_weight(t), get_weight(v)), get_weight(b))), + std::max(std::max(get_free_var_range(t), get_free_var_range(v)), dec(get_free_var_range(b))), + g), + m_name(n), m_type(t), m_value(v), m_body(b) { + m_hash = ::lean::hash(m_hash, m_weight); +} +void expr_let::dealloc(buffer & todelete) { + dec_ref(m_body, todelete); + dec_ref(m_value, todelete); + dec_ref(m_type, todelete); + this->~expr_let(); + get_let_allocator().recycle(this); +} + // Macro definition bool macro_definition_cell::lt(macro_definition_cell const &) const { return false; } bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); } @@ -361,6 +384,9 @@ expr mk_app(expr const & f, expr const & a, tag g) { expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i, tag g) { return cache(expr(new (get_binding_allocator().allocate()) expr_binding(k, n, t, e, i, g))); } +expr mk_let(name const & n, expr const & t, expr const & v, expr const & b, tag g) { + return cache(expr(new (get_let_allocator().allocate()) expr_let(n, t, v, b, g))); +} expr mk_sort(level const & l, tag g) { return cache(expr(new (get_sort_allocator().allocate()) expr_sort(l, g))); } @@ -385,7 +411,8 @@ void expr_cell::dealloc() { case expr_kind::App: static_cast(it)->dealloc(todo); break; case expr_kind::Lambda: case expr_kind::Pi: static_cast(it)->dealloc(todo); break; - } + case expr_kind::Let: static_cast(it)->dealloc(todo); break; + } } } catch (std::bad_alloc&) { // We need this catch, because push_back may fail when expanding the buffer. @@ -510,7 +537,7 @@ unsigned get_weight(expr const & e) { case expr_kind::Meta: case expr_kind::Local: return 1; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro: - case expr_kind::App: + case expr_kind::App: case expr_kind::Let: return static_cast(e.raw())->m_weight; } lean_unreachable(); // LCOV_EXCL_LINE @@ -591,6 +618,13 @@ expr update_macro(expr const & e, unsigned num, expr const * args) { return mk_macro(to_macro(e)->m_definition, num, args, e.get_tag()); } +expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body) { + if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_value) || !is_eqp(let_body(e), new_body)) + return mk_let(let_name(e), new_type, new_value, new_body); + else + return e; +} + bool is_atomic(expr const & e) { switch (e.kind()) { case expr_kind::Constant: case expr_kind::Sort: @@ -600,7 +634,7 @@ bool is_atomic(expr const & e) { return to_macro(e)->get_num_args() == 0; case expr_kind::App: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Lambda: - case expr_kind::Pi: + case expr_kind::Pi: case expr_kind::Let: return false; } lean_unreachable(); // LCOV_EXCL_LINE @@ -691,6 +725,7 @@ std::ostream & operator<<(std::ostream & out, expr_kind const & k) { case expr_kind::Lambda: out << "Lambda"; break; case expr_kind::Pi: out << "Pi"; break; case expr_kind::Macro: out << "Macro"; break; + case expr_kind::Let: out << "Let"; break; } return out; } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 339229e83f..2968619c81 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -41,10 +41,10 @@ class expr; | App expr expr | Lambda name expr expr | Pi name expr expr - + | Let name expr expr expr | Macro macro */ -enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Lambda, Pi, Macro }; +enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Lambda, Pi, Let, Macro }; class expr_cell { protected: // The bits of the following field mean: @@ -138,8 +138,8 @@ public: friend expr mk_app(expr const & f, expr const & a, tag g); friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i, tag g); + friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b, tag g); friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g); - friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } }; @@ -298,6 +298,22 @@ public: binder const & get_binder() const { return m_binder; } }; +/** \brief Let-expressions */ +class expr_let : public expr_composite { + 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, expr const & t, expr const & v, expr const & b, tag g); + 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 */ class expr_sort : public expr_cell { level m_level; @@ -397,6 +413,7 @@ inline bool is_macro(expr_ptr e) { return e->kind() == expr_kind::Macro; } inline bool is_app(expr_ptr e) { return e->kind() == expr_kind::App; } inline bool is_lambda(expr_ptr e) { return e->kind() == expr_kind::Lambda; } inline bool is_pi(expr_ptr e) { return e->kind() == expr_kind::Pi; } +inline bool is_let(expr_ptr e) { return e->kind() == expr_kind::Let; } inline bool is_sort(expr_ptr e) { return e->kind() == expr_kind::Sort; } inline bool is_binding(expr_ptr e) { return is_lambda(e) || is_pi(e); } inline bool is_mlocal(expr_ptr e) { return is_metavar(e) || is_local(e); } @@ -450,6 +467,7 @@ inline expr mk_lambda(name const & n, expr const & t, expr const & e, inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info(), tag g = nulltag) { return mk_binding(expr_kind::Pi, n, t, e, i, g); } +expr mk_let(name const & n, expr const & t, expr const & v, expr const & b, tag g = nulltag); expr mk_sort(level const & l, tag g = nulltag); expr mk_Prop(); @@ -496,6 +514,7 @@ inline expr_sort * to_sort(expr_ptr e) { lean_assert(is_sort(e)); inline expr_mlocal * to_mlocal(expr_ptr e) { lean_assert(is_mlocal(e)); return static_cast(e); } inline expr_local * to_local(expr_ptr e) { lean_assert(is_local(e)); return static_cast(e); } inline expr_mlocal * to_metavar(expr_ptr e) { lean_assert(is_metavar(e)); return static_cast(e); } +inline expr_let * to_let(expr_ptr e) { lean_assert(is_let(e)); return static_cast(e); } inline expr_macro * to_macro(expr_ptr e) { lean_assert(is_macro(e)); return static_cast(e); } // ======================================= @@ -524,6 +543,11 @@ inline name const & mlocal_name(expr_ptr e) { return to_mlocal(e)->g inline expr const & mlocal_type(expr_ptr e) { return to_mlocal(e)->get_type(); } inline name const & local_pp_name(expr_ptr e) { return to_local(e)->get_pp_name(); } inline binder_info const & local_info(expr_ptr e) { return to_local(e)->get_info(); } +inline name const & let_name(expr_ptr e) { return to_let(e)->get_name(); } +inline expr const & let_type(expr_ptr e) { return to_let(e)->get_type(); } +inline expr const & let_value(expr_ptr e) { return to_let(e)->get_value(); } +inline expr const & let_body(expr_ptr e) { return to_let(e)->get_body(); } + 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(); } @@ -609,6 +633,8 @@ expr update_local(expr const & e, binder_info const & bi); expr update_sort(expr const & e, level const & new_level); expr update_constant(expr const & e, levels const & new_levels); expr update_macro(expr const & e, unsigned num, expr const * args); +expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body); + // ======================================= // ======================================= diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 30d02c85b1..572119942b 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -97,6 +97,13 @@ class expr_eq_fn { apply(binding_body(a), binding_body(b)) && (!CompareBinderInfo || binding_name(a) == binding_name(b)) && (!CompareBinderInfo || binding_info(a) == binding_info(b)); + case expr_kind::Let: + check_system(); + return + apply(let_type(a), let_type(b)) && + apply(let_value(a), let_value(b)) && + apply(let_body(a), let_body(b)) && + (!CompareBinderInfo || let_name(a) == let_name(b)); case expr_kind::Sort: return sort_level(a) == sort_level(b); case expr_kind::Macro: diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp index 470ecf98b6..320d3c7510 100644 --- a/src/kernel/for_each_fn.cpp +++ b/src/kernel/for_each_fn.cpp @@ -106,6 +106,11 @@ class for_each_fn { todo.emplace_back(binding_body(e), offset + 1); todo.emplace_back(binding_domain(e), offset); goto begin_loop; + case expr_kind::Let: + todo.emplace_back(let_body(e), offset + 1); + todo.emplace_back(let_value(e), offset); + todo.emplace_back(let_type(e), offset); + goto begin_loop; } } } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 8e36e339c4..b6218f1d9a 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -216,6 +216,14 @@ protected: return update_binding(e, new_d, new_b); } + expr visit_let(expr const & e) { + lean_assert(is_let(e)); + expr new_t = visit(let_type(e)); + expr new_v = visit(let_value(e)); + expr new_b = visit(let_body(e)); + return update_let(e, new_t, new_v, new_b); + } + expr visit(expr const & e) { if (!has_metavar(e)) return e; @@ -238,6 +246,7 @@ protected: case expr_kind::App: return save_result(e, visit_app(e)); case expr_kind::Lambda: case expr_kind::Pi: return save_result(e, visit_binding(e)); + case expr_kind::Let: return save_result(e, visit_let(e)); } lean_unreachable(); } diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 69d0f2e41f..602bf6036f 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -58,6 +58,12 @@ class replace_rec_fn { expr new_b = apply(binding_body(e), offset+1); return save_result(e, offset, update_binding(e, new_d, new_b), shared); } + case expr_kind::Let: { + expr new_t = apply(let_type(e), offset); + expr new_v = apply(let_value(e), offset); + expr new_b = apply(let_body(e), offset+1); + return save_result(e, offset, update_let(e, new_t, new_v, new_b), shared); + } case expr_kind::Macro: { buffer new_args; unsigned nargs = macro_num_args(e); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index c55c4059ab..93b80c6d9d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -300,6 +300,25 @@ pair type_checker::infer_app(expr const & e, bool infer_on } } +pair type_checker::infer_let(expr const & e, bool infer_only) { + if (!infer_only) { + pair dtcs = infer_type_core(let_type(e), infer_only); + pair scs = ensure_sort_core(dtcs.first, e); + pair vcs = infer_type_core(let_value(e), infer_only); + expr v_type = vcs.first; + // TODO(Leo): we will remove justifications in the future. + as_delayed_justification jst(mk_justification("let mismatch")); + pair dcs = is_def_eq(v_type, let_type(e), jst); + if (!dcs.first) { + throw_kernel_exception(m_env, e, + [=](formatter const & fmt) { + return pp_def_type_mismatch(fmt, let_name(e), let_type(e), v_type, true); + }); + } + } + return infer_type_core(instantiate(let_body(e), let_value(e)), infer_only); +} + expr type_checker::infer_type_core(expr const & e, bool infer_only, constraint_seq & cs) { auto r = infer_type_core(e, infer_only); cs = cs + r.second; @@ -338,6 +357,7 @@ pair type_checker::infer_type_core(expr const & e, bool in case expr_kind::Lambda: r = infer_lambda(e, infer_only); break; case expr_kind::Pi: r = infer_pi(e, infer_only); break; case expr_kind::App: r = infer_app(e, infer_only); break; + case expr_kind::Let: r = infer_let(e, infer_only); break; } if (m_memoize) diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index ebf3f0aabc..2eb88a7fea 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -126,6 +126,7 @@ class type_checker { pair infer_lambda(expr const & e, bool infer_only); pair infer_pi(expr const & e, bool infer_only); pair infer_app(expr const & e, bool infer_only); + pair infer_let(expr const & e, bool infer_only); pair infer_type_core(expr const & e, bool infer_only); pair infer_type(expr const & e); expr infer_type_core(expr const & e, bool infer_only, constraint_seq & cs); diff --git a/src/library/abstract_expr_manager.cpp b/src/library/abstract_expr_manager.cpp index 392daaf948..67cf4bedfc 100644 --- a/src/library/abstract_expr_manager.cpp +++ b/src/library/abstract_expr_manager.cpp @@ -31,6 +31,9 @@ unsigned abstract_expr_manager::hash(expr const & e) { h = ::lean::hash(h, hash(binding_body(e))); m_locals.pop_back(); return h; + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::App: buffer args; expr const & f = get_app_args(e, args); @@ -80,6 +83,9 @@ bool abstract_expr_manager::is_equal(expr const & a, expr const & b) { is_eq = is_equal(binding_body(a), binding_body(b)); m_locals.pop_back(); return is_eq; + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::Macro: if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b)) return false; diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index 555ef7fc1c..ab336b18ca 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -957,6 +957,9 @@ void congruence_closure::internalize_core(name R, expr const & e, bool toplevel, switch (e.kind()) { case expr_kind::Var: lean_unreachable(); + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::Sort: return; case expr_kind::Constant: case expr_kind::Local: diff --git a/src/library/blast/discr_tree.cpp b/src/library/blast/discr_tree.cpp index b21a7769fe..6c0c943d1b 100644 --- a/src/library/blast/discr_tree.cpp +++ b/src/library/blast/discr_tree.cpp @@ -235,6 +235,7 @@ auto discr_tree::insert_erase(node && n, bool is_root, buffer> lean_unreachable(); case expr_kind::Sort: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro: + case expr_kind::Let: // unsupported return insert_erase_atom(std::move(n), edge(edge_kind::Unsupported), todo, v, skip, ins); } @@ -331,6 +332,7 @@ bool discr_tree::find(node const & n, list> todo, std::function lean_unreachable(); case expr_kind::Sort: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro: + case expr_kind::Let: // unsupported return find_atom(n, edge(edge_kind::Unsupported), tail(todo), fn); } diff --git a/src/library/blast/forward/ematch.cpp b/src/library/blast/forward/ematch.cpp index c05e656bd0..dd639fa1c1 100644 --- a/src/library/blast/forward/ematch.cpp +++ b/src/library/blast/forward/ematch.cpp @@ -76,6 +76,9 @@ public: for (unsigned i = 0; i < macro_num_args(e); i++) collect_apps(macro_arg(e, i)); break; + case expr_kind::Let: + // let-expressions must be unfolded + lean_unreachable(); case expr_kind::App: { buffer args; expr const & f = get_app_args(e, args); diff --git a/src/library/blast/forward/forward_extension.cpp b/src/library/blast/forward/forward_extension.cpp index 9d773a935a..c3f6036172 100644 --- a/src/library/blast/forward/forward_extension.cpp +++ b/src/library/blast/forward/forward_extension.cpp @@ -52,6 +52,9 @@ void forward_branch_extension::index_expr(expr const & e) { case expr_kind::Pi: // TODO(dhs): confirm that I only index quantified-free hypotheses break; + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::App: index_expr(app_fn(e)); index_expr(app_arg(e)); diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index 0a39132a66..88b0b7d1de 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -367,6 +367,9 @@ struct mk_hi_lemma_fn { case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: return candidate_set(); + case expr_kind::Let: + // let-expressions must be unfolded + lean_unreachable(); case expr_kind::Lambda: if (has_idx_metavar(a)) return candidate_set(candidate(a)); diff --git a/src/library/blast/simplifier/ceqv.cpp b/src/library/blast/simplifier/ceqv.cpp index 2123c7b126..9560d08bba 100644 --- a/src/library/blast/simplifier/ceqv.cpp +++ b/src/library/blast/simplifier/ceqv.cpp @@ -219,6 +219,9 @@ static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, return is_permutation(binding_domain(lhs), binding_domain(rhs), offset, p) && is_permutation(binding_body(lhs), binding_body(rhs), offset+1, p); + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::App: return is_permutation(app_fn(lhs), app_fn(rhs), offset, p) && diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp index b5e2747957..fb78806a26 100644 --- a/src/library/blast/simplifier/simplifier.cpp +++ b/src/library/blast/simplifier/simplifier.cpp @@ -430,6 +430,9 @@ result simplifier::simplify(expr const & e, bool is_root) { case expr_kind::App: r = join(r, simplify_app(r.get_new())); break; + case expr_kind::Let: + // whnf unfolds let-expressions + lean_unreachable(); } if (!m_top_down) r = join(r, rewrite(whnf_eta(r.get_new()))); diff --git a/src/library/class.cpp b/src/library/class.cpp index 6e5504735c..34ac5e21de 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -397,7 +397,7 @@ static lbool is_quick_ext_class(type_checker const & tc, expr const & type, name while (true) { switch (it->kind()) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Local: - case expr_kind::Meta: case expr_kind::Lambda: + case expr_kind::Meta: case expr_kind::Lambda: case expr_kind::Let: return l_false; case expr_kind::Macro: return l_undef; diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index 03cc8ebd44..c9265efe46 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -21,6 +21,7 @@ expr copy(expr const & a) { case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a)); case expr_kind::Local: return mk_local(mlocal_name(a), local_pp_name(a), mlocal_type(a), local_info(a)); + case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/defeq_simplifier.cpp b/src/library/defeq_simplifier.cpp index fd30f4f40b..02678b4953 100644 --- a/src/library/defeq_simplifier.cpp +++ b/src/library/defeq_simplifier.cpp @@ -140,6 +140,9 @@ class defeq_simplify_fn { case expr_kind::App: e = defeq_simplify_app(e); break; + case expr_kind::Let: + lean_unreachable(); + // whnf expands let-expressions } if (!m_top_down) e = rewrite(whnf_eta(e)); diff --git a/src/library/definition_cache.cpp b/src/library/definition_cache.cpp index d94355b2b4..8cb7efc790 100644 --- a/src/library/definition_cache.cpp +++ b/src/library/definition_cache.cpp @@ -101,6 +101,11 @@ class expr_eq_modulo_placeholders_fn { compare(binding_domain(a), binding_domain(b)) && compare(binding_body(a), binding_body(b)) && binding_info(a) == binding_info(b); + case expr_kind::Let: + return + compare(let_type(a), let_type(b)) && + compare(let_value(a), let_value(b)) && + compare(let_body(a), let_body(b)); case expr_kind::Sort: return compare(sort_level(a), sort_level(b)); case expr_kind::Macro: diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index 58c248b836..e8759556d4 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -1209,6 +1209,9 @@ class equation_compiler_fn { } return true; } + case expr_kind::Let: + // TODO(Leo): improve + return check_rhs(instantiate(let_body(e), let_value(e)), arg); case expr_kind::Lambda: case expr_kind::Pi: if (!check_rhs(binding_domain(e), arg)) { @@ -1416,6 +1419,10 @@ class equation_compiler_fn { expr local = mk_local(mk_fresh_name(), binding_name(e), new_domain, binding_info(e)); expr new_body = elim(instantiate(binding_body(e), local), b); return copy_tag(e, Pi(local, new_body)); + } + case expr_kind::Let: { + // TODO(Leo): improve + return elim(instantiate(let_body(e), let_value(e)), b); }} lean_unreachable(); } diff --git a/src/library/export.cpp b/src/library/export.cpp index cfa655c36c..cdd0b65210 100644 --- a/src/library/export.cpp +++ b/src/library/export.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "kernel/expr_maps.h" #include "kernel/for_each_fn.h" +#include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" #include "library/module.h" #include "library/unfold_macros.h" @@ -160,6 +161,9 @@ class exporter { i = m_expr2idx.size(); m_out << i << " #EA " << e1 << " " << e2 << "\n"; break; + case expr_kind::Let: + i = export_expr(instantiate(let_body(e), let_value(e))); + break; case expr_kind::Lambda: i = export_binding(e, "#EL"); break; diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index 19ede78f94..aa0228e5c2 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -38,6 +38,13 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { return is_lt(binding_domain(a), binding_domain(b), use_hash); else return is_lt(binding_body(a), binding_body(b), use_hash); + case expr_kind::Let: + if (let_type(a) != let_type(b)) + return is_lt(let_type(a), let_type(b), use_hash); + else if (let_value(a) != let_value(b)) + return is_lt(let_value(a), let_value(b), use_hash); + else + return is_lt(let_body(a), let_body(b), use_hash); case expr_kind::Sort: return is_lt(sort_level(a), sort_level(b), use_hash); case expr_kind::Local: case expr_kind::Meta: @@ -137,6 +144,17 @@ bool is_lt_no_level_params(expr const & a, expr const & b) { return false; else return is_lt_no_level_params(binding_body(a), binding_body(b)); + case expr_kind::Let: + if (is_lt_no_level_params(let_type(a), let_type(b))) + return true; + else if (is_lt_no_level_params(let_type(b), let_type(a))) + return false; + else if (is_lt_no_level_params(let_value(a), let_value(b))) + return true; + else if (is_lt_no_level_params(let_value(b), let_value(a))) + return false; + else + return is_lt_no_level_params(let_body(a), let_body(b)); case expr_kind::Sort: return is_lt_no_level_params(sort_level(a), sort_level(b)); case expr_kind::Local: case expr_kind::Meta: diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 560b4111cd..1f9880ac3f 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -182,6 +182,10 @@ class expr_serializer : public object_serializer(macro_def(e).raw()) != nullptr; } name const & get_let_var_name(expr const & e) { - lean_assert(is_let(e)); + lean_assert(is_let_macro(e)); return static_cast(macro_def(e).raw())->get_var_name(); } expr const & get_let_value(expr const & e) { - lean_assert(is_let(e)); + lean_assert(is_let_macro(e)); return macro_arg(e, 0); } expr const & get_let_body(expr const & e) { - lean_assert(is_let(e)); + lean_assert(is_let_macro(e)); return macro_arg(e, 1); } @@ -130,7 +130,7 @@ void initialize_let() { if (num != 2) throw corrupted_stream_exception(); name n; d >> n; - return mk_let(n, args[0], args[1]); + return mk_let_macro(n, args[0], args[1]); }); } diff --git a/src/library/let.h b/src/library/let.h index fb2e1ca451..300cdb14ee 100644 --- a/src/library/let.h +++ b/src/library/let.h @@ -7,13 +7,15 @@ Author: Leonardo de Moura #pragma once #include "kernel/expr.h" +// TODO(Leo): delete this module after we move to kernel let-expr + namespace lean { expr mk_let_value(expr const & e); bool is_let_value(expr const & e); expr get_let_value_expr(expr const e); -expr mk_let(name const & n, expr const & v, expr const & b); -bool is_let(expr const & e); +expr mk_let_macro(name const & n, expr const & v, expr const & b); +bool is_let_macro(expr const & e); name const & get_let_var_name(expr const & e); expr const & get_let_value(expr const & e); expr const & get_let_body(expr const & e); diff --git a/src/library/light_lt_manager.cpp b/src/library/light_lt_manager.cpp index 77e8a13a25..d5a5bd0bfc 100644 --- a/src/library/light_lt_manager.cpp +++ b/src/library/light_lt_manager.cpp @@ -27,6 +27,9 @@ unsigned light_lt_manager::get_weight_core(expr const & e) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: return 1; + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::Lambda: case expr_kind::Pi: return safe_add(1, safe_add(get_weight(binding_domain(e)), get_weight(binding_body(e)))); case expr_kind::Macro: @@ -76,6 +79,9 @@ bool light_lt_manager::is_lt(expr const & a, expr const & b) { if (a.kind() != b.kind()) return a.kind() < b.kind(); if (a == b) return false; switch (a.kind()) { + case expr_kind::Let: + // Let-expressions must be unfolded before invoking this method + lean_unreachable(); case expr_kind::Var: return var_idx(a) < var_idx(b); case expr_kind::Constant: diff --git a/src/library/locals.cpp b/src/library/locals.cpp index a91e9aa4ec..e3c5e2600d 100644 --- a/src/library/locals.cpp +++ b/src/library/locals.cpp @@ -95,6 +95,11 @@ void collect_locals(expr const & e, collected_locals & ls, bool restricted) { visit(binding_domain(e)); visit(binding_body(e)); break; + case expr_kind::Let: + visit(let_type(e)); + visit(let_value(e)); + visit(let_body(e)); + break; } }; visit(e); diff --git a/src/library/match.cpp b/src/library/match.cpp index 81ab796179..922e614b69 100644 --- a/src/library/match.cpp +++ b/src/library/match.cpp @@ -323,6 +323,9 @@ class match_fn : public match_context { return match_macro(p, t); case expr_kind::App: return match_app(p, t); + case expr_kind::Let: + // TODO(Leo): this module will be deleted in the future. + lean_unreachable(); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index d9e99e761f..c047bb6612 100644 --- a/src/library/max_sharing.cpp +++ b/src/library/max_sharing.cpp @@ -62,12 +62,25 @@ struct max_sharing_fn::imp { case expr_kind::Sort: res = update_sort(a, apply(sort_level(a))); break; - case expr_kind::App: - res = update_app(a, apply(app_fn(a)), apply(app_arg(a))); + case expr_kind::App: { + expr new_f = apply(app_fn(a)); + expr new_a = apply(app_arg(a)); + res = update_app(a, new_f, new_a); break; - case expr_kind::Lambda: case expr_kind::Pi: - res = update_binding(a, apply(binding_domain(a)), apply(binding_body(a))); + } + case expr_kind::Lambda: case expr_kind::Pi: { + expr new_d = apply(binding_domain(a)); + expr new_b = apply(binding_body(a)); + res = update_binding(a, new_d, new_b); break; + } + case expr_kind::Let: { + expr new_t = apply(let_type(a)); + expr new_v = apply(let_value(a)); + expr new_b = apply(let_body(a)); + res = update_let(a, new_t, new_v, new_b); + break; + } case expr_kind::Meta: case expr_kind::Local: res = update_mlocal(a, apply(mlocal_type(a))); break; diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 9f79dbf030..4b9192c66f 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -401,6 +401,9 @@ class normalize_fn { return normalize_binding(e); case expr_kind::App: return normalize_app(e); + case expr_kind::Let: + // whnf unfolds let-exprs + lean_unreachable(); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/print.cpp b/src/library/print.cpp index cc5fcbf345..965353577f 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -21,7 +21,8 @@ bool is_used_name(expr const & t, name const & n) { if (found) return false; // already found if ((is_constant(e) && const_name(e) == n) // t has a constant named n || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)) // t has a local constant named n - || (is_let(e) && get_let_var_name(e) == n)) { + // TODO(Leo): remove after we transition to kernel Let-expression + || (is_let_macro(e) && get_let_var_name(e) == n)) { found = true; return false; // found it } @@ -178,6 +179,15 @@ struct print_expr_fn { print_child(e); } + void print_let(expr const & e) { + out() << "let " << let_name(e) << " : "; + print(let_type(e)); + out() << " := "; + print(let_value(e)); + out() << " in "; + print(let_body(e)); + } + void print_const(expr const & a) { list const & ls = const_levels(a); out() << const_name(a); @@ -212,6 +222,9 @@ struct print_expr_fn { case expr_kind::App: print_app(a); break; + case expr_kind::Let: + print_let(a); + break; case expr_kind::Lambda: print_binding("fun", a); break; diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp index 572f9ef335..009b447d80 100644 --- a/src/library/replace_visitor.cpp +++ b/src/library/replace_visitor.cpp @@ -30,6 +30,13 @@ expr replace_visitor::visit_binding(expr const & e) { } expr replace_visitor::visit_lambda(expr const & e) { return visit_binding(e); } expr replace_visitor::visit_pi(expr const & e) { return visit_binding(e); } +expr replace_visitor::visit_let(expr const & e) { + lean_assert(is_let(e)); + expr new_t = visit(let_type(e)); + expr new_v = visit(let_value(e)); + expr new_b = visit(let_body(e)); + return update_let(e, new_t, new_v, new_b); +} expr replace_visitor::visit_macro(expr const & e) { lean_assert(is_macro(e)); buffer new_args; @@ -62,6 +69,7 @@ expr replace_visitor::visit(expr const & e) { case expr_kind::App: return save_result(e, visit_app(e), shared); case expr_kind::Lambda: return save_result(e, visit_lambda(e), shared); case expr_kind::Pi: return save_result(e, visit_pi(e), shared); + case expr_kind::Let: return save_result(e, visit_let(e), shared); } lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/library/replace_visitor.h b/src/library/replace_visitor.h index bfe389e2ea..e525b1a115 100644 --- a/src/library/replace_visitor.h +++ b/src/library/replace_visitor.h @@ -30,6 +30,7 @@ protected: virtual expr visit_binding(expr const &); virtual expr visit_lambda(expr const &); virtual expr visit_pi(expr const &); + virtual expr visit_let(expr const & e); virtual expr visit(expr const &); public: expr operator()(expr const & e) { return visit(e); } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 95b695795b..1af2496713 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -219,6 +219,8 @@ expr type_context::whnf_core(expr const & e) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda: return e; + case expr_kind::Let: + return whnf_core(instantiate(let_body(e), let_value(e))); case expr_kind::Macro: if (auto m = expand_macro(e)) return whnf_core(*m); @@ -309,6 +311,7 @@ expr type_context::whnf(expr const & e) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: return e; case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant: + case expr_kind::Let: break; } @@ -884,6 +887,7 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) { case expr_kind::Meta: case expr_kind::Var: case expr_kind::Local: case expr_kind::App: case expr_kind::Constant: case expr_kind::Macro: + case expr_kind::Let: // We do not handle these cases in this method. break; } @@ -1221,6 +1225,9 @@ expr type_context::infer(expr const & e) { case expr_kind::App: r = infer_app(e); break; + case expr_kind::Let: + r = infer(instantiate(let_body(e), let_value(e))); + break; } m_infer_cache.insert(mk_pair(e, r)); return r; @@ -1270,7 +1277,7 @@ lbool type_context::is_quick_class(expr const & type, name & result) { while (true) { switch (it->kind()) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Local: - case expr_kind::Meta: case expr_kind::Lambda: + case expr_kind::Meta: case expr_kind::Lambda: case expr_kind::Let: return l_false; case expr_kind::Macro: return l_undef; @@ -1449,7 +1456,7 @@ struct type_context::unification_hint_fn { && m_owner.is_def_eq(const_levels(pattern), const_levels(e)); case expr_kind::Sort: return is_sort(e) && m_owner.is_def_eq(sort_level(pattern), sort_level(e)); - case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Macro: + case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::Let: // Remark: we do not traverse inside of binders. return pattern == e; case expr_kind::App: @@ -2120,6 +2127,9 @@ expr normalizer::normalize(expr e) { return normalize_binding(e); case expr_kind::App: return normalize_app(e); + case expr_kind::Let: + // whnf unfolds let-expressions + lean_unreachable(); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp index df64ceba56..7b5fa0f3cb 100644 --- a/src/library/unfold_macros.cpp +++ b/src/library/unfold_macros.cpp @@ -74,6 +74,11 @@ class unfold_untrusted_macros_fn { return r; } + expr visit_let(expr const & e) { + // TODO(Leo): improve + return visit(instantiate(let_body(e), let_value(e))); + } + expr visit(expr const & e) { switch (e.kind()) { case expr_kind::Sort: case expr_kind::Constant: @@ -100,6 +105,8 @@ class unfold_untrusted_macros_fn { return save_result(e, visit_app(e)); case expr_kind::Lambda: case expr_kind::Pi: return save_result(e, visit_binding(e)); + case expr_kind::Let: + return save_result(e, visit_let(e)); } lean_unreachable(); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 227c47b03b..ce121fe44d 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -2162,6 +2162,7 @@ struct unifier_fn { mk_simple_projections(); mk_bindings_imitation(); break; + case expr_kind::Let: case expr_kind::Macro: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::App: diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index bbbd95dff4..766947f855 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -124,6 +124,8 @@ static unsigned count_core(expr const & a, expr_set & s) { return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; case expr_kind::Lambda: case expr_kind::Pi: return count_core(binding_domain(a), s) + count_core(binding_body(a), s) + 1; + case expr_kind::Let: + lean_unreachable(); } return 0; }