feat(library/tactic/tactic_state,library/init/meta): add helper tactics (context, num_goals, repeat, repeat_at_most, repeat_exactly), rename main_type ==> target

library/init/meta/base_tactic.lean

@@ -77,6 +77,22 @@ infix `<|>`:1 := or_else
 meta_definition skip : base_tactic S unit :=
 success ()
 
+open list
+meta_definition repeat : list A → (A → base_tactic S unit) → base_tactic S unit
+| []      fn := skip
+| (e::es) fn := do fn e, repeat es fn
+
+open nat
+/- (repeat n t): repeat the given tactic at most n times or until t fails -/
+meta_definition repeat_at_most : nat → base_tactic S unit → base_tactic S unit
+| 0        t := skip
+| (succ n) t := (do t, repeat_at_most n t) <|> skip
+
+/- (do n t) : execute t n times -/
+meta_definition repeat_exactly : nat → base_tactic S unit → base_tactic S unit
+| 0        t := skip
+| (succ n) t := do t, repeat_exactly n t
+
 meta_definition returnex (e : exceptional A) : base_tactic S A :=
 λ s, match e with
 | exceptional.success a    := base_tactic_result.success a s

library/init/meta/tactic.lean

@@ -44,24 +44,33 @@ meta_definition trace_state : tactic unit :=
 do s ← read,
    trace_fmt (to_fmt s)
 
+meta_definition format_expr (e : expr) : tactic format :=
+do s ← read, return (tactic_state.format_expr s e)
+
 inductive transparency :=
 | all | semireducible | reducible | none
 
-meta_constant result     : tactic expr
-meta_constant main_type  : tactic expr
-meta_constant intro      : name → tactic unit
-meta_constant assumption : tactic unit
-meta_constant rename     : name → name → tactic unit
-meta_constant clear      : name → tactic unit
-meta_constant revert_lst : list name → tactic unit
-meta_constant infer_type : expr → tactic expr
-meta_constant whnf       : expr → tactic expr
-meta_constant unify_core : expr → expr → transparency → tactic bool
-meta_constant get_local  : name → tactic expr
-open list
+/- Return the partial term/proof constructed so far. -/
+meta_constant result        : tactic expr
+/- Return target type of the main goal. Fail if tactic_state does not have any goal left. -/
+meta_constant target        : tactic expr
+meta_constant intro         : name → tactic unit
+meta_constant assumption    : tactic unit
+meta_constant rename        : name → name → tactic unit
+meta_constant clear         : name → tactic unit
+meta_constant revert_lst    : list name → tactic unit
+meta_constant infer_type    : expr → tactic expr
+meta_constant whnf          : expr → tactic expr
+meta_constant unify_core    : expr → expr → transparency → tactic bool
+meta_constant get_local     : name → tactic expr
+/- Return the hypothesis in the main goal. Fail if tactic_state does not have any goal left. -/
+meta_constant local_context : tactic (list expr)
+/- Return the number of goals that need to be solved -/
+meta_constant num_goals     : tactic nat
+open list nat
 
 meta_definition intros : tactic unit :=
-do t ← main_type,
+do t ← target,
    match t with
    | expr.pi   _ _ _ _ := do intro "_", intros
    | expr.elet _ _ _ _ := do intro "_", intros

src/library/tactic/tactic_state.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_format.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_expr.h"
+#include "library/vm/vm_list.h"
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
@@ -183,7 +184,7 @@ vm_obj tactic_result(vm_obj const & o) {
     return mk_tactic_success(to_obj(r), set_mctx(s, mctx));
 }
 
-vm_obj tactic_main_type(vm_obj const & o) {
+vm_obj tactic_target(vm_obj const & o) {
     tactic_state const & s = to_tactic_state(o);
     optional<metavar_decl> g = s.get_main_goal_decl();
     if (!g) return mk_no_goals_exception();
@@ -264,15 +265,31 @@ vm_obj tactic_get_local(vm_obj const & n, vm_obj const & s0) {
     return mk_tactic_success(to_obj(d->mk_ref()), s);
 }
 
+vm_obj tactic_local_context(vm_obj const & s0) {
+    tactic_state const & s   = to_tactic_state(s0);
+    optional<metavar_decl> g = s.get_main_goal_decl();
+    if (!g) return mk_no_goals_exception();
+    local_context lctx       = g->get_context();
+    buffer<expr> r;
+    lctx.for_each([&](local_decl const & d) { r.push_back(d.mk_ref()); });
+    return mk_tactic_success(to_obj(to_list(r)), s);
+}
+
+vm_obj tactic_num_goals(vm_obj const & s) {
+    return mk_tactic_success(mk_vm_nat(length(to_tactic_state(s).goals())), 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);
     DECLARE_VM_BUILTIN(name({"tactic_state", "to_format"}),   tactic_state_to_format);
-    DECLARE_VM_BUILTIN(name({"tactic", "main_type"}),         tactic_main_type);
+    DECLARE_VM_BUILTIN(name({"tactic", "target"}),            tactic_target);
     DECLARE_VM_BUILTIN(name({"tactic", "result"}),            tactic_result);
     DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}),        tactic_infer_type);
     DECLARE_VM_BUILTIN(name({"tactic", "unify_core"}),        tactic_unify_core);
     DECLARE_VM_BUILTIN(name({"tactic", "get_local"}),         tactic_get_local);
+    DECLARE_VM_BUILTIN(name({"tactic", "local_context"}),     tactic_local_context);
+    DECLARE_VM_BUILTIN(name({"tactic", "num_goals"}),         tactic_num_goals);
 }
 
 void finalize_tactic_state() {

tests/lean/run/meta_tac6.lean

@@ -1,3 +1,4 @@
+import data.list
 open tactic name list
 
 set_option pp.goal.compact true
@@ -6,11 +7,21 @@ set_option pp.binder_types true
 #tactic (∀ (A B : Prop), A → A ∧ B → A → A),
  do
     intro_lst ["_", "_", "H1", "H2", "H3"],
+    n : nat ← num_goals,
+    ctx : list expr ← local_context,
+    trace "Context: ",
+    repeat ctx (λ e,
+      do t ← infer_type e,
+         fmt₁ ← format_expr e,
+         fmt₂ ← format_expr t,
+         trace_fmt (fmt₁ + to_fmt " : " + fmt₂)),
+    trace "----------",
+    trace ("num: " + to_string n),
     trace_state,
     clear "H3",
-    (do {get_local "H3", skip} <|> trace "get_local failed"),
+    (do {get_local "H3", return ()} <|> trace "get_local failed"),
     trace_state,
     assumption,
-    r ← result,
-    trace_expr r,
+    n : nat ← num_goals,
+    trace ("num: " + to_string n),
     return ()