feat: PProd syntax (part 3) (#4756)

reworks #4730 based on feedback from @kmill:

 * Uses `×'` for PProd
 * No syntax for MProd for now
 * Angle brackets (without nesting) for the values

src/Init/Notation.lean

@@ -267,8 +267,7 @@ syntax (name := rawNatLit) "nat_lit " num : term
 
 @[inherit_doc] infixr:90 " ∘ "  => Function.comp
 @[inherit_doc] infixr:35 " × "  => Prod
-@[inherit_doc] infixr:35 " ×ₚ "  => PProd
-@[inherit_doc] infixr:35 " ×ₘ "  => MProd
+@[inherit_doc] infixr:35 " ×' " => PProd
 
 @[inherit_doc] infix:50  " ∣ " => Dvd.dvd
 @[inherit_doc] infixl:55 " ||| " => HOr.hOr

src/Init/NotationExtra.lean

@@ -163,16 +163,6 @@ end Lean
   | `($(_) $x $y)          => `(($x, $y))
   | _                      => throw ()
 
-@[app_unexpander PProd.mk] def unexpandPProdMk : Lean.PrettyPrinter.Unexpander
-  | `($(_) $x ($y, $ys,*)ₚ) => `(($x, $y, $ys,*)ₚ)
-  | `($(_) $x $y)           => `(($x, $y)ₚ)
-  | _                       => throw ()
-
-@[app_unexpander MProd.mk] def unexpandMProdMk : Lean.PrettyPrinter.Unexpander
-  | `($(_) $x ($y, $ys,*)ₘ) => `(($x, $y, $ys,*)ₘ)
-  | `($(_) $x $y)           => `(($x, $y)ₘ)
-  | _                       => throw ()
-
 @[app_unexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
   | `($(_) $c $t $e) => `(if $c then $t else $e)
   | _                => throw ()

src/Init/Prelude.lean

@@ -488,9 +488,9 @@ attribute [unbox] Prod
 
 /--
 Similar to `Prod`, but `α` and `β` can be propositions.
+You can use `α ×' β` as notation for `PProd α β`.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
-@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α

src/Lean/Elab/BuiltinNotation.lean

@@ -330,15 +330,6 @@ where
     return (← expandCDot? pairs).getD pairs
   | _ => Macro.throwUnsupported
 
-@[builtin_macro Lean.Parser.Term.ptuple] def expandPTuple : Macro
-  | `(()ₚ) => ``(PUnit.unit)
-  | `(($e, $es,*)ₚ) => mkPPairs (#[e] ++ es)
-  | _ => Macro.throwUnsupported
-
-@[builtin_macro Lean.Parser.Term.mtuple] def expandMTuple : Macro
-  | `(($e, $es,*)ₘ) => mkMPairs (#[e] ++ es)
-  | _ => Macro.throwUnsupported
-
 @[builtin_macro Lean.Parser.Term.typeAscription] def expandTypeAscription : Macro
   | `(($e : $(type)?)) => do
     match (← expandCDot? e) with

src/Lean/Parser/Term.lean

@@ -179,14 +179,6 @@ do not yield the right result.
 @[builtin_term_parser] def tuple := leading_parser
   "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
 
-/-- Universe polymorphic tuple notation; `()ₚ` is short for `PUnit.unit`, `(a, b, c)ₚ` for `PProd.mk a (PProd.mk b c)`, etc. -/
-@[builtin_term_parser] def ptuple := leading_parser
-  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")ₚ"
-
-/-- Universe monomorphic tuple notation; `(a, b, c)ₘ` for `MProd.mk a (MProd.mk b c)`, etc. -/
-@[builtin_term_parser] def mtuple := leading_parser
-  "(" >> withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true))) >> ")ₘ"
-
 /--
 Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
 Can also be used for creating simple functions when combined with `·`. Here are some examples:

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1139,6 +1139,24 @@ def delabSigma : Delab := delabSigmaCore (sigma := true)
 @[builtin_delab app.PSigma]
 def delabPSigma : Delab := delabSigmaCore (sigma := false)
 
