feat(library/tactic): add take and force tacticals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/tactic.cpp

@@ -247,4 +247,24 @@ tactic repeat_at_most(tactic t, unsigned k) {
             }
         });
 }
+
+tactic take(tactic t, unsigned k) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            tactic _t(t);
+            return take(k, _t(env, io, s));
+        });
+}
+
+tactic force(tactic t) {
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
+            tactic _t(t);
+            proof_state_seq r = _t(env, io, s);
+            buffer<proof_state> buf;
+            for (auto s2 : r) {
+                buf.push_back(s2);
+                check_interrupted();
+            }
+            return to_lazy(to_list(buf.begin(), buf.end()));
+        });
+}
 }

src/library/tactic/tactic.h

@@ -132,4 +132,22 @@ tactic repeat(tactic t);
    then tactic \c t will be applied 2^k times.
 */
 tactic repeat_at_most(tactic t, unsigned k);
+/**
+   \brief Return a tactic that applies \c t, but takes at most \c
+   k elements from the sequence produced by \c t.
+*/
+tactic take(tactic t, unsigned k);
+/**
+   \brief Return a tactic that forces \c t to produce all
+   the elements in the resultant sequence.
+
+   \remark proof_state_seq is a lazy-list, that is, their
+   elements are produced on demand. This tactic forces
+   all the elements in the sequence to be computed eagerly.
+
+   \remark The sequence may be infinite. So, consider
+   combining this tactical with \c take if the sequence
+   may be infinite or too big.
+*/
+tactic force(tactic t);
 }

src/tests/library/tactic/tactic.cpp

@@ -89,8 +89,8 @@ static void tst1() {
 
     std::cout << "proof 2: " << orelse(then(repeat_at_most(append(msg_tactic("hello1"), msg_tactic("hello2")), 5), fail_tactic()),
                                        t).solve(env, io, ctx, q) << "\n";
-
-
+    std::cout << "------------------\n";
+    std::cout << "proof 2: " << force(take(then(repeat_at_most(interleave(id_tactic(), id_tactic()), 100), then(msg_tactic("foo"), t)), 5)).solve(env, io, ctx, q) << "\n";
     std::cout << "done\n";
 }