feat: delaboration collapses parent projections (#3326)

When projection functions are delaborated, intermediate parent
projections are no longer printed. For example, rather than pretty
printing as `o.toB.toA.x` with these `toB` and `toA` parent projections,
it pretty prints as `o.x`.

This feature is being upstreamed from mathlib.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -793,23 +793,50 @@ def delabProj : Delab := do
   let idx := Syntax.mkLit fieldIdxKind (toString (idx + 1));
   `($(e).$idx:fieldIdx)
 
-/-- Delaborate a call to a projection function such as `Prod.fst`. -/
+/--
+Delaborates an application of a projection function, for example `Prod.fst p` as `p.fst`.
+Collapses intermediate parent projections, so for example rather than `o.toB.toA.x` it produces `o.x`.
+
+Does not delaborate projection functions from classes, since the instance parameter is implicit;
+we would rather see `default` than `instInhabitedNat.default`.
+-/
 @[builtin_delab app]
-def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
-  let Expr.app fn _ ← getExpr | failure
-  let .const c@(.str _ f) _ ← pure fn.getAppFn | failure
-  let env ← getEnv
-  let some info ← pure $ env.getProjectionFnInfo? c | failure
-  -- can't use with classes since the instance parameter is implicit
-  guard $ !info.fromClass
-  -- If pp.explicit is true, and the structure has parameters, we should not
-  -- use field notation because we will not be able to see the parameters.
-  let expl ← getPPOption getPPExplicit
-  guard $ !expl || info.numParams == 0
-  -- projection function should be fully applied (#struct params + 1 instance parameter)
-  withOverApp (info.numParams + 1) do
-    let appStx ← withAppArg delab
-    `($(appStx).$(mkIdent f):ident)
+partial def delabProjectionApp : Delab := whenPPOption getPPStructureProjections do
+  let (field, arity, _) ← projInfo
+  withOverApp arity do
+    let stx ← withAppArg <| withoutParentProjections delab
+    `($(stx).$(mkIdent field):ident)
+where
+  /--
+  If this is a projection that could delaborate using dot notation,
+  returns the field name, the arity of the projector, and whether this is a parent projection.
+  Otherwise it fails.
+  -/
+  projInfo : DelabM (Name × Nat × Bool) := do
+    let .app fn _ ← getExpr | failure
+    let .const c@(.str _ field) _ := fn.getAppFn | failure
+    let env ← getEnv
+    let some info := env.getProjectionFnInfo? c | failure
+    -- Don't delaborate for classes since the instance parameter is implicit.
+    guard <| !info.fromClass
+    -- If pp.explicit is true, and the structure has parameters, we should not
+    -- use field notation because we will not be able to see the parameters.
+    guard <| !(← getPPOption getPPExplicit) || info.numParams == 0
+    let arity := info.numParams + 1
+    let some (.ctorInfo cVal) := env.find? info.ctorName | failure
+    let isParentProj := (isSubobjectField? env cVal.induct field).isSome
+    return (field, arity, isParentProj)
+  /--
+  Consumes projections to parent structures.
+  For example, if the current expression is `o.toB.toA`, runs `d` with `o` as the current expression.
+  -/
+  withoutParentProjections {α} (d : DelabM α) : DelabM α :=
+    (do
+      let (_, arity, isParentProj) ← projInfo
+      guard isParentProj
+      guard <| (← getExpr).getAppNumArgs == arity
+      withAppArg <| withoutParentProjections d)
+    <|> d
 
 /--
 This delaborator tries to elide functions which are known coercions.

tests/lean/delabProjectionApp.lean

@@ -0,0 +1,93 @@
+/-!
+# Delaboration of projection functions
+-/
+
+structure A where
+  x : Nat
+
+structure B extends A where
+  y : Nat
+
+structure C extends B where
+  z : Nat
+
+variable (a : A) (b : B) (c : C)
+
+section
+/-!
+Checking projection delaboration, including parent projection collapse.
+-/
+
+#check a.x
+#check b.x
+#check c.x
+
+#check b.y
+#check c.y
+
+#check c.z
+
+end
+
+section
+/-!
+Checking `pp.structureProjections` can turn off this delaborator.
+-/
+
+set_option pp.structureProjections false
+
+#check a.x
+#check b.x
+#check c.x
+
+#check b.y
+#check c.y
+
+#check c.z
+
+end
+
+structure Fin' extends Fin 5
+
+structure Fin'' (n : Nat) extends Fin n
+
+structure D (n : Nat) extends A
+
+variable (x : Fin 5) (y : Fin') (z : Fin'' 5) (d : D 5)
+
+section
+/-!
+Checking handling of parameters.
+-/
+
+#check x.val
+#check y.val
+#check z.val
+#check d.x
+
+end
+
+section
+/-!
+Check handling of parameters when `pp.explicit` is true.
+-/
+set_option pp.explicit true
+
+#check c.x
+#check x.val
+#check y.val
+#check z.val
+#check d.x
+
+end
+
+structure Fn (α β : Type) where
+  toFun : α → β
+
+variable (f : Fn Nat Int)
+
+/-!
+Check overapplication.
+-/
+
+#check f.toFun 0

tests/lean/delabProjectionApp.lean.expected.out

@@ -0,0 +1,22 @@
+a.x : Nat
+b.x : Nat
+c.x : Nat
+b.y : Nat
+c.y : Nat
+c.z : Nat
+A.x a : Nat
+A.x (B.toA b) : Nat
+A.x (B.toA (C.toB c)) : Nat
+B.y b : Nat
+B.y (C.toB c) : Nat
+C.z c : Nat
+x.val : Nat
+y.val : Nat
+z.val : Nat
+d.x : Nat
+c.x : Nat
+@Fin.val 5 x : Nat
+@Fin.val 5 y.toFin : Nat
+@Fin.val 5 (@Fin''.toFin 5 z) : Nat
+(@D.toA 5 d).x : Nat
+f.toFun 0 : Int

tests/lean/diamond2.lean.expected.out

@@ -3,4 +3,4 @@ Foo2.mk {α : Type} (toBar : Bar (α → α)) (β : Type) (b : α → β) (x1 x2
 @[reducible] def Foo2.toBar : {α : Type} → Foo2 α → Bar (α → α) :=
 fun α self => self.1
 @[reducible] def Foo2.toBoo2 : {α : Type} → Foo2 α → Boo2 α :=
-fun α self => { toBoo1 := { toBaz := { a := self.toBar.a, β := self.β, b := self.b }, x1 := self.x1 }, x2 := self.x2 }
+fun α self => { toBoo1 := { toBaz := { a := self.a, β := self.β, b := self.b }, x1 := self.x1 }, x2 := self.x2 }

tests/lean/diamond3.lean.expected.out

@@ -1,2 +1,2 @@
 @[reducible] def D.toC : D → C :=
-fun self => { toA := self.toB.toA, w := self.w }
+fun self => { toA := self.toA, w := self.w }

tests/lean/structInstSourcesLeftToRight.lean.expected.out

@@ -7,6 +7,6 @@ fun a b => { toB := { x := a.x, y := b.y } }
 def biz : A → B → C :=
 fun a b => { toB := b }
 def faz : A → C → C :=
-fun a c => { toB := { x := a.x, y := c.toB.y } }
+fun a c => { toB := { x := a.x, y := c.y } }
 def fiz : A → C → C :=
 fun a c => { toB := c.toB }

tests/lean/toFieldNameIssue.lean.expected.out

@@ -1,4 +1,4 @@
 { toA_1 := { toA := { x := 0 }, y := 1 }, z := 2 } : B
 { toC := { x := 0, y := 1 }, z := 2 } : D
 @[reducible] def D.toC_1 : D → Boo.C :=
-fun self => { x := self.toC.x, z := self.z }
+fun self => { x := self.x, z := self.z }