+-- PProd and MProd value delaborator
+-- (like pp_using_anonymous_constructor but flattening nested tuples)
+
+def delabPProdMkCore (mkName : Name) : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
+  guard <| (← getExpr).getAppNumArgs == 4
+  let a ← withAppFn <| withAppArg delab
+  let b ← withAppArg <| delab
+  if (← getExpr).appArg!.isAppOfArity mkName 4 then
+    if let `(⟨$xs,*⟩) := b then
+      return ← `(⟨$a, $xs,*⟩)
+  `(⟨$a, $b⟩)
+
+@[builtin_delab app.PProd.mk]
+def delabPProdMk : Delab := delabPProdMkCore ``PProd.mk
+
+@[builtin_delab app.MProd.mk]
+def delabMProdMk : Delab := delabPProdMkCore ``MProd.mk
+
 partial def delabDoElems : DelabM (List Syntax) := do
   let e ← getExpr
   if e.isAppOfArity ``Bind.bind 6 then

tests/lean/348.lean.expected.out

@@ -1 +1 @@
-348.lean:3:24-3:25: error: unexpected token '⟩'; expected ')', ')ₘ' or ')ₚ'
+348.lean:3:24-3:25: error: unexpected token '⟩'; expected ')'

tests/lean/interactive/incrementalTactic.lean.expected.out

@@ -32,8 +32,7 @@ t 2
    "severity": 1,
    "range":
    {"start": {"line": 1, "character": 38}, "end": {"line": 4, "character": 3}},
-   "message":
-   "unexpected token '/-!'; expected ')', ')ₚ', '_', identifier or term",
+   "message": "unexpected token '/-!'; expected ')', '_', identifier or term",
    "fullRange":
    {"start": {"line": 1, "character": 38},
     "end": {"line": 4, "character": 3}}}]}

tests/lean/run/PProd_syntax.lean

@@ -0,0 +1,46 @@
+/-- info: Bool ×' Nat ×' List Unit : Type -/
+#guard_msgs in
+#check Bool ×' Nat ×' List Unit
+
+/-- info: Bool ×' Nat ×' List Unit : Type -/
+#guard_msgs in
+#check PProd Bool (PProd Nat (List Unit))
+
+/-- info: (Bool ×' Nat) ×' List Unit : Type -/
+#guard_msgs in
+#check PProd (PProd Bool Nat) (List Unit)
+
+/-- info: PUnit.{u} : Sort u -/
+#guard_msgs in
+#check PUnit
+
+/-- info: ⟨true, 5, [()]⟩ : Bool ×' Nat ×' List Unit -/
+#guard_msgs in
+#check (⟨true, 5, [()]⟩ : Bool ×' Nat ×' List Unit)
+
+/-- info: ⟨true, 5, [()]⟩ : MProd Bool (MProd Nat (List Unit)) -/
+#guard_msgs in
+#check (⟨true, 5, [()]⟩ : MProd Bool (MProd Nat (List Unit)))
+
+/-- info: ⟨true, 5, [()]⟩ : Bool ×' Nat ×' List Unit -/
+#guard_msgs in
+#check PProd.mk true (PProd.mk 5 [()])
+
+/-- info: ⟨true, 5, [()]⟩ : MProd Bool (MProd Nat (List Unit)) -/
+#guard_msgs in
+#check MProd.mk true (MProd.mk 5 [()])
+
+/-- info: PUnit.unit.{u} : PUnit -/
+#guard_msgs in
+#check PUnit.unit
+
+-- check that only `PProd` is flattened, not other structure
+
+@[pp_using_anonymous_constructor]
+structure TwoNats where
+  firstNat : Nat
+  secondNat : Nat
+
+/-- info: ⟨true, 5, ⟨23, 42⟩⟩ : Bool ×' Nat ×' TwoNats -/
+#guard_msgs in
+#check PProd.mk true (PProd.mk 5 (TwoNats.mk 23 42))

tests/lean/run/PUnit_syntax.lean

@@ -1,47 +0,0 @@
-/-- info: Bool ×ₚ Nat ×ₚ List Unit : Type -/
-#guard_msgs in
-#check Bool ×ₚ Nat ×ₚ List Unit
-
-/-- info: Bool ×ₚ Nat ×ₚ List Unit : Type -/
-#guard_msgs in
-#check PProd Bool (PProd Nat (List Unit))
-
-/-- info: (Bool ×ₚ Nat) ×ₚ List Unit : Type -/
-#guard_msgs in
-#check PProd (PProd Bool Nat) (List Unit)
-
-/-- info: Bool ×ₘ Nat ×ₘ List Unit : Type -/
-#guard_msgs in
-#check Bool ×ₘ Nat ×ₘ List Unit
-
-/-- info: Bool ×ₘ Nat ×ₘ List Unit : Type -/
-#guard_msgs in
-#check MProd Bool (MProd Nat (List Unit))
-
-/-- info: (Bool ×ₘ Nat) ×ₘ List Unit : Type -/
-#guard_msgs in
-#check MProd (MProd Bool Nat) (List Unit)
-
-/-- info: PUnit.unit : PUnit -/
-#guard_msgs in
-#check ()ₚ
-
-/-- info: (true, 5, [()])ₚ : Bool ×ₚ Nat ×ₚ List Unit -/
-#guard_msgs in
-#check (true, 5, [()])ₚ
-
-/-- info: (true, 5, [()])ₘ : Bool ×ₘ Nat ×ₘ List Unit -/
-#guard_msgs in
-#check (true, 5, [()])ₘ
-
-/-- info: (true, 5, [()])ₚ : Bool ×ₚ Nat ×ₚ List Unit -/
-#guard_msgs in
-#check PProd.mk true (PProd.mk 5 [()])
-
-/-- info: (true, 5, [()])ₘ : Bool ×ₘ Nat ×ₘ List Unit -/
-#guard_msgs in
-#check MProd.mk true (MProd.mk 5 [()])
-
-/-- info: PUnit.unit.{u} : PUnit -/
-#guard_msgs in
-#check PUnit.unit

tests/lean/trailingComma.lean.expected.out

@@ -1,4 +1,4 @@
 [1, 2, 3]
 (2, 3)
 trailingComma.lean:6:13-6:14: error: unexpected token ','; expected ']'
-trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')', ')ₘ' or ')ₚ'
+trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')'