chore: update stage0

stage0/src/Init/Lean/Elab/Quotation.lean

@@ -36,30 +36,30 @@ instance Nat.HasQuote : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
 
 private def quoteName : Name → Syntax
 | Name.anonymous => Unhygienic.run `(_root_.Lean.Name.anonymous)
-| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr %%(quoteName n) %%(Lean.HasQuote.quote s))
-| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum %%(quoteName n) %%(Lean.HasQuote.quote i))
+| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr $(quoteName n) $(Lean.HasQuote.quote s))
+| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum $(quoteName n) $(Lean.HasQuote.quote i))
 
 instance Name.HasQuote : HasQuote Name := ⟨quoteName⟩
 
 private def appN (fn : Syntax) (args : Array Syntax) : Syntax :=
-args.foldl (fun fn arg => Unhygienic.run `(%%fn %%arg)) fn
+args.foldl (fun fn arg => Unhygienic.run `($fn $arg)) fn
 
 instance Prod.HasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
-⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk %%(Lean.HasQuote.quote a) %%(Lean.HasQuote.quote b))⟩
+⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk $(Lean.HasQuote.quote a) $(Lean.HasQuote.quote b))⟩
 
 private def quoteList {α : Type} [HasQuote α] : List α → Syntax
 | [] =>      Unhygienic.run `(_root_.List.nil)
-| (x::xs) => Unhygienic.run `(_root_.List.cons %%(Lean.HasQuote.quote x) %%(quoteList xs))
+| (x::xs) => Unhygienic.run `(_root_.List.cons $(Lean.HasQuote.quote x) $(quoteList xs))
 
 instance List.HasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
 
 instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
-⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray %%stx)⟩
+⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray $stx)⟩
 
 namespace Elab
 namespace Term
 
--- `%%e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes
+-- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes
 private def isAntiquotSplice (stx : Syntax) : Bool :=
 stx.isOfKind `Lean.Parser.Term.antiquot && (stx.getArg 3).getOptional.isSome
 
@@ -78,10 +78,10 @@ private partial def quoteSyntax (env : Environment) : Syntax → TermElabM Synta
   let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
   let val := quote val;
   -- `scp` is bound in stxQuot.expand
-  val ← `(Lean.addMacroScope %%val scp);
+  val ← `(Lean.addMacroScope $val scp);
   let args := quote preresolved;
   -- TODO: simplify quotations when we're no longer limited by name resolution in the old frontend
-  `(Lean.Syntax.ident Option.none (String.toSubstring %%(Lean.mkStxStrLit (HasToString.toString rawVal))) %%val %%args)
+  `(Lean.Syntax.ident Option.none (String.toSubstring $(Lean.mkStxStrLit (HasToString.toString rawVal))) $val $args)
 -- if antiquotation, insert contents as-is, else recurse
 | stx@(Syntax.node k args) =>
   if k == `Lean.Parser.Term.antiquot then
@@ -91,13 +91,13 @@ private partial def quoteSyntax (env : Environment) : Syntax → TermElabM Synta
   else if isAntiquotSplicePat stx then
     -- top-level antiquotation splice pattern: inject args array
     let quoted := (args.get! 0).getArg 1;
-    `(Lean.Syntax.node Lean.nullKind %%quoted)
+    `(Lean.Syntax.node Lean.nullKind $quoted)
   else do
     let k := quote k;
     args ← quote <$> args.mapM quoteSyntax;
-    `(Lean.Syntax.node %%k %%args)
+    `(Lean.Syntax.node $k $args)
 | Syntax.atom info val =>
-  `(Lean.Syntax.atom Option.none %%(Lean.mkStxStrLit val))
+  `(Lean.Syntax.atom Option.none $(Lean.mkStxStrLit val))
 | Syntax.missing => unreachable!
 
 def stxQuot.expand (env : Environment) (stx : Syntax) : TermElabM Syntax := do
@@ -107,9 +107,9 @@ let quoted := stx.getArg 1;
    depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e.
    we preserve referential transparency), so we can refer to this same `scp` inside `quoteSyntax` by
    including it literally in a syntax quotation. -/
--- TODO: simplify to `(do scp ← getCurrMacroScope; pure %%(quoteSyntax env quoted))
+-- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax env quoted))
 stx ← quoteSyntax env quoted;
-`(HasBind.bind Lean.MonadQuotation.getCurrMacroScope (fun scp => HasPure.pure %%stx))
+`(HasBind.bind Lean.MonadQuotation.getCurrMacroScope (fun scp => HasPure.pure $stx))
 /- NOTE: It may seem like the newly introduced binding `scp` may accidentally
    capture identifiers in an antiquotation introduced by `quoteSyntax`. However,
    note that the syntax quotation above enjoys the same hygiene guarantees as
@@ -141,21 +141,21 @@ private abbrev Alt := List Syntax × Syntax
 -- bindings on the RHS.
 private def isVarPat? (pat : Syntax) : Option (Syntax → TermElabM Syntax) :=
 -- TODO: reimplement using match_syntax
