feat: enable pp.fieldNotation.generalized globally (#3744)

Sets the default value to `pp.fieldNotation.generalized` to `true`.
Updates tests, and fixes some minor flaws in the implementation of the
generalized field notation pretty printer.

Now generalized field notation won't be used for any function that has a
`motive` argument. This is intended to prevent recursors from pretty
printing using it as (1) recursors are more like control flow structures
than actual functions and (2) generalized field notation tends to cause
elaboration problems for recursors.

Note: be sure functions that have an `@[app_unexpander]` use
`@[pp_nodot]` if applicable. For example, `List.toArray` needs
`@[pp_nodot]` to ensure the unexpander prints it using `#[...]`
notation.

RELEASES.md

@@ -57,9 +57,9 @@ v4.8.0 (development in progress)
   rather than `{a := x, b := y, c := z}`.
   This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
 
-* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is a new suboption `pp.fieldNotation.generalized`
-  to enable pretty printing function applications using generalized field notation.
-  Field notation can now be disabled function-by-function using the `@[pp_nodot]` attribute.
+* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
+  to enable pretty printing function applications using generalized field notation (defaults to true).
+  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
 Breaking changes:
 

src/Init/Prelude.lean

@@ -2755,7 +2755,7 @@ def List.redLength : List α → Nat
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
-@[inline, match_pattern, export lean_list_to_array]
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -17,12 +17,12 @@ namespace Lean.PrettyPrinter.Delaborator
 open Meta
 
 /--
-If this is a structure projection that could delaborate using dot notation,
+If this constant is a structure projection that could delaborate using dot notation,
 returns the field name, the number of parameters before the structure argument, and whether this is a parent projection.
 Otherwise it fails.
 -/
-private def projInfo (f : Expr) : MetaM (Name × Nat × Bool) := do
-  let .const c@(.str _ field) _ := f.consumeMData | failure
+private def projInfo (c : Name) : MetaM (Name × Nat × Bool) := do
+  let .str _ field := c | failure
   let field := Name.mkSimple field
   let env ← getEnv
   let some info := env.getProjectionFnInfo? c | failure
@@ -33,32 +33,46 @@ private def projInfo (f : Expr) : MetaM (Name × Nat × Bool) := do
   return (field, info.numParams, isParentProj)
 
 /--
-If this function application could delaborate using generalized field notation,
+Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types.
+-/
+private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
+  if type.cleanupAnnotations.isAppOf baseName then
+    return true
+  else
+    return (← whnfR type).isAppOf baseName
+
+/--
+If this constant application could delaborate using generalized field notation with little confusion,
 returns the field name and the index for the argument to be used as the object of the field notation.
 Otherwise it fails.
 -/
-private def generalizedFieldInfo (f : Expr) (args : Array Expr) : MetaM (Name × Nat) := do
-  let .const name@(.str _ field) .. := f.consumeMData | failure
+private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × Nat) := do
+  let .str _ field := c | failure
   let field := Name.mkSimple field
-  let baseName := name.getPrefix
+  let baseName := c.getPrefix
   guard <| !baseName.isAnonymous
-  Meta.forallBoundedTelescope (← instantiateMVars <| ← inferType f) args.size fun params _ => do
+  -- Disallow `Function` since it is used for pi types.
+  guard <| baseName != `Function
+  let info ← getConstInfo c
+  -- Search for the first argument that could be used for field notation
+  -- and make sure it is the first explicit argument.
+  Meta.forallBoundedTelescope info.type args.size fun params _ => do
     for i in [0:params.size] do
       let fvarId := params[i]!.fvarId!
-      if (← fvarId.getBinderInfo).isExplicit then
-        -- We only consider the first explicit argument, so fail if the parameter does not have the correct type.
-        guard <| (← fvarId.getType).cleanupAnnotations.isAppOf baseName
-        let argTy ← instantiateMVars <| ← inferType args[i]!
-        -- Generalized field notation allows either an an exact match, or a match after `whnfR`.
-        if argTy.consumeMData.isAppOf baseName then
-          return (field, i)
-        else if (← Meta.whnfR argTy).isAppOf baseName then
-          return (field, i)
-        else
-          failure
+      -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
+      -- Plus, recursors tend to be riskier when using dot notation.
+      if (← fvarId.getUserName) == `motive then
+        failure
+      if (← typeMatchesBaseName (← fvarId.getType) baseName) then
+        guard (← fvarId.getBinderInfo).isExplicit
+        -- We require an exact match for the base name.
+        -- While `Lean.Elab.Term.resolveLValLoop` is able to unfold the type and iterate, we do not attempt to exploit this feature.
+        -- (To get it right, we would need to check that each relevant namespace does not contain a declaration named `field`.)
+        guard <| (← instantiateMVars <| ← inferType args[i]!).consumeMData.isAppOf baseName
+        return (field, i)
       else
