From ce9be52ffb71cb2298428740f9e4aa64023e966f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 10 Nov 2020 15:28:23 +0100
Subject: [PATCH] feat: pretty print lists and arrays

---
 src/Lean/Delaborator.lean               | 21 +++++++++++++++++++++
 tests/lean/match1.lean.expected.out     | 15 +++++++++++++++
 tests/lean/parserPrio.lean.expected.out |  2 +-
 tests/lean/rewrite.lean.expected.out    |  2 +-
 4 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 043f24ea70..2033b1dda3 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -747,6 +747,27 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
 @[builtinDelab app.Not] def delabNot : Delab := delabPrefixOp fun _ x => `(¬ $x)
 @[builtinDelab app.not] def delabBNot : Delab := delabPrefixOp fun _ x => `(! $x)
 
+@[builtinDelab app.List.nil]
+def delabNil : Delab := whenPPOption getPPNotation do
+  guard $ (← getExpr).getAppNumArgs == 1
+  `([])
+
+@[builtinDelab app.List.cons]
+def delabConsList : Delab := whenPPOption getPPNotation do
+  guard $ (← getExpr).getAppNumArgs == 3
+  let x ← withAppFn (withAppArg delab)
+  match_syntax (← withAppArg delab) with
+  | `([])     => `([$x])
+  | `([$xs*]) => `([$x, $xs*])
+  | _         => failure
+
+@[builtinDelab app.List.toArray]
+def delabListToArray : Delab := whenPPOption getPPNotation do
+  guard $ (← getExpr).getAppNumArgs == 2
+  match_syntax (← withAppArg delab) with
+  | `([$xs*]) => `(#[$xs*])
+  | _         => failure
+
 end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index a5307c9357..646600246d 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -31,3 +31,18 @@ fun (x : Bool × Bool) =>
 fun (x : Nat × Nat) =>
   match x with 
   | (a, b) => a + b : Nat × Nat → Nat
+fun (x x_1 : Option Nat) =>
+  match x, x_1 with 
+  | some a, some b => some (a + b)
+  | x_2, x_3 => none : Option Nat → Option Nat → Option Nat
+fun (x : Nat) =>
+  (match x with 
+    | 0 => id
+    | Nat.succ x_1 => id)
+    x : Nat → Nat
+fun (x : Array Nat) =>
+  match x with 
+  | #[1,2] => 2
+  | #[] => 0
+  | #[3,4,5] => 3
+  | x_1 => 4 : Array Nat → Nat
diff --git a/tests/lean/parserPrio.lean.expected.out b/tests/lean/parserPrio.lean.expected.out
index 82f10bce36..fbf3988349 100644
--- a/tests/lean/parserPrio.lean.expected.out
+++ b/tests/lean/parserPrio.lean.expected.out
@@ -3,6 +3,6 @@
 parserPrio.lean:26:7: error: ambiguous, possible interpretations 
   2 * 1
   
-  1 :: List.nil
+  [1]
 sorryAx ?m : ?m
 [1, 2, 3]
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index 0fcedeeeda..7c3aea7bbc 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -5,7 +5,7 @@ rewrite.lean:12:20: error: tactic 'rewrite' failed, did not find instance of the
   List.reverse (List.reverse ?m)
 α : Type _
 as bs : List α
-⊢ as ++ List.nil ++ List.nil ++ bs ++ bs = as ++ (bs ++ bs)
+⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)
 x y z : Nat
 h₁ : x = y
 h₂ : y = z