From 0b92f625ae1e5352fbfe544fbfdd35055aaedd6c Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 7 Aug 2022 06:36:57 -0400 Subject: [PATCH] feat: MissingDocs doesn't lint on struct redecl --- src/Lean/Elab/InfoTree/Main.lean | 9 ++++-- src/Lean/Elab/InfoTree/Types.lean | 13 +++++++++ src/Lean/Elab/Structure.lean | 1 + src/Lean/Linter/MissingDocs.lean | 20 +++++++++++-- src/Lean/Server/InfoUtils.lean | 3 +- tests/lean/linterMissingDocs.lean | 10 ++++++- .../lean/linterMissingDocs.lean.expected.out | 28 +++++++++++-------- 7 files changed, 67 insertions(+), 17 deletions(-) diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index fa6c08ddd9..194d776643 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -152,6 +152,9 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format := def FVarAliasInfo.format (info : FVarAliasInfo) : Format := f!"FVarAlias {info.id.name} -> {info.baseId.name}" +def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format := + f!"FieldRedecl @ {formatStxRange ctx info.stx}" + def Info.format (ctx : ContextInfo) : Info → IO Format | ofTacticInfo i => i.format ctx | ofTermInfo i => i.format ctx @@ -159,9 +162,10 @@ def Info.format (ctx : ContextInfo) : Info → IO Format | ofMacroExpansionInfo i => i.format ctx | ofFieldInfo i => i.format ctx | ofCompletionInfo i => i.format ctx - | ofUserWidgetInfo i => pure <| UserWidgetInfo.format i + | ofUserWidgetInfo i => pure <| i.format | ofCustomInfo i => pure <| Std.ToFormat.format i - | ofFVarAliasInfo i => pure <| FVarAliasInfo.format i + | ofFVarAliasInfo i => pure <| i.format + | ofFieldRedeclInfo i => pure <| i.format ctx def Info.toElabInfo? : Info → Option ElabInfo | ofTacticInfo i => some i.toElabInfo @@ -173,6 +177,7 @@ def Info.toElabInfo? : Info → Option ElabInfo | ofUserWidgetInfo _ => none | ofCustomInfo _ => none | ofFVarAliasInfo _ => none + | ofFieldRedeclInfo _ => none /-- Helper function for propagating the tactic metavariable context to its children nodes. diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index 8994f194cf..d6b8e3e0cf 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -102,6 +102,18 @@ structure FVarAliasInfo where id : FVarId baseId : FVarId +/-- +Contains the syntax of an identifier which is part of a field redeclaration, like: +``` +structure Foo := x : Nat +structure Bar extends Foo := + x := 0 +--^ here +``` +-/ +structure FieldRedeclInfo where + stx : Syntax + /-- Header information for a node in `InfoTree`. -/ inductive Info where | ofTacticInfo (i : TacticInfo) @@ -113,6 +125,7 @@ inductive Info where | ofUserWidgetInfo (i : UserWidgetInfo) | ofCustomInfo (i : CustomInfo) | ofFVarAliasInfo (i : FVarAliasInfo) + | ofFieldRedeclInfo (i : FieldRedeclInfo) deriving Inhabited /-- The InfoTree is a structure that is generated during elaboration and used diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index c596526903..b0a91900fe 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -557,6 +557,7 @@ where valStx ← `(fun $(view.binders.getArgs)* => $valStx:term) let fvarType ← inferType info.fvar let value ← Term.elabTermEnsuringType valStx fvarType + pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref } let infos := updateFieldInfoVal infos info.name value go (i+1) defaultValsOverridden infos match info.kind with diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 19baec793a..4d4c5d8a22 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -107,6 +107,9 @@ def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit := def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit := lint stx s!"{msg} {parent.getId}.{stx.getId}" +def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit := + lint stx s!"{msg} {parent.getId}.{stx.getId}" + def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do if k == ``«abbrev» then lintNamed id "public abbrev" else if k == ``«def» then lintNamed id "public def" @@ -136,14 +139,27 @@ def checkDecl : SimpleHandler := fun stx => do lintField rest[1][0] stx[1] "computed field" else if rest.getKind == ``«structure» then unless rest[5].isNone || rest[5][2].isNone do + let redecls : Std.HashSet String.Pos := + (← get).infoState.trees.foldl (init := {}) fun s tree => + tree.foldInfo (init := s) fun _ info s => + if let .ofFieldRedeclInfo info := info then + if let some range := info.stx.getRange? then + s.insert range.start + else s + else s + let parent := rest[1][0] + let lint1 stx := do + if let some range := stx.getRange? then + if redecls.contains range.start then return + lintField parent stx "public field" for stx in rest[5][2][0].getArgs do let head := stx[0] if head[2][0].getKind != ``«private» && head[0].isNone then if stx.getKind == ``structSimpleBinder then - lintField rest[1][0] stx[1] "public field" + lint1 stx[1] else for stx in stx[2].getArgs do - lintField rest[1][0] stx "public field" + lint1 stx @[builtinMissingDocsHandler «initialize»] def checkInit : SimpleHandler := fun stx => do diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 4f43a7a2fc..dce7d878b3 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -22,7 +22,7 @@ def Lean.Syntax.getRange? (stx : Syntax) (originalOnly := false) : Option String namespace Lean.Elab /-- Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up. -/ -partial def InfoTree.visitM [Monad m] [Inhabited α] +partial def InfoTree.visitM [Monad m] (preNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) (postNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → List (Option α) → m α) : InfoTree → m (Option α) := @@ -95,6 +95,7 @@ def Info.stx : Info → Syntax | ofCustomInfo i => i.stx | ofUserWidgetInfo i => i.stx | ofFVarAliasInfo _ => .missing + | ofFieldRedeclInfo i => i.stx def Info.lctx : Info → LocalContext | Info.ofTermInfo i => i.lctx diff --git a/tests/lean/linterMissingDocs.lean b/tests/lean/linterMissingDocs.lean index a60b295ae5..9eea46af76 100644 --- a/tests/lean/linterMissingDocs.lean +++ b/tests/lean/linterMissingDocs.lean @@ -54,10 +54,18 @@ structure Foo where [mk6 mk7 : Nat] class Bar (α : Prop) := mk :: + (foo bar := 1) + +class Bar2 (α : Prop) where + bar := 2 + +class Bar3 (α : Prop) extends Bar α where + bar := 3 + (foo baz := 3) theorem aThm : True := trivial example : True := trivial -instance : Bar True := ⟨⟩ +instance : Bar True := {} initialize init : Unit ← return initialize return diff --git a/tests/lean/linterMissingDocs.lean.expected.out b/tests/lean/linterMissingDocs.lean.expected.out index 5eb3291501..2c5f96aa7b 100644 --- a/tests/lean/linterMissingDocs.lean.expected.out +++ b/tests/lean/linterMissingDocs.lean.expected.out @@ -14,14 +14,20 @@ linterMissingDocs.lean:53:7-53:10: warning: missing doc string for public field linterMissingDocs.lean:54:3-54:6: warning: missing doc string for public field Foo.mk6 [linter.missingDocs] linterMissingDocs.lean:54:7-54:10: warning: missing doc string for public field Foo.mk7 [linter.missingDocs] linterMissingDocs.lean:56:6-56:9: warning: missing doc string for public structure Bar [linter.missingDocs] -linterMissingDocs.lean:62:11-62:15: warning: missing doc string for initializer init [linter.missingDocs] -linterMissingDocs.lean:65:19-65:24: warning: missing doc string for syntax category myCat [linter.missingDocs] -linterMissingDocs.lean:67:0-67:6: warning: missing doc string for syntax [linter.missingDocs] -linterMissingDocs.lean:68:16-68:24: warning: missing doc string for syntax namedSyn [linter.missingDocs] -linterMissingDocs.lean:75:0-75:4: warning: missing doc string for elab [linter.missingDocs] -linterMissingDocs.lean:76:0-76:5: warning: missing doc string for macro [linter.missingDocs] -linterMissingDocs.lean:78:13-78:22: warning: missing doc string for class abbrev [anonymous] [linter.missingDocs] -linterMissingDocs.lean:80:16-80:24: warning: missing doc string for option myOption [linter.missingDocs] -linterMissingDocs.lean:82:14-82:19: warning: missing doc string for elab myCmd [linter.missingDocs] -linterMissingDocs.lean:88:4-88:15: warning: missing doc string for public def handleMyCmd [linter.missingDocs] -linterMissingDocs.lean:95:11-95:12: warning: missing doc string for my_command z [linter.missingDocs] +linterMissingDocs.lean:57:3-57:6: warning: missing doc string for public field Bar.foo [linter.missingDocs] +linterMissingDocs.lean:57:7-57:10: warning: missing doc string for public field Bar.bar [linter.missingDocs] +linterMissingDocs.lean:59:6-59:10: warning: missing doc string for public structure Bar2 [linter.missingDocs] +linterMissingDocs.lean:60:2-60:5: warning: missing doc string for public field Bar2.bar [linter.missingDocs] +linterMissingDocs.lean:62:6-62:10: warning: missing doc string for public structure Bar3 [linter.missingDocs] +linterMissingDocs.lean:64:7-64:10: warning: missing doc string for public field Bar3.baz [linter.missingDocs] +linterMissingDocs.lean:70:11-70:15: warning: missing doc string for initializer init [linter.missingDocs] +linterMissingDocs.lean:73:19-73:24: warning: missing doc string for syntax category myCat [linter.missingDocs] +linterMissingDocs.lean:75:0-75:6: warning: missing doc string for syntax [linter.missingDocs] +linterMissingDocs.lean:76:16-76:24: warning: missing doc string for syntax namedSyn [linter.missingDocs] +linterMissingDocs.lean:83:0-83:4: warning: missing doc string for elab [linter.missingDocs] +linterMissingDocs.lean:84:0-84:5: warning: missing doc string for macro [linter.missingDocs] +linterMissingDocs.lean:86:13-86:22: warning: missing doc string for class abbrev [anonymous] [linter.missingDocs] +linterMissingDocs.lean:88:16-88:24: warning: missing doc string for option myOption [linter.missingDocs] +linterMissingDocs.lean:90:14-90:19: warning: missing doc string for elab myCmd [linter.missingDocs] +linterMissingDocs.lean:96:4-96:15: warning: missing doc string for public def handleMyCmd [linter.missingDocs] +linterMissingDocs.lean:103:11-103:12: warning: missing doc string for my_command z [linter.missingDocs]