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