src/lsp/enc.bend

bolt@1.27.0.0 · 208 lines · 26 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.27.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)