refactor: rename "antiquot scope" ~> "antiquot splice"

src/Lean/Elab/Binders.lean

@@ -46,7 +46,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
     else
       let mut quotedArgs ← `(Array.empty)
       for arg in args do
-        if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotScope) then
+        if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotSplice) then
           throwErrorAt arg "invalid auto tactic, antiquotation is not allowed"
         else
           let quotedArg ← quoteAutoTactic arg

src/Lean/Elab/Quotation.lean

@@ -16,7 +16,7 @@ namespace Lean.Elab.Term.Quotation
 open Lean.Syntax
 open Meta
 
-/-- `C[$(e)]` ~> `let a := e; C[$a]`. Used in the implementation of antiquot scopes. -/
+/-- `C[$(e)]` ~> `let a := e; C[$a]`. Used in the implementation of antiquot splices. -/
 private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermElabM Syntax) TermElabM Syntax
   | stx@(Syntax.node k args) => do
     if isAntiquot stx && !isEscapedAntiquot stx then
@@ -50,7 +50,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
     else if isAntiquotSuffixSplice stx && !isEscapedAntiquot stx then
       -- splices must occur in a `many` node
       throwErrorAt stx "unexpected antiquotation splice"
-    else if isAntiquotScope stx && !isEscapedAntiquot stx then
+    else if isAntiquotSplice stx && !isEscapedAntiquot stx then
       throwErrorAt stx "unexpected antiquotation splice"
     else
       let empty ← `(Array.empty);
@@ -66,12 +66,12 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
           | `many     => `(Array.appendCore $args $(getAntiquotTerm antiquot))
           | `sepBy    => `(Array.appendCore $args (@SepArray.elemsAndSeps $(getSepFromSplice arg) $(getAntiquotTerm antiquot)))
           | k         => throwErrorAt! arg "invalid antiquotation suffix splice kind '{k}'"
-        else if k == nullKind && isAntiquotScope arg then
-          let k := antiquotScopeKind? arg
+        else if k == nullKind && isAntiquotSplice arg then
+          let k := antiquotSpliceKind? arg
           let (arg, bindLets) ← floatOutAntiquotTerms arg |>.run pure
-          let inner ← (getAntiquotScopeContents arg).mapM quoteSyntax
+          let inner ← (getAntiquotSpliceContents arg).mapM quoteSyntax
           let arr ← match (← getAntiquotationIds arg) with
-            | #[] => throwErrorAt stx "antiquotation scope must contain at least one antiquotation"
+            | #[] => throwErrorAt stx "antiquotation splice must contain at least one antiquotation"
             | #[id] => match k with
               | `optional => `(match $id:ident with
                 | some $id:ident => $(quote inner)
@@ -82,7 +82,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
                 | some $id1:ident, some $id2:ident => $(quote inner)
                 | _                                => Array.empty)
               | _ => `(Array.zipWith $id1 $id2 fun $id1 $id2 => $(inner[0]))
-            | _ => throwErrorAt stx "too many antiquotations in antiquotation scope; don't be greedy"
+            | _ => throwErrorAt stx "too many antiquotations in antiquotation splice; don't be greedy"
           let arr ←
             if k == `sepBy then
               `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
@@ -161,7 +161,7 @@ structure BasicHeadInfo where
 
 inductive HeadInfo where
   | basic (bhi : BasicHeadInfo)
-  | antiquotScope (stx : Syntax)
+  | antiquotSplice (stx : Syntax)
 
 open HeadInfo
 
@@ -176,7 +176,7 @@ def HeadInfo.generalizes : HeadInfo → HeadInfo → Bool
   | basic { kind := some k1, argPats := some ps1, .. },
     basic { kind := some k2, argPats := some ps2, .. } => k1 == k2 && ps1.size == ps2.size
   -- roughmost approximation for now
-  | antiquotScope stx1, antiquotScope stx2             => stx1 == stx2
+  | antiquotSplice stx1, antiquotSplice stx2             => stx1 == stx2
   | _, _                                               => false
 
 partial def mkTuple : Array Syntax → TermElabM Syntax
@@ -217,7 +217,7 @@ private def getHeadInfo (alt : Alt) : HeadInfo :=
       if anti.isIdent then basic { kind := kind, rhsFn :=  fun rhs => `(let $anti := discr; $rhs) }
       else unconditional fun _ => throwErrorAt! anti "match_syntax: antiquotation must be variable {anti}"
     else if isAntiquotSuffixSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
