Skip to content

Commit e1154f9

Browse files
mhuisimhuisi
committed
fix: unknown identifier identifier minimization
1 parent 114f7e4 commit e1154f9

8 files changed

+325
-127
lines changed

‎src/Lean/Server/Completion/CompletionUtils.lean‎

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -41,13 +41,13 @@ structure ContextualizedCompletionInfo where
4141
ctx : ContextInfo
4242
info : CompletionInfo
4343

44-
def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name)
44+
partial def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name)
4545
: Name := Id.run do
46-
let mut minimized := shortenIn id currNamespace
46+
let mut minimized := shortenInCurrentNamespace id currNamespace
4747
for openDecl in openDecls do
4848
let candidate? := match openDecl with
4949
| .simple ns except =>
50-
let candidate := shortenIn id ns
50+
let candidate := shortenInOpenNamespace id ns
5151
if ! except.contains candidate then
5252
some candidate
5353
else
@@ -62,13 +62,20 @@ def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List O
6262
minimized := candidate
6363
return minimized
6464
where
65-
shortenIn (id : Name) (contextNamespace : Name) : Name :=
66-
if contextNamespace matches .anonymous then
65+
shortenInCurrentNamespace (id : Name) (currentNamespace : Name) : Name :=
66+
if currentNamespace matches .anonymous then
6767
id
68-
else if contextNamespace.isPrefixOf id then
69-
id.replacePrefix contextNamespace .anonymous
7068
else
69+
let maybeShortened := shortenInOpenNamespace id currentNamespace
70+
if maybeShortened != id then
71+
maybeShortened
72+
else
73+
shortenInCurrentNamespace id currentNamespace.getPrefix
74+
shortenInOpenNamespace (id : Name) (openNamespace : Name) : Name :=
75+
if openNamespace == id then
7176
id
77+
else
78+
id.replacePrefix openNamespace .anonymous
7279

7380
def unfoldDefinitionGuarded? (e : Expr) : MetaM (Option Expr) :=
7481
try Lean.Meta.unfoldDefinition? e catch _ => pure none

‎src/Lean/Server/Test/Refs.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ import Init.Prelude
1111

1212
public def LeanServerTestRefsTest0 := Nat
1313

14+
public def Lean.Server.Test.LeanServerTestRefsTest0' := Nat
15+
1416
namespace Lean.Server.Test.Refs
1517

1618
public def Test1 := Nat

‎tests/lean/interactive/findReferences.lean.expected.out‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,13 +18,13 @@
1818
{"start": {"line": 9, "character": 13}, "end": {"line": 9, "character": 40}}},
1919
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
2020
"range":
21-
{"start": {"line": 15, "character": 11},
22-
"end": {"line": 15, "character": 16}}},
21+
{"start": {"line": 17, "character": 11},
22+
"end": {"line": 17, "character": 16}}},
2323
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
2424
"range":
25-
{"start": {"line": 16, "character": 20},
26-
"end": {"line": 16, "character": 25}}},
25+
{"start": {"line": 18, "character": 20},
26+
"end": {"line": 18, "character": 25}}},
2727
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
2828
"range":
29-
{"start": {"line": 17, "character": 20},
30-
"end": {"line": 17, "character": 25}}}]
29+
{"start": {"line": 19, "character": 20},
30+
"end": {"line": 19, "character": 25}}}]

‎tests/lean/interactive/incomingCallHierarchy.lean.expected.out‎