-        -- If not explicit, then make sure that this parameter can't be used for field notation.
-        guard <| ! (← fvarId.getType).cleanupAnnotations.isAppOf baseName
+        -- We only use the first explicit argument for field notation.
+        guard !(← fvarId.getBinderInfo).isExplicit
     failure
 
 /--
@@ -67,20 +81,20 @@ returns the field name to use and the argument index for the object of the field
 -/
 def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldNotation : Bool) : MetaM (Option (Name × Nat)) := do
   let env ← getEnv
-  let .const name .. := f.consumeMData | return none
-  if name.getPrefix.isAnonymous then return none
+  let .const c .. := f.consumeMData | return none
+  if c.getPrefix.isAnonymous then return none
   -- If there is `pp_nodot` on this function, then don't use field notation for it.
-  if hasPPNoDotAttribute env name then
+  if hasPPNoDotAttribute env c then
     return none
   -- Handle structure projections
   try
-    let (field, numParams, _) ← projInfo f
+    let (field, numParams, _) ← projInfo c
     return (field, numParams)
   catch _ => pure ()
   -- Handle generalized field notation
   if useGeneralizedFieldNotation then
     try
-      return ← generalizedFieldInfo f args
+      return ← generalizedFieldInfo c args
     catch _ => pure ()
   -- It's not handled by any of the above.
   return none
@@ -92,7 +106,8 @@ If `explicit` is `true`, then further requires that the structure have no parame
 def isParentProj (explicit : Bool) (e : Expr) : MetaM Bool := do
   unless e.isApp do return false
   try
-    let (_, numParams, isParentProj) ← projInfo e.getAppFn
+    let .const c .. := e.getAppFn | failure
+    let (_, numParams, isParentProj) ← projInfo c
     return isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1
   catch _ =>
     return false

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -96,7 +96,7 @@ register_builtin_option pp.fieldNotation : Bool := {
   descr    := "(pretty printer) use field notation when pretty printing, including for structure projections, unless '@[pp_nodot]' is applied"
 }
 register_builtin_option pp.fieldNotation.generalized : Bool := {
-  defValue := false -- TODO(kmill): set to true
+  defValue := true
   group    := "pp"
   descr    := "(pretty printer) when `pp.fieldNotation` is true, enable using generalized field notation when the argument for field notation is the first explicit argument"
 }

tests/lean/1113.lean.expected.out

@@ -1,3 +1,3 @@
 n : Nat
-f : Fin (Nat.succ n)
+f : Fin n.succ
 ⊢ foo f = 0

tests/lean/1279.lean.expected.out

@@ -3,6 +3,6 @@ fun {α β γ} x x_1 =>
   match β, γ, x, x_1 with
   | β, .(β), Arrow.id, g => g
   | .(α), γ, f, Arrow.id => f
-  | β, γ, Arrow.comp f₁ f₂, g => Arrow.comp f₁ (Arrow.comp f₂ g)
-  | β, γ, f, g => Arrow.comp f g
+  | β, γ, f₁.comp f₂, g => f₁.comp (f₂.comp g)
+  | β, γ, f, g => f.comp g
 Arrow.unit

tests/lean/1616.lean.expected.out

@@ -1,5 +1,5 @@
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
@@ -14,12 +14,12 @@ context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) c.left
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
@@ -34,17 +34,17 @@ context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) c.left
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) c.left
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m

tests/lean/1763.lean.expected.out

@@ -1,4 +1,4 @@
 theorem ex1 : ∀ {p q : Prop}, (p ↔ q) → P q → P p :=
-fun {p q} h h' => Eq.mpr (id (propext (P_congr p q h))) h'
+fun {p q} h h' => (id (propext (P_congr p q h))).mpr h'
 theorem ex2 : ∀ {p q : Prop}, p = q → P q → P p :=