-    else if isAntiquotScope quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
+    else if isAntiquotSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
     else if quoted.getArgs.size == 1 && isAntiquotSuffixSplice quoted[0] then
       let anti := getAntiquotTerm (getAntiquotSuffixSpliceInner quoted[0])
       unconditional fun rhs => match antiquotSuffixSplice? quoted[0] with
@@ -226,8 +226,8 @@ private def getHeadInfo (alt : Alt) : HeadInfo :=
         | `sepBy    => `(let $anti := @SepArray.mk $(getSepFromSplice quoted[0]) (Syntax.getArgs discr); $rhs)
         | k         => throwErrorAt! quoted "invalid antiquotation suffix splice kind '{k}'"
       -- TODO: support for more complex antiquotation splices
-    else if quoted.getArgs.size == 1 && isAntiquotScope quoted[0] then
-      antiquotScope quoted[0]
+    else if quoted.getArgs.size == 1 && isAntiquotSplice quoted[0] then
+      antiquotSplice quoted[0]
     else
       -- not an antiquotation or escaped antiquotation: match head shape
       let quoted  := unescapeAntiquot quoted
@@ -247,7 +247,7 @@ private def explodeHeadPat (numArgs : Nat) : HeadInfo × Alt → TermElabM Alt
         | none         => List.replicate numArgs $ Unhygienic.run `(_)
       let rhs ← info.rhsFn rhs
       pure (newPats ++ pats, rhs)
-  | (antiquotScope _, (pat::pats, rhs)) => (pats, rhs)
+  | (antiquotSplice _, (pat::pats, rhs)) => (pats, rhs)
   | _ => unreachable!
 
 private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
@@ -283,10 +283,10 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
       let no ← mkNo
       `(let discr := $discr; ite (Eq $cond true) $yes $no)
     -- terrifying match step
-    | antiquotScope scope =>
-      let k := antiquotScopeKind? scope
-      let contents := getAntiquotScopeContents scope
-      let ids ← getAntiquotationIds scope
+    | antiquotSplice splice =>
+      let k := antiquotSpliceKind? splice
+      let contents := getAntiquotSpliceContents splice
+      let ids ← getAntiquotationIds splice
       let no ← mkNo
       match k with
       | `optional =>

src/Lean/Parser/Basic.lean

@@ -1646,7 +1646,7 @@ def withoutInfo (p : Parser) : Parser :=
   { fn := p.fn }
 
 /-- Parse `$[p]suffix`, e.g. `$[p],*`. -/
-def mkAntiquotScope (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
+def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
   let kind := kind ++ `antiquot_scope
   leadingNode kind maxPrec $ atomic $
     setExpected [] "$" >>
@@ -1671,9 +1671,9 @@ def mkAntiquotScope (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
   fn   := withAntiquotSuffixSpliceFn kind p.fn suffix.fn
 }
 
-def withAntiquotScopeAndSuffix (kind : SyntaxNodeKind) (p suffix : Parser) :=
+def withAntiquotSpliceAndSuffix (kind : SyntaxNodeKind) (p suffix : Parser) :=
   -- prevent `p`'s info from being collected twice
-  withAntiquot (mkAntiquotScope kind (withoutInfo p) suffix) (withAntiquotSuffixSplice kind p suffix)
+  withAntiquot (mkAntiquotSplice kind (withoutInfo p) suffix) (withAntiquotSuffixSplice kind p suffix)
 
 def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anonymous := false) : Parser :=
   withAntiquot (mkAntiquot name kind anonymous) $ node kind p
