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.
9	import Base
10	import ../lazy/lazy.bend as Lazy
11	import 0xa81e161008ecc2f297c0a3065cb9b188/main.bend as Ezjson
12	import 0xa81e161008ecc2f297c0a3065cb9b188/src/value.bend as J
13	
14	# the encodings the server speaks
15	type Enc is Data:
16	  Utf16{}
17	  Utf32{}
18	
19	# an encoding's name on the wire
20	def 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
29	def 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
38	def 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
46	def 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
55	def 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)?
62	def 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
66	def 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
75	def 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)
86	def 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
98	def 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
108	def 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
116	def 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
124	def 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
132	def 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
142	def 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
151	type Cols is Data:
152	  Cols{enc: Enc, lines: List<&2, String>}
153	
154	# a document's lines under an encoding
155	def 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
159	def cols(ee: Enc, text: String) -> Cols:
160	  cols.of(ee, String.lines(text))
161	
162	# a line's chars, none past the end
163	def 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
167	def 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
176	def 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
184	def 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
189	def 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
198	def 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
206	def into(cc: Cols, line: U32, col: U32) -> U32:
207	  Cols{ee, lines} = cc
208	  into.at(ee, lines, line, col)