michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-28 16:27:52 -07:00
parent 79acd3e1b7
commit 1e80a9dfe9
9 changed files with 127 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/frontends/lean/builtin_exprs.cpp
View file

@ -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<expr> 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");

76
src/frontends/lean/elaborator.cpp
View file

@ -293,6 +293,7 @@ class elaborator {
typedef std::vector<constraint> constraint_vect;
typedef name_map<expr> local_tactic_hints;
typedef std::unique_ptr<type_checker> type_checker_ptr;
typedef rb_map<expr, pair<expr, constraint_seq>, 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<expr> m_ctx;
list<expr> 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<expr> const & ctx, list<expr> 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<expr> m_ctx;
list<expr> 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<expr> const & ctx, list<expr> 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<expr, constraint_seq> 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<tactic_hint_entry> m_tactics;
proof_state_seq m_tactic_result; // result produce by last executed tactic.
buffer<expr> m_mvars_in_meta_type; // metavariables that occur in m_meta_type, the tactics may instantiate some of them
list<expr> m_ctx; // local context for m_meta
list<expr> 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<expr> const & local_insts, list<name> const & instances, list<tactic_hint_entry> const & tacs,
list<expr> const & ctx, list<expr> 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<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc.
expr r = rcs.first;
buffer<constraint> cs;
@ -617,8 +633,7 @@ public:
*/
expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
expr m = m_context.mk_meta(type, g);
list<expr> ctx = m_context.get_data();
list<expr> 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<expr> 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<name> insts = get_class_instances(meta_type);
list<tactic_hint_entry> tacs;
if (!s.is_assigned(mvar))
@ -634,7 +649,7 @@ public:
if (empty(local_insts) && empty(insts) && empty(tacs))
return lazy_list<constraints>(); // nothing to be done
bool ignore_failure = false; // we are always strict with placeholders associated with classes
return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, local_insts, insts, tacs, ctx, full_ctx,
return choose(std::make_shared<placeholder_elaborator>(*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<tactic_hint_entry> tacs = get_tactic_hints(env());
bool ignore_failure = !is_strict;
return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(), tacs, ctx, full_ctx,
j, ignore_failure, m_relax_main_opaque));
return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(),
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<expr> ctx = m_context.get_data();
list<expr> 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<choice_expr_elaborator>(*this, mvar, e, ctx, full_ctx, relax));
return choose(std::make_shared<choice_expr_elaborator>(*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)) {

3
src/frontends/lean/parser.cpp
View file

@ -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:

46
src/frontends/lean/pp.cpp
View file

@ -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<expr_pair> 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);

1
src/frontends/lean/pp.h
View file

@ -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);

26
src/library/annotation.cpp
View file

@ -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()); }
}

12
src/library/annotation.h
View file

@ -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();

31
src/library/print.cpp
View file

@ -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));
}
}

23
tests/lean/run/let2.lean Normal file
View file

@ -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