From d1adfd52e642692c4f76b661f4833ec581924ac5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 23 Nov 2013 15:53:45 -0800
Subject: [PATCH] feat(library/tactic): add mk_simple_tactic template

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/tactic.cpp |  4 ++--
 src/library/tactic/tactic.h   | 17 +++++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index d774f238b..fd28da4bd 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -77,7 +77,7 @@ tactic trace_tactic(char const * msg) {
 }
 
 tactic assumption_tactic() {
-    return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq {
+    return mk_simple_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
             list<std::pair<name, expr>> proofs;
             goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
                     expr const & c  = g.get_conclusion();
@@ -104,7 +104,7 @@ tactic assumption_tactic() {
                     }
                     return p(new_m, env, a);
                 });
-            return to_proof_state_seq(proof_state(s, new_goals, new_p));
+            return proof_state(s, new_goals, new_p);
         });
 }
 
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index f892a48ea..8b36c9645 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -65,6 +65,23 @@ public:
 template<typename F>
 tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell<F>(std::forward<F>(f))); }
 
+/**
+   \brief Create a tactic using the given functor.
+
+   <code>
+   proof_state operator()(environment const & env, io_state const & io, proof_state const & s)
+   </code>
+
+   \remark The functor is invoked on demand.
+*/
+template<typename F>
+tactic mk_simple_tactic(F && f) {
+    return
+        mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) {
+                return proof_state_seq([=]() { return some(mk_pair(f(env, io, s), proof_state_seq())); });
+            });
+}
+
 inline proof_state_seq to_proof_state_seq(proof_state const & s) {
     return proof_state_seq([=]() { return some(mk_pair(s, proof_state_seq())); });
 }