feat: PProd and MProd syntax (part 2)

actually enables the syntax, adds a test file and updates the test output.
leanprover · Jul 15, 2024 · c9fbd76 · c9fbd76
1 parent ab0241d
commit c9fbd76
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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