From 314c5c9d41d098801d300882bf64c4d2c1465bea Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 14 Dec 2020 17:12:14 +0100
Subject: [PATCH] feat: run single non-category quotation under interpreter as
 well

---
 src/Lean/Parser/Basic.lean                | 8 ++++++++
 src/Lean/Parser/Extension.lean            | 8 ++------
 src/Lean/Parser/Term.lean                 | 3 ++-
 src/Lean/PrettyPrinter/Formatter.lean     | 1 +
 src/Lean/PrettyPrinter/Parenthesizer.lean | 1 +
 5 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 63b0b83b1b..378eed8c23 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1715,6 +1715,14 @@ constant parserOfStackFn (offset : Nat) : ParserFn
 def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
   { fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
 
+/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
+def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
+  fn := fun c s =>
+    if c.insideQuot && c.env.contains declName then
+      evalParserConst declName c s
+    else
+      p.fn c s }
+
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
   if s.stackSize == iniSz + 1 then s
   else s.mkNode nullKind iniSz -- throw error instead?
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 81dc57137d..bca5f84a2f 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -144,13 +144,9 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit
   | Except.error msg     => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}")
 
 def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
-  let fn : ParserFn := fun c s =>
-    if c.insideQuot && c.env.contains declName then
-      evalParserConst declName c s
-    else
-      p.fn c s
+  let p := evalInsideQuot declName p
   let categories ← builtinParserCategoriesRef.get
-  let categories ← IO.ofExcept $ addParser categories catName declName leading { p with fn := fn } prio
+  let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
   builtinParserCategoriesRef.set categories
   builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
   updateBuiltinTokens p.info declName
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2481d75b5b..604a82e899 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -197,7 +197,8 @@ def isIdent (stx : Syntax) : Bool :=
 
 @[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
 
-@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
+-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
+@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
 
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index c9f15a06e3..b6ede88d69 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -404,6 +404,7 @@ def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :
 
 @[combinatorFormatter Lean.Parser.toggleInsideQuot] def toggleInsideQuot.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (declName : Name) (p : Formatter) : Formatter := p
 
 @[combinatorFormatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do
   let st ← get
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index dea8fc612e..7f8e9b4758 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -464,6 +464,7 @@ def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Par
 
 @[combinatorParenthesizer Lean.Parser.toggleInsideQuot] def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 @[combinatorParenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (declName : Name) (p : Parenthesizer) : Parenthesizer := p
 
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()