From fdbe8ee98a3d9043b4c81deac0eb97f9f3e8bf21 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Mar 2016 13:35:54 -0800
Subject: [PATCH] feat(library/local_context): add
 get_local_decl_from_user_name

---
 src/library/local_context.cpp | 8 ++++++++
 src/library/local_context.h   | 6 ++++++
 2 files changed, 14 insertions(+)

diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
index f1392d6b6d..8acf8a09dd 100644
--- a/src/library/local_context.cpp
+++ b/src/library/local_context.cpp
@@ -84,6 +84,14 @@ optional<local_decl> local_context::find_if(std::function<bool(local_decl const
     return m_idx2local_decl.find_if([&](unsigned, local_decl const & d) { return pred(d); });
 }
 
+optional<local_decl> local_context::back_find_if(std::function<bool(local_decl const &)> const & pred) const { // NOLINT
+    return m_idx2local_decl.find_if([&](unsigned, local_decl const & d) { return pred(d); });
+}
+
+optional<local_decl> local_context::get_local_decl_from_user_name(name const & n) const {
+    return back_find_if([&](local_decl const & d) { return d.get_pp_name() == n; });
+}
+
 void local_context::for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const {
     m_idx2local_decl.for_each_greater(d.get_idx(), [&](unsigned, local_decl const & d) { return fn(d); });
 }
diff --git a/src/library/local_context.h b/src/library/local_context.h
index dbc81a670c..d9a5bdbcb6 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -93,6 +93,12 @@ public:
     /** \brief Traverse local declarations based on the order they were created */
     void for_each(std::function<void(local_decl const &)> const & fn) const;
     optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
+    optional<local_decl> back_find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
+
+    /** \brief Return the most recently added local_decl \c d s.t. d.get_pp_name() == n
+        \remark This method is used to implement tactics such as 'revert'. */
+    optional<local_decl> get_local_decl_from_user_name(name const & n) const;
+
     /** \brief Execute fn for each local declaration created after \c d. */
     void for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const;