feat(init/meta/interactive): rw goal info on ,

library/init/meta/interactive.lean

@@ -26,7 +26,7 @@ variables {α β : Type}
 -- optimized pretty printer
 meta def brackets (l r : string) (p : parser α) := tk l *> p <* tk r
 
-meta def list_of (p : parser α) := brackets "[" "]" $ sep_by "," p
+meta def list_of (p : parser α) := brackets "[" "]" $ sep_by (skip_info (tk ",")) p
 
 /-- A 'tactic expression', which uses right-binding power 2 so that it is terminated by
     '<|>' (rbp 2), ';' (rbp 1), and ',' (rbp 0). It should be used for any (potentially)
@@ -63,6 +63,8 @@ private meta def parser_desc_aux : expr → tactic (list format)
 | ```(tk %%c) := return <$> to_fmt <$> eval_expr string c
 | ```(return ._) := return []
 | ```(._ <$> %%p) := parser_desc_aux p
+| ```(skip_info %%p) := parser_desc_aux p
+| ```(set_goal_info_pos %%p) := parser_desc_aux p
 | ```(%%p₁ <*> %%p₂) := do
   f₁ ← parser_desc_aux p₁,
   f₂ ← parser_desc_aux p₂,
@@ -82,9 +84,9 @@ private meta def parser_desc_aux : expr → tactic (list format)
   f ← parser_desc_aux p,
   return [maybe_paren f ++ "?"]
 | ```(sep_by %%sep %%p) := do
-  f ← parser_desc_aux p,
-  fs ← eval_expr string sep,
-  return [maybe_paren f ++ to_fmt fs, " ..."]
+  f₁ ← parser_desc_aux sep,
+  f₂ ← parser_desc_aux p,
+  return [maybe_paren f₂ ++ join f₁, " ..."]
 | ```(%%p₁ <|> %%p₂) := do
   f₁ ← parser_desc_aux p₁,
   f₂ ← parser_desc_aux p₂,
@@ -312,27 +314,29 @@ private meta def rw_hyps : transparency → list symm_expr → list name → tac
 | m es  []      := return ()
 | m es  (h::hs) := rw_hyp m es h >> rw_hyps m es hs
 
-private meta def rw_core (m : transparency) (hs : parse qexpr_list_or_texpr) (loc : parse location) : tactic unit :=
+meta def rw_rules := list_of (set_goal_info_pos (qexpr 0)) <|> return <$> texpr
+
+private meta def rw_core (m : transparency) (hs : parse rw_rules) (loc : parse location) : tactic unit :=
 do hlist ← to_symm_expr_list hs,
    match loc with
    | [] := rw_goal m hlist >> try (reflexivity reducible)
    | hs := rw_hyps m hlist hs >> try (reflexivity reducible)
    end
 
-meta def rewrite : parse qexpr_list_or_texpr → parse location → tactic unit :=
+meta def rewrite : parse rw_rules → parse location → tactic unit :=
 rw_core reducible
 
-meta def rw : parse qexpr_list_or_texpr → parse location → tactic unit :=
+meta def rw : parse rw_rules → parse location → tactic unit :=
 rewrite
 
 /- rewrite followed by assumption -/
-meta def rwa (q : parse qexpr_list_or_texpr) (l : parse location) : tactic unit :=
+meta def rwa (q : parse rw_rules) (l : parse location) : tactic unit :=
 rewrite q l >> try assumption
 
-meta def erewrite : parse qexpr_list_or_texpr → parse location → tactic unit :=
+meta def erewrite : parse rw_rules → parse location → tactic unit :=
 rw_core semireducible
 
-meta def erw : parse qexpr_list_or_texpr → parse location → tactic unit :=
+meta def erw : parse rw_rules → parse location → tactic unit :=
 erewrite
 
 private meta def get_type_name (e : expr) : tactic name :=

library/init/meta/lean/parser.lean

@@ -30,6 +30,11 @@ meta constant tk (tk : string) : parser unit
     may contain antiquotations (`%%e`). -/
 meta constant qexpr (rbp := nat.of_num std.prec.max) : parser pexpr
 
+/-- Do not report info from content parsed by `p`. -/
+meta constant skip_info {α : Type} (p : parser α) : parser α
+/-- Set goal info position of content parsed by `p` to current position. Nested calls take precedence. -/
+meta constant set_goal_info_pos {α : Type} (p : parser α) : parser α
+
 /-- Return the current parser position without consuming any input. -/
 meta def cur_pos : parser pos := λ s, success (parser_state.cur_pos s) s
 
@@ -61,8 +66,8 @@ meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type
 local postfix `?`:100 := optional
 local postfix * := many
 
-meta def sep_by {α : Type} : string → parser α → parser (list α)
-| s p := (list.cons <$> p <*> (tk s *> p)*) <|> return []
+meta def sep_by {α : Type} : parser unit → parser α → parser (list α)
+| s p := (list.cons <$> p <*> (s *> p)*) <|> return []
 
 end parser
 end lean

src/frontends/lean/interactive.cpp

