feat(library/init/meta/tactic): add 'focus' and 'all_goals' tacticals

library/init/meta/tactic.lean

@@ -114,6 +114,8 @@ meta_constant change        : expr → tactic unit
 meta_constant assert        : name → expr → tactic unit
 /- rotate goals to the left -/
 meta_constant rotate_left   : nat → tactic unit
+meta_constant get_goals     : tactic (list expr)
+meta_constant set_goals     : list expr → tactic unit
 open list nat
 
 meta_definition intros : tactic unit :=
@@ -174,4 +176,30 @@ do ng ← num_goals,
 meta_definition rotate : nat → tactic unit :=
 rotate_left
 
+meta_definition focus (tac : tactic unit) : tactic unit :=
+do gs ← get_goals,
+   match gs with
+   | []      := fail "focus tactic failed, there isn't any goal left to focus"
+   | (g::rs) :=
+     do set_goals [g],
+        tac,
+        gs' ← get_goals,
+        match gs' with
+        | [] := set_goals gs
+        | _  := fail "focus tactic failed, focused goal has not been solved"
+        end
+   end
+
+private meta_definition all_goals_core : tactic unit → list expr → list expr → tactic unit
+| tac []        acc := set_goals acc
+| tac (g :: gs) acc :=
+  do set_goals [g],
+     tac,
+     new_gs ← get_goals,
+     all_goals_core tac gs (acc ++ new_gs)
+
+meta_definition all_goals (tac : tactic unit) : tactic unit :=
+do gs ← get_goals,
+   all_goals_core tac gs []
+
 end tactic

src/library/tactic/tactic_state.cpp

@@ -378,6 +378,29 @@ vm_obj tactic_rotate_left(vm_obj const & n, vm_obj const & s) {
     return rotate_left(force_to_unsigned(n, 0), to_tactic_state(s));
 }
 
+vm_obj tactic_get_goals(vm_obj const & s0) {
+    tactic_state const & s   = to_tactic_state(s0);
+    return mk_tactic_success(to_obj(s.goals()), s);
+}
+
+vm_obj set_goals(list<expr> const & gs, tactic_state const & s) {
+    buffer<expr> new_gs;
+    metavar_context const & mctx = s.mctx();
+    for (expr const & g : gs) {
+        if (!mctx.get_metavar_decl(g)) {
+            return mk_tactic_exception("invalid set_goals tactic, expressions must be meta-variables "
+                                       "that have been declared in the current tactic_state", s);
+        }
+        if (!mctx.is_assigned(g))
+            new_gs.push_back(g);
+    }
+    return mk_tactic_success(set_goals(s, to_list(new_gs)));
+}
+
+vm_obj tactic_set_goals(vm_obj const & gs, vm_obj const & s) {
+    return set_goals(to_list_expr(gs), to_tactic_state(s));
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),         tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);
@@ -395,6 +418,8 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}),           tactic_to_expr);
     DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp"}),        tactic_defeq_simp);
     DECLARE_VM_BUILTIN(name({"tactic", "rotate_left"}),       tactic_rotate_left);
+    DECLARE_VM_BUILTIN(name({"tactic", "get_goals"}),         tactic_get_goals);
+    DECLARE_VM_BUILTIN(name({"tactic", "set_goals"}),         tactic_set_goals);
 }
 
 void finalize_tactic_state() {

tests/lean/focus_tac.lean

@@ -0,0 +1,26 @@
+open tactic
+
+example (a : nat) : a = a :=
+by do
+   assert "x" (expr.const "nat" []),
+   trace "---- after assert ----",
+   trace_state,
+   focus (do trace "--- inside focus tac ---", trace_state), -- SHOULD FAIL HERE
+   trace "---- after focus tac ----",
+   trace_state,
+   x ← get_local "x",
+   mk_app ("eq" <.> "refl") [x] >>= exact,
+   return ()
+
+
+definition tst2 (a : nat) : a = a :=
+by do
+   assert "x" (expr.const "nat" []),
+   trace "---- after assert ----",
+   trace_state,
+   focus (do trace "--- inside focus tac ---", trace_state, assumption),
+   trace "---- after focus tac ----",
+   trace_state,
+   x ← get_local "x",
+   mk_app ("eq" <.> "refl") [x] >>= exact,
+   return ()

tests/lean/focus_tac.lean.expected.out

@@ -0,0 +1,31 @@
+---- after assert ----
+a : ℕ
+⊢ ℕ
+
+a : ℕ,
+x : ℕ := ?M_1
+⊢ a = a
+--- inside focus tac ---
+a : ℕ
+⊢ ℕ
+focus_tac.lean:4:0: error: focus tactic failed, focused goal has not been solved
+state:
+a : ℕ
+⊢ ℕ
+focus_tac.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1
+---- after assert ----
+a : ℕ
+⊢ ℕ
+
+a : ℕ,
+x : ℕ := ?M_1
+⊢ a = a
+--- inside focus tac ---
+a : ℕ
+⊢ ℕ
+---- after focus tac ----
+a : ℕ,
+x : ℕ := ?M_1
+⊢ a = a

tests/lean/run/all_goals1.lean

@@ -0,0 +1,14 @@
+open tactic
+
+example (a b c : Prop) : a → a :=
+by do intro "H",
+      a ← get_local "a",
+      assert "H1" a,
+      assert "H2" a,
+      assert "H3" a,
+      assert "H4" a,
+      assert "H5" a,
+      trace_state,
+      all_goals assumption,
+      trace "--- after all_goals assumption ---",
+      trace_result