-fun {p q} h h' => Eq.mpr (id (propext (P_congr p q (Iff.of_eq h)))) h'
+fun {p q} h h' => (id (propext (P_congr p q (Iff.of_eq h)))).mpr h'

tests/lean/2161.lean.expected.out

@@ -1,12 +1,12 @@
 2161.lean:15:48-15:54: error: tactic 'decide' failed for proposition
-  mul (mul (mul 4 1) 1) 1 = 4
+  ((mul 4 1).mul 1).mul 1 = 4
 since its 'Decidable' instance reduced to
   Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
-    (instDecidableEqNat (mul (mul (mul 4 1) 1) 1).num 4)
+    (instDecidableEqNat (((mul 4 1).mul 1).mul 1).num 4)
 rather than to the 'isTrue' constructor.
 2161.lean:22:48-22:54: error: tactic 'decide' failed for proposition
-  add (add (add 4 1) 1) 1 = 4
+  ((add 4 1).add 1).add 1 = 4
 since its 'Decidable' instance reduced to
   Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
-    (instDecidableEqNat (add (add (add 4 1) 1) 1).num 4)
+    (instDecidableEqNat (((add 4 1).add 1).add 1).num 4)
 rather than to the 'isTrue' constructor.

tests/lean/415.lean.expected.out

@@ -1,4 +1,4 @@
-Set.insert (Set.insert (Set.insert Set.empty 1) 2) 3 : Set Nat
+((Set.empty.insert 1).insert 2).insert 3 : Set Nat
 fun x y => g { x := x, y := y } : Nat → Nat → Nat
-fun x y => Set.insert (Set.insert Set.empty x) y : Nat → Nat → Set Nat
+fun x y => (Set.empty.insert x).insert y : Nat → Nat → Set Nat
 fun x y => { x := x, y := y } : Nat → Nat → Point

tests/lean/445.lean.expected.out

@@ -1,7 +1,7 @@
 true
 (match i with
   | 0 => true
-  | Nat.succ n => true) &&
+  | n.succ => true) &&
   f i
 if i < 5 then 0 else 1
 if i < 5 then 0 else g i j

tests/lean/449.lean.expected.out

@@ -2,7 +2,7 @@
 context:
 m n : Nat
 ih : m * n = n * m
-⊢ m * n + m = m * n + succ zero * m
+⊢ m * n + m = m * n + zero.succ * m
 449.lean:13:19-13:20: error: don't know how to synthesize placeholder
 context:
 x y : Prop

tests/lean/474.lean.expected.out

@@ -1,8 +1,8 @@
 let y := Nat.zero;
-Nat.add y y
-fun y_1 => Nat.add y y_1
+y.add y
+fun y_1 => y.add y_1
 fun y => Nat.add _fvar.1 y
 fun (y : Nat) => Nat.add y y
-Nat.add ?m y
+?m.add y
 Nat.add (?m #0) #0
-fun y => Nat.add (Nat.add y y) y
+fun y => (y.add y).add y

tests/lean/550.lean.expected.out

@@ -1,4 +1,4 @@
 550.lean:3:2-3:6: error: unsolved goals
 x : Nat
-h : ∀ (x : Nat), x + 1 = Nat.succ x
-⊢ Nat.succ (x + 1) = 1 + (x + 1)
+h : ∀ (x : Nat), x + 1 = x.succ
+⊢ (x + 1).succ = 1 + (x + 1)

tests/lean/690.lean.expected.out

@@ -2,12 +2,12 @@
 690.lean:6:0-6:7: warning: declaration uses 'sorry'
 case step
 a b m✝ : Nat
-hStep : Nat.le a m✝
-ih : Nat.le a (m✝ + 1)
-⊢ Nat.le a (Nat.succ m✝ + 1)
+hStep : a.le m✝
+ih : a.le (m✝ + 1)
+⊢ a.le (m✝.succ + 1)
 690.lean:11:0-11:7: warning: declaration uses 'sorry'
 case step
 a b x : Nat
-hStep : Nat.le a x
-ih : Nat.le a (x + 1)
-⊢ Nat.le a (Nat.succ x + 1)
+hStep : a.le x
+ih : a.le (x + 1)
+⊢ a.le (x.succ + 1)

tests/lean/arrayGetU.lean.expected.out

@@ -1,14 +1,14 @@
 i j : Nat
 a : Array Nat
 v : Nat
-h₁ : i < Array.size a
-h₂ : j < Array.size a
+h₁ : i < a.size
+h₂ : j < a.size
 h₃ : i = j
 ⊢ f a i v h₁ = f a j v h₂
 i j : Nat
 a : Array Nat
 v : Nat
-h₁ : 0 + i < Array.size a
-h₂ : j < Array.size a
+h₁ : 0 + i < a.size
+h₂ : j < a.size
 h₃ : i = j
-⊢ f a i v (Nat.zero_add i ▸ h₁) = f a j v h₂
+⊢ f a i v (i.zero_add ▸ h₁) = f a j v h₂

tests/lean/autoImplicitChainNameIssue.lean.expected.out

@@ -2,5 +2,5 @@ autoImplicitChainNameIssue.lean:8:11-8:15: error: unsolved goals
 case nil
 α✝ : Type u_1
 as : List α✝
-⊢ Palindrome (List.reverse [])
-palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)
+⊢ Palindrome [].reverse
+palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverse

