feat: double-quoted quotation semantics and basic precheck hooks

src/Lean/Elab/Binders.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
 import Lean.Parser.Term
 
@@ -494,6 +495,18 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
   | stx@`(fun $m:matchAlts) => expandMatchAltsIntoMatch stx m
   | _ => Macro.throwUnsupported
 
+open Lean.Elab.Term.Quotation in
+@[builtinQuotPrecheck Lean.Parser.Term.fun] def precheckFun : Precheck
+  | `(fun $binders* => $body) => do
+    let (binders, body, expandedPattern) ← liftMacroM <| expandFunBinders binders body
+    let mut ids := #[]
+    for b in binders do
+      for v in ← matchBinder b do
+        Quotation.withNewLocals ids <| precheck v.type
+        ids := ids.push v.id.getId
+    Quotation.withNewLocals ids <| precheck body
+  | _ => throwUnsupportedSyntax
+
 @[builtinTermElab «fun»] partial def elabFun : TermElab := fun stx expectedType? =>
   match stx with
   | `(fun $binders* => $body) => do

src/Lean/Elab/Do.lean

@@ -561,11 +561,6 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Name) (k : CodeBl
 def getLetIdDeclVar (letIdDecl : Syntax) : Name :=
   letIdDecl[0].getId
 
-def getPatternVarNames (pvars : Array PatternVar) : Array Name :=
-  pvars.filterMap fun
-    | PatternVar.localVar x => some x
-    | _ => none
-
 -- support both regular and syntax match
 def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Name) :=
   getPatternVarNames <$> getPatternVars pattern <|>

src/Lean/Elab/Match.lean

@@ -512,7 +512,7 @@ private def collectPatternVars (alt : MatchAltView) : TermElabM (Array PatternVa
   return (s.vars, alt)
 
 /- Return the pattern variables in the given pattern.
-  Remark: this method is not used here, but in other macros (e.g., at `Do.lean`). -/
+   Remark: this method is not used by the main `match` elaborator, but in the precheck hook and other macros (e.g., at `Do.lean`). -/
 def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do
   let patternStx ← liftMacroM <| expandMacros patternStx
   let (_, s) ← (CollectPatternVars.collect patternStx).run {}
@@ -525,6 +525,24 @@ def getPatternsVars (patterns : Array Syntax) : TermElabM (Array PatternVar) :=
   let (_, s) ← collect.run {}
   return s.vars
 
+def getPatternVarNames (pvars : Array PatternVar) : Array Name :=
+  pvars.filterMap fun
+    | PatternVar.localVar x => some x
+    | _ => none
+
+open Lean.Elab.Term.Quotation in
+@[builtinQuotPrecheck Lean.Parser.Term.match] def precheckMatch : Precheck
+  | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
+    discrs.forM precheck
+    for (pats, rhs) in patss.zip rhss do
+      let vars ←
+        try
+          getPatternsVars pats
+        catch
+          | _ => return  -- can happen in case of pattern antiquotations
+      Quotation.withNewLocals (getPatternVarNames vars) <| precheck rhs
+  | _ => throwUnsupportedSyntax
+
 /- We convert the collected `PatternVar`s intro `PatternVarDecl` -/
 inductive PatternVarDecl where
   /- For `anonymousVar`, we create both a metavariable and a free variable. The free variable is used as an assignment for the metavariable

src/Lean/Elab/Quotation/Precheck.lean

@@ -11,6 +11,7 @@ import Lean.Elab.Quotation.Util
 
 namespace Lean.Elab.Term.Quotation
 open Lean.Elab.Term
+open Lean.Parser.Term
 
 structure Precheck.Context where
   quotLCtx : NameSet
@@ -18,6 +19,12 @@ structure Precheck.Context where
 abbrev PrecheckM := ReaderT Precheck.Context TermElabM
 abbrev Precheck  := Syntax → PrecheckM Unit
 
+protected def withNewLocal (l : Name) (x : PrecheckM α) : PrecheckM α :=
+  withReader (fun ctx => { ctx with quotLCtx := ctx.quotLCtx.insert l }) x
+
+protected def withNewLocals (ls : Array Name) (x : PrecheckM α) : PrecheckM α :=
+  withReader (fun ctx => { ctx with quotLCtx := ls.foldl NameSet.insert ctx.quotLCtx }) x
+
 unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) :=
   KeyedDeclsAttribute.init {
     builtinName := `builtinQuotPrecheck,
