feat: PProd and MProd syntax (part 1) (#4747)

the internal constructions for structural and well-founded recursion
use plenty of `PProd` and `MProd`, and reading these, deeply
nested and in prefix notation, is unnecessarily troublesome.

Therefore this introduces notations
```
a ×ₚ b   -- PProd a b
a ×ₘ b   -- MProd a b
()ₚ      -- PUnit.unit
(x,y,z)ₚ -- PProd.mk x (PProd.mk y z)
(x,y,z)ₘ -- MProd.mk x (MProd.mk y z)
```

(This is part 1, the rest will follow in #4730 after a stage0 update.)

Author: nomeata

src/Init/Notation.lean

@@ -267,6 +267,8 @@ 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] infix:50  " ∣ " => Dvd.dvd
 @[inherit_doc] infixl:55 " ||| " => HOr.hOr

src/Init/NotationExtra.lean

@@ -163,6 +163,18 @@ 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/Lean/Elab/BuiltinNotation.lean

@@ -220,6 +220,31 @@ partial def mkPairs (elems : Array Term) : MacroM Term :=
       pure acc
   loop (elems.size - 1) elems.back
 
+/-- Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
+partial def mkPPairs (elems : Array Term) : MacroM Term :=
+  let rec loop (i : Nat) (acc : Term) := do
+    if i > 0 then
+      let i    := i - 1
+      let elem := elems[i]!
+      let acc ← `(PProd.mk $elem $acc)
+      loop i acc
+    else
+      pure acc
+  loop (elems.size - 1) elems.back
+
+/-- Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
+partial def mkMPairs (elems : Array Term) : MacroM Term :=
+  let rec loop (i : Nat) (acc : Term) := do
+    if i > 0 then
+      let i    := i - 1
+      let elem := elems[i]!
+      let acc ← `(MProd.mk $elem $acc)
+      loop i acc
+    else
+      pure acc
+  loop (elems.size - 1) elems.back
+
+
 open Parser in
 partial def hasCDot : Syntax → Bool
   | Syntax.node _ k args =>
@@ -305,6 +330,17 @@ 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

@@ -174,9 +174,19 @@ do not yield the right result.
 -/
 @[builtin_term_parser] def typeAscription := leading_parser
   "(" >> (withoutPosition (withoutForbidden (termParser >> " :" >> optional (ppSpace >> termParser)))) >> ")"
+
 /-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. -/
 @[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:

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/348.lean.expected.out

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

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

@@ -32,7 +32,8 @@ 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/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 ')'
+trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')', ')ₘ' or ')ₚ'