src/lsp/enc.bend source
src/lsp/enc.bend on the hub · documented module
# lsp/enc: position encodings (LSP 3.17 `positionEncoding`), the one place a# character offset crosses the protocol boundary. Pure. bolt counts columns in# code points (a Bend String is a list of them); a client that offers# `utf-32` gets exactly those, and any other gets UTF-16 code units, where a# char outside the Basic Multilingual Plane counts 2. Every position the# server reads goes through `into`, and every one it sends through `out`# (proto.bend's position, semantic.bend's tokens).import Baseimport ../lazy/lazy.bend as Lazyimport 0x81c67699424929b5c44cd8577e18117f/main.bend as Ezjsonimport 0x81c67699424929b5c44cd8577e18117f/src/value.bend as J# the encodings the server speakstype Enc is Data: Utf16{} Utf32{}# an encoding's name on the wiredef name(ee: Enc) -> String: match ee: case Utf16{}: "utf-16" case Utf32{}: "utf-32"# does a list of encodings (JSON cells) offer utf-32? A cell that is not a# string offers nothingdef offers(cells: J.Json) -> Bool: match cells: case J.JCons{h, t}: +more = offers(t) Bool.or(String.eq(Maybe.default(&2, String, Ezjson.as_str(h), ""), "utf-32"), more) case _other: False{}# the cells of an array, JNil when it is not onedef cells(jj: J.Json) -> J.Json: match jj: case J.JArr{items}: items case _other: J.JNil{}# the encoding for utf-32 offered or notdef chosen(yes: Bool) -> Enc: match yes: case True{}: Utf32{} case False{}: Utf16{}# the encoding initialize settles on: utf-32 when the client's# general.positionEncodings offers it, else UTF-16, LSP's defaultdef negotiate(params: J.Json) -> Enc: chosen(offers(cells(Ezjson.get(Ezjson.get(Ezjson.get(params, "capabilities"), "general"), "positionEncodings"))))# counting# --------# does a char take two UTF-16 code units (it lies past U+FFFF)?def wide(cc: Char) -> Bool: U32.is_le(65536, Char.to_u32(cc))# the units a char and the ones after it take: two for a wide char, else onedef units.step(isw: Bool, rest: Nat) -> Nat: match isw: case True{}: 2n+rest case False{}: 1n+rest# the UTF-16 code units the first n chars of a line take; a column past the# line's end counts one unit a columndef units(cs: List<&2, Char>, nn: Nat) -> Nat: match cs nn: case Nil{} _: nn case Con{_c, _t} 0n: 0n case Con{c, t} 1n+p: units.step(wide(c), units(t, p))# the units left after a char, from 1+p units: p after a narrow one, one# fewer after a wide one (none when the offset falls inside its pair)def points.skip(isw: Bool, pp: Nat) -> Nat: match isw pp: case True{} 0n: 0n case True{} 1n+q: q case False{} _: pp# the chars the first u UTF-16 code units of a line cover; an offset inside# a pair covers its char, and one past the line's end counts one column a# unitdef points(cs: List<&2, Char>, uu: Nat) -> Nat: match cs uu: case Nil{} _: uu case Con{_c, _t} 0n: 0n case Con{c, t} 1n+p: 1n+points(t, points.skip(wide(c), p))# a code-point column of a line in an encodingdef out.of(ee: Enc, cs: List<&2, Char>, nn: Nat) -> Nat: match ee: case Utf16{}: units(cs, nn) case Utf32{}: nn# an encoding's column of a line as a code-point columndef into.of(ee: Enc, cs: List<&2, Char>, uu: Nat) -> Nat: match ee: case Utf16{}: points(cs, uu) case Utf32{}: uu# does a line hold a char past U+FFFF? Stops at the firstdef wide_in(cs: List<&2, Char>) -> Bool: match cs: case Nil{}: False{} case Con{c, t}: Lazy.or_else(wide(c), _u => wide_in(t))# does any line hold one? Stops at the firstdef wide_any(lines: List<&2, String>) -> Bool: match lines: case Nil{}: False{} case Con{l, t}: Lazy.or_else(wide_in(String.to_list(l)), _u => wide_any(t))# the encoding a document's columns convert by: UTF-16 on lines with no wide# char counts exactly as utf-32 does (LAWS.bend's enc_narrow), so such a# document converts as utf-32 and never looks a line updef narrowed(ee: Enc, wide: Bool) -> Enc: match ee: case Utf16{}: Bool.pick(Enc, wide, Utf16{}, Utf32{}) case Utf32{}: Utf32{}# a document as the boundary sees it: the encoding its columns convert by# and the text's linestype Cols is Data: Cols{enc: Enc, lines: List<&2, String>}# a document's lines under an encodingdef cols.of(ee: Enc, +lines: List<&2, String>) -> Cols: Cols{narrowed(ee, wide_any(lines)), lines}# a document's text under an encodingdef cols(ee: Enc, text: String) -> Cols: cols.of(ee, String.lines(text))# a line's chars, none past the enddef chars(lines: List<&2, String>, line: U32) -> List<&2, Char>: String.to_list(Maybe.default(&2, String, List.get(&2, String, lines, U32.to_nat(line)), ""))# a code-point column of a line's chars, sent in an encodingdef out.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32: match ee: case Utf16{}: U32.from_nat(out.of(Utf16{}, cs, U32.to_nat(col))) case Utf32{}: col# a code-point column of a document's line, sent in an encoding; utf-32# never looks the line updef out.at(ee: Enc, lines: List<&2, String>, line: U32, col: U32) -> U32: match ee: case Utf16{}: out.col(Utf16{}, chars(lines, line), col) case Utf32{}: col# a code-point column sent in the negotiated encodingdef out(cc: Cols, line: U32, col: U32) -> U32: Cols{ee, lines} = cc out.at(ee, lines, line, col)# a column of a line's chars read in an encoding, as a code-point columndef into.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32: match ee: case Utf16{}: U32.from_nat(into.of(Utf16{}, cs, U32.to_nat(col))) case Utf32{}: col# a column of a document's line read in an encoding; utf-32 never looks the# line updef into.at(ee: Enc, lines: List<&2, String>, line: U32, col: U32) -> U32: match ee: case Utf16{}: into.col(Utf16{}, chars(lines, line), col) case Utf32{}: col# a column read in the negotiated encoding, as a code-point columndef into(cc: Cols, line: U32, col: U32) -> U32: Cols{ee, lines} = cc into.at(ee, lines, line, col)