feat: support for big list literals

This encoding prevents stack overflows.

src/Init/Notation.lean

@@ -83,18 +83,6 @@ macro "if" h:ident " : " c:term " then " t:term " else " e:term : term =>
 macro "if" c:term " then " t:term " else " e:term : term =>
   `(ite $c $t $e)
 
-syntax "[" term,* "]"  : term
-
-open Lean in
-macro_rules
-  | `([ $elems* ]) => do
-    let rec expandListLit (i : Nat) (skip : Bool) (result : Syntax) : MacroM Syntax := do
-      match i, skip with
-      | 0,   _     => pure result
-      | i+1, true  => expandListLit i false result
-      | i+1, false => expandListLit i true  (← `(List.cons $(elems[i]) $result))
-    expandListLit elems.size false (← `(List.nil))
-
 syntax:0 term "<|" term:0 : term
 
 macro_rules
@@ -127,7 +115,24 @@ macro_rules
   expected type is known. So, `withoutExpected!` is not effective in this case. -/
 macro "withoutExpectedType! " x:term : term => `(let aux := $x; aux)
 
-namespace Lean.Parser.Tactic
+syntax "[" term,* "]"  : term
+syntax "%[" term,* "|" term "]" : term -- auxiliary notation for creating big list literals
+
+namespace Lean
+
+macro_rules
+  | `([ $elems* ]) => do
+    let rec expandListLit (i : Nat) (skip : Bool) (result : Syntax) : MacroM Syntax := do
+      match i, skip with
+      | 0,   _     => pure result
+      | i+1, true  => expandListLit i false result
+      | i+1, false => expandListLit i true  (← `(List.cons $(elems[i]) $result))
+    if elems.size < 64 then
+      expandListLit elems.size false (← `(List.nil))
+    else
+      `(%[ $elems* | List.nil ])
+
+namespace Parser.Tactic
 
 syntax[intro] "intro " notFollowedBy("|") (colGt term:max)* : tactic
 syntax[intros] "intros " (colGt (ident <|> "_"))* : tactic
@@ -228,4 +233,5 @@ syntax "repeat " tacticSeq : tactic
 macro_rules
   | `(tactic| repeat $seq) => `(tactic| (($seq); repeat $seq) <|> skip)
 
-end Lean.Parser.Tactic
+end Parser.Tactic
+end Lean

src/Init/NotationExtra.lean

@@ -94,3 +94,15 @@ macro_rules
       `(tactic| apply funext; intro $(xs[0]):term)
     else
       `(tactic| apply funext; intro $(xs[0]):term; funext $(xs[1:])*)
+
+macro_rules
+  | `(%[ $[$x],* | $k ]) =>
+    if x.size < 8 then
+      x.foldrM (init := k) fun x k =>
+        `(List.cons $x $k)
+    else
+      let m := x.size / 2
+      let y := x[m:]
+      let z := x[:m]
+      `(let y := %[ $[$y],* | $k ]
+        %[ $[$z],* | y ])

tests/lean/run/typeclass_append.lean

@@ -17,6 +17,7 @@ instance AppendStep {α : Type} (x : α) (xs₁ xs₂ out : List α) [AppendList
 {}
 
 #synth AppendList
-[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50]
-[200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250]
-[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250]
+[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
+[200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211]
+[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16,
+ 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211]