@@ -1683,7 +1683,7 @@ def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anony
 /- ===================== -/
 
 def sepByElemParser (p : Parser) (sep : String) : Parser :=
-  withAntiquotScopeAndSuffix `sepBy p (symbol (sep.trim ++ "*"))
+  withAntiquotSpliceAndSuffix `sepBy p (symbol (sep.trim ++ "*"))
 
 def sepBy (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser :=
   sepByNoAntiquot (sepByElemParser p sep) psep allowTrailingSep

src/Lean/Parser/Extra.lean

@@ -17,13 +17,13 @@ attribute [runBuiltinParserAttributeHooks]
   leadingNode termParser commandParser mkAntiquot nodeWithAntiquot sepBy sepBy1
 
 @[runBuiltinParserAttributeHooks] def optional (p : Parser) : Parser :=
-  optionalNoAntiquot (withAntiquotScopeAndSuffix `optional p (symbol "?"))
+  optionalNoAntiquot (withAntiquotSpliceAndSuffix `optional p (symbol "?"))
 
 @[runBuiltinParserAttributeHooks] def many (p : Parser) : Parser :=
-  manyNoAntiquot (withAntiquotScopeAndSuffix `many p (symbol "*"))
+  manyNoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
 
 @[runBuiltinParserAttributeHooks] def many1 (p : Parser) : Parser :=
-  many1NoAntiquot (withAntiquotScopeAndSuffix `many p (symbol "*"))
+  many1NoAntiquot (withAntiquotSpliceAndSuffix `many p (symbol "*"))
 
 @[runBuiltinParserAttributeHooks] def ident : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) identNoAntiquot

src/Lean/Syntax.lean

@@ -358,11 +358,11 @@ def mkAntiquotNode (term : Syntax) (nesting := 0) (name : Option String := none)
     | none      => mkNullNode
   mkNode (kind ++ `antiquot) #[mkAtom "$", nesting, term, name]
 
--- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros. Also works for antiquotation scopes.
+-- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros. Also works for antiquotation splices.
 def isEscapedAntiquot (stx : Syntax) : Bool :=
   !stx[1].getArgs.isEmpty
 
--- Also works for antiquotation scopes.
+-- Also works for antiquotation splices.
 def unescapeAntiquot (stx : Syntax) : Syntax :=
   if isAntiquot stx then
     stx.setArg 1 $ mkNullNode stx[1].getArgs.pop
@@ -384,20 +384,20 @@ def antiquotKind? : Syntax → Option SyntaxNodeKind
       some Name.anonymous
   | _                                          => none
 
--- An "antiquotation scope" is something like `$[...]?` or `$[...]*`.
-def antiquotScopeKind? : Syntax → Option SyntaxNodeKind
+-- An "antiquotation splice" is something like `$[...]?` or `$[...]*`.
+def antiquotSpliceKind? : Syntax → Option SyntaxNodeKind
   | Syntax.node (Name.str k "antiquot_scope" _) args => some k
   | _                                                => none
 
-def isAntiquotScope (stx : Syntax) : Bool :=
-  antiquotScopeKind? stx |>.isSome
+def isAntiquotSplice (stx : Syntax) : Bool :=
+  antiquotSpliceKind? stx |>.isSome
 
-def getAntiquotScopeContents (stx : Syntax) : Array Syntax :=
+def getAntiquotSpliceContents (stx : Syntax) : Array Syntax :=
   stx[3].getArgs
 
 -- `$[..],*` or `$x,*` ~> `,*`
 def getAntiquotSpliceSuffix (stx : Syntax) : Syntax :=
-  if stx.isAntiquotScope then
+  if stx.isAntiquotSplice then
     stx[5]
   else
     stx[1]