From 5bc42bf5ca94af4ee7746a44084f25cf087811e6 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 26 Aug 2025 20:30:52 -0700 Subject: [PATCH] fix: pretty print dot notation for private definitions on public types (#10122) This PR adds support for pretty printing using generalized field notation (dot notation) for private definitions on public types. It also modifies dot notation elaboration to resolve names after removing the private prefix, which enables using dot notation for private definitions on private imported types. It won't pretty print with dot notation for definitions on inaccessible private types from other modules. Closes #7297 --- src/Lean/Elab/App.lean | 2 +- .../Delaborator/FieldNotation.lean | 23 +++++++++---- tests/lean/private.lean.expected.out | 2 +- tests/lean/run/cleanupTypeAnnotations.lean | 2 +- tests/lean/run/delabProjectionApp.lean | 33 +++++++++++++++++++ tests/lean/run/grind_9572.lean | 6 ++-- 6 files changed, 56 insertions(+), 12 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index bd6c8afe02..050581e1b6 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1270,7 +1270,7 @@ If it resolves to `name`, returns `(S', name)`. private partial def findMethod? (structName fieldName : Name) : MetaM (Option (Name × Name)) := do let env ← getEnv let find? structName' : MetaM (Option (Name × Name)) := do - let fullName := structName' ++ fieldName + let fullName := privateToUserName structName' ++ fieldName -- We do not want to make use of the current namespace for resolution. let candidates := ResolveName.resolveGlobalName (← getEnv) Name.anonymous (← getOpenDecls) fullName |>.filter (fun (_, fieldList) => fieldList.isEmpty) diff --git a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean index 2affb6634d..dee0ec76e0 100644 --- a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean +++ b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean @@ -44,16 +44,25 @@ private def projInfo (c : Name) : MetaM (Option (Name × Nat × Bool × Bool × else return none +/-- +Checks that `e` is an application of a constant that equals `baseName`, taking into consideration private name mangling. +-/ +private def isAppOfBaseName (env : Environment) (e : Expr) (baseName : Name) : Bool := + if let some c := e.cleanupAnnotations.getAppFn.constName? then + privateToUserName c == baseName && !isInaccessiblePrivateName env c + else + false + /-- Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types. -/ private partial def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do withReducibleAndInstances do - if type.cleanupAnnotations.isAppOf baseName then + if isAppOfBaseName (← getEnv) type baseName then return true else let type ← whnfCore type - if type.isAppOf baseName then + if isAppOfBaseName (← getEnv) type baseName then return true else match ← unfoldDefinition? type with @@ -66,10 +75,10 @@ returns the field name and the index for the argument to be used as the object o Otherwise it fails. -/ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × Nat) := do - let .str _ field := c | failure - let field := Name.mkSimple field - let baseName := c.getPrefix + let .str baseName field := c | failure + let baseName := privateToUserName baseName guard <| !baseName.isAnonymous + let field := Name.mkSimple field -- Disallow `Function` since it is used for pi types. guard <| baseName != `Function let info ← getConstInfo c @@ -87,7 +96,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × -- 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 + guard <| isAppOfBaseName (← getEnv) (← instantiateMVars <| ← inferType args[i]!) baseName return (field, i) else -- We only use the first explicit argument for field notation. @@ -107,6 +116,8 @@ 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 c .. := f.consumeMData | return none + if isInaccessiblePrivateName (← getEnv) c then + 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 c then diff --git a/tests/lean/private.lean.expected.out b/tests/lean/private.lean.expected.out index adb893faeb..a12cfe4ae2 100644 --- a/tests/lean/private.lean.expected.out +++ b/tests/lean/private.lean.expected.out @@ -8,6 +8,6 @@ Boo.Bla.boo == "world" : Bool Boo.boo == 100 : Bool Boo.Bla.boo == "world" : Bool Boo.boo == 100 : Bool -Nat.mul10 x : Nat +x.mul10 : Nat private.lean:65:12-65:13: error: a non-private declaration `y` has already been declared private.lean:68:4-68:5: error: a private declaration `z` has already been declared diff --git a/tests/lean/run/cleanupTypeAnnotations.lean b/tests/lean/run/cleanupTypeAnnotations.lean index 1a391fc6d4..a98674f60e 100644 --- a/tests/lean/run/cleanupTypeAnnotations.lean +++ b/tests/lean/run/cleanupTypeAnnotations.lean @@ -49,7 +49,7 @@ instance i1 (b := 0) : Decidable (a.toNat = b) := have : True := by trace_state; trivial inferInstance -/-- info: i1 (a : Bool := true) (b : Nat := 0) : Decidable (Bool.toNat a = b) -/ +/-- info: i1 (a : Bool := true) (b : Nat := 0) : Decidable (a.toNat = b) -/ #guard_msgs in #check i1 /-! diff --git a/tests/lean/run/delabProjectionApp.lean b/tests/lean/run/delabProjectionApp.lean index 452e9a53c1..624e412a20 100644 --- a/tests/lean/run/delabProjectionApp.lean +++ b/tests/lean/run/delabProjectionApp.lean @@ -184,3 +184,36 @@ set_option pp.notation false in set_option pp.notation false in set_option pp.fieldNotation.generalized false in /-- info: ∀ {α : Type} (s t : MySet α), MySet.MySubset s t : Prop -/ #guard_msgs in #check ∀ {α : Type} (s t : MySet α), s ⊆⊆ t + +/-! +Private definition on public type. +-/ +private def Char.MyIsA (c : Char) : Prop := c = 'A' + +/-- info: ∀ (c : Char), c.MyIsA : Prop -/ +#guard_msgs in #check ∀ (c : Char), c.MyIsA + +/-! +Public definition on public type. +-/ +def Char.MyIsA' (c : Char) : Prop := c = 'A' + +/-- info: ∀ (c : Char), c.MyIsA' : Prop -/ +#guard_msgs in #check ∀ (c : Char), c.MyIsA' + +/-! +Private definition on private type. +-/ +private structure Char' +private def Char'.MyIsA (_ : Char') : Prop := true + +/-- info: ∀ (c : Char'), c.MyIsA : Prop -/ +#guard_msgs in #check ∀ (c : Char'), c.MyIsA + +/-! +Public definition on private type. +-/ +def Char'.MyIsA' (_ : Char') : Prop := true + +/-- info: ∀ (c : Char'), c.MyIsA' : Prop -/ +#guard_msgs in #check ∀ (c : Char'), c.MyIsA' diff --git a/tests/lean/run/grind_9572.lean b/tests/lean/run/grind_9572.lean index f1bc1cff43..0bfc0c5aac 100644 --- a/tests/lean/run/grind_9572.lean +++ b/tests/lean/run/grind_9572.lean @@ -12,7 +12,7 @@ l : List Nat h : ¬List.Pairwise (fun x y => - List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []) + (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else [])) l ⊢ False @@ -20,13 +20,13 @@ h : [facts] Asserted facts [prop] ¬List.Pairwise (fun x y => - List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []) + (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else [])) l [eqc] False propositions [prop] List.Pairwise (fun x y => - List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []) + (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else [])) l -/