-if pat.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let %%pat := discr; %%rhs)
+if pat.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let $pat := discr; $rhs)
 else if pat.isOfKind `Lean.Parser.Term.hole then some pure
 else if pat.isOfKind `Lean.Parser.Term.stxQuot then
   let quoted := pat.getArg 1;
   -- We assume that atoms are uniquely determined by the surrounding node and never have to be checked
   if quoted.isAtom then some pure
-  -- TODO: antiquotations with kinds (`%%id:id`) probably can't be handled as unconditional patterns
+  -- TODO: antiquotations with kinds (`$id:id`) probably can't be handled as unconditional patterns
   else if quoted.isOfKind `Lean.Parser.Term.antiquot then
     let anti := quoted.getArg 1;
     if isAntiquotSplice quoted then some $ fun _ => throwError quoted "unexpected antiquotation splice"
-    else if anti.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let %%anti := discr; %%rhs)
+    else if anti.isOfKind `Lean.Parser.Term.id then some $ fun rhs => `(let $anti := discr; $rhs)
     else unreachable!
   else if isAntiquotSplicePat quoted then
     let anti := (quoted.getArg 0).getArg 1;
-    some $ fun rhs => `(let %%anti := Lean.Syntax.getArgs discr; %%rhs)
+    some $ fun rhs => `(let $anti := Lean.Syntax.getArgs discr; $rhs)
   else none
 else none
 
@@ -170,7 +170,7 @@ private def altNextNode? : Alt → Option SyntaxNode
 
 -- Assuming that the first pattern of the alternative is taken, replace it with patterns (if any) for its
 -- child nodes.
--- Ex: `(%%a + (- %%b)) => `(%%a), `(+), `(- %%b)
+-- Ex: `($a + (- $b)) => `($a), `(+), `(- $b)
 -- Note: The atom pattern `(+) will be discarded in a later step
 private def explodeHeadPat (numArgs : Nat) : Alt → TermElabM Alt
 | (pat::pats, rhs) => match isVarPat? pat with
@@ -202,7 +202,7 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt
   | some node => do
     let shape := nodeShape node;
     -- introduce pattern matches on the discriminant's children
-    newDiscrs ← (List.range node.getArgs.size).mapM $ fun i => `(Lean.Syntax.getArg discr %%(Lean.HasQuote.quote i));
+    newDiscrs ← (List.range node.getArgs.size).mapM $ fun i => `(Lean.Syntax.getArg discr $(Lean.HasQuote.quote i));
     -- collect matching alternatives and explode them
     let yesAlts := alts.filter $ fun alt => match altNextNode? alt with some n => nodeShape n == shape | none => true;
     yesAlts ← yesAlts.mapM $ explodeHeadPat node.getArgs.size;
@@ -212,12 +212,12 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt
     -- NOTE: use fresh macro scopes for recursion so that different `discr`s introduced by the quotation below do not collide
     yes ← withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts;
     no  ← withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts;
-    `(let discr := %%discr; if Lean.Syntax.isOfKind discr %%(Lean.HasQuote.quote (Prod.fst shape)) && Array.size (Lean.Syntax.getArgs discr) == %%(Lean.HasQuote.quote (Prod.snd shape)) then %%yes else %%no)
+    `(let discr := $discr; if Lean.Syntax.isOfKind discr $(Lean.HasQuote.quote (Prod.fst shape)) && Array.size (Lean.Syntax.getArgs discr) == $(Lean.HasQuote.quote (Prod.snd shape)) then $yes else $no)
   -- only unconditional patterns: introduce binds and discard patterns
   | none => do
     alts ← alts.mapM $ explodeHeadPat 0;
     res ← withFreshMacroScope $ compileStxMatch discrs alts;
-    `(let discr := %%discr; %%res)
+    `(let discr := $discr; $res)
 | _, _ => unreachable!
 
 private partial def getAntiquotVarsAux : Syntax → TermElabM (List Syntax)
