max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: combineFvars

Browse source
This commit is contained in:
Sebastian Ullrich 2022-05-07 21:45:07 +02:00 • committed by Leonardo de Moura
parent 2f461d201e
commit daa9e03e78
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Server/References.lean
View file

@ -131,8 +131,7 @@ partial def combineFvars (refs : Array Reference) : Array Reference := Id.run do
let mut posMap : HashMap Lsp.Range FVarId := HashMap.empty
for ref in refs do
if let { ident := RefIdent.fvar id, range, isBinder := true } := ref then
if !posMap.contains range then
posMap := posMap.insert range id
posMap := posMap.insert range id
-- Map fvar defs to overlapping fvar defs/uses
-- NOTE: poor man's union-find; see also `findCanonicalBinder?`
@ -140,7 +139,8 @@ partial def combineFvars (refs : Array Reference) : Array Reference := Id.run do
for ref in refs do
if let { ident := RefIdent.fvar baseId, range, .. } := ref then
if let some id := posMap.find? range then
let baseId := idMap.findD baseId baseId
let id := findCanonicalBinder idMap id
let baseId := findCanonicalBinder idMap baseId
if baseId != id then
idMap := idMap.insert id baseId
@ -152,7 +152,7 @@ partial def combineFvars (refs : Array Reference) : Array Reference := Id.run do
-- for the base id exists.
unless idMap.contains id do -- Only keep the base definition
refs' := refs'.push ref
| { ident := ident@(RefIdent.fvar fv), range, isBinder := false } =>
| { ident, range, isBinder := false } =>
refs' := refs'.push { ident := applyIdMap idMap ident, range, isBinder := false }
| _ =>
refs' := refs'.push ref