@@ -98,18 +98,8 @@ void report_info(environment const & env, options const & opts, io_state const &
     g_context = e.m_token_info.m_context;
     json record;
 
-    bool has_token_info = false;
-    if (e.m_token_info.m_context == break_at_pos_exception::token_context::interactive_tactic &&
-        e.m_token_info.m_token.size()) {
-        record = serialize_decl(e.m_token_info.m_token,
-                                get_interactive_tactic_full_name(e.m_token_info.m_tac_class, e.m_token_info.m_token),
-                                env, opts);
-        if (auto idx = e.m_token_info.m_tac_param_idx)
-            record["tactic_param_idx"] = *idx;
-        has_token_info = true;
-    }
-
     // info data not dependent on elaboration/info_manager
+    bool has_token_info = false;
     auto const & tk = e.m_token_info.m_token;
     if (tk.size()) {
         switch (e.m_token_info.m_context) {
@@ -132,6 +122,14 @@ void report_info(environment const & env, options const & opts, io_state const &
                 if (auto it = get_option_declarations().find(tk))
                     record["doc"] = it->get_description();
                 break;
+            case break_at_pos_exception::token_context::interactive_tactic:
+                record = serialize_decl(e.m_token_info.m_token,
+                                        get_interactive_tactic_full_name(e.m_token_info.m_tac_class, e.m_token_info.m_token),
+                                        env, opts);
+                if (auto idx = e.m_token_info.m_tac_param_idx)
+                    record["tactic_param_idx"] = *idx;
+                has_token_info = true;
+                break;
             default:
                 break;
         }

src/frontends/lean/tactic_notation.cpp

@@ -255,7 +255,9 @@ struct parse_tactic_fn {
             try {
                 r = parse_interactive_tactic(m_p, *dname, m_tac_class, m_use_rstep, m_report_error);
             } catch (break_at_pos_exception & e) {
-                if (!m_p.get_complete() && !e.m_token_info.m_token.size()) {
+                if (!m_p.get_complete() &&
+                    (!e.m_token_info.m_token.size() ||
+                     e.m_token_info.m_context == break_at_pos_exception::token_context::none)) {
                     e.m_token_info.m_pos       = pos;
                     e.m_token_info.m_token     = dname->get_string();
                     e.m_token_info.m_context   = break_at_pos_exception::token_context::interactive_tactic;

src/library/vm/vm_parser.cpp

@@ -76,11 +76,31 @@ vm_obj vm_parser_qexpr(vm_obj const & vm_rbp, vm_obj const & o) {
     CATCH;
 }
 
+vm_obj vm_parser_skip_info(vm_obj const &, vm_obj const & vm_p, vm_obj const & o) {
+    auto const & s = lean_parser::to_state(o);
+    return s.m_p->without_break_at_pos<vm_obj>([&]() {
+        return invoke(vm_p, o);
+    });
+}
+
+vm_obj vm_parser_set_goal_info_pos(vm_obj const &, vm_obj const & vm_p, vm_obj const & o) {
+    auto const & s = lean_parser::to_state(o);
+    auto pos = s.m_p->pos();
+    try {
+        return invoke(vm_p, o);
+    } catch (break_at_pos_exception & ex) {
+        ex.report_goal_pos(pos);
+        throw;
+    }
+}
+
 void initialize_vm_parser() {
-    DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}), vm_parser_state_cur_pos);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),         vm_parser_ident);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "tk"}),            vm_parser_tk);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),         vm_parser_qexpr);
+    DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}),     vm_parser_state_cur_pos);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),             vm_parser_ident);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "tk"}),                vm_parser_tk);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),             vm_parser_qexpr);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "skip_info"}),         vm_parser_skip_info);
+    DECLARE_VM_BUILTIN(name({"lean", "parser", "set_goal_info_pos"}), vm_parser_set_goal_info_pos);
 }
 
 void finalize_vm_parser() {

tests/lean/interactive/focus.lean.expected.out

@@ -1,4 +1,4 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.irtactic → tactic unit"},"response":"ok","seq_num":5}
-{"record":{"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0"},"response":"ok","seq_num":7}
+{"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.irtactic → tactic unit"},"response":"ok","seq_num":7}
 {"record":{"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0\n\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"},"response":"ok","seq_num":9}

tests/lean/interactive/goal_info_rw.lean

@@ -0,0 +1,7 @@
+example (p q r : Prop) (h₁ : p = q) (h₂ : q = r) : p = r :=
+by rw [h₁,
+       --^ "command": "info"
+       -h₂,
+     --^ "command": "info"
+       -h₁]
+       --^ "command": "info"

tests/lean/interactive/goal_info_rw.lean.expected.out

@@ -0,0 +1,4 @@
+{"message":"file invalidated","response":"ok","seq_num":0}
+{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([expr, ...] | expr)","(at id*)?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → tactic unit"},"response":"ok","seq_num":3}
+{"record":{"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r"},"response":"ok","seq_num":5}
+{"record":{"full-id":"h₁","state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = q","type":"p = q"},"response":"ok","seq_num":7}