@@ -249,13 +249,13 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li
     rhs' ← `(rhs ());
     -- NOTE: new macro scope so that introduced bindings do not collide
     stx ← withFreshMacroScope $ letBindRhss alts ((pats, rhs')::altsRev');
-    `(let rhs := fun _ => %%rhs; %%stx)
+    `(let rhs := fun _ => $rhs; $stx)
   | _ => do
-    -- rhs ← `(fun %%vars* => %%rhs)
+    -- rhs ← `(fun $vars* => $rhs)
     let rhs := Syntax.node `Lean.Parser.Term.fun #[mkAtom "fun", Syntax.node `null vars.toArray, mkAtom "=>", rhs];
     rhs' ← `(rhs);
     stx ← withFreshMacroScope $ letBindRhss alts ((pats, rhs')::altsRev');
-    `(let rhs := %%rhs; %%stx)
+    `(let rhs := $rhs; $stx)
 
 def match_syntax.expand (stx : SyntaxNode) : TermElabM Syntax := do
 let discr := stx.getArg 1;
@@ -325,17 +325,17 @@ private unsafe partial def toPreterm (env : Environment) : Syntax → Except Str
     let con := args.get! 2;
     let yes := args.get! 4;
     let no := args.get! 6;
-    toPreterm $ Unhygienic.run `(ite %%con %%yes %%no)
+    toPreterm $ Unhygienic.run `(ite $con $yes $no)
   | `Lean.Parser.Term.paren =>
     let inner := (args.get! 1).getArgs;
     if inner.size == 0 then pure $ Lean.mkConst `Unit.unit
     else toPreterm $ inner.get! 0
   | `Lean.Parser.Term.band =>
     let lhs := args.get! 0; let rhs := args.get! 2;
-    toPreterm $ Unhygienic.run `(and %%lhs %%rhs)
+    toPreterm $ Unhygienic.run `(and $lhs $rhs)
   | `Lean.Parser.Term.beq =>
     let lhs := args.get! 0; let rhs := args.get! 2;
-    toPreterm $ Unhygienic.run `(HasBeq.beq %%lhs %%rhs)
+    toPreterm $ Unhygienic.run `(HasBeq.beq $lhs $rhs)
   | `strLit => pure $ mkStrLit $ stx.isStrLit?.getD ""
   | `numLit => pure $ mkNatLit $ stx.isNatLit?.getD 0
   | `expr => pure $ unsafeCast $ stx.getArg 0  -- HACK: see below

stage0/src/Init/Lean/Elab/Term.lean

@@ -292,7 +292,7 @@ def expandCDot? : Syntax → TermElabM (Option Syntax)
   if args.any hasCDot then do
     (args, binders) ← (expandCDotArgs args).run #[];
     let newNode := Syntax.node k args;
-    result ← `(fun %%binders* => %%newNode);
+    result ← `(fun $binders* => $newNode);
     pure result
   else
     pure none
@@ -513,7 +513,7 @@ partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Nat → Ar
       ident ← mkFreshAnonymousIdent binder;
       (binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident mkHole);
       let major := mkTermIdFromIdent ident;
-      newBody ← `(match %%major with | %%pattern => %%newBody);
+      newBody ← `(match $major with | $pattern => $newBody);
       pure (binders, newBody)
     };
     match binder with
@@ -582,7 +582,7 @@ partial def mkPairsAux (elems : Array Syntax) : Nat → Syntax → TermElabM Syn
   if i > 0 then do
     let i    := i - 1;
     let elem := elems.get! i;
-    acc ← `(Prod.mk %%elem %%acc);
+    acc ← `(Prod.mk $elem $acc);
     mkPairsAux i acc
   else
     pure acc
@@ -601,13 +601,13 @@ fun stx expectedType? =>
   let ref := stx.val;
   match_syntax ref with
   | `(())             => pure $ Lean.mkConst `Unit.unit
-  | `((%%e : %%type)) => do
+  | `(($e : $type)) => do
     type ← elabType type;
     e ← elabCDot e expectedType?;
     eType ← inferType ref e;
     ensureHasType ref type eType e
-  | `((%%e))          => elabCDot e expectedType?
-  | `((%%e, %%es*))   => do
+  | `(($e))          => elabCDot e expectedType?
+  | `(($e, $es*))   => do
     pairs ← mkPairs (#[e] ++ es.getEvenElems);
     withMacroExpansion stx.val (elabTerm pairs expectedType?)
   | _ => throwError stx.val "unexpected parentheses notation"

stage0/src/Init/Lean/Parser/Term.lean

@@ -40,11 +40,13 @@ pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
 def infixL (sym : String) (lbp : Nat) : TrailingParser :=
 pushLeading >> symbol sym lbp >> termParser lbp
 
--- Define parser for `%%e` (if name = none) or `%%e:n` (if name = some n). Both
+def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1
+
+-- Define parser for `$e` (if name = none) or `$e:n` (if name = some n). Both
 -- forms can also be used with an appended `*` to turn them into an
 -- antiquotation "splice".
 def mkAntiquot (name : Option String) : Parser leading :=
-leadingNode `Lean.Parser.Term.antiquot $ symbol "$" 1 >> checkNoWsBefore "no space before" >> termParser appPrec >> (
+leadingNode `Lean.Parser.Term.antiquot $ dollarSymbol >> checkNoWsBefore "no space before" >> termParser appPrec >> (
   match name with
   | some name => let sym := ":" ++ name; checkNoWsBefore ("no space before '" ++ sym ++ "'") >> sym
   -- make sure to generate as many children (1) as in the first case to keep arity constant
@@ -140,7 +142,7 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
 @[builtinTermParser] def arrow   := tparser! unicodeInfixR " → " " -> " 25
 @[builtinTermParser] def arrayRef := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]"
 
-@[builtinTermParser] def dollar := tparser! try (pushLeading >> symbol " $ " 1 >> checkWsBefore "space expected") >> termParser 0
+@[builtinTermParser] def dollar := tparser! try (pushLeading >> dollarSymbol >> checkWsBefore "space expected") >> termParser 0
 @[builtinTermParser] def fcomp  := tparser! infixR " ∘ " 90
 
 @[builtinTermParser] def prod  := tparser! infixR " × " 35