chore: add auxiliary functions and simplify Quotation

src/Init/Lean/Elab/BuiltinNotation.lean

@@ -50,7 +50,7 @@ match expectedType? with
       if val.ctors.length != 1 then
         throwError ref ("invalid constructor ⟨...⟩, '" ++ constName ++ "' must have only one constructor")
       else
-        let ctor := mkTermId ref val.ctors.head!;
+        let ctor := mkTermIdFrom ref val.ctors.head!;
         let args := (stx.getArg 1).getArgs.getEvenElems; do
         withMacroExpansion ref $ elabTerm (mkAppStx ctor args) expectedType?
     | _ => throwError ref ("invalid constructor ⟨...⟩, '" ++ constName ++ "' is not an inductive type")
@@ -58,13 +58,13 @@ match expectedType? with
 
 @[builtinTermElab «show»] def elabShow : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
+| `(show $type from $val) => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $thisId) $val)
 | _                       => throwUnsupportedSyntax
 
 @[builtinTermElab «have»] def elabHave : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `(have $type from $val; $body)      => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
-| `(have $type := $val; $body)        => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
+| `(have $type from $val; $body)      => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val)
+| `(have $type := $val; $body)        => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val)
 | `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
 | `(have $x : $type := $val; $body)   => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
 | _                                   => throwUnsupportedSyntax
@@ -114,7 +114,7 @@ fun stx expectedType? => do
   elabTerm (mkAppStx f #[a, b]) expectedType?
 
 def elabInfixOp (op : Name) : TermElab :=
-fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType?
+fun stx expectedType? => elabInfix (mkTermIdFrom (stx.getArg 1) op) stx expectedType?
 
 @[builtinTermElab prod] def elabProd : TermElab := elabInfixOp `Prod
 @[builtinTermElab fcomp] def ElabFComp : TermElab := elabInfixOp `Function.comp

src/Init/Lean/Elab/Quotation.lean

@@ -33,32 +33,30 @@ export HasQuote (quote)
 instance Syntax.HasQuote : HasQuote Syntax := ⟨id⟩
 instance String.HasQuote : HasQuote String := ⟨fun s => Syntax.node `Lean.Parser.Term.str #[mkStxStrLit s]⟩
 instance Nat.HasQuote : HasQuote Nat := ⟨fun n => Syntax.node `Lean.Parser.Term.num #[mkStxNumLit $ toString n]⟩
+instance Substring.HasQuote : HasQuote Substring := ⟨fun s => mkCAppStx `_root_.String.toSubstring #[quote s.toString]⟩
 
 private def quoteName : Name → Syntax
-| Name.anonymous => Unhygienic.run `(_root_.Lean.Name.anonymous)
-| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr $(quoteName n) $(quote s))
-| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum $(quoteName n) $(quote i))
+| Name.anonymous => mkTermId `_root_.Lean.Name.anonymous
+| Name.str n s _ => mkCAppStx `_root_.Lean.mkNameStr #[quoteName n, quote s]
+| Name.num n i _ => mkCAppStx `_root_.Lean.mkNameNum #[quoteName n, 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
-
 instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
-⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk $(quote a) $(quote b))⟩
+⟨fun ⟨a, b⟩ => mkCAppStx `_root_.Prod.mk #[quote a, quote b]⟩
 
 private def quoteList {α : Type} [HasQuote α] : List α → Syntax
-| [] =>      Unhygienic.run `(_root_.List.nil)
-| (x::xs) => Unhygienic.run `(_root_.List.cons $(quote x) $(quoteList xs))
+| []      => mkTermId `_root_.List.nil
+| (x::xs) => mkCAppStx `_root_.List.cons #[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 => mkCAppStx `_root_.List.toArray #[quote xs.toList]⟩
 
 private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
-| none     => Unhygienic.run `(_root_.Option.none)
-| (some x) => Unhygienic.run `(_root_.Option.some $(quote x))
+| none     => mkTermId `_root_.Option.none
+| (some x) => mkCAppStx `_root_.Option.some #[quote x]
 
 instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
 