@@ -31,7 +38,9 @@ unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) :=
 
 partial def precheck : Precheck := fun stx => do
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
-    p stx
+    if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; true) (fun _ => false) then
+      return
+  if stx.isAntiquot then
     return
   if !hasIdent stx then
     return  -- we only precheck identifiers, so there is nothing to check here
@@ -42,11 +51,49 @@ partial def precheck : Precheck := fun stx => do
 where
   hasIdent stx := do
     for stx in stx.topDown do
-        if stx.isIdent then
+      if stx.isIdent then
         return true
     return false
 
 def runPrecheck (stx : Syntax) : TermElabM Unit :=
   precheck stx |>.run { quotLCtx := {} }
 
+@[builtinQuotPrecheck ident] def precheckIdent : Precheck
+  | Syntax.ident info rawVal val preresolved => do
+    if !preresolved.isEmpty then
+      return
+    if let _::_ ← resolveGlobalName val then
+      return
+    if (← read).quotLCtx.contains val then
+      return
+    throwError "unknown identifier '{val}'"
+  | _ => throwUnsupportedSyntax
+
+@[builtinQuotPrecheck Lean.Parser.Term.app] def precheckApp : Precheck
+  | `($f $args*) => do
+    precheck f
+    for arg in args do
+      match arg with
+      | `(argument| ($n := $e)) => precheck e
+      | `(argument| $e:term)    => precheck e
+      | `(argument| ..)         => pure ()
+      | _ => throwUnsupportedSyntax
+  | _ => throwUnsupportedSyntax
+
+@[builtinQuotPrecheck Lean.Parser.Term.paren] def precheckParen : Precheck
+  | `(())           => pure ()
+  | `(($e : $type)) => do
+    precheck e
+    precheck type
+  | `(($e))         => precheck e
+  | `(($e, $es,*))  => do
+    precheck e
+    es.getElems.forM precheck
+  | _ => throwUnsupportedSyntax
+
+@[builtinTermElab precheckedQuot] def elabPrecheckedQuot : TermElab := fun stx expectedType? => do
+  let singleQuot := stx[1]
+  runPrecheck singleQuot.getQuotContent
+  adaptExpander (fun _ => singleQuot) stx expectedType?
+
 end Lean.Elab.Term.Quotation

tests/lean/StxQuot.lean

@@ -97,3 +97,11 @@ open Parser.Term
   match Syntax.setHeadInfo (← `(fun x =>%$(Syntax.atom (SourceInfo.synthetic 2 2) "") x)) (SourceInfo.synthetic 1 1) with
   | `(fun%$i1 $x =>%$i2 $y) => pure #[i1.getPos?, i2.getPos?]
   | _ => unreachable!
+
+#eval run ``(x)
+#eval run ``(id)
+#eval run ``(pure)
+#eval run ``(fun x => x)
+#eval run ``(fun x => y)
+#eval run ``(fun x y => x y)
+#eval run ``(fun ⟨x, y⟩ => x)

tests/lean/StxQuot.lean.expected.out

@@ -46,3 +46,9 @@ StxQuot.lean:18:15: error: expected term
 StxQuot.lean:94:39-94:44: error: unexpected antiquotation splice
 fun (a : ?m) => sorry : (a : ?m) → ?m a
 "#[(some 1), (some 2)]"
+StxQuot.lean:101:13-101:14: error: unknown identifier 'x'
+"`id._@.UnhygienicMain._hyg.1"
+"`pure._@.UnhygienicMain._hyg.1"
+"(Term.fun \"fun\" (Term.basicFun [`x._@.UnhygienicMain._hyg.1] \"=>\" `x._@.UnhygienicMain._hyg.1))"
+"(Term.fun\n \"fun\"\n (Term.basicFun\n  [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n  \"=>\"\n  (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))"
+"(Term.fun\n \"fun\"\n (Term.basicFun\n  [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n  \"=>\"\n  `x._@.UnhygienicMain._hyg.1))"