-
Notifications
You must be signed in to change notification settings - Fork 330
/
DeclarationRange.lean
58 lines (47 loc) · 2.37 KB
/
DeclarationRange.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.MonadEnv
import Lean.AuxRecursor
import Lean.ToExpr
namespace Lean
structure DeclarationRange where
pos : Position
/-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
file, which is IO-heavy. -/
charUtf16 : Nat
endPos : Position
/-- See `charUtf16`. -/
endCharUtf16 : Nat
deriving Inhabited, DecidableEq, Repr
instance : ToExpr DeclarationRange where
toExpr r := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
toTypeExpr := mkConst ``DeclarationRange
structure DeclarationRanges where
range : DeclarationRange
selectionRange : DeclarationRange
deriving Inhabited, Repr
instance : ToExpr DeclarationRanges where
toExpr r := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
toTypeExpr := mkConst ``DeclarationRanges
builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) ← IO.mkRef {}
builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges ← mkMapDeclarationExtension `declranges
def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRanges) : IO Unit :=
builtinDeclRanges.modify (·.insert declName declRanges)
def addDeclarationRanges [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit :=
modifyEnv fun env => declRangeExt.insert env declName declRanges
def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
return declRangeExt.find? (← getEnv) declName
def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m (Option DeclarationRanges) := do
if let some ranges := (← builtinDeclRanges.get (m := IO)).find? declName then
return ranges
let env ← getEnv
if isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName) then
findDeclarationRangesCore? declName.getPrefix
else
findDeclarationRangesCore? declName
end Lean