feat: add pp.fieldNotation.generalized for generalized field notati…

…on, add `@[pp_nodot]` attribute (#3737)

Refactors app delaborator, merging in the projection delaborator, to
support pretty printing with generalized field notation.

Renames option `pp.structureProjections` to `pp.fieldNotation` and adds
sub-option `pp.fieldNotation.generalized` to enable/disable generalized
field notation. Adds `@[pp_nodot]` attribute to permanently disable
using field notation for a given declaration.

For now, the default value of `pp.fieldNotation.generalized` is false
since we need a stage0 update to add `@[pp_nodot]` to some core
definitions (such as `List.toArray`) before updating the tests.

[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60pp.2EgeneralizedFieldNotation.60/near/425856054)

RELEASES.md

@@ -57,6 +57,10 @@ 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.
+
 Breaking changes:
 
 * Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:

src/Lean/PrettyPrinter/Delaborator/Attributes.lean

@@ -17,10 +17,19 @@ namespace Lean
 builtin_initialize ppUsingAnonymousConstructorAttr : TagAttribute ←
   registerTagAttribute `pp_using_anonymous_constructor "mark structure to be pretty printed using `⟨a,b,c⟩` notation"
 
+builtin_initialize ppNoDotAttr : TagAttribute ←
+  registerTagAttribute `pp_nodot "mark declaration to never be pretty printed using field notation"
+
 /--
-Returns whether or not the given declaration has been given the `@[pp_using_anonymous_constructor]` attribute.
+Returns whether or not the given declaration has the `@[pp_using_anonymous_constructor]` attribute.
 -/
 def hasPPUsingAnonymousConstructorAttribute (env : Environment) (declName : Name) : Bool :=
   ppUsingAnonymousConstructorAttr.hasTag env declName
 
+/--
+Returns whether or not the given declaration has the `@[pp_nodot]` attribute.
+-/
+def hasPPNoDotAttribute (env : Environment) (declName : Name) : Bool :=
+  ppNoDotAttr.hasTag env declName
+
 end Lean

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Meta.Basic
+import Lean.PrettyPrinter.Delaborator.Attributes
+import Lean.PrettyPrinter.Delaborator.Options
+import Lean.Structure
+
+/-!
+# Functions for analyzing projections for pretty printing
+-/
+
+namespace Lean.PrettyPrinter.Delaborator
+open Meta
+
+/--
+If this 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
+  let field := Name.mkSimple field
+  let env ← getEnv
+  let some info := env.getProjectionFnInfo? c | failure
+  -- Don't use projection notation for instances of classes.
+  guard <| !info.fromClass
+  let some (.ctorInfo cVal) := env.find? info.ctorName | failure
+  let isParentProj := (isSubobjectField? env cVal.induct field).isSome
+  return (field, info.numParams, isParentProj)
+
+/--
+If this function application could delaborate using generalized field notation,
+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
+  let field := Name.mkSimple field
+  let baseName := name.getPrefix
+  guard <| !baseName.isAnonymous
+  Meta.forallBoundedTelescope (← instantiateMVars <| ← inferType f) 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
+      else
+        -- If not explicit, then make sure that this parameter can't be used for field notation.
+        guard <| ! (← fvarId.getType).cleanupAnnotations.isAppOf baseName
+    failure
+
+/--
+If `f` is a function that can be used for field notation,
+returns the field name to use and the argument index for the object of the field notation.
+-/
+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
+  -- If there is `pp_nodot` on this function, then don't use field notation for it.
+  if hasPPNoDotAttribute env name then
+    return none
+  -- Handle structure projections
+  try
+    let (field, numParams, _) ← projInfo f
+    return (field, numParams)
+  catch _ => pure ()
+  -- Handle generalized field notation
+  if useGeneralizedFieldNotation then
+    try
+      return ← generalizedFieldInfo f args
+    catch _ => pure ()
+  -- It's not handled by any of the above.
+  return none
+
+/--
+Returns `true` if `e` is an application that is a projection to a parent structure.
+If `explicit` is `true`, then further requires that the structure have no parameters.
+-/
+def isParentProj (explicit : Bool) (e : Expr) : MetaM Bool := do
+  unless e.isApp do return false
+  try
+    let (_, numParams, isParentProj) ← projInfo e.getAppFn
+    return isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1
+  catch _ =>
+    return false

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -90,10 +90,15 @@ register_builtin_option pp.structureInstances : Bool := {
   descr    := "(pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation, \
               or using '⟨fieldValue, ... ⟩' if structure is tagged with the '@[pp_using_anonymous_constructor]' attribute"
 }
-register_builtin_option pp.structureProjections : Bool := {
+register_builtin_option pp.fieldNotation : Bool := {
   defValue := true
   group    := "pp"
-  descr    := "(pretty printer) display structure projections using field notation"
+  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
+  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"
 }
 register_builtin_option pp.explicit : Bool := {
   defValue := false
@@ -215,7 +220,8 @@ def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
 def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false
 def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o)
-def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o)
+def getPPFieldNotation (o : Options) : Bool := o.get pp.fieldNotation.name (!getPPAll o)
+def getPPFieldNotationGeneralized (o : Options) : Bool := o.get pp.fieldNotation.generalized.name pp.fieldNotation.generalized.defValue
 def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o)
 def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o)
 def getPPTagAppFns (o : Options) : Bool := o.get pp.tagAppFns.name (getPPAll o)

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -11,6 +11,7 @@ import Lean.Util.FindMVar
 import Lean.Util.FindLevelMVar
 import Lean.Util.CollectLevelParams
 import Lean.Util.ReplaceLevel
