chore: update stage0

stage0/src/Lean/Elab/Quotation.lean

@@ -114,7 +114,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
       match stx[0] with
       | Syntax.atom _ val => `(Syntax.atom (Option.getD (getHeadInfo? $(getAntiquotTerm stx)) info) $(quote val))
       | _                 => throwErrorAt stx "expected token"
-    else if isAntiquotSuffixSplice stx && !isEscapedAntiquot stx then
+    else if isAntiquotSuffixSplice stx && !isEscapedAntiquot (getCanonicalAntiquot (getAntiquotSuffixSpliceInner stx)) then
       -- splices must occur in a `many` node
       throwErrorAt stx "unexpected antiquotation splice"
     else if isAntiquotSplice stx && !isEscapedAntiquot stx then
@@ -125,7 +125,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
       let mut args := ArrayStxBuilder.empty
       let appendName := if (← getEnv).contains ``Array.append then ``Array.append else ``Array.appendCore
       for arg in stx.getArgs do
-        if k == nullKind && isAntiquotSuffixSplice arg then
+        if k == nullKind && isAntiquotSuffixSplice arg && !isEscapedAntiquot (getCanonicalAntiquot (getAntiquotSuffixSpliceInner arg)) then
           let antiquot := getAntiquotSuffixSpliceInner arg
           let ks := antiquotKinds antiquot |>.map (·.1)
           let val := getAntiquotTerm (getCanonicalAntiquot antiquot)
@@ -139,7 +139,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
               let sep := quote <| getSepFromSplice arg
               `(@TSepArray.elemsAndSeps $(quote ks) $sep $val)
             | k         => throwErrorAt arg "invalid antiquotation suffix splice kind '{k}'"
-        else if k == nullKind && isAntiquotSplice arg then
+        else if k == nullKind && isAntiquotSplice arg && !isEscapedAntiquot arg then
           let k := antiquotSpliceKind? arg
           let (arg, bindLets) ← floatOutAntiquotTerms arg |>.run pure
           let inner ← (getAntiquotSpliceContents arg).mapM quoteSyntax

stage0/src/Lean/Linter/Basic.lean

@@ -6,7 +6,7 @@ import Lean.Server.References
 import Std.Data.HashMap
 
 namespace Lean.Linter
