feat: add delaborators for <|>, <*>, >>, <*, and *> (leanprover#5854)

Closes leanprover#5668

Author: kmill

src/Init/Notation.lean

@@ -341,16 +341,19 @@ macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b)
 
 @[inherit_doc] infixr:67 " :: " => List.cons
-@[inherit_doc HOrElse.hOrElse] syntax:20 term:21 " <|> " term:20 : term
-@[inherit_doc HAndThen.hAndThen] syntax:60 term:61 " >> " term:60 : term
-@[inherit_doc] infixl:55  " >>= " => Bind.bind
-@[inherit_doc] notation:60 a:60 " <*> " b:61 => Seq.seq a fun _ : Unit => b
-@[inherit_doc] notation:60 a:60 " <* " b:61 => SeqLeft.seqLeft a fun _ : Unit => b
-@[inherit_doc] notation:60 a:60 " *> " b:61 => SeqRight.seqRight a fun _ : Unit => b
 @[inherit_doc] infixr:100 " <$> " => Functor.map
+@[inherit_doc] infixl:55  " >>= " => Bind.bind
+@[inherit_doc HOrElse.hOrElse]   syntax:20 term:21 " <|> " term:20 : term
+@[inherit_doc HAndThen.hAndThen] syntax:60 term:61 " >> " term:60 : term
+@[inherit_doc Seq.seq]           syntax:60 term:60 " <*> " term:61 : term
+@[inherit_doc SeqLeft.seqLeft]   syntax:60 term:60 " <* " term:61 : term
+@[inherit_doc SeqRight.seqRight] syntax:60 term:60 " *> " term:61 : term
 
 macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
 macro_rules | `($x >> $y)  => `(binop_lazy% HAndThen.hAndThen $x $y)
+macro_rules | `($x <*> $y) => `(Seq.seq $x fun _ : Unit => $y)
+macro_rules | `($x <* $y)  => `(SeqLeft.seqLeft $x fun _ : Unit => $y)
+macro_rules | `($x *> $y)  => `(SeqRight.seqRight $x fun _ : Unit => $y)
 
 namespace Lean
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1218,6 +1218,30 @@ def delabDo : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotati
   let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem))
   `(do $items:doSeqItem*)
 
+/-- Delaborates a function application of the form `f ... x (fun _ : Unit => y)`. -/
+def delabLazyBinop (arity : Nat) (k : Term → Term → DelabM Term) : DelabM Term :=
+  whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp arity do
+    let y ← withAppArg do
+      let b := (← getExpr).beta #[mkConst ``Unit.unit]
+      withTheReader SubExpr (fun s => {s with pos := s.pos.pushBindingBody, expr := b}) delab
+    let x ← withAppFn <| withAppArg delab
+    k x y
+
+@[builtin_delab app.HOrElse.hOrElse]
+def delabHOrElse : Delab := delabLazyBinop 6 (fun x y => `($x <|> $y))
+
+@[builtin_delab app.HAndThen.hAndThen]
+def delabHAndThen : Delab := delabLazyBinop 6 (fun x y => `($x >> $y))
+
+@[builtin_delab app.Seq.seq]
+def delabSeq : Delab := delabLazyBinop 6 (fun x y => `($x <*> $y))
+
+@[builtin_delab app.SeqLeft.seqLeft]
+def delabSeqLeft : Delab := delabLazyBinop 6 (fun x y => `($x <* $y))
+
+@[builtin_delab app.SeqRight.seqRight]
+def delabSeqRight : Delab := delabLazyBinop 6 (fun x y => `($x *> $y))
+
 @[builtin_delab app.Lean.Name.str,
   builtin_delab app.Lean.Name.mkStr1, builtin_delab app.Lean.Name.mkStr2, builtin_delab app.Lean.Name.mkStr3, builtin_delab app.Lean.Name.mkStr4,
   builtin_delab app.Lean.Name.mkStr5, builtin_delab app.Lean.Name.mkStr6, builtin_delab app.Lean.Name.mkStr7, builtin_delab app.Lean.Name.mkStr8]

tests/lean/eagerCoeExpansion.lean.expected.out

@@ -18,4 +18,4 @@ fun (a : Nat) =>
       (@bne.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
       Bool.true)
 def s : Option Nat :=
-HOrElse.hOrElse (myFun.f 3) fun x => myFun.f 4
+myFun.f 3 <|> myFun.f 4

tests/lean/run/5668.lean

@@ -0,0 +1,36 @@
+import Lean
+/-!
+# Pretty printing of `<|>`, `<*>`, `>>`, `<*`, and `*>`
+
+https://github.com/leanprover/lean4/issues/5668
+-/
+
+/-- info: none <|> some false : Option Bool -/
+#guard_msgs in #check none <|> some false
+
+variable [Monad m] (a : m α) (b : m β) (f : m (α → β))
+
+/-- info: f <*> a : m β -/
+#guard_msgs in #check f <*> a
+
+/-- info: a <* b : m α -/
+#guard_msgs in #check a <* b
+
+/-- info: a *> b : m β -/
+#guard_msgs in #check a *> b
+
+/-- info: Lean.Parser.ident >> Lean.Parser.symbol "hi" : Lean.Parser.Parser -/
+#guard_msgs in #check Lean.Parser.ident >> "hi"
+
+
+/-!
+Dependent, substitutes in `()`.
+-/
+/-- info: some true <|> some (() == ()) : Option Bool -/
+#guard_msgs in #check HOrElse.hOrElse (some true) (fun h => some <| h == ())
+
+/-!
+Not a lambda, applies `()`.
+-/
+/-- info: some true <|> Function.const Unit (some true) () : Option Bool -/
+#guard_msgs in #check HOrElse.hOrElse (some true) (Function.const _ (some true))