feat: antiquotation escapes

src/Init/Lean/Elab/Quotation.lean

@@ -69,24 +69,33 @@ def isAntiquot : Syntax → Bool
 | Syntax.node (Name.str _ "antiquot" _) _ => true
 | _                                       => false
 
+-- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros.
+def isEscapedAntiquot (stx : Syntax) : Bool :=
+!(stx.getArg 1).getArgs.isEmpty
+
+def unescapeAntiquot (stx : Syntax) : Syntax :=
+if isAntiquot stx then
+  stx.setArg 1 $ mkNullNode (stx.getArg 1).getArgs.pop
+else stx
+
+def getAntiquotTerm (stx : Syntax) : Syntax :=
+stx.getArg 2
+
 def antiquotKind? : Syntax → Option SyntaxNodeKind
 | Syntax.node (Name.str k "antiquot" _) args =>
   -- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`)
-  if (args.get! 2).isNone then some Name.anonymous
+  if (args.get! 3).isNone then some Name.anonymous
   else some k
 | _                                          => none
 
-def getAntiquotTerm (stx : Syntax) : Syntax :=
-stx.getArg 1
-
 -- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes
 def isAntiquotSplice (stx : Syntax) : Bool :=
-isAntiquot stx && (stx.getArg 4).getOptional?.isSome
+isAntiquot stx && (stx.getArg 5).getOptional?.isSome
 
 -- If any item of a `many` node is an antiquotation splice, its result should
 -- be substituted into the `many` node's children
 def isAntiquotSplicePat (stx : Syntax) : Bool :=
-stx.isOfKind nullKind && stx.getArgs.any isAntiquotSplice
+stx.isOfKind nullKind && stx.getArgs.any (fun arg => isAntiquotSplice arg && !isEscapedAntiquot arg)
 
 /-- A term like `($e) is actually ambiguous: the antiquotation could be of kind `term`,
     or `ident`, or ... . But it shouldn't really matter because antiquotations without
@@ -110,14 +119,16 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
   -- `scp` is bound in stxQuot.expand
   `(Syntax.ident none $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
 -- if antiquotation, insert contents as-is, else recurse
-| stx@(Syntax.node k args) =>
-  if isAntiquot stx then
+| stx@(Syntax.node k _) =>
+  if isAntiquot stx && !isEscapedAntiquot stx then
     -- splices must occur in a `many` node
     if isAntiquotSplice stx then throwError stx "unexpected antiquotation splice"
     else pure $ getAntiquotTerm stx
   else do
     empty ← `(Array.empty);
