chore: unexpanders for Name.mkStr* and Array.mkArray*

closes #1675

src/Init/NotationExtra.lean

@@ -210,6 +210,70 @@ syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosi
   | `($_ $array $index) => `($array[$index]?)
   | _ => throw ()
 
+@[appUnexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
+  | _  => throw ()
+
+@[appUnexpander Array.mkArray1] def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1) => `(#[$a1])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray2] def unexpandMkArray2 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2) => `(#[$a1, $a2])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray3] def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2 $a3) => `(#[$a1, $a2, $a3])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray4] def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2 $a3 $a4) => `(#[$a1, $a2, $a3, $a4])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray5] def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2 $a3 $a4 $a5) => `(#[$a1, $a2, $a3, $a4, $a5])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray6] def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2 $a3 $a4 $a5 $a6) => `(#[$a1, $a2, $a3, $a4, $a5, $a6])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray7] def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7])
+  | _ => throw ()
+
+@[appUnexpander Array.mkArray8] def unexpandMkArray8 : Lean.PrettyPrinter.Unexpander
+  | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7 $a8) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7, $a8])
+  | _ => throw ()
+
 /--
 Apply function extensionality and introduce new hypotheses.
 The tactic `funext` will keep applying new the `funext` lemma until the goal target is not reducible to

tests/lean/1321.lean.expected.out

@@ -1,5 +1,4 @@
 @[reducible] def fooParser : Lean.ParserDescr :=
-Lean.ParserDescr.node (Lean.Name.mkStr1 "fooParser") 1022
-  (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "foo")
-    (Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 0))
+Lean.ParserDescr.node `fooParser 1022
+  (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "foo") (Lean.ParserDescr.cat `term 0))
 5 + 1 : Nat

tests/lean/586.lean.expected.out

@@ -1,4 +1,4 @@
 Nat.zero : Nat
