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).
8	import Base
9	import ../lazy/lazy.bend as Lazy
10	import 0x81c67699424929b5c44cd8577e18117f/main.bend as Ezjson
11	import 0x81c67699424929b5c44cd8577e18117f/src/value.bend as J
12	
13	# the encodings the server speaks
14	type Enc is Data:
15	  Utf16{}
16	  Utf32{}
17	
18	# an encoding's name on the wire
19	def 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
28	def 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
37	def 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
45	def 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
54	def 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)?
61	def 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
65	def 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
74	def 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)
85	def 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
97	def 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
107	def 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
115	def 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
123	def 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
131	def 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
141	def 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
150	type Cols is Data:
151	  Cols{enc: Enc, lines: List<&2, String>}
152	
153	# a document's lines under an encoding
154	def 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
158	def cols(ee: Enc, text: String) -> Cols:
159	  cols.of(ee, String.lines(text))
160	
161	# a line's chars, none past the end
162	def 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
166	def 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
175	def 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
183	def 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
188	def 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
197	def 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
205	def into(cc: Cols, line: U32, col: U32) -> U32:
206	  Cols{ee, lines} = cc
207	  into.at(ee, lines, line, col)