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

refactor(rewrite): use scoped_map as a type of substitution

Browse source
This commit is contained in:
Soonho Kong 2013-09-27 01:45:22 -07:00
parent 1d4a1b68f5
commit 285495313b
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/rewriter/rewriter.cpp
View file

@ -8,6 +8,7 @@
#include "kernel/abstract.h"
#include "kernel/builtin.h"
#include "kernel/context.h"
#include "kernel/expr.h"
#include "kernel/environment.h"
#include "kernel/replace.h"
#include "library/basic_thms.h"
@ -80,8 +81,8 @@ pair<expr, expr> theorem_rewriter_cell::operator()(environment const &, context
<< ", idx = " << var_idx(e) << endl;);
auto it = s.find(idx);
if (it != s.end()) {
lean_trace("rewriter", tout << "Inside of apply : s[" << idx << "] = " << s[idx] << endl;);
return s[idx];
lean_trace("rewriter", tout << "Inside of apply : s[" << idx << "] = " << it->second << endl;);
return it->second;
}
return e;
};
@ -91,8 +92,10 @@ pair<expr, expr> theorem_rewriter_cell::operator()(environment const &, context
expr proof = m_body;
for (int i = m_num_args -1 ; i >= 0; i--) {
proof = mk_app(proof, s[i]);
lean_trace("rewriter", tout << "proof: " << i << "\t" << s[i] << "\t" << proof << endl;);
auto it = s.find(i);
lean_assert(it != s.end());
proof = mk_app(proof, it->second);
lean_trace("rewriter", tout << "proof: " << i << "\t" << it->second << "\t" << proof << endl;);
}
lean_trace("rewriter", tout << "Proof = " << proof << endl;);
return make_pair(new_rhs, proof);