From c9fbd7624e45ffb9bae32f4af56d9e0820c88e07 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 12 Jul 2024 10:29:00 +0200
Subject: [PATCH] feat: PProd and MProd syntax (part 2)

actually enables the syntax, adds a test file and updates the test
output.
---
 src/Init/NotationExtra.lean        |  2 --
 src/Lean/Elab/BuiltinNotation.lean |  2 --
 tests/lean/run/PUnit_syntax.lean   | 47 ++++++++++++++++++++++++++++++
 3 files changed, 47 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/PUnit_syntax.lean

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index fea8cf51631c..88ebef2dc3f9 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -163,7 +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)ₚ)
@@ -173,7 +172,6 @@ end Lean
   | `($(_) $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)
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index f94542c88b9e..944319eb73b9 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -330,7 +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)
@@ -339,7 +338,6 @@ where
 @[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
diff --git a/tests/lean/run/PUnit_syntax.lean b/tests/lean/run/PUnit_syntax.lean
new file mode 100644
index 000000000000..ff535167f0cd
--- /dev/null
+++ b/tests/lean/run/PUnit_syntax.lean
@@ -0,0 +1,47 @@
+/-- 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