-    args ← args.foldlM (fun args arg =>
+    -- if escaped antiquotation, decrement by one escape level
+    let stx := unescapeAntiquot stx;
+    args ← stx.getArgs.foldlM (fun args arg =>
       if k == nullKind && isAntiquotSplice arg then
         -- antiquotation splice pattern: inject args array
         `(Array.append $args $(getAntiquotTerm arg))
@@ -201,9 +212,9 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
   if quoted.isAtom then
     -- We assume that atoms are uniquely determined by the node kind and never have to be checked
     unconditional pure
-  else match antiquotKind? quoted with
-  -- quotation is a single antiquotation
-  | some k =>
+  else if isAntiquot quoted && !isEscapedAntiquot quoted then
+    -- quotation contains a single antiquotation
+    let k := antiquotKind? quoted;
     -- Antiquotation kinds like `$id:id` influence the parser, but also need to be considered by
     -- match_syntax (but not by quotation terms). For example, `($id:id) and `($e) are not
     -- distinguishable without checking the kind of the node to be captured. Note that some
@@ -214,7 +225,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
     --   let id := stx; ...
     -- else
     --   let e := stx; ...
-    let kind := if k == Name.anonymous then none else some k;
+    let kind := if k == Name.anonymous then none else k;
     let anti := match_syntax getAntiquotTerm quoted with
     | `(($e)) => e
     | anti    => anti;
@@ -222,16 +233,16 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
     if isAntiquotSplice quoted then unconditional $ fun _ => throwError quoted "unexpected antiquotation splice"
     else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn :=  fun rhs => `(let $anti := discr; $rhs) }
     else unconditional $ fun _ => throwError anti ("match_syntax: antiquotation must be variable " ++ toString anti)
-  | _ =>
-    if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then
-      -- quotation is a single antiquotation splice => bind args array
-      let anti := getAntiquotTerm (quoted.getArg 0);
-      unconditional $ fun rhs => `(let $anti := Syntax.getArgs discr; $rhs)
-      -- TODO: support for more complex antiquotation splices
-    else
-      -- not an antiquotation: match head shape
-      let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"];
-      { kind := quoted.getKind, argPats := argPats }
+  else if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then
+    -- quotation is a single antiquotation splice => bind args array
+    let anti := getAntiquotTerm (quoted.getArg 0);
+    unconditional $ fun rhs => `(let $anti := Syntax.getArgs discr; $rhs)
+    -- TODO: support for more complex antiquotation splices
+  else
+    -- not an antiquotation or escaped antiquotation: match head shape
+    let quoted := unescapeAntiquot quoted;
+    let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"];
+    { kind := quoted.getKind, argPats := argPats }
 else
   unconditional $ fun _ => throwError pat ("match_syntax: unexpected pattern kind " ++ toString pat)
 
@@ -279,8 +290,8 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt
 
 private partial def getPatternVarsAux : Syntax → List Syntax
 | stx@(Syntax.node k args) =>
-  if isAntiquot stx then
-    let anti := args.get! 1;
+  if isAntiquot stx && !isEscapedAntiquot stx then
+    let anti := getAntiquotTerm stx;
     let anti := match_syntax anti with
     | `(($e)) => e
     | _       => anti;

src/Init/Lean/Elab/Syntax.lean

@@ -259,7 +259,7 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
 | stx => match_syntax stx with
 | `($id:ident) =>
   if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
-    Syntax.node `antiquot #[mkAtom "$", Unhygienic.run `($id:ident), mkNullNode, mkNullNode]
+    Syntax.node `antiquot #[mkAtom "$", mkNullNode, Unhygienic.run `($id:ident), mkNullNode, mkNullNode]
   else
     stx
 | _ => match stx with
@@ -290,7 +290,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.identPrec then
   let item := stx.getArg 0;
-  pure $ mkNode `antiquot #[mkAtom "$", mkTermIdFromIdent item, mkNullNode, mkNullNode]
+  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, mkTermIdFromIdent item, mkNullNode, mkNullNode]
 else if k == `Lean.Parser.Command.quotedSymbolPrec then
   pure $ (stx.getArg 0).getArg 1
 else if k == `Lean.Parser.Command.strLitPrec then
@@ -346,7 +346,7 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.macroArgSimple then
   let item := stx.getArg 0;
-  pure $ mkNode `antiquot #[mkAtom "$", mkTermIdFromIdent item, mkNullNode, mkNullNode]
+  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, mkTermIdFromIdent item, mkNullNode, mkNullNode]
 else if k == `Lean.Parser.Command.strLitPrec then
   strLitPrecToPattern stx
 else

src/Init/Lean/Parser/Parser.lean

@@ -1432,7 +1432,8 @@ private def antiquotExpr : Parser       := antiquotId <|> antiquotNestedExpr
   Define parser for `$e` (if anonymous == true) and `$e:name`. Both
   forms can also be used with an appended `*` to turn them into an
   antiquotation "splice". If `kind` is given, it will additionally be checked
-  when evaluating `match_syntax`. -/
+  when evaluating `match_syntax`. Antiquotations can be escaped as in `$$e`, which
+  produces the syntax tree for `$e`. -/
 def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser :=
 let kind := (kind.getD Name.anonymous) ++ `antiquot;
 let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux ":" >> nonReservedSymbol name;
@@ -1440,7 +1441,12 @@ let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux
 -- antiquotation kind via `noImmediateColon`
 let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
 -- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error
-node kind $ try $ setExpected [] dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional (checkNoWsBefore "" >> "*")
+node kind $ try $
+  setExpected [] dollarSymbol >>
+  many (checkNoWsBefore "" >> dollarSymbol) >>
+  checkNoWsBefore "no space before spliced term" >> antiquotExpr >>
+  nameP >>
+  optional (checkNoWsBefore "" >> "*")
 
 def tryAnti (c : ParserContext) (s : ParserState) : Bool :=
 let (s, stx?) := peekToken c s;

src/Init/LeanInit.lean

@@ -697,10 +697,6 @@ match stx.isStrLit? with
 | none     => stx
 | some val => Syntax.atom stx.getHeadInfo val
 
-/-- Given `var` a `Term.id`, created the antiquotation syntax representing `$<var>:<catName>` -/
-def termIdToAntiquot (var : Syntax) (catName : String) : Syntax :=
-Syntax.node `Lean.Parser.antiquot #[mkAtomFrom var "$", var, mkAtomFrom var ":", mkAtomFrom var catName, mkNullNode]
-
 def isAtom : Syntax → Bool
 | atom _ _ => true
 | _        => false

tests/lean/run/bigop.lean

@@ -105,11 +105,7 @@ macro_rules `(Σ $idx:index => $F:term) => `(Prod ($idx:index) $F)
 syntax "def_bigop" str term:max term:max : command
 macro_rules
 | `(def_bigop $head:strLit $op $unit) =>
-   -- We have to use `$(mkAntiquotStx idx "index"):index` instead of `$idx:index` because it occurs inside of a nested quasiquotation.
-   -- We have to use write `(HasBind.bind `(idx) (fund idx => ...))` to make sure `idx` contains the same macro scopes of the `idx` occurring
-   -- on the left-hand-side of the macro command.
-   HasBind.bind `(idx) (fun idx => HasBind.bind `(F) (fun F =>
-    `(macro $head:strLit "(" idx:index ")" F:term : term => `(_big [$op, $unit] ($(idx.termIdToAntiquot "index"):index) $(F.termIdToAntiquot "term")))))
+   `(macro $head:strLit "(" idx:index ")" F:term : term => `(_big [$op, $unit] ($$idx:index) $$F))
 
 def_bigop "SUM" Nat.add 0
 #check SUM (i <- [0, 1, 2]) i+1