-Lean.Name.mkStr2 "Nat" "succ" : Lean.Name
+`Nat.succ : Lean.Name
 586.lean:13:0-13:3: error: unknown identifier 'zero✝'
 586.lean:13:0-13:3: error: unknown constant 'succ✝'

tests/lean/macroResolveName.lean.expected.out

@@ -1,2 +1,2 @@
-[Name.mkStr2 "Lean" "Macro"] : List Name
-[(Lean.Name.mkStr2 "Nat" "succ", [])] : List (Lean.Name × List ?m)
+[`Lean.Macro] : List Name
+[(`Nat.succ, [])] : List (Lean.Name × List ?m)

tests/lean/ppNotationCode.lean.expected.out

@@ -1,11 +1,10 @@
 [Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
-    Lean.ParserDescr.trailingNode (Lean.Name.mkStr1 "term_+++_") 45 46
-      (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "+++")
-        (Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 46))
+    Lean.ParserDescr.trailingNode `term_+++_ 45 46
+      (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
 [Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
     fun x =>
       let discr := x;
-      if Lean.Syntax.isOfKind discr (Lean.Name.mkStr1 "term_+++_") = true then
+      if Lean.Syntax.isOfKind discr `term_+++_ = true then
         let discr_1 := Lean.Syntax.getArg discr 0;
         let discr_2 := Lean.Syntax.getArg discr 1;
         let discr := Lean.Syntax.getArg discr 2;
@@ -17,22 +16,20 @@
         let mainModule ← Lean.getMainModule
         pure
             { raw :=
-                  Lean.Syntax.node info (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app")
-                    (Array.mkArray2
-                      (Lean.Syntax.ident info (String.toSubstring' "Nat.add")
-                        (Lean.addMacroScope mainModule (Lean.Name.mkStr2 "Nat" "add") scp)
-                        [Lean.Syntax.Preresolved.decl (Lean.Name.mkStr2 "Nat" "add") [],
-                          Lean.Syntax.Preresolved.namespace (Lean.Name.mkStr2 "Nat" "add")])
-                      (Lean.Syntax.node info (Lean.Name.mkStr1 "null") (Array.mkArray2 lhs.raw rhs.raw))) }.raw
+                  Lean.Syntax.node info `Lean.Parser.Term.app
+                    #[Lean.Syntax.ident info (String.toSubstring' "Nat.add")
+                        (Lean.addMacroScope mainModule `Nat.add scp)
+                        [Lean.Syntax.Preresolved.decl `Nat.add [], Lean.Syntax.Preresolved.namespace `Nat.add],
+                      Lean.Syntax.node info `null #[lhs.raw, rhs.raw]] }.raw
       else
         let discr := x;
         throw Lean.Macro.Exception.unsupportedSyntax
 [Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
     fun x =>
       let discr := x;
-      if Lean.Syntax.isOfKind discr (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app") = true then
+      if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then
         let discr_1 := Lean.Syntax.getArg discr 0;
-        bif false || Lean.Syntax.isOfKind discr_1 (Lean.Name.mkStr1 "ident") then
+        bif false || Lean.Syntax.isOfKind discr_1 `ident then
           let discr_2 := Lean.Syntax.getArg discr 1;
           if Lean.Syntax.matchesNull discr_2 2 = true then
             let discr := Lean.Syntax.getArg discr_2 0;
@@ -44,18 +41,15 @@
               let info ← Lean.MonadRef.mkInfoFromRefPos
               let _ ← Lean.getCurrMacroScope
               let _ ← Lean.getMainModule
-              pure
-                  { raw :=
-                        Lean.Syntax.node info (Lean.Name.mkStr1 "term_+++_")
-                          (Array.mkArray3 lhs.raw (Lean.Syntax.atom info "+++") rhs.raw) }.raw
+              pure { raw := Lean.Syntax.node info `term_+++_ #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw
           else
             let discr := Lean.Syntax.getArg discr 1;
             throw ()
         else
           let discr_2 := Lean.Syntax.getArg discr 0;
-          if Lean.Syntax.isOfKind discr_2 (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app") = true then
+          if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.app = true then
             let discr_3 := Lean.Syntax.getArg discr_2 0;
-            bif false || Lean.Syntax.isOfKind discr_3 (Lean.Name.mkStr1 "ident") then
+            bif false || Lean.Syntax.isOfKind discr_3 `ident then
               let discr_4 := Lean.Syntax.getArg discr_2 1;
               if Lean.Syntax.matchesNull discr_4 2 = true then
                 let discr_5 := Lean.Syntax.getArg discr_4 0;
@@ -71,12 +65,10 @@
                   let _ ← Lean.getMainModule
                   pure
                       { raw :=
-                            Lean.Syntax.node info (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app")
-                              (Array.mkArray2
-                                (Lean.Syntax.node info (Lean.Name.mkStr1 "term_+++_")
-                                  (Array.mkArray3 lhs.raw (Lean.Syntax.atom info "+++") rhs.raw))
-                                (Lean.Syntax.node info (Lean.Name.mkStr1 "null")
-                                  (Array.append Array.mkArray0 (Lean.TSyntaxArray.raw moreArgs)))) }.raw
+                            Lean.Syntax.node info `Lean.Parser.Term.app
+                              #[Lean.Syntax.node info `term_+++_ #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw],
+                                Lean.Syntax.node info `null
+                                  (Array.append Array.mkArray0 (Lean.TSyntaxArray.raw moreArgs))] }.raw
               else
                 let discr_5 := Lean.Syntax.getArg discr_2 1;
                 let discr := Lean.Syntax.getArg discr 1;

tests/lean/syntaxInNamespacesAndPP.lean.expected.out

@@ -1,6 +1,5 @@
 true : Bool
 true : Bool
 def Bla.bla : Lean.ParserDescr :=
-Lean.ParserDescr.node (Lean.Name.mkStr2 "Bla" "bla") 1022
-  (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "bla")
-    (Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 0))
+Lean.ParserDescr.node `Bla.bla 1022
+  (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "bla") (Lean.ParserDescr.cat `term 0))