Lean.Server.References

Lean.Lsp.RefInfo.addRef x x = match x, x with | i@h:{ definition := none, usages := x }, { ident := x_1, range := range, isDeclaration := true } => { definition := some range, usages := i.usages } | i@h:{ definition := x, usages := usages }, { ident := x_1, range := range, isDeclaration := false } => { definition := i.definition, usages := Array.push usages range } | i, x => i

source

def Lean.Lsp.RefInfo.contains (self : Lean.Lsp.RefInfo) (pos : Lean.Lsp.Position) :

Bool

Equations

Lean.Lsp.RefInfo.contains self pos = (fun contains => Id.run (let _do_jp := fun y => do let r ← let col := self.usages; forIn col { fst := none, snd := PUnit.unit } fun range r => let r := r.snd; if contains range pos = true then pure (ForInStep.done { fst := some true, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Id Bool := fun y => false match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a; match self.definition with | some range => if contains range pos = true then pure true else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y)) Lean.Lsp.RefInfo.contains.contains

source

def Lean.Lsp.RefInfo.contains.contains (range : Lean.Lsp.Range) (pos : Lean.Lsp.Position) :

Bool

Equations

Lean.Lsp.RefInfo.contains.contains range pos = (decide (range.start ≤ pos) && decide (pos < range.end))

source

def Lean.Lsp.ModuleRefs.addRef (self : Lean.Lsp.ModuleRefs) (ref : Lean.Server.Reference) :

Lean.Lsp.ModuleRefs

Equations

Lean.Lsp.ModuleRefs.addRef self ref = let refInfo := Std.HashMap.findD self ref.ident Lean.Lsp.RefInfo.empty; Std.HashMap.insert self ref.ident (Lean.Lsp.RefInfo.addRef refInfo ref)

source

def Lean.Lsp.ModuleRefs.findAt? (self : Lean.Lsp.ModuleRefs) (pos : Lean.Lsp.Position) :

Option Lean.Lsp.RefIdent

Equations

Lean.Lsp.ModuleRefs.findAt? self pos = Id.run do let r ← let col := Std.HashMap.toList self; forIn col { fst := none, snd := PUnit.unit } fun x r => match x with | (ident, info) => let r := r.snd; if Lean.Lsp.RefInfo.contains info pos = true then pure (ForInStep.done { fst := some (some ident), snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Id (Option Lean.Lsp.RefIdent) := fun y => none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

structure Lean.Server.Ilean :

Type

version : Nat
module : Lean.Name
references : Lean.Lsp.ModuleRefs

source

instance Lean.Server.instFromJsonIlean :

Lean.FromJson Lean.Server.Ilean

Equations

Lean.Server.instFromJsonIlean = { fromJson? := [anonymous] }

source

instance Lean.Server.instToJsonIlean :

Lean.ToJson Lean.Server.Ilean

Equations

Lean.Server.instToJsonIlean = { toJson := [anonymous] }

source

def Lean.Server.Ilean.load (path : System.FilePath) :

IO Lean.Server.Ilean

Equations

Lean.Server.Ilean.load path = do let content ← IO.FS.readFile path match Lean.Json.parse content >>= Lean.fromJson? with | Except.ok ilean => pure ilean | Except.error msg => IO.throwServerError (toString "Failed to load ilean at " ++ toString path ++ toString ": " ++ toString msg ++ toString "")

source

def Lean.Server.identOf :

Lean.Elab.Info → Option (Lean.Lsp.RefIdent × Bool)

Equations

Lean.Server.identOf x = match x with | Lean.Elab.Info.ofTermInfo ti => match ti.expr with | Lean.Expr.const n x x_1 => some (Lean.Lsp.RefIdent.const n, ti.isBinder) | Lean.Expr.fvar id x => some (Lean.Lsp.RefIdent.fvar id, ti.isBinder) | x => none | Lean.Elab.Info.ofFieldInfo fi => some (Lean.Lsp.RefIdent.const fi.projName, false) | x => none

source

def Lean.Server.findReferences (text : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) :

Array Lean.Server.Reference

Equations

Lean.Server.findReferences text trees = Id.run (let refs := #[]; do let r ← forIn trees refs fun tree r => let refs := r; let refs := Array.appendList refs (Lean.Elab.InfoTree.deepestNodes (fun x info x => Id.run (let _do_jp := fun y => pure none; match Lean.Server.identOf info with | some (ident, isDeclaration) => match Lean.Elab.Info.range? info with | some range => pure (some { ident := ident, range := String.Range.toLspRange text range, isDeclaration := isDeclaration }) | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y)) tree); do pure PUnit.unit pure (ForInStep.yield refs) let x : Array Lean.Server.Reference := r let refs : Array Lean.Server.Reference := x refs)

source

def Lean.Server.combineFvars (refs : Array Lean.Server.Reference) :

Array Lean.Server.Reference

Equations

Lean.Server.combineFvars refs = (fun applyIdMap => Id.run (let posMap := Std.HashMap.empty; let idMap := Std.HashMap.empty; do let r ← forIn refs { fst := posMap, snd := idMap } fun ref r => let posMap := r.fst; let idMap := r.snd; match ref with | { ident := Lean.Lsp.RefIdent.fvar id, range := range, isDeclaration := true } => match Std.HashMap.find? posMap range with | some baseId => let idMap := Std.HashMap.insert idMap id baseId; do pure PUnit.unit pure (ForInStep.yield { fst := posMap, snd := idMap }) | x => let posMap := Std.HashMap.insert posMap range id; let idMap := Std.HashMap.insert idMap id id; do pure PUnit.unit pure (ForInStep.yield { fst := posMap, snd := idMap }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := posMap, snd := idMap }) let x : MProd (Std.HashMap Lean.Lsp.Range Lean.FVarId) (Std.HashMap Lean.FVarId Lean.FVarId) := r match x with | { fst := posMap, snd := idMap } => Array.foldl (fun refs ref => match ref with | { ident := Lean.Lsp.RefIdent.fvar id, range := range, isDeclaration := true } => Id.run (let _do_jp := fun y => pure refs; match Std.HashMap.find? idMap id with | some baseId => if (id == baseId) = true then pure (Array.push refs ref) else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y) | { ident := ident@h:(Lean.Lsp.RefIdent.fvar x), range := range, isDeclaration := false } => Array.push refs { ident := applyIdMap idMap ident, range := range, isDeclaration := false } | x => Array.push refs ref) #[] refs 0 (Array.size refs))) Lean.Server.combineFvars.applyIdMap

source

def Lean.Server.combineFvars.applyIdMap :

Std.HashMap Lean.FVarId Lean.FVarId → Lean.Lsp.RefIdent → Lean.Lsp.RefIdent

Equations

Lean.Server.combineFvars.applyIdMap x x = match x, x with | m, Lean.Lsp.RefIdent.fvar id => Lean.Lsp.RefIdent.fvar (Std.HashMap.findD m id id) | x, ident => ident

source

def Lean.Server.dedupReferences (refs : Array Lean.Server.Reference) :

Array Lean.Server.Reference

Equations

Lean.Server.dedupReferences refs = Id.run (let refsByIdAndRange := Std.HashMap.empty; do let r ← forIn refs refsByIdAndRange fun ref r => let refsByIdAndRange := r; if (ref.isDeclaration || !Std.HashMap.contains refsByIdAndRange (ref.ident, ref.range)) = true then let refsByIdAndRange := Std.HashMap.insert refsByIdAndRange (ref.ident, ref.range) ref; do pure PUnit.unit pure (ForInStep.yield refsByIdAndRange) else do pure PUnit.unit pure (ForInStep.yield refsByIdAndRange) let x : Std.HashMap (Lean.Lsp.RefIdent × Lean.Lsp.Range) Lean.Server.Reference := r let refsByIdAndRange : Std.HashMap (Lean.Lsp.RefIdent × Lean.Lsp.Range) Lean.Server.Reference := x let dedupedRefs : Array Lean.Server.Reference := Std.HashMap.fold (fun refs x ref => Array.push refs ref) #[] refsByIdAndRange pure (Array.qsort dedupedRefs (fun a a_1 => decide (a.range < a_1.range)) 0 (Array.size dedupedRefs - 1)))

source

def Lean.Server.findModuleRefs (text : Lean.FileMap) (trees : Array Lean.Elab.InfoTree) (localVars : optParam Bool true) :

Lean.Lsp.ModuleRefs

Equations

Lean.Server.findModuleRefs text trees localVars = Id.run (let refs := Lean.Server.dedupReferences (Lean.Server.combineFvars (Lean.Server.findReferences text trees)); let _do_jp := fun refs y => Array.foldl (fun m ref => Lean.Lsp.ModuleRefs.addRef m ref) Std.HashMap.empty refs 0 (Array.size refs); if (!localVars) = true then let refs := Array.filter (fun x => match x with | { ident := Lean.Lsp.RefIdent.fvar x, range := x_1, isDeclaration := x_2 } => false | x => true) refs 0 (Array.size refs); do let y ← pure PUnit.unit _do_jp refs y else do let y ← pure PUnit.unit _do_jp refs y)

source

structure Lean.Server.References :

Type

ileans : Std.HashMap Lean.Name (System.FilePath × Lean.Lsp.ModuleRefs)
workers : Std.HashMap Lean.Name (Nat × Lean.Lsp.ModuleRefs)

source

def Lean.Server.References.empty :

Lean.Server.References

Equations

Lean.Server.References.empty = { ileans := Std.HashMap.empty, workers := Std.HashMap.empty }

source

def Lean.Server.References.addIlean (self : Lean.Server.References) (path : System.FilePath) (ilean : Lean.Server.Ilean) :

Lean.Server.References

Equations

Lean.Server.References.addIlean self path ilean = { ileans := Std.HashMap.insert self.ileans ilean.module (path, ilean.references), workers := self.workers }

source

def Lean.Server.References.removeIlean (self : Lean.Server.References) (path : System.FilePath) :

Lean.Server.References

Equations

Lean.Server.References.removeIlean self path = let namesToRemove := List.map (fun x => match x with | (n, x, x_1) => n) (List.filter (fun x => match x with | (x, p, x_1) => p == path) (Std.HashMap.toList self.ileans)); List.foldl (fun self name => { ileans := Std.HashMap.erase self.ileans name, workers := self.workers }) self namesToRemove

source

def Lean.Server.References.updateWorkerRefs (self : Lean.Server.References) (name : Lean.Name) (version : Nat) (refs : Lean.Lsp.ModuleRefs) :

Lean.Server.References

Equations

Lean.Server.References.updateWorkerRefs self name version refs = Id.run (let _do_jp := fun y => pure self; match Std.HashMap.find? self.workers name with | some (currVersion, x) => let _do_jp := fun y => if (version == currVersion) = true then let current := Std.HashMap.findD self.workers name (version, Std.HashMap.empty); let merged := Std.HashMap.fold (fun m ident info => Std.HashMap.insert m ident (Lean.Lsp.RefInfo.merge (Std.HashMap.findD m ident Lean.Lsp.RefInfo.empty) info)) current.snd refs; pure { ileans := self.ileans, workers := Std.HashMap.insert self.workers name (version, merged) } else do let y ← pure PUnit.unit _do_jp y; if version > currVersion then pure { ileans := self.ileans, workers := Std.HashMap.insert self.workers name (version, refs) } else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y)

source

def Lean.Server.References.finalizeWorkerRefs (self : Lean.Server.References) (name : Lean.Name) (version : Nat) (refs : Lean.Lsp.ModuleRefs) :

Lean.Server.References

Equations

Lean.Server.References.finalizeWorkerRefs self name version refs = Id.run (let _do_jp := fun y => pure { ileans := self.ileans, workers := Std.HashMap.insert self.workers name (version, refs) }; match Std.HashMap.find? self.workers name with | some (currVersion, x) => if version < currVersion then pure self else do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y)

source

def Lean.Server.References.removeWorkerRefs (self : Lean.Server.References) (name : Lean.Name) :

Lean.Server.References

Equations

Lean.Server.References.removeWorkerRefs self name = { ileans := self.ileans, workers := Std.HashMap.erase self.workers name }

source

def Lean.Server.References.allRefs (self : Lean.Server.References) :

Std.HashMap Lean.Name Lean.Lsp.ModuleRefs

Equations

Lean.Server.References.allRefs self = let ileanRefs := List.foldl (fun m x => match x with | (name, x, refs) => Std.HashMap.insert m name refs) Std.HashMap.empty (Std.HashMap.toList self.ileans); List.foldl (fun m x => match x with | (name, x, refs) => Std.HashMap.insert m name refs) ileanRefs (Std.HashMap.toList self.workers)

source

def Lean.Server.References.findAt? (self : Lean.Server.References) (module : Lean.Name) (pos : Lean.Lsp.Position) :

Option Lean.Lsp.RefIdent

Equations

Lean.Server.References.findAt? self module pos = Id.run (let _do_jp := fun y => none; match Std.HashMap.find? (Lean.Server.References.allRefs self) module with | some refs => pure (Lean.Lsp.ModuleRefs.findAt? refs pos) | x => do let y ← pure PUnit.unit _do_jp y)

source

def Lean.Server.References.referringTo (self : Lean.Server.References) (ident : Lean.Lsp.RefIdent) (srcSearchPath : Lean.SearchPath) (includeDefinition : optParam Bool true) :

IO (Array Lean.Lsp.Location)

Equations

Lean.Server.References.referringTo self ident srcSearchPath includeDefinition = let result := #[]; do let r ← let col := Std.HashMap.toList (Lean.Server.References.allRefs self); forIn col result fun x r => match x with | (module, refs) => let result := r; match Std.HashMap.find? refs ident with | some info => do let a ← Lean.SearchPath.findModuleWithExt srcSearchPath "lean" module match a with | some path => do let a ← IO.FS.realPath path let uri : Lean.Lsp.DocumentUri := Lean.Lsp.DocumentUri.ofPath a let _do_jp : Array Lean.Lsp.Location → PUnit → IO (ForInStep (Array Lean.Lsp.Location)) := fun result y => do let r ← let col := info.usages; forIn col result fun range r => let result := r; let result := Array.push result { uri := uri, range := range }; do pure PUnit.unit pure (ForInStep.yield result) let x : Array Lean.Lsp.Location := r let result : Array Lean.Lsp.Location := x pure PUnit.unit pure (ForInStep.yield result) if includeDefinition = true then match info.definition with | some range => let result := Array.push result { uri := uri, range := range }; do let y ← pure PUnit.unit _do_jp result y | x => do let y ← pure PUnit.unit _do_jp result y else do let y ← pure PUnit.unit _do_jp result y | x => do pure PUnit.unit pure (ForInStep.yield result) | x => do pure PUnit.unit pure (ForInStep.yield result) let x : Array Lean.Lsp.Location := r let result : Array Lean.Lsp.Location := x pure result

source

def Lean.Server.References.definitionOf? (self : Lean.Server.References) (ident : Lean.Lsp.RefIdent) (srcSearchPath : Lean.SearchPath) :

IO (Option Lean.Lsp.Location)

Equations

Lean.Server.References.definitionOf? self ident srcSearchPath = do let r ← let col := Std.HashMap.toList (Lean.Server.References.allRefs self); forIn col { fst := none, snd := PUnit.unit } fun x r => match x with | (module, refs) => let r := r.snd; match Std.HashMap.find? refs ident with | some info => match info.definition with | some definition => do let a ← Lean.SearchPath.findModuleWithExt srcSearchPath "lean" module match a with | some path => do let a ← IO.FS.realPath path let uri : Lean.Lsp.DocumentUri := Lean.Lsp.DocumentUri.ofPath a pure (ForInStep.done { fst := some (some { uri := uri, range := definition }), snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → IO (Option Lean.Lsp.Location) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

def Lean.Server.References.definitionsMatching {α : Type} (self : Lean.Server.References) (srcSearchPath : Lean.SearchPath) (filter : Lean.Name → Option α) (maxAmount? : optParam (Option Nat) none) :

IO (Array (α × Lean.Lsp.Location))

Equations

Lean.Server.References.definitionsMatching self srcSearchPath filter maxAmount? = let result := #[]; do let r ← let col := Std.HashMap.toList (Lean.Server.References.allRefs self); forIn col { fst := none, snd := result } fun x r => match x with | (module, refs) => let r := r.snd; let result := r; do let a ← Lean.SearchPath.findModuleWithExt srcSearchPath "lean" module match a with | some path => do let a ← IO.FS.realPath path let uri : Lean.Lsp.DocumentUri := Lean.Lsp.DocumentUri.ofPath a let r ← let col := Std.HashMap.toList refs; forIn col { fst := none, snd := result } fun x r => match x with | (ident, info) => let r := r.snd; let result := r; match (ident, info.definition) with | (Lean.Lsp.RefIdent.const name, some definition) => match filter name with | some a => let result := Array.push result (a, { uri := uri, range := definition }); match maxAmount? with | some maxAmount => if Array.size result ≥ maxAmount then pure (ForInStep.done { fst := some result, snd := result }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := result }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := result }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := result }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := result }) let x : Array (α × Lean.Lsp.Location) := r.snd let result : Array (α × Lean.Lsp.Location) := x match r.fst with | none => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := result }) | some a => pure (ForInStep.done { fst := some a, snd := result }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := result }) let x : Array (α × Lean.Lsp.Location) := r.snd let result : Array (α × Lean.Lsp.Location) := x let _do_jp : PUnit → IO (Array (α × Lean.Lsp.Location)) := fun y => pure result match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a