From 285495313be09afa42d6bb71b88167ed4e94945c Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 27 Sep 2013 01:45:22 -0700 Subject: [PATCH] refactor(rewrite): use scoped_map as a type of substitution --- src/library/rewriter/rewriter.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 66e0f211a4..6ef15f467e 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -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 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 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);