From c50f04ace0b591027ce48db93d09dbf3e6199e9f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 26 Oct 2024 16:49:16 -0700 Subject: [PATCH] feat: add delaborators for `<|>`, `<*>`, `>>`, `<*`, and `*>` (#5854) Closes #5668 --- src/Init/Notation.lean | 15 ++++---- .../PrettyPrinter/Delaborator/Builtins.lean | 24 +++++++++++++ .../lean/eagerCoeExpansion.lean.expected.out | 2 +- tests/lean/run/5668.lean | 36 +++++++++++++++++++ 4 files changed, 70 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/5668.lean diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index b1fa482a50..0ffae63324 100644 --- a/src/Init/Notation.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index aa13f8f2c5..17e0d219e5 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/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] diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out index 8ececc770a..66d54a390f 100644 --- a/tests/lean/eagerCoeExpansion.lean.expected.out +++ b/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 diff --git a/tests/lean/run/5668.lean b/tests/lean/run/5668.lean new file mode 100644 index 0000000000..ef086f316d --- /dev/null +++ b/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))