From 8119daeb18e170a892b118e03f1c8a599f16f199 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 26 Apr 2021 17:08:24 +0200
Subject: [PATCH] feat: syntax & attribute for double-quoted quotations

---
 src/Lean/Elab/Quotation.lean          |  1 +
 src/Lean/Elab/Quotation/Precheck.lean | 52 +++++++++++++++++++++++++++
 src/Lean/Parser/Command.lean          |  1 +
 3 files changed, 54 insertions(+)
 create mode 100644 src/Lean/Elab/Quotation/Precheck.lean

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 94d92bdda7..12a0b14482 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -10,6 +10,7 @@ import Lean.Syntax
 import Lean.ResolveName
 import Lean.Elab.Term
 import Lean.Elab.Quotation.Util
+import Lean.Elab.Quotation.Precheck
 import Lean.Parser.Term
 
 namespace Lean.Elab.Term.Quotation
diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
new file mode 100644
index 0000000000..3be63981d4
--- /dev/null
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+
+import Lean.KeyedDeclsAttribute
+import Lean.Parser.Command  -- for `precheckedQuot`
+import Lean.Elab.Term
+import Lean.Elab.Quotation.Util
+
+namespace Lean.Elab.Term.Quotation
+open Lean.Elab.Term
+
+structure Precheck.Context where
+  quotLCtx : NameSet
+
+abbrev PrecheckM := ReaderT Precheck.Context TermElabM
+abbrev Precheck  := Syntax → PrecheckM Unit
+
+unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) :=
+  KeyedDeclsAttribute.init {
+    builtinName := `builtinQuotPrecheck,
+    name := `quotPrecheck,
+    descr    := "Register a double backtick syntax quotation precheck.
+
+  [quotPrecheck k] registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the `SyntaxNodeKind` `k`.",
+    valueTypeName := ``Precheck
+  } `Lean.Elab.Term.Quotation.precheckAttribute
+@[builtinInit mkPrecheckAttribute] constant precheckAttribute : KeyedDeclsAttribute Precheck
+
+partial def precheck : Precheck := fun stx => do
+  if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
+    p stx
+    return
+  if !hasIdent stx then
+    return  -- we only precheck identifiers, so there is nothing to check here
+  if let some stx' ← liftMacroM <| Macro.expandMacro? stx then
+    precheck stx'
+    return
+  throwErrorAt stx "no macro or precheck hook for syntax kind '{stx.getKind}' found{indentD stx}"
+where
+  hasIdent stx := do
+    for stx in stx.topDown do
+        if stx.isIdent then
+        return true
+    return false
+
+def runPrecheck (stx : Syntax) : TermElabM Unit :=
+  precheck stx |>.run { quotLCtx := {} }
+
+end Lean.Elab.Term.Quotation
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 4d877ab14a..15f7169cab 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -16,6 +16,7 @@ namespace Parser
   match against a quotation in a command kind's elaborator). -/
 -- TODO: use two separate quotation parsers with parser priorities instead
 @[builtinTermParser] def Term.quot := leading_parser "`(" >> toggleInsideQuot (termParser <|> many1Unbox commandParser) >> ")"
+@[builtinTermParser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
 
 namespace Command