From 1e80a9dfe902146aad34f6ebfaa19e0744b7e2f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Aug 2014 16:27:52 -0700 Subject: [PATCH] feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 31 +++++------- src/frontends/lean/elaborator.cpp | 76 +++++++++++++++++++--------- src/frontends/lean/parser.cpp | 3 ++ src/frontends/lean/pp.cpp | 46 +++-------------- src/frontends/lean/pp.h | 1 - src/library/annotation.cpp | 26 +++++++--- src/library/annotation.h | 12 +++-- src/library/print.cpp | 31 ++---------- tests/lean/run/let2.lean | 23 +++++++++ 9 files changed, 127 insertions(+), 122 deletions(-) create mode 100644 tests/lean/run/let2.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 99f5e7103..35df00b50 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -55,11 +55,6 @@ static expr parse_let_body(parser & p, pos_info const & pos) { } } -static expr mk_let(parser & p, name const & id, expr const & t, expr const & v, expr const & b, pos_info const & pos, binder_info const & bi) { - expr l = p.save_pos(mk_let_annotation(p.save_pos(mk_lambda(id, t, b, bi), pos)), pos); - return p.mk_app(l, v, pos); -} - static void parse_let_modifiers(parser & p, bool & is_fact) { while (true) { if (p.curr_is_token(g_fact)) { @@ -79,11 +74,11 @@ static expr parse_let(parser & p, pos_info const & pos) { auto pos = p.pos(); name id = p.check_atomic_id_next("invalid let declaration, identifier expected"); bool is_fact = false; - expr type, value; + optional type; + expr value; parse_let_modifiers(p, is_fact); if (p.curr_is_token(g_assign)) { p.next(); - type = p.save_pos(mk_expr_placeholder(), pos); value = p.parse_expr(); } else if (p.curr_is_token(g_colon)) { p.next(); @@ -97,22 +92,20 @@ static expr parse_let(parser & p, pos_info const & pos) { if (p.curr_is_token(g_colon)) { p.next(); type = p.parse_scoped_expr(ps, lenv); - } else { - type = p.save_pos(mk_expr_placeholder(), pos); + type = Pi(ps, *type, p); } p.check_token_next(g_assign, "invalid let declaration, ':=' expected"); value = p.parse_scoped_expr(ps, lenv); - type = Pi(ps, type, p); value = Fun(ps, value, p); } - // expr l = p.save_pos(mk_local(id, type), pos); - // p.add_local(l); - // expr body = abstract(parse_let_body(p, pos), l); - // return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact)); - // } else { - p.add_local_expr(id, p.save_pos(mk_typed_expr(type, value), p.pos_of(value))); + expr v; + if (type) + v = p.save_pos(mk_typed_expr(*type, value), p.pos_of(value)); + else + v = value; + v = p.save_pos(mk_let_value_annotation(v), pos); + p.add_local_expr(id, v); return parse_let_body(p, pos); - // } } } @@ -268,7 +261,9 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) expr prop = p.parse_expr(); p.check_token_next(g_comma, "invalid 'show' declaration, ',' expected"); expr proof = parse_proof(p, prop); - return mk_let(p, H_show, prop, proof, Var(0), pos, mk_contextual_info(false)); + expr b = p.save_pos(mk_lambda(H_show, prop, Var(0)), pos); + expr r = p.mk_app(b, proof, pos); + return p.save_pos(mk_show_annotation(r), pos); } static name g_exists_elim("exists_elim"); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 39b996e4b..769245f05 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -293,6 +293,7 @@ class elaborator { typedef std::vector constraint_vect; typedef name_map local_tactic_hints; typedef std::unique_ptr type_checker_ptr; + typedef rb_map, expr_quick_cmp> cache; elaborator_context & m_env; name_generator m_ngen; @@ -301,6 +302,7 @@ class elaborator { // representing the context where ?m was created. context m_context; // current local context: a list of local constants context m_full_context; // superset of m_context, it also contains non-contextual locals. + cache m_cache; local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. // this mapping is populated by the 'by tactic-expr' expression. @@ -309,10 +311,22 @@ class elaborator { bool m_noinfo; // when true, we do not collect information when true, we set is to true whenever we find noinfo annotation. info_manager m_pre_info_data; + // Auxiliary object to "saving" elaborator state + struct saved_state { + list m_ctx; + list m_full_ctx; + cache m_cache; + saved_state(elaborator & e): + m_ctx(e.m_context.get_data()), m_full_ctx(e.m_full_context.get_data()), m_cache(e.m_cache) {} + }; + struct scope_ctx { + elaborator & m_main; context::scope m_scope1; context::scope m_scope2; - scope_ctx(elaborator & e):m_scope1(e.m_context), m_scope2(e.m_full_context) {} + cache m_old_cache; + scope_ctx(elaborator & e):m_main(e), m_scope1(e.m_context), m_scope2(e.m_full_context), m_old_cache(e.m_cache) {} + ~scope_ctx() { m_main.m_cache = m_old_cache; } }; /** \brief Auxiliary object for creating backtracking points, and replacing the local scopes. */ @@ -321,13 +335,19 @@ class elaborator { bool m_old_noinfo; context::scope_replace m_context_scope; context::scope_replace m_full_context_scope; - new_scope(elaborator & e, list const & ctx, list const & full_ctx, bool noinfo = false): - m_main(e), m_context_scope(e.m_context, ctx), m_full_context_scope(e.m_full_context, full_ctx) { + cache m_old_cache; + new_scope(elaborator & e, saved_state const & s, bool noinfo = false): + m_main(e), + m_context_scope(e.m_context, s.m_ctx), + m_full_context_scope(e.m_full_context, s.m_full_ctx){ m_old_noinfo = m_main.m_noinfo; m_main.m_noinfo = noinfo; + m_old_cache = m_main.m_cache; + m_main.m_cache = s.m_cache; } ~new_scope() { m_main.m_noinfo = m_old_noinfo; + m_main.m_cache = m_old_cache; } }; @@ -347,14 +367,12 @@ class elaborator { elaborator & m_elab; expr m_mvar; expr m_choice; - list m_ctx; - list m_full_ctx; + saved_state m_state; unsigned m_idx; bool m_relax_main_opaque; choice_expr_elaborator(elaborator & elab, expr const & mvar, expr const & c, - list const & ctx, list const & full_ctx, - bool relax): - m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_full_ctx(full_ctx), + saved_state const & s, bool relax): + m_elab(elab), m_mvar(mvar), m_choice(c), m_state(s), m_idx(get_num_choices(m_choice)), m_relax_main_opaque(relax) { } @@ -365,7 +383,7 @@ class elaborator { expr const & f = get_app_fn(c); m_elab.save_identifier_info(f); try { - new_scope s(m_elab, m_ctx, m_full_ctx); + new_scope s(m_elab, m_state); pair rcs = m_elab.visit(c); expr r = rcs.first; constraint_seq cs = mk_eq_cnstr(m_mvar, r, justification(), m_relax_main_opaque) + rcs.second; @@ -402,18 +420,16 @@ class elaborator { list m_tactics; proof_state_seq m_tactic_result; // result produce by last executed tactic. buffer m_mvars_in_meta_type; // metavariables that occur in m_meta_type, the tactics may instantiate some of them - list m_ctx; // local context for m_meta - list m_full_ctx; + saved_state m_state; justification m_jst; bool m_relax_main_opaque; placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type, list const & local_insts, list const & instances, list const & tacs, - list const & ctx, list const & full_ctx, - justification const & j, bool ignore_failure, bool relax): + saved_state const & s, justification const & j, bool ignore_failure, bool relax): choice_elaborator(ignore_failure), m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances), - m_tactics(tacs), m_ctx(ctx), m_full_ctx(full_ctx), m_jst(j), m_relax_main_opaque(relax) { + m_tactics(tacs), m_state(s), m_jst(j), m_relax_main_opaque(relax) { collect_metavars(meta_type, m_mvars_in_meta_type); } @@ -430,7 +446,7 @@ class elaborator { } try { bool noinfo = true; - new_scope s(m_elab, m_ctx, m_full_ctx, noinfo); + new_scope s(m_elab, m_state, noinfo); pair rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc. expr r = rcs.first; buffer cs; @@ -617,8 +633,7 @@ public: */ expr mk_placeholder_meta(optional const & type, tag g, bool is_strict, constraint_seq & cs) { expr m = m_context.mk_meta(type, g); - list ctx = m_context.get_data(); - list full_ctx = m_full_context.get_data(); + saved_state st(*this); justification j = mk_failed_to_synthesize_jst(m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & /* ngen */) { expr const & mvar = get_app_fn(meta); @@ -626,7 +641,7 @@ public: name const & cls_name = const_name(get_app_fn(meta_type)); list local_insts; if (use_local_instances()) - local_insts = get_local_instances(ctx, cls_name); + local_insts = get_local_instances(st.m_ctx, cls_name); list insts = get_class_instances(meta_type); list tacs; if (!s.is_assigned(mvar)) @@ -634,7 +649,7 @@ public: if (empty(local_insts) && empty(insts) && empty(tacs)) return lazy_list(); // nothing to be done bool ignore_failure = false; // we are always strict with placeholders associated with classes - return choose(std::make_shared(*this, meta, meta_type, local_insts, insts, tacs, ctx, full_ctx, + return choose(std::make_shared(*this, meta, meta_type, local_insts, insts, tacs, st, j, ignore_failure, m_relax_main_opaque)); } else if (s.is_assigned(mvar)) { // if the metavariable is assigned and it is not a class, then we just ignore it, and return @@ -643,8 +658,8 @@ public: } else { list tacs = get_tactic_hints(env()); bool ignore_failure = !is_strict; - return choose(std::make_shared(*this, meta, meta_type, list(), list(), tacs, ctx, full_ctx, - j, ignore_failure, m_relax_main_opaque)); + return choose(std::make_shared(*this, meta, meta_type, list(), list(), + tacs, st, j, ignore_failure, m_relax_main_opaque)); } }; cs += mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::ClassInstance), false, j, m_relax_main_opaque); @@ -689,11 +704,10 @@ public: lean_assert(is_choice(e)); // Possible optimization: try to lookahead and discard some of the alternatives. expr m = m_full_context.mk_meta(t, e.get_tag()); - list ctx = m_context.get_data(); - list full_ctx = m_full_context.get_data(); + saved_state s(*this); bool relax = m_relax_main_opaque; auto fn = [=](expr const & mvar, expr const & /* type */, substitution const & /* s */, name_generator const & /* ngen */) { - return choose(std::make_shared(*this, mvar, e, ctx, full_ctx, relax)); + return choose(std::make_shared(*this, mvar, e, s, relax)); }; justification j = mk_justification("none of the overloads is applicable", some_expr(e)); cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque); @@ -1077,11 +1091,25 @@ public: return v; } + expr visit_let_value(expr const & e, constraint_seq & cs) { + if (auto p = m_cache.find(e)) { + cs += p->second; + return p->first; + } else { + auto ecs = visit(get_annotation_arg(e)); + m_cache.insert(e, mk_pair(ecs.first, ecs.second)); + cs += ecs.second; + return ecs.first; + } + } + expr visit_core(expr const & e, constraint_seq & cs) { if (is_placeholder(e)) { return visit_placeholder(e, cs); } else if (is_choice(e)) { return visit_choice(e, none_expr(), cs); + } else if (is_let_value_annotation(e)) { + return visit_let_value(e, cs); } else if (is_by(e)) { return visit_by(e, none_expr(), cs); } else if (is_noinfo(e)) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 85a2e17c3..24fe908fa 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/scoped_ext.h" #include "library/explicit.h" +#include "library/annotation.h" #include "library/num.h" #include "library/string.h" #include "library/sorry.h" @@ -281,6 +282,8 @@ expr parser::rec_save_pos(expr const & e, pos_info p) { /** \brief Create a copy of \c e, and the position of new expression with p */ expr parser::copy_with_new_pos(expr const & e, pos_info p) { + if (is_let_value_annotation(e)) + return e; switch (e.kind()) { case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Var: diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 99a036f77..3d5351fba 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -316,43 +316,10 @@ auto pretty_fn::pp_pi(expr const & e) -> result { } } -static bool is_let(expr const & e) { return is_app(e) && is_let_annotation(app_fn(e)); } static bool is_have(expr const & e) { return is_app(e) && is_have_annotation(app_fn(e)); } static bool is_show(expr const & e) { - if (!is_let(e)) - return false; - expr b = get_annotation_arg(app_fn(e)); - return is_show_aux_name(binding_name(b)) && is_var(binding_body(b), 0); -} - -auto pretty_fn::pp_let(expr e) -> result { - buffer decls; - while (true) { - if (!is_let(e)) - break; - expr v = app_arg(e); - auto p = binding_body_fresh(get_annotation_arg(app_fn(e)), true); - decls.emplace_back(p.second, v); - e = p.first; - } - if (decls.empty()) - return pp(e); - format r = g_let_fmt; - unsigned sz = decls.size(); - for (unsigned i = 0; i < sz; i++) { - auto const & d = decls[i]; - format beg = i == 0 ? space() : line(); - format sep = i < sz - 1 ? comma() : format(); - name const & n = local_pp_name(d.first); - format t = pp_child(mlocal_type(d.first), 0).first; - format v = pp_child(d.second, 0).first; - r += nest(3 + 1, compose(beg, group(format(n) + space() + colon() - + nest(n.size() + 1 + 1 + 1, space() + t) + space() + g_assign_fmt - + nest(m_indent, line() + v + sep)))); - } - format b = pp_child(e, 0).first; - r += line() + g_in_fmt + space() + nest(2 + 1, b); - return mk_result(r, 0); + return is_show_annotation(e) && is_app(get_annotation_arg(e)) && + is_lambda(app_fn(get_annotation_arg(e))); } auto pretty_fn::pp_have(expr const & e) -> result { @@ -377,9 +344,11 @@ auto pretty_fn::pp_have(expr const & e) -> result { } auto pretty_fn::pp_show(expr const & e) -> result { - expr proof = app_arg(e); - expr binding = get_annotation_arg(app_fn(e)); - format type_fmt = pp_child(binding_domain(binding), 0).first; + lean_assert(is_show(e)); + expr s = get_annotation_arg(e); + expr proof = app_arg(s); + expr type = binding_domain(app_fn(s)); + format type_fmt = pp_child(type, 0).first; format proof_fmt = pp_child(proof, 0).first; format r = g_show_fmt + space() + nest(5, type_fmt) + comma() + space() + g_from_fmt; r = group(r); @@ -418,7 +387,6 @@ auto pretty_fn::pp(expr const & e) -> result { if (is_placeholder(e)) return mk_result(g_placeholder_fmt); if (is_show(e)) return pp_show(e); - if (is_let(e)) return pp_let(e); if (is_have(e)) return pp_have(e); if (is_typed_expr(e)) return pp(get_typed_expr_expr(e)); if (auto n = to_num(e)) return pp_num(*n); diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index ff2a63499..20844d51a 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -66,7 +66,6 @@ private: result pp_app(expr const & e); result pp_lambda(expr const & e); result pp_pi(expr const & e); - result pp_let(expr e); result pp_have(expr const & e); result pp_show(expr const & e); result pp_macro(expr const & e); diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index 587e5ee40..e1c80daf9 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -91,8 +91,8 @@ expr const & get_annotation_arg(expr const & e) { return macro_arg(e, 0); } -name const & get_let_name() { - static name g_let("let"); +name const & get_let_value_name() { + static name g_let("letv"); static register_annotation_fn g_let_annotation(g_let); return g_let; } @@ -102,11 +102,21 @@ name const & get_have_name() { static register_annotation_fn g_have_annotation(g_have); return g_have; } -static name g_let_name = get_let_name(); // force 'let' annotation to be registered -static name g_have_name = get_have_name(); // force 'have' annotation to be registered -expr mk_let_annotation(expr const & e) { return mk_annotation(get_let_name(), e); } -expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); } -bool is_let_annotation(expr const & e) { return is_annotation(e, get_let_name()); } -bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); } +name const & get_show_name() { + static name g_show("show"); + static register_annotation_fn g_show_annotation(g_show); + return g_show; +} + +static name g_let_name = get_let_value_name(); // force 'let value' annotation to be registered +static name g_have_name = get_have_name(); // force 'have' annotation to be registered +static name g_show_name = get_show_name(); // force 'show' annotation to be registered + +expr mk_let_value_annotation(expr const & e) { return mk_annotation(get_let_value_name(), e); } +expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); } +expr mk_show_annotation(expr const & e) { return mk_annotation(get_show_name(), e); } +bool is_let_value_annotation(expr const & e) { return is_annotation(e, get_let_value_name()); } +bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); } +bool is_show_annotation(expr const & e) { return is_annotation(e, get_show_name()); } } diff --git a/src/library/annotation.h b/src/library/annotation.h index ac1369d2b..0e57878f8 100644 --- a/src/library/annotation.h +++ b/src/library/annotation.h @@ -40,14 +40,18 @@ expr const & get_annotation_arg(expr const & e); */ name const & get_annotation_kind(expr const & e); -/** \brief Tag \c e as a 'let'-expression. 'let' is a pre-registered annotation. */ -expr mk_let_annotation(expr const & e); +/** \brief Tag \c e as a 'let value'-expression. 'let value' is a pre-registered annotation. */ +expr mk_let_value_annotation(expr const & e); /** \brief Tag \c e as a 'have'-expression. 'have' is a pre-registered annotation. */ expr mk_have_annotation(expr const & e); -/** \brief Return true iff \c e was created using #mk_let_annotation. */ -bool is_let_annotation(expr const & e); +/** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */ +expr mk_show_annotation(expr const & e); +/** \brief Return true iff \c e was created using #mk_let_value_annotation. */ +bool is_let_value_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_have_annotation. */ bool is_have_annotation(expr const & e); +/** \brief Return true iff \c e was created using #mk_show_annotation. */ +bool is_show_annotation(expr const & e); /** \brief Return the serialization 'opcode' for annotation macros. */ std::string const & get_annotation_opcode(); diff --git a/src/library/print.cpp b/src/library/print.cpp index e30f861b3..e575274b7 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -89,35 +89,10 @@ struct print_expr_fn { } } - bool print_let(expr const & a) { - if (!is_let_annotation(a)) - return false; - expr l = get_annotation_arg(a); - if (!is_app(l) || !is_lambda(app_fn(l))) - return false; - name n = binding_name(app_fn(l)); - expr t = binding_domain(app_fn(l)); - expr b = binding_body(app_fn(l)); - expr v = app_arg(l); - n = pick_unused_name(b, n); - expr c = mk_local(n, expr()); - b = instantiate(b, c); - out() << "let " << c; - out() << " : "; - print(t); - out() << " := "; - print(v); - out() << " in "; - print_child(b); - return true; - } - void print_macro(expr const & a) { - if (!print_let(a)) { - macro_def(a).display(out()); - for (unsigned i = 0; i < macro_num_args(a); i++) { - out() << " "; print_child(macro_arg(a, i)); - } + macro_def(a).display(out()); + for (unsigned i = 0; i < macro_num_args(a); i++) { + out() << " "; print_child(macro_arg(a, i)); } } diff --git a/tests/lean/run/let2.lean b/tests/lean/run/let2.lean new file mode 100644 index 000000000..e29cd1cbc --- /dev/null +++ b/tests/lean/run/let2.lean @@ -0,0 +1,23 @@ +import logic + +definition b := + let a := true ∧ true, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a, + a := a ∧ a in + a + +check b