+import Lean.PrettyPrinter.Delaborator.FieldNotation
 import Lean.PrettyPrinter.Delaborator.Options
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.Elab.Config
@@ -123,6 +124,7 @@ def getPPAnalysisNamedArg        (o : Options) : Bool := o.get `pp.analysis.name
 def getPPAnalysisLetVarType      (o : Options) : Bool := o.get `pp.analysis.letVarType false
 def getPPAnalysisNeedsType       (o : Options) : Bool := o.get `pp.analysis.needsType false
 def getPPAnalysisBlockImplicit   (o : Options) : Bool := o.get `pp.analysis.blockImplicit false
+def getPPAnalysisNoDot           (o : Options) : Bool := o.get `pp.analysis.noDot false
 
 namespace PrettyPrinter.Delaborator
 
@@ -401,6 +403,17 @@ mutual
       -- Unify with the expected type
       if (← read).knowsType then tryUnify (← inferType (mkAppN f args)) resultType
 
+      -- Prevent using dot notation if the expected of the argument can't be determined.
+      -- TODO: is canBottomUp sufficient for this?
+      if getPPFieldNotation (← getOptions) then
+        if let some (_, idx) ← fieldNotationCandidate? f args (getPPFieldNotationGeneralized (← getOptions)) then
+          if idx < args.size then
+            withKnowing false false do
+              if !(← canBottomUp args[idx]!) then
+                annotateBool `pp.analysis.noDot
+          else
+            annotateBool `pp.analysis.noDot
+
       let forceRegularApp : Bool :=
         (getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr))
         || (getPPAnalyzeTrustSubtypeMk (← getOptions) && (← getExpr).isAppOfArity ``Subtype.mk 4)

tests/lean/439.lean.expected.out

@@ -1,4 +1,4 @@
-fn.imp : {p : P} → Bar.fn p
+@Fn.imp ((p : P) → Bar.fn p) ({p : P} → Bar.fn p) fn : {p : P} → Bar.fn p
 439.lean:18:7-18:12: error: function expected at
   fn.imp
 term has type

tests/lean/run/PPTopDownAnalyze.lean

@@ -330,7 +330,7 @@ set_option pp.analyze.explicitHoles false in
 
 set_option pp.analyze.trustSubtypeMk true in
 #testDelab fun (n : Nat) (val : List Nat) (property : List.length val = n) => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n
-  expecting fun n val property => List.length (⟨val, property⟩ : { x : List Nat // List.length x = n }).val = n
+  expecting fun n val property => List.length (Subtype.val (p := fun x => List.length x = n) (⟨val, property⟩ : { x : List Nat // List.length x = n })) = n
 
 #testDelabN Nat.brecOn
 #testDelabN Nat.below