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

fix(library/tactic/goal): bug creating main proof builder

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-08 08:40:44 -08:00
parent 24528ff685
commit 1c43020fc9
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -121,19 +121,20 @@ 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<optional<expr>> bodies; // normalized bodies of the entries processed so far
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 {
if (is_var(e)) {
unsigned vidx = var_idx(e);
if (vidx >= offset) {
unsigned nvidx = vidx - offset;
unsigned nfv = consts.size();
unsigned nfv = padded_consts.size();
if (nvidx >= nfv)
throw exception("failed to create goal, unknown free variable");
unsigned lvl = nfv - nvidx - 1;
if (bodies[lvl])
return *(bodies[lvl]);
else
return consts[lvl];
return padded_consts[lvl];
}
}
return e;
@ -154,12 +155,14 @@ std::pair<goal, goal_proof_fn> to_goal(ro_environment const & env, context const
replacer.clear();
if (b && !inferer.is_proposition(*d)) {
bodies.push_back(b);
consts.push_back(expr());
padded_consts.push_back(expr());
} else {
lean_assert(d);
hypotheses.emplace_back(n, *d);
bodies.push_back(none_expr());
consts.push_back(mk_constant(n, *d));
expr c = mk_constant(n, *d);
padded_consts.push_back(c);
consts.push_back(c);
}
}
expr conclusion = replacer(t);