feat(frontends/lean/elaborator,init/meta/interactive): relax expr pattern elaboration and use it to implement a tactic signature pretty printer

library/init/meta/interactive.lean

@@ -58,6 +58,73 @@ to_expr q ff tt
 namespace interactive
 open interactive interactive.types expr
 
+open format
+private meta def maybe_paren : list format → format
+| []  := ""
+| [f] := f
+| fs  := paren (join fs)
+
+private meta def unfold (e : expr) : tactic expr := do
+(expr.const f_name f_lvls) ← return e^.get_app_fn | pp e >>= fail,
+env   ← get_env,
+decl  ← env^.get f_name,
+new_f ← decl^.instantiate_value_univ_params f_lvls,
+head_beta (expr.mk_app new_f e^.get_app_args)
+
+private meta def parser_desc_aux : expr → tactic (list format)
+| ```(ident)  := return ["id"]
+| ```(qexpr) := return ["expr"]
+| ```(tk %%c) := return <$> to_fmt <$> eval_expr string c
+| ```(return ._) := return []
+| ```(._ <$> %%p) := parser_desc_aux p
+| ```(%%p₁ <*> %%p₂) := do
+  f₁ ← parser_desc_aux p₁,
+  f₂ ← parser_desc_aux p₂,
+  return $ f₁ ++ [" "] ++ f₂
+| ```(%%p₁ <* %%p₂) := do
+  f₁ ← parser_desc_aux p₁,
+  f₂ ← parser_desc_aux p₂,
+  return $ f₁ ++ [" "] ++ f₂
+| ```(%%p₁ *> %%p₂) := do
+  f₁ ← parser_desc_aux p₁,
+  f₂ ← parser_desc_aux p₂,
+  return $ f₁ ++ [" "] ++ f₂
+| ```(many %%p) := do
+  f ← parser_desc_aux p,
+  return [maybe_paren f ++ "*"]
+| ```(optional %%p) := do
+  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, " ..."]
+| ```(%%p₁ <|> %%p₂) := do
+  f₁ ← parser_desc_aux p₁,
+  f₂ ← parser_desc_aux p₂,
+  return $ if list.empty f₁ then [maybe_paren f₂ ++ "?"] else
+    if list.empty f₂ then [maybe_paren f₁ ++ "?"] else
+    [maybe_paren f₁, " | ", maybe_paren f₂]
+| e          := do
+  e' ← unfold e,
+  if e ≠ e' then parser_desc_aux e'
+  else pp e >>= fail
+
+private meta def param_desc : expr → tactic format
+| ```(parse %%p) := join <$> parser_desc_aux p
+| ```(opt_param %%t ._) := (++ "?") <$> pp t
+| e := paren <$> pp e
+
+meta def interactive_desc_aux : expr → tactic (list format)
+| (expr.pi _ _ d b) := list.cons <$> param_desc d <*> interactive_desc_aux b
+| _ := return []
+
+meta def interactive_desc (n : name) : tactic format := do
+env ← get_env,
+decl ← env^.get n,
+f ← interactive_desc_aux decl^.type,
+return $ to_fmt n^.components^.ilast ++ " " ++ join (list.intersperse " " f)
+
 /-
 itactic: parse a nested "interactive" tactic. That is, parse
   `(` tactic `)`

src/frontends/lean/elaborator.cpp

@@ -128,11 +128,11 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const
 
 elaborator::elaborator(environment const & env, options const & opts, name const & decl_name,
                        metavar_context const & mctx, local_context const & lctx, bool recover_from_errors,
-                       bool in_pattern):
+                       bool in_pattern, bool in_quote):
     m_env(env), m_opts(opts), m_decl_name(decl_name),
     m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible),
     m_recover_from_errors(recover_from_errors),
-    m_uses_infom(get_global_info_manager() != nullptr), m_in_pattern(in_pattern) {
+    m_uses_infom(get_global_info_manager() != nullptr), m_in_pattern(in_pattern), m_in_quote(in_quote) {
     m_coercions = get_elaborator_coercions(opts);
 }
 
@@ -307,7 +307,9 @@ bool elaborator::ready_to_synthesize(expr inst_type) {
 }
 
 expr elaborator::mk_instance(expr const & C, expr const & ref) {
-    if (!ready_to_synthesize(C)) {
+    if (m_in_pattern && m_in_quote) {
+        return mk_expr_placeholder(some(C));
+    } else if (!ready_to_synthesize(C)) {
         expr inst = mk_metavar(C, ref);
         m_instances = cons(inst, m_instances);
         return inst;
@@ -1245,6 +1247,9 @@ optional<expr> elaborator::process_optional_and_auto_params(expr type, expr cons
             new_arg = mk_local(mk_fresh_name(), binding_name(type), d, binding_info(type));
             eta_args.push_back(new_arg);
         }
+        // implicit arguments are tagged as inaccessible in patterns
+        if (found && m_in_pattern)
+            new_arg = copy_tag(ref, mk_inaccessible(new_arg));
         new_args.push_back(new_arg);
         type = instantiate(binding_body(type), new_arg);
         if (found) {
@@ -2742,7 +2747,7 @@ expr elaborate_quote(expr e, environment const &env, options const &opts, bool i
 
     metavar_context ctx;
     local_context lctx;
-    elaborator elab(env, opts, "_elab_quote", ctx, lctx, false, in_pattern);
+    elaborator elab(env, opts, "_elab_quote", ctx, lctx, false, in_pattern, /* in_quote */ true);
     e = elab.elaborate(e);
     e = elab.finalize(e, true, true).first;
 
@@ -3261,7 +3266,7 @@ void elaborator::report_error(tactic_state const & s, char const * state_header,
 
 void elaborator::ensure_no_unassigned_metavars(expr & e) {
     // TODO(gabriel): this needs to change e
-    if (!has_expr_metavar(e)) return;
+    if (!has_expr_metavar(e) || (m_in_pattern && m_in_quote)) return;
     for_each(e, [&](expr const & e, unsigned) {
             if (!has_expr_metavar(e)) return false;
             if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) {

src/frontends/lean/elaborator.h

@@ -96,6 +96,7 @@ private:
     bool              m_no_info{false};
 
     bool              m_in_pattern{false};
+    bool              m_in_quote{false};
 
     expr get_default_numeral_type();
 
@@ -265,7 +266,7 @@ private:
 public:
     elaborator(environment const & env, options const & opts, name const & decl_name,
                metavar_context const & mctx, local_context const & lctx,
-               bool recover_from_errors = true, bool in_pattern = false);
+               bool recover_from_errors = true, bool in_pattern = false, bool in_quote = false);
     ~elaborator();
     metavar_context const & mctx() const { return m_ctx.mctx(); }
     local_context const & lctx() const { return m_ctx.lctx(); }

src/frontends/lean/parser.cpp

@@ -114,7 +114,7 @@ LEAN_THREAD_VALUE(id_behavior, g_outer_id_behavior, id_behavior::ErrorIfUndef);
 parser::quote_scope::quote_scope(parser & p, bool q, id_behavior i):
     m_p(p), m_id_behavior(m_p.m_id_behavior), m_old_in_quote(m_p.m_in_quote), m_in_quote(q),
     m_saved_in_pattern(p.m_in_pattern) {
-    m_p.m_in_pattern = false;
+    // m_p.m_in_pattern = false;
     if (m_in_quote && !m_old_in_quote) {
         g_outer_id_behavior = m_p.m_id_behavior;
         m_p.m_id_behavior = i;