fix: getParentDeclName? inside where inside public def (#12119)
This PR fixes the call hierarchy for `where` declarations under the module system --------- Co-authored-by: mhuisi <mhuisi@protonmail.com>
This commit is contained in:
Sebastian Ullrich
GitHub
parent
dae0d6fa05
commit
9f9531fa13
5 changed files with 112 additions and 29 deletions
|
|
@ -48,7 +48,10 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
|
|||
throwErrorAt declId "'let rec' expressions must be named"
|
||||
let shortDeclName := declId.getId
|
||||
let parentName? ← getDeclName?
|
||||
let declName := parentName?.getD Name.anonymous ++ shortDeclName
|
||||
let mut declName := parentName?.getD Name.anonymous ++ shortDeclName
|
||||
let env ← getEnv
|
||||
if env.header.isModule && !env.isExporting then
|
||||
declName := mkPrivateName env declName
|
||||
if decls.any fun decl => decl.declName == declName then
|
||||
withRef declId do
|
||||
throwError "`{.ofConstName declName}` has already been declared"
|
||||
|
|
@ -116,15 +119,12 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
|
|||
let toLift ← views.mapIdxM fun i view => do
|
||||
let value := values[i]!
|
||||
let termination := view.termination.rememberExtraParams view.binderIds.size value
|
||||
let env ← getEnv
|
||||
pure {
|
||||
ref := view.ref
|
||||
fvarId := fvars[i]!.fvarId!
|
||||
attrs := view.attrs
|
||||
shortDeclName := view.shortDeclName
|
||||
declName :=
|
||||
if env.isExporting || !env.header.isModule then view.declName
|
||||
else mkPrivateName env view.declName
|
||||
declName := view.declName
|
||||
parentName? := view.parentName?
|
||||
lctx
|
||||
localInstances
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
#include "util/options.h"
|
||||
|
||||
// Please update
|
||||
namespace lean {
|
||||
options get_default_options() {
|
||||
options opts;
|
||||
|
|
|
|||
17
tests/lean/interactive/incomingCallHierarchyWhere.lean
Normal file
17
tests/lean/interactive/incomingCallHierarchyWhere.lean
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
--^ waitForILeans
|
||||
module
|
||||
|
||||
-- Regression test for a bug where the module system broke the call hierarchy when tracking it
|
||||
-- through a `where` in a `public def` of a `module`.
|
||||
|
||||
public section
|
||||
|
||||
def f := 0
|
||||
--^ incomingCallHierarchy
|
||||
|
||||
def foo : Nat :=
|
||||
bar
|
||||
where
|
||||
bar : Nat := f
|
||||
|
||||
def foobar := foo
|
||||
|
|
@ -0,0 +1,65 @@
|
|||
[{"item":
|
||||
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
||||
"selectionRange":
|
||||
{"start": {"line": 8, "character": 4}, "end": {"line": 8, "character": 5}},
|
||||
"range":
|
||||
{"start": {"line": 8, "character": 4}, "end": {"line": 8, "character": 5}},
|
||||
"name": "f",
|
||||
"kind": 14,
|
||||
"data":
|
||||
{"name": "f",
|
||||
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
||||
"fromRanges": [],
|
||||
"children":
|
||||
[{"item":
|
||||
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
||||
"selectionRange":
|
||||
{"start": {"line": 14, "character": 2},
|
||||
"end": {"line": 14, "character": 5}},
|
||||
"range":
|
||||
{"start": {"line": 14, "character": 2},
|
||||
"end": {"line": 14, "character": 16}},
|
||||
"name": "foo.bar",
|
||||
"kind": 14,
|
||||
"data":
|
||||
{"name":
|
||||
"_private.«external:file:///incomingCallHierarchyWhere.lean».0.foo.bar",
|
||||
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
||||
"fromRanges":
|
||||
[{"start": {"line": 14, "character": 15},
|
||||
"end": {"line": 14, "character": 16}}],
|
||||
"children":
|
||||
[{"item":
|
||||
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
||||
"selectionRange":
|
||||
{"start": {"line": 11, "character": 4},
|
||||
"end": {"line": 11, "character": 7}},
|
||||
"range":
|
||||
{"start": {"line": 11, "character": 0},
|
||||
"end": {"line": 14, "character": 16}},
|
||||
"name": "foo",
|
||||
"kind": 14,
|
||||
"data":
|
||||
{"name": "foo",
|
||||
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
||||
"fromRanges":
|
||||
[{"start": {"line": 12, "character": 2},
|
||||
"end": {"line": 12, "character": 5}}],
|
||||
"children":
|
||||
[{"item":
|
||||
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
||||
"selectionRange":
|
||||
{"start": {"line": 16, "character": 4},
|
||||
"end": {"line": 16, "character": 10}},
|
||||
"range":
|
||||
{"start": {"line": 16, "character": 0},
|
||||
"end": {"line": 16, "character": 17}},
|
||||
"name": "foobar",
|
||||
"kind": 14,
|
||||
"data":
|
||||
{"name": "foobar",
|
||||
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
||||
"fromRanges":
|
||||
[{"start": {"line": 16, "character": 14},
|
||||
"end": {"line": 16, "character": 17}}],
|
||||
"children": []}]}]}]}]
|
||||
|
|
@ -1,78 +1,78 @@
|
|||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
|
||||
[Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
|
||||
[Elab.snapshotTree] Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] ⟨15, 2⟩-⟨15, 9⟩
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] ⟨16, 2⟩-⟨16, 11⟩
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] Lean.cdot⟨17, 2⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.induction<range inherited>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩
|
||||
[Elab.snapshotTree] ⟨20, 6⟩-⟨20, 15⟩
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] ⟨23, 6⟩-⟨23, 15⟩
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalTactic.expandEval<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
|
||||
[Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <range inherited>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] <no range>
|
||||
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range>
|
||||
• Goals accomplished!
|
||||
|
||||
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd<no range>
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
|
||||
[Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
|
||||
[Elab.snapshotTree] Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
|
||||
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
|
||||
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue