From a9bdb2f70a99d3590d4e99a83f8a52ea82fcd52e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 14 Dec 2020 16:45:32 +0100
Subject: [PATCH] feat: prefer interpreter for running builtin parsers in
 quotations

---
 src/Lean/Parser/Basic.lean     | 25 ++++++++++++++++---------
 src/Lean/Parser/Extension.lean |  7 ++++++-
 src/Lean/Parser/Term.lean      |  2 +-
 3 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 4579705c2b..63b0b83b1b 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1681,6 +1681,15 @@ 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 evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s =>
+  match ctx.env.evalConstCheck Parser {} `Lean.Parser.Parser declName <|>
+        ctx.env.evalConstCheck Parser {} `Lean.Parser.TrailingParser declName with
+  | Except.ok p    => p.fn ctx s
+  | Except.error e => s.mkUnexpectedError s!"error running parser {declName}: {e}"
+
+@[implementedBy evalParserConstUnsafe]
+constant evalParserConst (declName : Name) : ParserFn
+
 unsafe def parserOfStackFnUnsafe (offset : Nat) : ParserFn := fun ctx s =>
   let stack := s.stxStack
   if stack.size < offset + 1 then
@@ -1689,15 +1698,13 @@ unsafe def parserOfStackFnUnsafe (offset : Nat) : ParserFn := fun ctx s =>
     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    =>
-          let iniSz := s.stackSize
-          let s := p.fn ctx s
-          if !s.hasError && s.stackSize != iniSz + 1 then
-            s.mkUnexpectedError "expected parser to return exactly one syntax object"
-          else
-            s
-        | Except.error e => s.mkUnexpectedError s!"error running parser {parserName}: {e}"
+      | [(parserName, [])] =>
+        let iniSz := s.stackSize
+        let s := evalParserConst parserName ctx s
+        if !s.hasError && s.stackSize != iniSz + 1 then
+          s.mkUnexpectedError "expected parser to return exactly one syntax object"
+        else
+          s
       | _::_::_ => 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")
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index a9b2fe63f7..81dc57137d 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -144,8 +144,13 @@ 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 categories ← builtinParserCategoriesRef.get
-  let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
+  let categories ← IO.ofExcept $ addParser categories catName declName leading { p with fn := fn } 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 640efb84fb..2481d75b5b 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -211,7 +211,7 @@ 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 >> ")"
+@[builtinTermParser] def dynamicQuot := parser! "`(" >> ident >> "|" >> toggleInsideQuot (parserOfStack 1) >> ")"
 
 end Term