From 11ae8bae42509eaca43db69ed95fbdd9570d5039 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 18 Oct 2024 17:38:32 +0200 Subject: [PATCH] fix: include references in attributes in call hierarchy (#5650) By ensuring all `declModifiers` are included in `addDeclarationRanges`, `implementedBy` references etc are included in the call hierarchy --- src/Lean/Elab/BuiltinCommand.lean | 13 +++--- src/Lean/Elab/BuiltinEvalCommand.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 19 ++++---- src/Lean/Elab/Declaration.lean | 19 ++++---- src/Lean/Elab/DeclarationRange.lean | 44 +++++++++++-------- src/Lean/Elab/MutualDef.lean | 5 ++- src/Lean/Elab/PreDefinition/Basic.lean | 2 +- .../Structural/SmartUnfolding.lean | 2 +- src/Lean/Elab/Structure.lean | 4 +- src/Lean/Elab/Tactic/Ext.lean | 8 +--- src/Lean/Elab/Term.lean | 4 +- tests/lean/docStr.lean.expected.out | 12 ++--- tests/lean/interactive/goTo.lean.expected.out | 3 +- 13 files changed, 72 insertions(+), 65 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index bbc2f43754..64ab21f3b9 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -16,12 +16,13 @@ import Lean.Elab.SetOption namespace Lean.Elab.Command @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do - match stx[1] with - | Syntax.atom _ val => - let doc := val.extract 0 (val.endPos - ⟨2⟩) - let range ← Elab.getDeclarationRange stx - modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩ - | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}" + match stx[1] with + | Syntax.atom _ val => + let doc := val.extract 0 (val.endPos - ⟨2⟩) + let some range ← Elab.getDeclarationRange? stx + | return -- must be from partial syntax, ignore + modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩ + | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}" private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do modify fun s => { s with diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean index 3a11ed0fd8..659908dda2 100644 --- a/src/Lean/Elab/BuiltinEvalCommand.lean +++ b/src/Lean/Elab/BuiltinEvalCommand.lean @@ -84,7 +84,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages -- such as "failed to infer definition type" can surface. - let defView := mkDefViewOfDef { isUnsafe := true } + let defView := mkDefViewOfDef { isUnsafe := true, stx := ⟨.missing⟩ } (← `(Parser.Command.definition| def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value))) Term.elabMutualDef #[] { header := "" } #[defView] diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index ff46120587..55db381c1a 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -57,6 +57,7 @@ inductive RecKind where /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/ structure Modifiers where + stx : TSyntax ``Parser.Command.declModifiers docString? : Option String := none visibility : Visibility := Visibility.regular isNoncomputable : Bool := false @@ -121,16 +122,16 @@ section Methods variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/ -def elabModifiers (stx : Syntax) : m Modifiers := do - let docCommentStx := stx[0] - let attrsStx := stx[1] - let visibilityStx := stx[2] - let noncompStx := stx[3] - let unsafeStx := stx[4] +def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do + let docCommentStx := stx.raw[0] + let attrsStx := stx.raw[1] + let visibilityStx := stx.raw[2] + let noncompStx := stx.raw[3] + let unsafeStx := stx.raw[4] let recKind := - if stx[5].isNone then + if stx.raw[5].isNone then RecKind.default - else if stx[5][0].getKind == ``Parser.Command.partial then + else if stx.raw[5][0].getKind == ``Parser.Command.partial then RecKind.partial else RecKind.nonrec @@ -148,7 +149,7 @@ def elabModifiers (stx : Syntax) : m Modifiers := do | none => pure #[] | some attrs => elabDeclAttrs attrs return { - docString?, visibility, recKind, attrs, + stx, docString?, visibility, recKind, attrs, isUnsafe := !unsafeStx.isNone isNoncomputable := !noncompStx.isNone } diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 84c7f59497..21c01998a8 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -104,7 +104,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do let (binders, typeStx) := expandDeclSig stx[2] let scopeLevelNames ← getLevelNames let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers - addDeclarationRanges declName stx + addDeclarationRanges declName modifiers.stx stx runTermElabM fun vars => Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration @@ -144,10 +144,10 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm let (binders, type?) := expandOptDeclSig decl[2] let declId := decl[1] let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers - addDeclarationRanges declName decl + addDeclarationRanges declName modifiers.stx decl let ctors ← decl[4].getArgs.mapM fun ctor => withRef ctor do -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig - let mut ctorModifiers ← elabModifiers ctor[2] + let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩ if let some leadingDocComment := ctor[0].getOptional? then if ctorModifiers.docString?.isSome then logErrorAt leadingDocComment "duplicate doc string" @@ -214,17 +214,18 @@ def elabDeclaration : CommandElab := fun stx => do -- only case implementing incrementality currently elabMutualDef #[stx] else withoutCommandIncrementality true do + let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩ if declKind == ``Lean.Parser.Command.«axiom» then - let modifiers ← elabModifiers stx[0] + let modifiers ← elabModifiers modifiers elabAxiom modifiers decl else if declKind == ``Lean.Parser.Command.«inductive» then - let modifiers ← elabModifiers stx[0] + let modifiers ← elabModifiers modifiers elabInductive modifiers decl else if declKind == ``Lean.Parser.Command.classInductive then - let modifiers ← elabModifiers stx[0] + let modifiers ← elabModifiers modifiers elabClassInductive modifiers decl else if declKind == ``Lean.Parser.Command.«structure» then - let modifiers ← elabModifiers stx[0] + let modifiers ← elabModifiers modifiers elabStructure modifiers decl else throwError "unexpected declaration" @@ -238,7 +239,7 @@ private def isMutualInductive (stx : Syntax) : Bool := private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do let views ← elems.mapM fun stx => do - let modifiers ← elabModifiers stx[0] + let modifiers ← elabModifiers ⟨stx[0]⟩ inductiveSyntaxToView modifiers stx[1] elabInductiveViews views @@ -399,7 +400,7 @@ def elabMutual : CommandElab := fun stx => do -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as -- otherwise the info context created by `with_decl_name` will be incomplete and break the -- call hierarchy - addDeclarationRanges fullId defStx + addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1] elabCommand (← `( $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq $defStx:command)) diff --git a/src/Lean/Elab/DeclarationRange.lean b/src/Lean/Elab/DeclarationRange.lean index 6d6b39e5ee..610fad80a3 100644 --- a/src/Lean/Elab/DeclarationRange.lean +++ b/src/Lean/Elab/DeclarationRange.lean @@ -11,12 +11,14 @@ import Lean.Data.Lsp.Utf16 namespace Lean.Elab -def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do +def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) := do + let some range := stx.getRange? + | return none let fileMap ← getFileMap - let pos := stx.getPos?.getD 0 - let endPos := stx.getTailPos?.getD pos |> fileMap.toPosition - let pos := pos |> fileMap.toPosition - return { + --let range := fileMap.utf8RangeToLspRange + let pos := fileMap.toPosition range.start + let endPos := fileMap.toPosition range.stop + return some { pos := pos charUtf16 := fileMap.leanPosToLspPos pos |>.character endPos := endPos @@ -49,23 +51,27 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax := /-- - Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`. - This method is for the builtin declarations only. - User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/ -def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do - if stx.getKind == ``Parser.Command.«example» then +Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and +`cmdStx` the remaining part of the syntax tree for `declName`. + +This method is for the builtin declarations only. User-defined commands should use +`Lean.addDeclarationRanges` to store this information for their commands. +-/ +def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) + (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do + if declStx.getKind == ``Parser.Command.«example» then return () - else - Lean.addDeclarationRanges declName { - range := (← getDeclarationRange stx) - selectionRange := (← getDeclarationRange (getDeclarationSelectionRef stx)) - } + let stx := mkNullNode #[modsStx, declStx] + -- may fail on partial syntax, ignore in that case + let some range ← getDeclarationRange? stx | return + let some selectionRange ← getDeclarationRange? (getDeclarationSelectionRef declStx) | return + Lean.addDeclarationRanges declName { range, selectionRange } /-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/ def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do - Lean.addDeclarationRanges declName { - range := (← getDeclarationRange stx) - selectionRange := (← getDeclarationRange header) - } + -- may fail on partial syntax, ignore in that case + let some range ← getDeclarationRange? stx | return + let some selectionRange ← getDeclarationRange? header | return + Lean.addDeclarationRanges declName { range, selectionRange } end Lean.Elab diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index d37aa73817..a4646595d5 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -887,6 +887,7 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind := else DefKind.«def» def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := { + stx := ⟨mkNullNode #[]⟩ -- ignore when computing declaration range isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable recKind := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default isUnsafe := mainHeaders.any fun h => h.modifiers.isUnsafe @@ -997,7 +998,7 @@ where for view in views, header in headers do -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting -- that depends only on a part of the ref - addDeclarationRanges header.declName view.ref + addDeclarationRanges header.declName view.modifiers.stx view.ref processDeriving (headers : Array DefViewElabHeader) := do @@ -1021,7 +1022,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do let mut reusedAllHeaders := true for h : i in [0:ds.size], headerPromise in headerPromises do let d := ds[i] - let modifiers ← elabModifiers d[0] + let modifiers ← elabModifiers ⟨d[0]⟩ if ds.size > 1 && modifiers.isNonrec then throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block" let mut view ← mkDefView modifiers d[1] diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index f654645f60..e0a5eac99f 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -221,7 +221,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit := else none | _ => none - modifiers := {} } + modifiers := default } private def containsRecFn (recFnNames : Array Name) (e : Expr) : Bool := (e.find? fun e => e.isConst && recFnNames.contains e.constName!).isSome diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean index 4a0de80d1e..ea3ef8af45 100644 --- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean @@ -15,7 +15,7 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) : return { preDef with declName := mkSmartUnfoldingNameFor preDef.declName value := (← visit preDef.value) - modifiers := {} + modifiers := default } where /-- diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index a7439d9efb..5f2d4c9034 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -95,7 +95,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc let declName := structDeclName ++ defaultCtorName let ref := structStx[1].mkSynthetic addAuxDeclarationRanges declName ref ref - pure { ref, modifiers := {}, name := defaultCtorName, declName } + pure { ref, modifiers := default, name := defaultCtorName, declName } if structStx[5].isNone then useDefault else @@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := let scopeLevelNames ← Term.getLevelNames let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do - addDeclarationRanges declName stx + addDeclarationRanges declName modifiers.stx stx Term.withDeclName declName do let ctor ← expandCtor stx modifiers declName let fields ← expandFields stx modifiers declName diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index 4bc60e6036..dbfe47f466 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/src/Lean/Elab/Tactic/Ext.lean @@ -123,9 +123,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl levelParams := info.levelParams } modifyEnv fun env => addProtected env extName - Lean.addDeclarationRanges extName { - range := ← getDeclarationRange (← getRef) - selectionRange := ← getDeclarationRange (← getRef) } + addAuxDeclarationRanges extName (← getRef) (← getRef) catch e => throwError m!"\ Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}" @@ -163,9 +161,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do -- Only declarations in a namespace can be protected: unless extIffName.isAtomic do modifyEnv fun env => addProtected env extIffName - Lean.addDeclarationRanges extIffName { - range := ← getDeclarationRange (← getRef) - selectionRange := ← getDeclarationRange (← getRef) } + addAuxDeclarationRanges extName (← getRef) (← getRef) catch e => throwError m!"\ Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\ diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 6665bae27d..d2943cadaa 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -914,7 +914,9 @@ private def applyAttributesCore Remark: if the declaration has syntax errors, `declName` may be `.anonymous` see issue #4309 In this case, we skip attribute application. -/ - unless declName == .anonymous do + if declName == .anonymous then + return + withDeclName declName do for attr in attrs do withRef attr.stx do withLogging do let env ← getEnv diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index d5f07d2ed4..6b5d000ce6 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -19,7 +19,7 @@ doc string for 'g' is not available "Auxiliary declaration used to implement named patterns like `x@h:p`. " "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n" Foo := - { range := { pos := { line := 4, column := 0 }, + { range := { pos := { line := 3, column := 0 }, charUtf16 := 0, endPos := { line := 6, column := 58 }, endCharUtf16 := 58 }, @@ -46,7 +46,7 @@ Foo.val := endPos := { line := 6, column := 47 }, endCharUtf16 := 47 } } myAxiom := - { range := { pos := { line := 9, column := 0 }, + { range := { pos := { line := 8, column := 0 }, charUtf16 := 0, endPos := { line := 9, column := 19 }, endCharUtf16 := 19 }, @@ -91,7 +91,7 @@ Boo.y := endPos := { line := 15, column := 5 }, endCharUtf16 := 5 } } Tree := - { range := { pos := { line := 18, column := 0 }, + { range := { pos := { line := 17, column := 0 }, charUtf16 := 0, endPos := { line := 20, column := 56 }, endCharUtf16 := 56 }, @@ -100,7 +100,7 @@ Tree := endPos := { line := 18, column := 14 }, endCharUtf16 := 14 } } Tree.rec := - { range := { pos := { line := 18, column := 0 }, + { range := { pos := { line := 17, column := 0 }, charUtf16 := 0, endPos := { line := 20, column := 56 }, endCharUtf16 := 56 }, @@ -109,7 +109,7 @@ Tree.rec := endPos := { line := 18, column := 14 }, endCharUtf16 := 14 } } Tree.casesOn := - { range := { pos := { line := 18, column := 0 }, + { range := { pos := { line := 17, column := 0 }, charUtf16 := 0, endPos := { line := 20, column := 56 }, endCharUtf16 := 56 }, @@ -136,7 +136,7 @@ Tree.leaf := endPos := { line := 20, column := 43 }, endCharUtf16 := 43 } } Bla.test := - { range := { pos := { line := 25, column := 0 }, + { range := { pos := { line := 24, column := 0 }, charUtf16 := 0, endPos := { line := 31, column := 16 }, endCharUtf16 := 16 }, diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out index 316024c5f5..23cd65299e 100644 --- a/tests/lean/interactive/goTo.lean.expected.out +++ b/tests/lean/interactive/goTo.lean.expected.out @@ -92,8 +92,7 @@ {"start": {"line": 38, "character": 26}, "end": {"line": 38, "character": 38}}, "targetRange": - {"start": {"line": 38, "character": 22}, - "end": {"line": 40, "character": 78}}, + {"start": {"line": 38, "character": 0}, "end": {"line": 40, "character": 78}}, "originSelectionRange": {"start": {"line": 43, "character": 7}, "end": {"line": 43, "character": 11}}}]