tests/lean/badIhName.lean.expected.out

@@ -5,4 +5,4 @@ case z
 case s
 a✝ : Nat
 a_ih✝ : add Nat.z a✝ = a✝
-⊢ add Nat.z (Nat.s a✝) = Nat.s a✝
+⊢ add Nat.z a✝.s = a✝.s

tests/lean/congrThmIssue.lean.expected.out

@@ -4,7 +4,7 @@ cap : Nat
 backing : Fin cap → Option α
 size : Nat
 h_size : size ≤ cap
-h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing ⟨i, ⋯⟩) = true
+h_full : ∀ (i : Nat) (h : i < size), (backing ⟨i, ⋯⟩).isSome = true
 i : Nat
 h : i < size
-⊢ Option.isSome (if h_1 : i < cap then backing ⟨i, ⋯⟩ else none) = true
+⊢ (if h_1 : i < cap then backing ⟨i, ⋯⟩ else none).isSome = true

tests/lean/conv1.lean.expected.out

@@ -5,10 +5,10 @@ x y : Nat
 x y : Nat
 | x + y = y + x + 0
 x y : Nat
-⊢ x + y = Nat.add y x
+⊢ x + y = y.add x
 case x
 x y : Nat
-⊢ x + y = Nat.add y x
+⊢ x + y = y.add x
 case a
 a b : Nat
 | foo (0 + a) (b + 0)
@@ -48,11 +48,11 @@ case y
 a b : Nat
 | b
 x y : Nat
-⊢ x + y = Nat.add y x
+⊢ x + y = y.add x
 x y : Nat
-⊢ Nat.add x y = Nat.add y x
+⊢ x.add y = y.add x
 x y : Nat
-⊢ f x (Nat.add x y) y = y + x
+⊢ f x (x.add y) y = y + x
 x y : Nat
 | x + y
 case h.h

tests/lean/diamond9.lean.expected.out

@@ -1,2 +1,2 @@
 constructor Ring.mk.{u} : {R : Type u} → [toZero : Zero R] → (gsmul : Int → R → R) → (∀ (a : R), gsmul 0 a = 0) → Ring R
-Ring.mk (fun x n => Int.toNat x * n) ⋯ : Ring Nat
+Ring.mk (fun x n => x.toNat * n) ⋯ : Ring Nat

tests/lean/doIssue.lean.expected.out

@@ -5,15 +5,15 @@ has type
 but is expected to have type
   IO PUnit : Type
 doIssue.lean:10:2-10:13: error: type mismatch
-  Array.set! xs 0 1
+  xs.set! 0 1
 has type
   Array Nat : Type
 but is expected to have type
   IO PUnit : Type
 doIssue.lean:18:7-18:20: error: application type mismatch
-  pure (Array.set! xs 0 1)
+  pure (xs.set! 0 1)
 argument
-  Array.set! xs 0 1
+  xs.set! 0 1
 has type
   Array Nat : Type
 but is expected to have type

tests/lean/eta.lean.expected.out

@@ -1,5 +1,5 @@
 [Meta.debug] >> fun x => Nat.add
 [Meta.debug] >> Nat.add
 [Meta.debug] >> HAdd.hAdd 1
-[Meta.debug] >> fun x y z => Nat.add z y
-[Meta.debug] >> fun y => Nat.add y y
+[Meta.debug] >> fun x y z => z.add y
+[Meta.debug] >> fun y => y.add y