feat(Data/Finsupp): add notation (#6367)

This PR provides `fun₀ | 3 => a | 7 => b` notation for `Finsupp`, which desugars to `Finsupp.update` and `Finsupp.single`, in the same way that `{a, b}` desugars to `insert` and `singleton`.

It also provides a matching delaborator: as an example of the effect of this, `Finsupp.single_add` now shows as:
```lean
Finsupp.single_add.{u_2, u_1} {α : Type u_1} {M : Type u_2} [inst✝ : AddZeroClass M] (a : α) (b₁ b₂ : M) :
  (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂
```

Finally, it provides a `Repr` instance; though this is somewhat misleading as the syntax that is produced by `Repr` isn't actually computable so can't round-trip!

[Discussed on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20.60Finsupp.60/near/381919585).

Mathlib.lean

@@ -1437,6 +1437,7 @@ import Mathlib.Data.Finsupp.Interval
 import Mathlib.Data.Finsupp.Lex
 import Mathlib.Data.Finsupp.Multiset
 import Mathlib.Data.Finsupp.NeLocus
+import Mathlib.Data.Finsupp.Notation
 import Mathlib.Data.Finsupp.Order
 import Mathlib.Data.Finsupp.Pointwise
 import Mathlib.Data.Finsupp.Pwo

Mathlib/Data/Finsupp/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Algebra.Hom.GroupAction
 import Mathlib.Algebra.Regular.SMul
 import Mathlib.Data.Finset.Preimage
+import Mathlib.Data.Finsupp.Notation
 import Mathlib.Data.Rat.BigOperators
 import Mathlib.Data.Set.Countable
 

Mathlib/Data/Finsupp/Notation.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Data.Finsupp.Defs
+
+/-!
+# Notation for `Finsupp`
+
+This file provides `fun₀ | 3 => a | 7 => b` notation for `Finsupp`, which desugars to
+`Finsupp.update` and `Finsupp.single`, in the same way that `{a, b}` desugars to `insert` and
+`singleton`.
+-/
+
+namespace Finsupp
+
+open Lean
+open Lean.Parser
+open Lean.Parser.Term
+
+/-- A variant of `Lean.Parser.Term.matchAlts` with less line wrapping. -/
+def fun₀.matchAlts : Parser :=
+  leading_parser withPosition $ ppRealGroup <| many1Indent (ppSpace >> ppGroup matchAlt)
+
+@[term_parser, inherit_doc Finsupp]
+def fun₀ := leading_parser:maxPrec
+  ppAllowUngrouped >> unicodeSymbol "λ₀" "fun₀" >> fun₀.matchAlts
+
+macro_rules
+  | `(term| fun₀ $x:matchAlt*) => do
+    let mut stx : Term ← `(0)
+    let mut fst : Bool := true
+    for xi in x do
+      for xii in (← Elab.Term.expandMatchAlt xi) do
+        match xii with
+        | `(matchAltExpr| | $pat => $val) =>
+          if fst then
+            stx ← `(Finsupp.single $pat $val)
+          else
+            stx ← `(Finsupp.update $stx $pat $val)
+          fst := false
+        | _ => Macro.throwUnsupported
+    pure stx
+
+/-- Unexpander for the `fun₀ | i => x` notation. -/
+@[app_unexpander Finsupp.single]
+def singleUnexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $pat $val) => `(fun₀ | $pat => $val)
+  | _ => throw ()
+
+/-- Unexpander for the `fun₀ | i => x` notation. -/
+@[app_unexpander Finsupp.update]
+def updateUnexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $f $pat $val) => match f with
+    | `(fun₀ $xs:matchAlt*) => `(fun₀ $xs:matchAlt* | $pat => $val)
+    | _ => throw ()
+  | _ => throw ()
+
+/-- Display `Finsupp` using `fun₀` notation. -/
+unsafe instance {α β} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β) where
+  reprPrec f p :=
+    if f.support.card = 0 then
+      "0"
+    else
+      let ret := "fun₀" ++
+        Std.Format.join (f.support.val.unquot.map <|
+          fun a => " | " ++ repr a ++ " => " ++ repr (f a))
+      if p ≥ leadPrec then Format.paren ret else ret
+
+end Finsupp

test/finsupp_notation.lean

@@ -0,0 +1,16 @@
+import Mathlib.Data.Finsupp.Notation
+
+example : (fun₀ | 1 => 3) 1 = 3 :=
+by simp
+
+example : (fun₀ | 1 | 2 | 3 => 3 | 3 => 4) 1 = 3 :=
+by simp
+example : (fun₀ | 1 | 2 | 3 => 3 | 3 => 4) 2 = 3 :=
+by simp
+example : (fun₀ | 1 | 2 | 3 => 3 | 3 => 4) 3 = 4 :=
+by simp
+
+#eval show Lean.MetaM Unit from
+  guard <|
+    reprStr (Finsupp.mk {1, 2} (fun | 1 | 2 => 3 | _ => 0) (fun x => by aesop))
+      = "fun₀ | 1 => 3 | 2 => 3"