Lines changed: 28 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -45,11 +45,11 @@
4545
[{"item":
4646
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
4747
"selectionRange":
48-
{"start": {"line": 15, "character": 11},
49-
"end": {"line": 15, "character": 16}},
48+
{"start": {"line": 17, "character": 11},
49+
"end": {"line": 17, "character": 16}},
5050
"range":
51-
{"start": {"line": 15, "character": 11},
52-
"end": {"line": 15, "character": 16}},
51+
{"start": {"line": 17, "character": 11},
52+
"end": {"line": 17, "character": 16}},
5353
"name": "Lean.Server.Test.Refs.Test1",
5454
"kind": 14,
5555
"data":
@@ -59,70 +59,70 @@
5959
[{"item":
6060
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
6161
"selectionRange":
62-
{"start": {"line": 16, "character": 11},
63-
"end": {"line": 16, "character": 16}},
62+
{"start": {"line": 18, "character": 11},
63+
"end": {"line": 18, "character": 16}},
6464
"range":
65-
{"start": {"line": 16, "character": 0},
66-
"end": {"line": 16, "character": 25}},
65+
{"start": {"line": 18, "character": 0},
66+
"end": {"line": 18, "character": 25}},
6767
"name": "Lean.Server.Test.Refs.Test2",
6868
"kind": 14,
6969
"data":
7070
{"name": "Lean.Server.Test.Refs.Test2",
7171
"module": "Lean.Server.Test.Refs"}},
7272
"fromRanges":
73-
[{"start": {"line": 16, "character": 20},
74-
"end": {"line": 16, "character": 25}}],
73+
[{"start": {"line": 18, "character": 20},
74+
"end": {"line": 18, "character": 25}}],
7575
"children":
7676
[{"item":
7777
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
7878
"selectionRange":
79-
{"start": {"line": 18, "character": 11},
80-
"end": {"line": 18, "character": 16}},
79+
{"start": {"line": 20, "character": 11},
80+
"end": {"line": 20, "character": 16}},
8181
"range":
82-
{"start": {"line": 18, "character": 0},
83-
"end": {"line": 18, "character": 25}},
82+
{"start": {"line": 20, "character": 0},
83+
"end": {"line": 20, "character": 25}},
8484
"name": "Lean.Server.Test.Refs.Test4",
8585
"kind": 14,
8686
"data":
8787
{"name": "Lean.Server.Test.Refs.Test4",
8888
"module": "Lean.Server.Test.Refs"}},
8989
"fromRanges":
90-
[{"start": {"line": 18, "character": 20},
91-
"end": {"line": 18, "character": 25}}],
90+
[{"start": {"line": 20, "character": 20},
91+
"end": {"line": 20, "character": 25}}],
9292
"children": []},
9393
{"item":
9494
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
9595
"selectionRange":
96-
{"start": {"line": 19, "character": 11},
97-
"end": {"line": 19, "character": 16}},
96+
{"start": {"line": 21, "character": 11},
97+
"end": {"line": 21, "character": 16}},
9898
"range":
99-
{"start": {"line": 19, "character": 0},
100-
"end": {"line": 19, "character": 25}},
99+
{"start": {"line": 21, "character": 0},
100+
"end": {"line": 21, "character": 25}},
101101
"name": "Lean.Server.Test.Refs.Test5",
102102
"kind": 14,
103103
"data":
104104
{"name": "Lean.Server.Test.Refs.Test5",
105105
"module": "Lean.Server.Test.Refs"}},
106106
"fromRanges":
107-
[{"start": {"line": 19, "character": 20},
108-
"end": {"line": 19, "character": 25}}],
107+
[{"start": {"line": 21, "character": 20},
108+
"end": {"line": 21, "character": 25}}],
109109
"children": []}]},
110110
{"item":
111111
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
112112
"selectionRange":
113-
{"start": {"line": 17, "character": 11},
114-
"end": {"line": 17, "character": 16}},
113+
{"start": {"line": 19, "character": 11},
114+
"end": {"line": 19, "character": 16}},
115115
"range":
116-
{"start": {"line": 17, "character": 0},
117-
"end": {"line": 17, "character": 25}},
116+
{"start": {"line": 19, "character": 0},
117+
"end": {"line": 19, "character": 25}},
118118
"name": "Lean.Server.Test.Refs.Test3",
119119
"kind": 14,
120120
"data":
121121
{"name": "Lean.Server.Test.Refs.Test3",
122122
"module": "Lean.Server.Test.Refs"}},
123123
"fromRanges":
124-
[{"start": {"line": 17, "character": 20},
125-
"end": {"line": 17, "character": 25}}],
124+
[{"start": {"line": 19, "character": 20},
125+
"end": {"line": 19, "character": 25}}],
126126
"children": []},
127127
{"item":
128128
{"uri": "file:///incomingCallHierarchy.lean",

‎tests/lean/interactive/outgoingCallHierarchy.lean.expected.out‎

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -286,11 +286,11 @@
286286
[{"item":
287287
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
288288
"selectionRange":
289-
{"start": {"line": 26, "character": 11},
290-
"end": {"line": 26, "character": 17}},
289+
{"start": {"line": 28, "character": 11},
290+
"end": {"line": 28, "character": 17}},
291291
"range":
292-
{"start": {"line": 26, "character": 11},
293-
"end": {"line": 26, "character": 17}},
292+
{"start": {"line": 28, "character": 11},
293+
"end": {"line": 28, "character": 17}},
294294
"name": "Lean.Server.Test.Refs.test10",
295295
"kind": 14,
296296
"data":
@@ -303,70 +303,70 @@
303303
[{"item":
304304
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
305305
"selectionRange":
306-
{"start": {"line": 25, "character": 11},
307-
"end": {"line": 25, "character": 16}},
306+
{"start": {"line": 27, "character": 11},
307+
"end": {"line": 27, "character": 16}},
308308
"range":
309-
{"start": {"line": 25, "character": 11},
310-
"end": {"line": 25, "character": 16}},
309+
{"start": {"line": 27, "character": 11},
310+
"end": {"line": 27, "character": 16}},
311311
"name": "Lean.Server.Test.Refs.test9",
312312
"kind": 14,
313313
"data":
314314
{"name": "Lean.Server.Test.Refs.test9",
315315
"module": "Lean.Server.Test.Refs"}},
316316
"fromRanges":
317-
[{"start": {"line": 26, "character": 21},
318-
"end": {"line": 26, "character": 26}}],
317+
[{"start": {"line": 28, "character": 21},
318+
"end": {"line": 28, "character": 26}}],
319319
"children":
320320
[{"item":
321321
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
322322
"selectionRange":
323-
{"start": {"line": 23, "character": 11},
324-
"end": {"line": 23, "character": 16}},
323+
{"start": {"line": 25, "character": 11},
324+
"end": {"line": 25, "character": 16}},
325325
"range":
326-
{"start": {"line": 23, "character": 11},
327-
"end": {"line": 23, "character": 16}},
326+
{"start": {"line": 25, "character": 11},
327+
"end": {"line": 25, "character": 16}},
328328
"name": "Lean.Server.Test.Refs.test7",
329329
"kind": 14,
330330
"data":
331331
{"name": "Lean.Server.Test.Refs.test7",
332332
"module": "Lean.Server.Test.Refs"}},
333333
"fromRanges":
334-
[{"start": {"line": 25, "character": 20},
335-
"end": {"line": 25, "character": 25}}],
334+
[{"start": {"line": 27, "character": 20},
335+
"end": {"line": 27, "character": 25}}],
336336
"children":
337337
[{"item":
338338
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
339339
"selectionRange":
340-
{"start": {"line": 21, "character": 17},
341-
"end": {"line": 21, "character": 22}},
340+
{"start": {"line": 23, "character": 17},
341+
"end": {"line": 23, "character": 22}},
342342
"range":
343-
{"start": {"line": 21, "character": 17},
344-
"end": {"line": 21, "character": 22}},
343+
{"start": {"line": 23, "character": 17},
344+
"end": {"line": 23, "character": 22}},
345345
"name": "Lean.Server.Test.Refs.Test6",
346346
"kind": 14,
347347
"data":
348348
{"name": "Lean.Server.Test.Refs.Test6",
349349
"module": "Lean.Server.Test.Refs"}},
350350
"fromRanges":
351-
[{"start": {"line": 23, "character": 19},
352-
"end": {"line": 23, "character": 24}}],
351+
[{"start": {"line": 25, "character": 19},
352+
"end": {"line": 25, "character": 24}}],
353353
"children": []},
354354
{"item":
355355
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
356356
"selectionRange":
357-
{"start": {"line": 22, "character": 4},
358-
"end": {"line": 22, "character": 6}},
357+
{"start": {"line": 24, "character": 4},
358+
"end": {"line": 24, "character": 6}},
359359
"range":
360-
{"start": {"line": 22, "character": 4},
361-
"end": {"line": 22, "character": 6}},
360+
{"start": {"line": 24, "character": 4},
361+
"end": {"line": 24, "character": 6}},
362362
"name": "Lean.Server.Test.Refs.Test6.mk",
363363
"kind": 14,
364364
"data":
365365
{"name": "Lean.Server.Test.Refs.Test6.mk",
366366
"module": "Lean.Server.Test.Refs"}},
367367
"fromRanges":
368-
[{"start": {"line": 23, "character": 28},
369-
"end": {"line": 23, "character": 31}}],
368+
[{"start": {"line": 25, "character": 28},
369+
"end": {"line": 25, "character": 31}}],
370370
"children": []}]}]}]},
371371
{"item":
372372
{"uri": "file:///outgoingCallHierarchy.lean",
@@ -694,11 +694,11 @@
694694
[{"item":
695695
{"uri": "file:///src/Lean/Server/Test/Refs.lean",
696696
"selectionRange":
697-
{"start": {"line": 21, "character": 17},
698-
"end": {"line": 21, "character": 22}},
697+
{"start": {"line": 23, "character": 17},
698+
"end": {"line": 23, "character": 22}},
699699
"range":
700-
{"start": {"line": 21, "character": 17},
701-
"end": {"line": 21, "character": 22}},
700+
{"start": {"line": 23, "character": 17},
701+
"end": {"line": 23, "character": 22}},
702702
"name": "Lean.Server.Test.Refs.Test6",
703703
"kind": 14,
704704
"data":

‎tests/lean/interactive/unknownIdentifierCodeActions.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,28 @@
55
example : LeanServerTestRefsTest0
66
--^ codeAction
77

8+
namespace Lean.Server.Test.Refs
9+
#check Lean.Server.Test.Refs.test1
10+
--^ codeAction
11+
end Lean.Server.Test.Refs
12+
13+
namespace Lean.Server.Test.Refs.Foobar
14+
#check Lean.Server.Test.LeanServerTestRefsTest0'
15+
end Lean.Server.Test.Refs.Foobar
16+
17+
open Lean.Server.Test.Refs.Foobar
18+
#check Lean.Server.Test.Refs.test1
19+
--^ codeAction
20+
821
#check Lean.Server.Test.Refs.test
922
--^ codeAction
1023

24+
namespace Lean.Server.Test.Refs.Test1
25+
#check Lean.Server.Test.Refs.Test1
26+
--^ codeAction
27+
end Lean.Server.Test.Refs.Test1
28+
29+
1130
structure Foobar where
1231
veryLongAndHopefullyVeryUniqueBar0 : Nat
1332

0 commit comments

Comments
 (0)