@@ -108,7 +106,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
   let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
   let val := quote val;
   -- `scp` is bound in stxQuot.expand
-  `(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) (addMacroScope $val scp) $(quote preresolved))
+  `(Syntax.ident none $(quote rawVal) (addMacroScope $val scp) $(quote preresolved))
 -- if antiquotation, insert contents as-is, else recurse
 | stx@(Syntax.node k args) =>
   if isAntiquot stx then

src/Init/Lean/Elab/Syntax.lean

@@ -210,7 +210,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.identPrec then
   let item := stx.getArg 0;
-  pure $ mkNode `antiquot #[mkAtom "$", Term.mkTermIdFromIdent item, mkNullNode, mkNullNode]
+  pure $ mkNode `antiquot #[mkAtom "$", 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

src/Init/Lean/Elab/Term.lean

@@ -355,21 +355,6 @@ let instIdx := s.instImplicitIdx;
 modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s};
 pure $ (`_inst).appendIndexAfter instIdx
 
-def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]
-
-/-- Convert a `Syntax.ident` into a `Lean.Parser.Term.id` node -/
-def mkTermIdFromIdent (ident : Syntax) : Syntax :=
-match ident with
-| Syntax.ident _ _ _ _ => mkNode `Lean.Parser.Term.id #[ident, mkNullNode]
-| _                    => unreachable!
-
-/--
-  Create a simple `Lean.Parser.Term.id` syntax using position
-  information from `ref` and name `n`. By simple, we mean that
-  `optional (explicitUniv <|> namedPattern)` is none. -/
-def mkTermId (ref : Syntax) (n : Name) : Syntax :=
-mkTermIdFromIdent (mkIdentFrom ref n)
-
 /--
   Return true if the given syntax is a `Lean.Parser.Term.cdot` or
   is a `Lean.Parser.Term.app` containing a `cdot`.
@@ -710,8 +695,8 @@ fun stx expectedType? => do
   let openBkt  := stx.getArg 0;
   let args     := stx.getArg 1;
   let closeBkt := stx.getArg 2;
-  let consId   := mkTermId openBkt `List.cons;
-  let nilId    := mkTermId closeBkt `List.nil;
+  let consId   := mkTermIdFrom openBkt `List.cons;
+  let nilId    := mkTermIdFrom closeBkt `List.nil;
   let newStx   := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId;
   elabTerm newStx expectedType?
 

src/Init/Lean/Parser/Term.lean

@@ -185,6 +185,27 @@ open Parser
 def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax :=
 args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
 
+def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]
+
+/-- Convert a `Syntax.ident` into a `Lean.Parser.Term.id` node -/
+def mkTermIdFromIdent (ident : Syntax) : Syntax :=
+match ident with
+| Syntax.ident _ _ _ _ => mkNode `Lean.Parser.Term.id #[ident, mkNullNode]
+| _                    => unreachable!
+
+/--
+  Create a simple `Lean.Parser.Term.id` syntax using position
+  information from `ref` and name `n`. By simple, we mean that
+  `optional (explicitUniv <|> namedPattern)` is none. -/
+def mkTermIdFrom (ref : Syntax) (n : Name) : Syntax :=
+mkTermIdFromIdent (mkIdentFrom ref n)
+
+def mkTermId (n : Name) : Syntax :=
+mkTermIdFromIdent (Syntax.ident none n.toString.toSubstring n [])
+
+def mkCAppStx (fn : Name) (args : Array Syntax) : Syntax :=
+mkAppStx (mkTermId fn) args
+
 def Syntax.isTermId? (stx : Syntax) : Option (Syntax × Syntax) :=
 stx.ifNode
  (fun node =>

src/Init/Lean/Syntax.lean

@@ -305,7 +305,7 @@ end SyntaxNode
 /- Helper functions for creating Syntax objects using C++ -/
 
 @[export lean_mk_syntax_atom]
-def mkSimpleAtomCore (val : String) : Syntax :=
+def mkSimpleAtom (val : String) : Syntax :=
 Syntax.atom none val
 
 @[export lean_mk_syntax_ident]