feat: arbitrary quotation kinds via name resolution in the parser and execution in the interpreter

src/Lean/Parser/Basic.lean

@@ -1664,6 +1664,27 @@ def categoryParserOfStackFn (offset : Nat) : ParserFn := fun ctx s =>
 def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
   { fn := fun c s => categoryParserOfStackFn offset { c with prec := prec } s }
 
+unsafe def parserOfStackFnUnsafe (offset : Nat) : ParserFn := fun ctx s =>
+  let stack := s.stxStack
+  if stack.size < offset + 1 then
+    s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
+  else
+    match stack.get! (stack.size - offset - 1) with
+    | Syntax.ident (val := parserName) .. =>
+      match ctx.resolveName parserName with
+      | [(parserName, [])] => match ctx.env.evalConstCheck Parser {} `Lean.Parser.Parser parserName with
+        | Except.ok p    => p.fn ctx s
+        | Except.error e => s.mkUnexpectedError s!"error running parser {parserName}: {e}"
+      | _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
+      | _ => s.mkUnexpectedError s!"unknown parser {parserName}"
+    | _ => s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
+
+@[implementedBy parserOfStackFnUnsafe]
+constant parserOfStackFn (offset : Nat) : ParserFn
+
+def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
+  { fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
+
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
   if s.stackSize == iniSz + 1 then s
   else s.mkNode nullKind iniSz -- throw error instead?

src/Lean/Parser/Term.lean

@@ -207,6 +207,8 @@ def macroLastArg   := macroDollarArg <|> macroArg
 -- Macro for avoiding exponentially big terms when using `STWorld`
 @[builtinTermParser] def stateRefT   := parser! "StateRefT" >> macroArg >> macroLastArg
 
+@[builtinTermParser] def dynamicQuot := parser! "`(" >> ident >> "|" >> parserOfStack 1 >> ")"
+
 end Term
 
 @[builtinTermParser 1] def Tactic.quot    : Parser := parser! "`(tactic|" >> toggleInsideQuot tacticParser >> ")"

src/Lean/PrettyPrinter/Formatter.lean

@@ -190,6 +190,12 @@ def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
   let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
   categoryParser.formatter stx.getId
 
+@[combinatorFormatter Lean.Parser.parserOfStack]
+def parserOfStack.formatter (offset : Nat) (prec : Nat := 0) : Formatter := do
+  let st ← get
+  let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
+  formatterForKind stx.getKind
+
 @[combinatorFormatter Lean.Parser.error]
 def error.formatter (msg : String) : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.errorAtSavedPos]

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -310,6 +310,12 @@ def categoryParserOfStack.parenthesizer (offset : Nat) (prec : Nat) : Parenthesi
   let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
   categoryParser.parenthesizer stx.getId prec
 
+@[combinatorParenthesizer Lean.Parser.parserOfStack]
+def parserOfStack.parenthesizer (offset : Nat) (prec : Nat := 0) : Parenthesizer := do
+  let st ← get
+  let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
+  parenthesizerForKind stx.getKind
+
 @[builtinCategoryParenthesizer term]
 def term.parenthesizer : CategoryParenthesizer | prec => do
   let stx ← getCur