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

fix(library/tactic/goal): bug in the proof builder

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-09 15:02:36 -08:00
parent 4c76f6abb9
commit 2d70e2f4f2
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/tactic/goal.cpp
View file

@ -109,6 +109,9 @@ static name mk_unique_name(name_set & s, name const & suggestion) {
} }
} }
static name g_unused = name::mk_internal_unique_name();
static expr g_unused_const = mk_constant(g_unused);
std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const & ctx, expr const & t) { std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const & ctx, expr const & t) {
type_inferer inferer(env); type_inferer inferer(env);
if (!inferer.is_proposition(t, ctx)) if (!inferer.is_proposition(t, ctx))
@ -121,20 +124,19 @@ std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const
buffer<hypothesis> hypotheses; // normalized names and types of the entries processed so far buffer<hypothesis> hypotheses; // normalized names and types of the entries processed so far
buffer<optional<expr>> bodies; // normalized bodies of the entries processed so far buffer<optional<expr>> bodies; // normalized bodies of the entries processed so far
std::vector<expr> consts; // cached consts[i] == mk_constant(names[i], hypotheses[i]) std::vector<expr> consts; // cached consts[i] == mk_constant(names[i], hypotheses[i])
buffer<expr> padded_consts; // similar to consts, but it is padded to make sure bodies.size() == padded_consts.size()
auto replace_vars = [&](expr const & e, unsigned offset) -> expr { auto replace_vars = [&](expr const & e, unsigned offset) -> expr {
if (is_var(e)) { if (is_var(e)) {
unsigned vidx = var_idx(e); unsigned vidx = var_idx(e);
if (vidx >= offset) { if (vidx >= offset) {
unsigned nvidx = vidx - offset; unsigned nvidx = vidx - offset;
unsigned nfv = padded_consts.size(); unsigned nfv = consts.size();
if (nvidx >= nfv) if (nvidx >= nfv)
throw exception("failed to create goal, unknown free variable"); throw exception("failed to create goal, unknown free variable");
unsigned lvl = nfv - nvidx - 1; unsigned lvl = nfv - nvidx - 1;
if (bodies[lvl]) if (bodies[lvl])
return *(bodies[lvl]); return *(bodies[lvl]);
else else
return padded_consts[lvl]; return consts[lvl];
} }
} }
return e; return e;
@ -155,13 +157,14 @@ std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const
replacer.clear(); replacer.clear();
if (b && !inferer.is_proposition(*d)) { if (b && !inferer.is_proposition(*d)) {
bodies.push_back(b); bodies.push_back(b);
padded_consts.push_back(expr()); // Insert a dummy just to make sure consts has the right size.
// The dummy must be a closed term, and should not be used anywhere else.
consts.push_back(g_unused_const);
} else { } else {
lean_assert(d); lean_assert(d);
hypotheses.emplace_back(n, *d); hypotheses.emplace_back(n, *d);
bodies.push_back(none_expr()); bodies.push_back(none_expr());
expr c = mk_constant(n, *d); expr c = mk_constant(n, *d);
padded_consts.push_back(c);
consts.push_back(c); consts.push_back(c);
} }
} }