-open Lean.Server Std
+open Lean.Elab.Command Lean.Server Std
 
 register_builtin_option linter.unusedVariables : Bool := {
   defValue := true,
@@ -25,6 +25,131 @@ def getLinterUnusedVariables (o : Options) : Bool := o.get linter.unusedVariable
 def getLinterUnusedVariablesFunArgs (o : Options) : Bool := o.get linter.unusedVariables.funArgs.name (getLinterUnusedVariables o)
 def getLinterUnusedVariablesPatternVars (o : Options) : Bool := o.get linter.unusedVariables.patternVars.name (getLinterUnusedVariables o)
 
+
+builtin_initialize builtinUnusedVariablesIgnoreFnsRef : IO.Ref <| Array IgnoreFunction ← IO.mkRef #[]
+
+def addBuiltinUnusedVariablesIgnoreFn (ignoreFn : IgnoreFunction) : IO Unit := do
+  (← builtinUnusedVariablesIgnoreFnsRef.get) |> (·.push ignoreFn) |> builtinUnusedVariablesIgnoreFnsRef.set
+
+
+-- matches builtinUnused variable pattern
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun stx _ _ =>
+    stx.getId.toString.startsWith "_")
+
+-- is variable
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.variable])
+
+-- is in structure
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+  stackMatches stack [`null, none, `null, ``Lean.Parser.Command.structure])
+
+-- is in inductive
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+  stackMatches stack [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
+  (stack.get? 3 |>.any fun (stx, pos) =>
+    pos == 0 &&
+    [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
+
+-- in in constructor or structure binder
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+  stackMatches stack [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
+  (stack.get? 4 |>.any fun (stx, _) =>
+    [``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·)))
+
+-- is in opaque or axiom
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+  stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
+  (stack.get? 4 |>.any fun (stx, _) =>
+    [``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·)))
+
+-- is in definition with foreign definition
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+  stackMatches stack [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
+  (stack.get? 3 |>.any fun (stx, _) =>
+    stx.isOfKind ``Lean.Parser.Command.optDeclSig ||
+    stx.isOfKind ``Lean.Parser.Command.declSig) &&
+  (stack.get? 5 |>.any fun (stx, _) => Id.run <| do
+    let declModifiers := stx[0]
+    if !declModifiers.isOfKind ``Lean.Parser.Command.declModifiers then
+      return false
+    let termAttributes := declModifiers[1][0]
+    if !termAttributes.isOfKind ``Lean.Parser.Term.attributes then
+      return false
+    let termAttrInstance := termAttributes[1][0]
+    if !termAttrInstance.isOfKind ``Lean.Parser.Term.attrInstance then
+      return false
+
+    let attr := termAttrInstance[1]
+    if attr.isOfKind ``Lean.Parser.Attr.extern then
+      return true
+    else if attr.isOfKind ``Lean.Parser.Attr.simple then
+      return attr[0].getId == `implementedBy
+    else
+      return false))
+
+-- is in dependent arrow
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ =>
+  stackMatches stack [`null, ``Lean.Parser.Term.explicitBinder, ``Lean.Parser.Term.depArrow])
+
+-- is in let declaration
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
+  !getLinterUnusedVariablesFunArgs opts &&
+  stackMatches stack [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
+  (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
+  (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField))
+
+-- is in declaration signature
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
+  !getLinterUnusedVariablesFunArgs opts &&
+  stackMatches stack [`null, none, `null, none] &&
+  (stack.get? 3 |>.any fun (stx, pos) =>
+    pos == 0 &&
+    [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·)))
+
+-- is in function definition
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
+  !getLinterUnusedVariablesFunArgs opts &&
+  (stackMatches stack [`null, ``Lean.Parser.Term.basicFun] ||
+  stackMatches stack [`null, ``Lean.Parser.Term.paren, `null, ``Lean.Parser.Term.basicFun]))
+
+-- is pattern variable
+builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
+  !getLinterUnusedVariablesPatternVars opts &&
+  stack.any fun (stx, pos) =>
+    (stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
+    (stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2))
+
+
+builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Name Unit ←
+  registerSimplePersistentEnvExtension {
+    name          := `unusedVariablesIgnoreFns
+    addEntryFn    := fun _ _ => ()
+    addImportedFn := fun _ => ()
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `unusedVariablesIgnoreFn
+    descr := "Marks a function of type `Lean.Linter.IgnoreFunction` for suppressing unused variable warnings"
+    add   := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do throwError "invalid attribute 'unusedVariablesIgnoreFn', must be global"
+      unless (← getConstInfo decl).type.isConstOf ``IgnoreFunction do
+        throwError "invalid attribute 'unusedVariablesIgnoreFn', must be of type `Lean.Linter.IgnoreFunction`"
+      let env ← getEnv
+      setEnv <| unusedVariablesIgnoreFnsExt.addEntry env decl
+  }
+
+unsafe def getUnusedVariablesIgnoreFnsImpl : CommandElabM (Array IgnoreFunction) := do
+  let ents := unusedVariablesIgnoreFnsExt.getEntries (← getEnv)
+  let ents ← ents.mapM (evalConstCheck IgnoreFunction ``IgnoreFunction)
+  return (← builtinUnusedVariablesIgnoreFnsRef.get) ++ ents
+
+@[implementedBy getUnusedVariablesIgnoreFnsImpl]
+opaque getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction)
+
+
 def unusedVariables : Linter := fun cmdStx => do
   -- NOTE: `messages` is local to the current command
   if (← get).messages.hasErrors then
@@ -74,6 +199,10 @@ def unusedVariables : Linter := fun cmdStx => do
         | _        => pure ()
       return s
 
+  -- collect ignore functions
+  let ignoreFns := (← getUnusedVariablesIgnoreFns)
+    |>.insertAt 0 (isTopLevelDecl constDecls)
+
   -- determine unused variables
   for (id, ⟨decl?, uses⟩) in vars.toList do
     -- process declaration
@@ -96,32 +225,9 @@ def unusedVariables : Linter := fun cmdStx => do
     if !getLinterUnusedVariables opts then
       continue
 
-    -- collect ignore functions
-    let mut ignoreFns := #[
-      isTopLevelDecl constDecls,
-      matchesUnusedPattern,
-      isVariable,
-      isInStructure,
-      isInInductive,
-      isInCtorOrStructBinder,
-      isInOpaqueOrAxiom,
-      isInDefWithForeignDefinition,
-      isInDepArrow
-    ]
-    if !getLinterUnusedVariablesFunArgs opts then
-      ignoreFns := ignoreFns.append #[
-        isInLetDeclaration,
-        isInDeclarationSignature,
-        isInFun
-      ]
-    if !getLinterUnusedVariablesPatternVars opts then
-      ignoreFns := ignoreFns.append #[
-        isPatternVar
-      ]
-
     -- evaluate ignore functions on original syntax
     if let some stack := findSyntaxStack? cmdStx declStx then
-      if ignoreFns.any (· declStx stack) then
+      if ignoreFns.any (· declStx stack opts) then
         continue
     else
       continue
@@ -131,7 +237,7 @@ def unusedVariables : Linter := fun cmdStx => do
       if let some macroExpansions ← collectMacroExpansions? range tree then
         return macroExpansions.any fun expansion =>
           if let some stack := findSyntaxStack? expansion.output declStx then
-            ignoreFns.any (· declStx stack)
+            ignoreFns.any (· declStx stack opts)
           else
             false
       else
@@ -149,74 +255,11 @@ where
       stx[0]
     else
       stx
-
-  isTopLevelDecl (constDecls : HashSet String.Range) (stx : Syntax) (stack : SyntaxStack) := Id.run <| do
+  isTopLevelDecl (constDecls : HashSet String.Range) : IgnoreFunction := fun stx stack _ => Id.run <| do
     let some declRange := stx.getRange?
       | false
     constDecls.contains declRange &&
     !stackMatches stack [``Lean.Parser.Term.letIdDecl]
-  matchesUnusedPattern (stx : Syntax) (_ : SyntaxStack) :=
-    stx.getId.toString.startsWith "_"
-  isVariable (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.variable]
-  isInStructure (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.structure]
-  isInInductive (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
-    (stack.get? 3 |>.any fun (stx, pos) =>
-      pos == 0 &&
-      [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))
-  isInCtorOrStructBinder (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
-    (stack.get? 4 |>.any fun (stx, _) =>
-      [``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
-  isInOpaqueOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
-    (stack.get? 4 |>.any fun (stx, _) =>
-      [``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))
-  isInDefWithForeignDefinition (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
-    (stack.get? 3 |>.any fun (stx, _) =>
-      stx.isOfKind ``Lean.Parser.Command.optDeclSig ||
-      stx.isOfKind ``Lean.Parser.Command.declSig) &&
-    (stack.get? 5 |>.any fun (stx, _) => Id.run <| do
-      let declModifiers := stx[0]
-      if !declModifiers.isOfKind ``Lean.Parser.Command.declModifiers then
-        return false
-      let termAttributes := declModifiers[1][0]
-      if !termAttributes.isOfKind ``Lean.Parser.Term.attributes then
-        return false
-      let termAttrInstance := termAttributes[1][0]
-      if !termAttrInstance.isOfKind ``Lean.Parser.Term.attrInstance then
-        return false
-
-      let attr := termAttrInstance[1]
-      if attr.isOfKind ``Lean.Parser.Attr.extern then
-        return true
-      else if attr.isOfKind ``Lean.Parser.Attr.simple then
-        return attr[0].getId == `implementedBy
-      else
-        return false)
-  isInDepArrow (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, ``Lean.Parser.Term.explicitBinder, ``Lean.Parser.Term.depArrow]
-
-  isInLetDeclaration (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
-    (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
-    (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField)
-  isInDeclarationSignature (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, none] &&
-    (stack.get? 3 |>.any fun (stx, pos) =>
-      pos == 0 &&
-      [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))
-  isInFun (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, ``Lean.Parser.Term.basicFun] ||
-    stackMatches stack [`null, ``Lean.Parser.Term.paren, `null, ``Lean.Parser.Term.basicFun]
-
-  isPatternVar (_ : Syntax) (stack : SyntaxStack) :=
-    stack.any fun (stx, pos) =>
-      (stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
-      (stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2)
 
 builtin_initialize addLinter unusedVariables
 

stage0/src/Lean/Linter/Util.lean

@@ -85,4 +85,6 @@ def stackMatches (stack : SyntaxStack) (pattern : List $ Option SyntaxNodeKind)
     |>.zipWith (fun (s, _) p => p |>.map (s.isOfKind ·) |>.getD true) pattern
     |>.all id)
 
+abbrev IgnoreFunction := Syntax → SyntaxStack → Options → Bool
+
 end Lean.Linter