feat: notation3 delaborator generation (leanprover-community#4533)

Gives the `notation3` command the ability to generate a delaborator in most common situations. When it succeeds, `notation3`-defined syntax is pretty printable.

Examples:
```
(⋃ (i : ι) (i' : ι'), s i i') = ⋃ (i' : ι') (i : ι), s i i'
(⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ
```



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Data/Pi/Lex.lean

@@ -51,7 +51,7 @@ protected def Lex (x y : ∀ i, β i) : Prop :=
 /- This unfortunately results in a type that isn't delta-reduced, so we keep the notation out of the
 basic API, just in case -/
 /-- The notation `Πₗ i, α i` refers to a pi type equipped with the lexicographic order. -/
-notation3 "Πₗ "(...)", "r:(scoped p => Lex (∀ i, p i)) => r
+notation3 (prettyPrint := false) "Πₗ "(...)", "r:(scoped p => Lex (∀ i, p i)) => r
 
 @[simp]
 theorem toLex_apply (x : ∀ i, β i) (i : ι) : toLex x i = x i :=

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

@@ -522,7 +522,7 @@ def isoCycle' : { f : Perm α // IsCycle f } ≃ { s : Cycle α // s.Nodup ∧ s
 #align equiv.perm.iso_cycle' Equiv.Perm.isoCycle'
 
 notation3 "c["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
-  Cycle.formPerm (↑l) (Cycle.nodup_coe_iff.mpr _)
+  Cycle.formPerm (Cycle.ofList l) (Iff.mpr Cycle.nodup_coe_iff _)
 
 unsafe instance repr_perm [Repr α] : Repr (Perm α) :=
   ⟨fun f _ => repr (Multiset.pmap (fun (g : Perm α) (hg : g.IsCycle) => isoCycle ⟨g, hg⟩)

Mathlib/MeasureTheory/Integral/Lebesgue.lean

@@ -117,23 +117,6 @@ notation3 "∫⁻ "(...)" in "s", "r:(scoped f => f)" ∂"μ => lintegral (Measu
 @[inherit_doc MeasureTheory.lintegral]
 notation3 "∫⁻ "(...)" in "s", "r:(scoped f => lintegral (Measure.restrict volume s) f) => r
 
-open Lean in
-@[app_unexpander MeasureTheory.lintegral]
-def _root_.unexpandLIntegral : PrettyPrinter.Unexpander
-  | `($(_) $μ fun $x:ident => $b) =>
-    match μ with
-    | `(Measure.restrict volume $s) => `(∫⁻ $x:ident in $s, $b)
-    | `(volume) => `(∫⁻ $x:ident, $b)
-    | `(Measure.restrict $ν $s) => `(∫⁻ $x:ident in $s, $b ∂$ν)
-    | _ => `(∫⁻ $x:ident, $b ∂$μ)
-  | `($(_) $μ fun ($x:ident : $t) => $b) =>
-    match μ with
-    | `(Measure.restrict volume $s) => `(∫⁻ ($x:ident : $t) in $s, $b)
-    | `(volume) => `(∫⁻ ($x:ident : $t), $b)
-    | `(Measure.restrict $ν $s) => `(∫⁻ ($x:ident : $t) in $s, $b ∂$ν)
-    | _ => `(∫⁻ ($x:ident : $t), $b ∂$μ)
-  | _ => throw ()
-
 theorem SimpleFunc.lintegral_eq_lintegral {m : MeasurableSpace α} (f : α →ₛ ℝ≥0∞) (μ : Measure α) :
     (∫⁻ a, f a ∂μ) = f.lintegral μ := by
   rw [MeasureTheory.lintegral]

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -638,11 +638,11 @@ section MeasureSpace
 
 -- mathport name: «expr∀ᵐ , »
 notation3 "∀ᵐ "(...)", "r:(scoped P =>
-  Filter.Eventually P MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r
+  Filter.Eventually P <| MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r
 
 -- mathport name: «expr∃ᵐ , »
 notation3 "∃ᵐ "(...)", "r:(scoped P =>
-  Filter.Frequently P MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r
+  Filter.Frequently P <| MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r
 
 /-- The tactic `exact volume`, to be used in optional (`autoParam`) arguments. -/
 macro "volume_tac" : tactic =>

Mathlib/Order/CompleteLattice.lean

@@ -110,23 +110,9 @@ macro_rules
 /-- Indexed supremum. -/
 notation3 "⨆ "(...)", "r:(scoped f => iSup f) => r
 
-/-- Unexpander for the indexed supremum notation.-/
-@[app_unexpander iSup]
-def iSup.unexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ fun $x:ident ↦ $p) => `(⨆ $x:ident, $p)
-  | `($_ fun ($x:ident : $ty:term) ↦ $p) => `(⨆ ($x:ident : $ty:term), $p)
-  | _ => throw ()
-
 /-- Indexed infimum. -/
 notation3 "⨅ "(...)", "r:(scoped f => iInf f) => r
 
-/-- Unexpander for the indexed infimum notation.-/
-@[app_unexpander iInf]
-def iInf.unexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ fun $x:ident ↦ $p) => `(⨅ $x:ident, $p)
-  | `($_ fun ($x:ident : $ty:term) ↦ $p) => `(⨅ ($x:ident : $ty:term), $p)
-  | _ => throw ()
-
 instance OrderDual.supSet (α) [InfSet α] : SupSet αᵒᵈ :=
   ⟨(sInf : Set α → α)⟩
 

Mathlib/Order/Filter/FilterProduct.lean

@@ -32,7 +32,7 @@ open Classical
 
 namespace Filter
 
-local notation3 "∀* "(...)", "r:(scoped p => Filter.Eventually p φ) => r
+local notation3 "∀* "(...)", "r:(scoped p => Filter.Eventually p (Ultrafilter.toFilter φ)) => r
 
 namespace Germ
 

test/notation3.lean

@@ -3,6 +3,8 @@ import Mathlib.Init.Data.Nat.Lemmas
 
 namespace Test
 
+-- set_option trace.notation3 true
+
 def Filter (α : Type) : Type := (α → Prop) → Prop
 def Filter.atTop [Preorder α] : Filter α := fun _ => True
 def Filter.eventually (p : α → Prop) (f : Filter α) := f p
@@ -16,10 +18,38 @@ notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) =>
 notation3 "∃' " (...) ", " r:(scoped p => Exists p) => r
 #check ∃' x < 3, x < 3
 
+def func (x : α) : α := x
+notation3 "func! " (...) ", " r:(scoped p => func p) => r
+-- Make sure it handles additional arguments. Should not consume `(· * 2)`.
+-- Note: right now this causes the notation to not pretty print at all.
+#check (func! (x : Nat → Nat), x) (· * 2)
 
-notation3 "~{" (x";"* => foldl (a b => (a, b)) ()) "}~" => x
+structure MyUnit
+notation3 "~{" (x"; "* => foldl (a b => Prod.mk a b) MyUnit) "}~" => x
 #check ~{1; true; ~{2}~}~
 #check ~{}~
 
-notation3 "%[" (x","* => foldr (a b => a :: b) []) "]" => x
+notation3 "%[" (x", "* => foldr (a b => List.cons a b) List.nil) "]" => x
 #check %[1, 2, 3]
+
+def foo (a : Nat) (f : Nat → Nat) := a + f a
+def bar (a b : Nat) := a * b
+notation3 "*[" x "] " (...) ", " v:(scoped c => bar x (foo x c)) => v
+#check *[1] (x) (y), x + y
+#check bar 1
+
+-- Checking that the `<|` macro is expanded when making matcher
+def foo' (a : Nat) (f : Nat → Nat) := a + f a
+def bar' (a b : Nat) := a * b
+notation3 "*'[" x "] " (...) ", " v:(scoped c => bar' x <| foo' x c) => v
+#check *'[1] (x) (y), x + y
+#check bar' 1
+
+-- Currently does not pretty print due to pi type
+notation3 (prettyPrint := false) "MyPi " (...) ", " r:(scoped p => (x : _) → p x) => r
+#check MyPi (x : Nat) (y : Nat), x < y
+
+-- The notation parses fine, but the delaborator never succeeds, which is expected
+def myId (x : α) := x
+notation3 "BAD " c "; " (x", "* => foldl (a b => b) c) " DAB" => myId x
+#check BAD 1; 2, 3 DAB