fix: panic in delabPRange (#9920)

This PR fixes a panic in the delaborator for `Std.PRange`. It also
modifies the delaborators for both `Std.Range` and `Std.PRange` to not
use `let_expr`, which cleans up annotations and metadata, since
delaborators must follow the structures of expressions. It adds support
for `pp.notation` and `pp.explicit` options. It also adds tests for
these delaborators.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1275,53 +1275,63 @@ def delabPProdMk : Delab := delabPProdMkCore ``PProd.mk
 def delabMProdMk : Delab := delabPProdMkCore ``MProd.mk
 
 @[builtin_delab app.Std.Range.mk]
-def delabRange : Delab := do
-  -- Std.Range.mk : Nat → Nat → (step : Nat) → 0 < step → Std.Range
-  let_expr Std.Range.mk start _stop step _prf := (← getExpr) | failure
-  let start_zero := Lean.Expr.nat? start == some 0
-  let step_one := Lean.Expr.nat? step == some 1
-  withAppFn do -- skip the proof
-  let step ← withAppArg delab
-  withAppFn do
-  let stop ← withAppArg delab
-  withAppFn do
-  let start ← withAppArg delab
-  match start_zero, step_one with
-  | false, false => `([$start : $stop : $step])
-  | false, true => `([$start : $stop])
-  | true, false => `([: $stop : $step])
-  | true, true => `([: $stop])
+def delabRange : Delab := whenPPOption getPPNotation do
+  -- Std.Range.mk : (start : Nat) → (stop : Nat) → (step : Nat) → 0 < step → Std.Range
+  guard <| (← getExpr).getAppNumArgs == 4
+  -- `none` if the start is `0`
+  let start? ← withNaryArg 0 do
+    if Lean.Expr.nat? (← getExpr) == some 0 then
+      return none
+    else
+      some <$> delab
+  let stop ← withNaryArg 1 delab
+  -- `none` if the step is `1`
+  let step? ← withNaryArg 2 do
+    if Lean.Expr.nat? (← getExpr) == some 1 then
+      return none
+    else
+      some <$> delab
+  match start?, step? with
+  | some start, some step => `([$start : $stop : $step])
+  | some start, none      => `([$start : $stop])
+  | none,       some step => `([: $stop : $step])
+  | none,       none      => `([: $stop])
 
 @[builtin_delab app.Std.PRange.mk]
-def delabPRange : Delab := do
-  -- Std.PRange.mk : {shape : Std.PRange.RangeShape} → {α : Type u} → Std.PRange.Bound shape.lower α → Std.PRange.Bound shape.upper α → Std.PRange shape α
-  let_expr Std.PRange.mk shape _α lower upper := (← getExpr) | failure
+def delabPRange : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExplicit <| do
+  -- Std.PRange.mk : {shape : Std.PRange.RangeShape} → {α : Type u} →
+  --   (lower : Std.PRange.Bound shape.lower α) → (upper : Std.PRange.Bound shape.upper α) → Std.PRange shape α
+  guard <| (← getExpr).getAppNumArgs == 4
   let reflectBoundShape (e : Expr) : Option Std.PRange.BoundShape := match e.constName? with
-    | some `Std.PRange.BoundShape.closed => Std.PRange.BoundShape.closed
-    | some `Std.PRange.BoundShape.open => Std.PRange.BoundShape.open
-    | some `Std.PRange.BoundShape.unbounded => Std.PRange.BoundShape.unbounded
+    | some ``Std.PRange.BoundShape.closed => Std.PRange.BoundShape.closed
+    | some ``Std.PRange.BoundShape.open => Std.PRange.BoundShape.open
+    | some ``Std.PRange.BoundShape.unbounded => Std.PRange.BoundShape.unbounded
     | _ => failure
   let reflectRangeShape (e : Expr) : Option Std.PRange.RangeShape := do
-    let_expr Std.PRange.RangeShape.mk lower upper := e | failure
+    -- Std.PRange.RangeShape.mk (lower upper : Std.PRange.BoundShape) : Std.PRange.RangeShape
+    guard <| e.isAppOfArity ``Std.PRange.RangeShape.mk 2
+    let lower := e.appFn!.appArg!
+    let upper := e.appArg!
     return ⟨← reflectBoundShape lower, ← reflectBoundShape upper⟩
-  let some shape := reflectRangeShape shape | failure
-  let a ← withAppArg <| withAppArg <| delab
-  let b ← withAppArg <| delab
-  match (shape, lower.constName?, upper.constName?) with
-  | (⟨.closed, .closed⟩, _, _) => `($a...=$b)
-  | (⟨.unbounded, .closed⟩, some `PUnit.unit, _) => `(*...=$b)
-  | (⟨.closed, .unbounded⟩, _, some `PUnit.unit) => `($a...*)
-  | (⟨.unbounded, .unbounded⟩, some `PUnit.unit, some `PUnit.unit) => `(*...*)
-  | (⟨.open, .closed⟩, _, _) => `($a<...=$b)
-  | (⟨.open, .unbounded⟩, _, some `PUnit.unit) => `($a<...*)
-  | (⟨.closed, .open⟩, _, _) => `($a...$b)
-  | (⟨.unbounded, .open⟩, some `PUnit.unit, _) => `(*...$b)
-  | (⟨.open, .open⟩, _, _) => `($a<...$b)
+  let some shape := reflectRangeShape ((← getExpr).getArg! 0) | failure
+  -- Lower bound
+  let a ← withAppFn <| withAppArg delab
+  -- Upper bound
+  let b ← withAppArg delab
+  match shape with
+  | ⟨.closed, .closed⟩       => `($a...=$b)
+  | ⟨.unbounded, .closed⟩    => `(*...=$b)
+  | ⟨.closed, .unbounded⟩    => `($a...*)
+  | ⟨.unbounded, .unbounded⟩ => `(*...*)
+  | ⟨.open, .closed⟩         => `($a<...=$b)
+  | ⟨.open, .unbounded⟩      => `($a<...*)
+  | ⟨.closed, .open⟩         => `($a...$b)
+  | ⟨.unbounded, .open⟩      => `(*...$b)
+  | ⟨.open, .open⟩           => `($a<...$b)
   -- The remaining cases are aliases for explicit `<` upper bound notation:
-  -- | (⟨.closed, .open⟩, _, _) => `($a...<$b)
-  -- | (⟨.unbounded, .open⟩, some `PUnit.unit, _) => `(*...<$b)
-  -- | (⟨.open, .open⟩, _, _) => `($a<...<$b)
-  | _ => failure
+  -- | ⟨.closed, .open⟩    => `($a...<$b)
+  -- | ⟨.unbounded, .open⟩ => `(*...<$b)
+  -- | ⟨.open, .open⟩      => `($a<...<$b)
 
 partial def delabDoElems : DelabM (List Syntax) := do
   let e ← getExpr

tests/lean/ellipsisProjIssue.lean.expected.out

@@ -1,4 +1,3 @@
 ellipsisProjIssue.lean:1:18-1:22: error(lean.unknownIdentifier): Unknown identifier `succ`
-(Function.const Lean.Name ()
-    `ellipsisProjIssue.1.18.1.22.18.22._sorry._@.ellipsisProjIssue._hyg.11)...sorry : Std.PRange
-  { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } (Nat → Nat → Nat)
+Nat.add...sorry : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open }
+  (Nat → Nat → Nat)

tests/lean/run/delabStdRange.lean

@@ -0,0 +1,118 @@
+/-!
+# Tests for delaborators for Std.Range and Std.PRange
+-/
+
+/-!
+## Tests for `Std.Range`
+-/
+
+/-!
+Default lower bound and step
+-/
+/-- info: [:10] : Std.Range -/
+#guard_msgs in #check Std.Range.mk 0 10 1 (by grind)
+
+/-!
+Default step
+-/
+/-- info: [5:10] : Std.Range -/
+#guard_msgs in #check Std.Range.mk 5 10 1 (by grind)
+
+/-!
+Default lower bound
+-/
+/-- info: [:10:2] : Std.Range -/
+#guard_msgs in #check Std.Range.mk 0 10 2 (by grind)
+
+/-!
+No defaults
+-/
+/-- info: [5:10:2] : Std.Range -/
+#guard_msgs in #check Std.Range.mk 5 10 2 (by grind)
+
+/-!
+Disable notation
+-/
+/-- info: { stop := 10, step_pos := _check._proof_1 } : Std.Range -/
+#guard_msgs in set_option pp.notation false in #check Std.Range.mk 0 10 1 (by grind)
+
+/-!
+## Tests for `Std.PRange`
+-/
+
+/-!
+Each of the possibilities, in order of appearance in `Lean.PrettyPrinter.Delaborator.delabPRange`.
+-/
+/--
+info: 1...=10 : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.closed } Nat
+-/
+#guard_msgs in #check 1...=10
+/--
+info: *...=10 : Std.PRange { lower := Std.PRange.BoundShape.unbounded, upper := Std.PRange.BoundShape.closed } Nat
+-/
+#guard_msgs in #check *...=10
+/--
+info: 1...* : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.unbounded } Nat
+-/
+#guard_msgs in #check 1...*
+/--
+info: *...* : Std.PRange { lower := Std.PRange.BoundShape.unbounded, upper := Std.PRange.BoundShape.unbounded } Nat
+-/
+#guard_msgs in #check (*...* : Std.PRange _ Nat)
+/--
+info: 1<...=10 : Std.PRange { lower := Std.PRange.BoundShape.open, upper := Std.PRange.BoundShape.closed } Nat
+-/
+#guard_msgs in #check 1<...=10
+/--
+info: 1<...* : Std.PRange { lower := Std.PRange.BoundShape.open, upper := Std.PRange.BoundShape.unbounded } Nat
+-/
+#guard_msgs in #check 1<...*
+/--
+info: 1...10 : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in #check 1...10
+/--
+info: *...10 : Std.PRange { lower := Std.PRange.BoundShape.unbounded, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in #check *...10
+/--
+info: 1<...10 : Std.PRange { lower := Std.PRange.BoundShape.open, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in #check 1<...10
+
+/-!
+Synonyms for other ranges.
+-/
+/--
+info: 1...10 : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in #check 1...<10
+/--
+info: *...10 : Std.PRange { lower := Std.PRange.BoundShape.unbounded, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in #check *...<10
+/--
+info: 1<...10 : Std.PRange { lower := Std.PRange.BoundShape.open, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in #check 1<...<10
+
+/-!
+Check that responds to both `pp.notation` and `pp.explicit`.
+-/
+/--
+info: { lower := 1,
+  upper := 10 } : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in set_option pp.notation false in #check 1...10
+/--
+info: @Std.PRange.mk { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } Nat
+  (@OfNat.ofNat
+    (Std.PRange.Bound { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open }.lower Nat)
+    (nat_lit 1) (instOfNatNat (nat_lit 1)))
+  (@OfNat.ofNat
+    (Std.PRange.Bound { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open }.upper Nat)
+    (nat_lit 10)
+    (instOfNatNat
+      (nat_lit 10))) : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } Nat
+-/
+#guard_msgs in set_option pp.explicit true in #check 1...10