src/lsp/enc.bend
bolt@1.24.0.0 · 208 lines · 0 definitions
1# lsp/enc: position encodings (LSP 3.17 `positionEncoding`), the one place a
2# character offset crosses the protocol boundary. Pure. bolt counts columns in
3# code points (a Bend String is a list of them); a client that offers
4# `utf-32` gets exactly those, and any other gets UTF-16 code units, where a
5# char outside the Basic Multilingual Plane counts 2. Every position the
6# server reads goes through `into`, and every one it sends through `out`
7# (proto.bend's position, semantic.bend's tokens). ezjson v1.2.0, pinned by
8# hash, is trusted to parse and print JSON correctly; it proves that itself.
9import Base
10import bolt@1.24.0.0/src/lazy/lazy.bend as Lazy
11import emerging-ezjson@1.2.0.0/main.bend as Ezjson
12import emerging-ezjson@1.2.0.0/src/value.bend as J
13
14# the encodings the server speaks
15type Enc is Data:
16 Utf16{}
17 Utf32{}
18
19# an encoding's name on the wire
20def name(ee: Enc) -> String:
21 match ee:
22 case Utf16{}:
23 "utf-16"
24 case Utf32{}:
25 "utf-32"
26
27# does a list of encodings (JSON cells) offer utf-32? A cell that is not a
28# string offers nothing
29def offers(cells: J.Json) -> Bool:
30 match cells:
31 case J.JCons{h, t}:
32 +more = offers(t)
33 Bool.or(String.eq(Maybe.default(&2, String, Ezjson.as_str(h), ""), "utf-32"), more)
34 case _other:
35 False{}
36
37# the cells of an array, JNil when it is not one
38def cells(jj: J.Json) -> J.Json:
39 match jj:
40 case J.JArr{items}:
41 items
42 case _other:
43 J.JNil{}
44
45# the encoding for utf-32 offered or not
46def chosen(yes: Bool) -> Enc:
47 match yes:
48 case True{}:
49 Utf32{}
50 case False{}:
51 Utf16{}
52
53# the encoding initialize settles on: utf-32 when the client's
54# general.positionEncodings offers it, else UTF-16, LSP's default
55def negotiate(params: J.Json) -> Enc:
56 chosen(offers(cells(Ezjson.get(Ezjson.get(Ezjson.get(params, "capabilities"), "general"), "positionEncodings"))))
57
58# counting
59# --------
60
61# does a char take two UTF-16 code units (it lies past U+FFFF)?
62def wide(cc: Char) -> Bool:
63 U32.is_le(65536, Char.to_u32(cc))
64
65# the units a char and the ones after it take: two for a wide char, else one
66def units.step(isw: Bool, rest: Nat) -> Nat:
67 match isw:
68 case True{}:
69 2n+rest
70 case False{}:
71 1n+rest
72
73# the UTF-16 code units the first n chars of a line take; a column past the
74# line's end counts one unit a column
75def units(cs: List<&2, Char>, nn: Nat) -> Nat:
76 match cs nn:
77 case Nil{} _:
78 nn
79 case Con{_c, _t} 0n:
80 0n
81 case Con{c, t} 1n+p:
82 units.step(wide(c), units(t, p))
83
84# the units left after a char, from 1+p units: p after a narrow one, one
85# fewer after a wide one (none when the offset falls inside its pair)
86def points.skip(isw: Bool, pp: Nat) -> Nat:
87 match isw pp:
88 case True{} 0n:
89 0n
90 case True{} 1n+q:
91 q
92 case False{} _:
93 pp
94
95# the chars the first u UTF-16 code units of a line cover; an offset inside
96# a pair covers its char, and one past the line's end counts one column a
97# unit
98def points(cs: List<&2, Char>, uu: Nat) -> Nat:
99 match cs uu:
100 case Nil{} _:
101 uu
102 case Con{_c, _t} 0n:
103 0n
104 case Con{c, t} 1n+p:
105 1n+points(t, points.skip(wide(c), p))
106
107# a code-point column of a line in an encoding
108def out.of(ee: Enc, cs: List<&2, Char>, nn: Nat) -> Nat:
109 match ee:
110 case Utf16{}:
111 units(cs, nn)
112 case Utf32{}:
113 nn
114
115# an encoding's column of a line as a code-point column
116def into.of(ee: Enc, cs: List<&2, Char>, uu: Nat) -> Nat:
117 match ee:
118 case Utf16{}:
119 points(cs, uu)
120 case Utf32{}:
121 uu
122
123# does a line hold a char past U+FFFF? Stops at the first
124def wide_in(cs: List<&2, Char>) -> Bool:
125 match cs:
126 case Nil{}:
127 False{}
128 case Con{c, t}:
129 Lazy.or_else(wide(c), _u => wide_in(t))
130
131# does any line hold one? Stops at the first
132def wide_any(lines: List<&2, String>) -> Bool:
133 match lines:
134 case Nil{}:
135 False{}
136 case Con{l, t}:
137 Lazy.or_else(wide_in(String.to_list(l)), _u => wide_any(t))
138
139# the encoding a document's columns convert by: UTF-16 on lines with no wide
140# char counts exactly as utf-32 does (LAWS.bend's enc_narrow), so such a
141# document converts as utf-32 and never looks a line up
142def narrowed(ee: Enc, wide: Bool) -> Enc:
143 match ee:
144 case Utf16{}:
145 Bool.pick(Enc, wide, Utf16{}, Utf32{})
146 case Utf32{}:
147 Utf32{}
148
149# a document as the boundary sees it: the encoding its columns convert by
150# and the text's lines
151type Cols is Data:
152 Cols{enc: Enc, lines: List<&2, String>}
153
154# a document's lines under an encoding
155def cols.of(ee: Enc, +lines: List<&2, String>) -> Cols:
156 Cols{narrowed(ee, wide_any(lines)), lines}
157
158# a document's text under an encoding
159def cols(ee: Enc, text: String) -> Cols:
160 cols.of(ee, String.lines(text))
161
162# a line's chars, none past the end
163def chars(lines: List<&2, String>, line: U32) -> List<&2, Char>:
164 String.to_list(Maybe.default(&2, String, List.get(&2, String, lines, U32.to_nat(line)), ""))
165
166# a code-point column of a line's chars, sent in an encoding
167def out.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32:
168 match ee:
169 case Utf16{}:
170 U32.from_nat(out.of(Utf16{}, cs, U32.to_nat(col)))
171 case Utf32{}:
172 col
173
174# a code-point column of a document's line, sent in an encoding; utf-32
175# never looks the line up
176def out.at(ee: Enc, lines: List<&2, String>, line: U32, col: U32) -> U32:
177 match ee:
178 case Utf16{}:
179 out.col(Utf16{}, chars(lines, line), col)
180 case Utf32{}:
181 col
182
183# a code-point column sent in the negotiated encoding
184def out(cc: Cols, line: U32, col: U32) -> U32:
185 Cols{ee, lines} = cc
186 out.at(ee, lines, line, col)
187
188# a column of a line's chars read in an encoding, as a code-point column
189def into.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32:
190 match ee:
191 case Utf16{}:
192 U32.from_nat(into.of(Utf16{}, cs, U32.to_nat(col)))
193 case Utf32{}:
194 col
195
196# a column of a document's line read in an encoding; utf-32 never looks the
197# line up
198def into.at(ee: Enc, lines: List<&2, String>, line: U32, col: U32) -> U32:
199 match ee:
200 case Utf16{}:
201 into.col(Utf16{}, chars(lines, line), col)
202 case Utf32{}:
203 col
204
205# a column read in the negotiated encoding, as a code-point column
206def into(cc: Cols, line: U32, col: U32) -> U32:
207 Cols{ee, lines} = cc
208 into.at(ee, lines, line, col)