-
Notifications
You must be signed in to change notification settings - Fork 329
/
Internal.lean
95 lines (76 loc) · 2.97 KB
/
Internal.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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
/-
Copyright (c) 2022 Joscha Mennicken. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joscha Mennicken
-/
import Lean.Expr
import Lean.Data.Lsp.Basic
/-! This file contains types for communication between the watchdog and the
workers. These messages are not visible externally to users of the LSP server.
-/
namespace Lean.Lsp
open Std
/- Most reference-related types have custom FromJson/ToJson implementations to
reduce the size of the resulting JSON. -/
inductive RefIdent where
| const : Name → RefIdent
| fvar : FVarId → RefIdent
deriving BEq, Hashable, Inhabited
namespace RefIdent
def toString : RefIdent → String
| RefIdent.const n => s!"c:{n}"
| RefIdent.fvar id => s!"f:{id.name}"
def fromString (s : String) : Except String RefIdent := do
let sPrefix := s.take 2
let sName := s.drop 2
-- See `FromJson Name`
let name ← match sName with
| "[anonymous]" => pure Name.anonymous
| _ => match Syntax.decodeNameLit ("`" ++ sName) with
| some n => pure n
| none => throw s!"expected a Name, got {sName}"
match sPrefix with
| "c:" => return RefIdent.const name
| "f:" => return RefIdent.fvar <| FVarId.mk name
| _ => throw "string must start with 'c:' or 'f:'"
end RefIdent
structure RefInfo where
definition : Option Lsp.Range
usages : Array Lsp.Range
instance : ToJson RefInfo where
toJson i :=
let rangeToList (r : Lsp.Range) : List Nat :=
[r.start.line, r.start.character, r.end.line, r.end.character]
Json.mkObj [
("definition", toJson $ i.definition.map rangeToList),
("usages", toJson $ i.usages.map rangeToList)
]
instance : FromJson RefInfo where
fromJson? j := do
let listToRange (l : List Nat) : Except String Lsp.Range := match l with
| [sLine, sChar, eLine, eChar] => pure ⟨⟨sLine, sChar⟩, ⟨eLine, eChar⟩⟩
| _ => throw s!"Expected list of length 4, not {l.length}"
let definition ← j.getObjValAs? (Option $ List Nat) "definition"
let definition ← match definition with
| none => pure none
| some list => some <$> listToRange list
let usages ← j.getObjValAs? (Array $ List Nat) "usages"
let usages ← usages.mapM listToRange
pure { definition, usages }
/-- References from a single module/file -/
def ModuleRefs := HashMap RefIdent RefInfo
instance : ToJson ModuleRefs where
toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toString, toJson info)
instance : FromJson ModuleRefs where
fromJson? j := do
let node ← j.getObj?
node.foldM (init := HashMap.empty) fun m k v =>
return m.insert (← RefIdent.fromString k) (← fromJson? v)
/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
Contains the file's definitions and references. -/
structure LeanIleanInfoParams where
/-- Version of the file these references are from. -/
version : Nat
references : ModuleRefs
deriving FromJson, ToJson
end Lean.Lsp