From 0671a4e3d700f3462bfdf3039426b1ce8559a263 Mon Sep 17 00:00:00 2001 From: noah-emp <182041600+noah-emp@users.noreply.github.com> Date: Sat, 26 Sep 2026 11:28:37 -0400 Subject: [PATCH 1/3] perf(lsp): semantic tokens up to 10x faster, symbols up to 2.8x on large files Semantic tokens looked each use's binder up by scanning every binder of the document, with no early exit; they now look it up in a trie keyed by line (locals) or by name hash (items and constructors) built once per request, each leaf in source order, so the answer is the scan's. Enc.cols now reads a document with no char past U+FFFF as utf-32, where UTF-16 agrees, so a position crosses the boundary without walking to its line; the new law enc_narrow (BOLT-LSP-7) proves that agreement both ways. Bind.kind_at and Bind.kind_of_item had no other caller and are gone. Co-Authored-By: Claude Opus 5.5 --- src/lsp/LAWS.bend | 11 +++ src/lsp/PROOF.bend | 92 +++++++++++++++++++++++++ src/lsp/enc.bend | 58 ++++++++++++++-- src/lsp/semantic.bend | 154 +++++++++++++++++++++++++++++++++++++++--- src/syntax/bind.bend | 23 ------- 5 files changed, 302 insertions(+), 36 deletions(-) diff --git a/src/lsp/LAWS.bend b/src/lsp/LAWS.bend index c6cfa8f..571a15d 100644 --- a/src/lsp/LAWS.bend +++ b/src/lsp/LAWS.bend @@ -888,3 +888,14 @@ law enc_utf32: for +col: U32 {Enc.out(Enc.Cols{Enc.Utf32{}, lines}, line, col) == col : U32} & {Enc.into(Enc.Cols{Enc.Utf32{}, lines}, line, col) == col : U32} + +# LAW: on lines with no char past U+FFFF, UTF-16 counts every column as a +# code point, both ways: why Enc.cols converts such a document as utf-32 +# BOLT-LSP-7 +law enc_narrow: + for +lines: List<&2, String> + for h: {Enc.wide_any(lines) == False{} : Bool} + for +line: U32 + for +nn: Nat + {Enc.out.of(Enc.Utf16{}, Enc.chars(lines, line), nn) == nn : Nat} + & {Enc.into.of(Enc.Utf16{}, Enc.chars(lines, line), nn) == nn : Nat} diff --git a/src/lsp/PROOF.bend b/src/lsp/PROOF.bend index 94bfc7b..59247b9 100644 --- a/src/lsp/PROOF.bend +++ b/src/lsp/PROOF.bend @@ -2508,3 +2508,95 @@ def Laws.enc_tokens(_ee, _cs, _line, _col, _len, _typ): def Laws.enc_utf32(_lines, _line, _col): ({==}, {==}) +# an or_else that is False was False on its left +law nav.or_else_left: + for a: Bool + for -f: Unit -> Bool + for h: {Lazy.or_else(a, f) == False{} : Bool} + {a == False{} : Bool} + +def nav.or_else_left(a, _f, h): + match a: + case True{}: + Empty.absurd({True{} == False{} : Bool}, true_false(h)) + case False{}: + {==} + +# an or_else that is False was False on its right +law nav.or_else_right: + for a: Bool + for -f: Unit -> Bool + for h: {Lazy.or_else(a, f) == False{} : Bool} + {f(Unit{}) == False{} : Bool} + +def nav.or_else_right(a, f, h): + match a: + case True{}: + Empty.absurd({f(Unit{}) == False{} : Bool}, true_false(h)) + case False{}: + h + +# on a line with no wide char, UTF-16 units are the code points counted +law nav.units_narrow: + for cs: List<&2, Char> + for +h: {Enc.wide_in(cs) == False{} : Bool} + for nn: Nat + {Enc.units(cs, nn) == nn : Nat} + +def nav.units_narrow(cs, h, nn): + match cs: + case Nil{}: + {==} + case Con{+c, +t}: + match nn: + case 0n: + {==} + case 1n+p: + +hw = Equal.sym(Bool, Enc.wide(c), False{}, nav.or_else_left(Enc.wide(c), _u => Enc.wide_in(t), h)) + %hw : {Enc.units.step(_, Enc.units(t, p)) == 1n+p : Nat} + Equal.cong(Nat, Nat, x => 1n+x, Enc.units(t, p), p, + nav.units_narrow(t, nav.or_else_right(Enc.wide(c), _u => Enc.wide_in(t), h), p)) + +# on a line with no wide char, UTF-16 units read back as themselves +law nav.points_narrow: + for cs: List<&2, Char> + for +h: {Enc.wide_in(cs) == False{} : Bool} + for nn: Nat + {Enc.points(cs, nn) == nn : Nat} + +def nav.points_narrow(cs, h, nn): + match cs: + case Nil{}: + {==} + case Con{+c, +t}: + match nn: + case 0n: + {==} + case 1n+p: + +hw = Equal.sym(Bool, Enc.wide(c), False{}, nav.or_else_left(Enc.wide(c), _u => Enc.wide_in(t), h)) + %hw : {1n+Enc.points(t, Enc.points.skip(_, p)) == 1n+p : Nat} + Equal.cong(Nat, Nat, x => 1n+x, Enc.points(t, p), p, + nav.points_narrow(t, nav.or_else_right(Enc.wide(c), _u => Enc.wide_in(t), h), p)) + +# every line of lines with no wide char has none +law nav.chars_narrow: + for lines: List<&2, String> + for h: {Enc.wide_any(lines) == False{} : Bool} + for ii: Nat + {Enc.wide_in(String.to_list(Maybe.default(&2, String, List.get(&2, String, lines, ii), ""))) == False{} : Bool} + +def nav.chars_narrow(lines, h, ii): + match lines: + case Nil{}: + {==} + case Con{+l, +t}: + match ii: + case 0n: + nav.or_else_left(Enc.wide_in(String.to_list(l)), _u => Enc.wide_any(t), h) + case 1n+p: + nav.chars_narrow(t, nav.or_else_right(Enc.wide_in(String.to_list(l)), _u => Enc.wide_any(t), h), p) + +def Laws.enc_narrow(lines, h, line, nn): + +hc = nav.chars_narrow(lines, h, U32.to_nat(line)) + (nav.units_narrow(Enc.chars(lines, line), hc, nn), nav.points_narrow(Enc.chars(lines, line), hc, nn)) + diff --git a/src/lsp/enc.bend b/src/lsp/enc.bend index 4a4b34a..f9a6376 100644 --- a/src/lsp/enc.bend +++ b/src/lsp/enc.bend @@ -6,6 +6,7 @@ # server reads goes through `into`, and every one it sends through `out` # (proto.bend's position, semantic.bend's tokens). import Base +import ../lazy/lazy.bend as Lazy import 0x81c67699424929b5c44cd8577e18117f/main.bend as Ezjson import 0x81c67699424929b5c44cd8577e18117f/src/value.bend as J @@ -118,13 +119,44 @@ def into.of(ee: Enc, cs: List<&2, Char>, uu: Nat) -> Nat: case Utf32{}: uu -# a document as the boundary sees it: the encoding and the text's lines +# does a line hold a char past U+FFFF? Stops at the first +def 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 first +def 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 up +def 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 lines type Cols is Data: Cols{enc: Enc, lines: List<&2, String>} +# a document's lines under an encoding +def cols.of(ee: Enc, +lines: List<&2, String>) -> Cols: + Cols{narrowed(ee, wide_any(lines)), lines} + # a document's text under an encoding def cols(ee: Enc, text: String) -> Cols: - Cols{ee, String.lines(text)} + cols.of(ee, String.lines(text)) # a line's chars, none past the end def chars(lines: List<&2, String>, line: U32) -> List<&2, Char>: @@ -138,10 +170,19 @@ def out.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32: case Utf32{}: col +# a code-point column of a document's line, sent in an encoding; utf-32 +# never looks the line up +def 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 encoding def out(cc: Cols, line: U32, col: U32) -> U32: Cols{ee, lines} = cc - out.col(ee, chars(lines, line), col) + out.at(ee, lines, line, col) # a column of a line's chars read in an encoding, as a code-point column def into.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32: @@ -151,7 +192,16 @@ def into.col(ee: Enc, cs: List<&2, Char>, col: U32) -> U32: case Utf32{}: col +# a column of a document's line read in an encoding; utf-32 never looks the +# line up +def 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 column def into(cc: Cols, line: U32, col: U32) -> U32: Cols{ee, lines} = cc - into.col(ee, chars(lines, line), col) + into.at(ee, lines, line, col) diff --git a/src/lsp/semantic.bend b/src/lsp/semantic.bend index 019f512..ccb14bf 100644 --- a/src/lsp/semantic.bend +++ b/src/lsp/semantic.bend @@ -5,6 +5,7 @@ # from elsewhere is read by its shape: `Bool.pick` a function, `U32` a type, # `Nil{` a constructor. import Base +import ../lazy/lazy.bend as Lazy import ../syntax/lex.bend as Lex import ../syntax/bind.bend as Bind import ./enc.bend as Enc @@ -122,18 +123,153 @@ def head_bind_kind(binds: List<&2, Bind.Bind>) -> U32: case Con{Bind.Bind{n, l, c, k, note}, rest}: of_kind(k, n) +# a binder where the index keeps it: its name, position and kind +type Entry is Data: + Entry{name: String, line: U32, col: U32, kind: Bind.BindKind} + +# binders as a binary trie on the low bits of a key (a binder's line, or its +# name's hash), a leaf holding the entries that reach it in source order: a +# lookup is a walk down and a short scan, and finds what a scan of every +# binder from the front would, as a miss down the path is a miss everywhere +type Index is Data: + INone{} + ILeaf{es: List<&2, Entry>} + INode{lo: Index, hi: Index} + +# how many bits of a key the index branches on +def depth() -> Nat: + 16n + +# a key's way down the index: its low bits, lowest first +def path(dd: Nat, +key: U32) -> List<&2, Bool>: + match dd: + case 0n: + Nil{} + case 1n+p: + U32.is_even(key) <> path(p, U32.shr(key)) + +# the entries at a leaf, none elsewhere +def idx.es(ii: Index) -> List<&2, Entry>: + match ii: + case INone{}: + Nil{} + case ILeaf{es}: + es + case INode{_lo, _hi}: + Nil{} + +# the half of a node a bit goes down, empty elsewhere +def idx.near(bb: Bool, ii: Index) -> Index: + match ii: + case INone{}: + INone{} + case ILeaf{_es}: + INone{} + case INode{lo, hi}: + Bool.pick(Index, bb, lo, hi) + +# a node whose half down a bit is sub, and the other half far +def idx.join(bb: Bool, sub: Index, far: Index) -> Index: + match bb: + case True{}: + INode{sub, far} + case False{}: + INode{far, sub} + +# the index with an entry in front of the ones down its path +def idx.put(pp: List<&2, Bool>, +ii: Index, +ee: Entry) -> Index: + match pp: + case Nil{}: + ILeaf{ee <> idx.es(ii)} + case Con{+bb, rest}: + idx.join(bb, idx.put(rest, idx.near(bb, ii), ee), idx.near(Bool.not(bb), ii)) + +# the entries at the end of a key's path +def idx.find(pp: List<&2, Bool>, ii: Index) -> List<&2, Entry>: + match pp: + case Nil{}: + idx.es(ii) + case Con{bb, rest}: + idx.find(rest, idx.near(bb, ii)) + +# a name's key: its chars folded, base 31 +def hash(ss: String, +acc: U32) -> U32: + match ss: + case SNil{}: + acc + case SCon{c, t}: + hash(t, (acc * 31 + Char.to_u32(c) : U32)) + +# every binder, keyed by its line, in source order +def by_line(binds: List<&2, Bind.Bind>) -> Index: + match binds: + case Nil{}: + INone{} + case Con{Bind.Bind{name, +line, col, kind, _note}, rest}: + idx.put(path(depth(), line), by_line(rest), Entry{name, line, col, kind}) + +# an item or constructor into the index by its name's key; other binders pass +def by_name.one(+name: String, line: U32, col: U32, kk: Bind.BindKind, ii: Index) -> Index: + match kk: + case Bind.KItem{}: + idx.put(path(depth(), hash(name, 0)), ii, Entry{name, line, col, Bind.KItem{}}) + case Bind.KCtor{}: + idx.put(path(depth(), hash(name, 0)), ii, Entry{name, line, col, Bind.KCtor{}}) + case _other: + ii + +# the file's items and constructors, keyed by name, in source order +def by_name(binds: List<&2, Bind.Bind>) -> Index: + match binds: + case Nil{}: + INone{} + case Con{Bind.Bind{name, line, col, kind, _note}, rest}: + by_name.one(name, line, col, kind, by_name(rest)) + +# the first entry at a position, as Bind.kind_at finds it +def at.go(es: List<&2, Entry>, +line: U32, +col: U32) -> Maybe<&2, Bind.BindKind>: + match es: + case Nil{}: + None{} + case Con{Entry{_n, l, c, k}, rest}: + Lazy.stop(Maybe<&2, Bind.BindKind>, Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)), Some{k}, + _u => at.go(rest, line, col)) + +# the first entry of a name, as Bind.kind_of_item finds it +def named.go(es: List<&2, Entry>, +name: String) -> Maybe<&2, Bind.BindKind>: + match es: + case Nil{}: + None{} + case Con{Entry{n, _l, _c, k}, rest}: + Lazy.stop(Maybe<&2, Bind.BindKind>, Bind.same(n, name), Some{k}, _u => named.go(rest, name)) + +# a document's binders, indexed once for every use's lookup: by position, +# and its items and constructors by name +type Kinds is Data: + Kinds{at: Index, named: Index} + +# the kind of the binder at a position +def kind_at(kk: Kinds, +line: U32, col: U32) -> Maybe<&2, Bind.BindKind>: + Kinds{at, _named} = kk + at.go(idx.find(path(depth(), line), at), line, col) + +# the kind of an item or constructor of the file, by name +def kind_of_item(kk: Kinds, +name: String) -> Maybe<&2, Bind.BindKind>: + Kinds{_at, named} = kk + named.go(idx.find(path(depth(), hash(name, 0)), named), name) + # the type of a use, from what it refers to -def of_target(tg: Bind.Target, all: List<&2, Bind.Bind>, name: String, braced: Bool) -> U32: +def of_target(tg: Bind.Target, all: Kinds, name: String, braced: Bool) -> U32: match tg: case Bind.TLocal{tl, tc}: - of_maybe_kind(Bind.kind_at(all, tl, tc), name) + of_maybe_kind(kind_at(all, tl, tc), name) case Bind.TItem{i}: - of_maybe_kind(Bind.kind_of_item(all, i), name) + of_maybe_kind(kind_of_item(all, i), name) case other: by_shape(name, braced) # the type of the next use -def head_use_class(uses: List<&2, Bind.Use>, all: List<&2, Bind.Bind>, braced: Bool) -> U32: +def head_use_class(uses: List<&2, Bind.Use>, all: Kinds, braced: Bool) -> U32: match uses: case Nil{}: 5 @@ -161,7 +297,7 @@ type Step is Data: Step{typ: Maybe<&2, U32>, cur: Cursor} # the class of a name: the use that sits on its head, else its own shape -def use_class(+hu: Bool, +us: List<&2, Bind.Use>, +all: List<&2, Bind.Bind>, +name: String, +braced: Bool) -> U32: +def use_class(+hu: Bool, +us: List<&2, Bind.Use>, +all: Kinds, +name: String, +braced: Bool) -> U32: match hu: case True{}: head_use_class(us, all, braced) @@ -170,7 +306,7 @@ def use_class(+hu: Bool, +us: List<&2, Bind.Use>, +all: List<&2, Bind.Bind>, +na # a name token's type, taking the binder or the use that sits on it, and the # cursor after it -def name_step(cur: Cursor, +all: List<&2, Bind.Bind>, +name: String, +line: U32, +col: U32, +braced: Bool) -> Step: +def name_step(cur: Cursor, +all: Kinds, +name: String, +line: U32, +col: U32, +braced: Bool) -> Step: Cursor{+binds, +uses} = cur +bs = Bool.pick(List<&2, Bind.Bind>, behind_bind(binds, line, col), tail_binds(binds), binds) +us = Bool.pick(List<&2, Bind.Use>, behind_use(uses, line, col), tail_uses(uses), uses) @@ -186,7 +322,7 @@ def name_step(cur: Cursor, +all: List<&2, Bind.Bind>, +name: String, +line: U32, def of_tok( kk: Lex.TokKind, cur: Cursor, - all: List<&2, Bind.Bind>, + all: Kinds, name: String, line: U32, col: U32, @@ -231,7 +367,7 @@ def put(mm: Maybe<&2, U32>, +line: U32, +col: U32, +len: U32, rest: List<&2, Sem Sem{line, col, len, typ} <> rest # every token, in order, against the cursor -def classify(toks: List<&2, Lex.Tok>, cur: Cursor, +all: List<&2, Bind.Bind>) -> List<&2, Sem>: +def classify(toks: List<&2, Lex.Tok>, cur: Cursor, +all: Kinds) -> List<&2, Sem>: match toks: case Nil{}: Nil{} @@ -275,7 +411,7 @@ def encode(sems: List<&2, Sem>, +pl: U32, +pc: U32) -> List<&2, U32>: def data.of(ee: Enc.Enc, +lines: List<&2, String>, bb: Bind.Bound, toks: List<&2, Lex.Tok>) -> List<&2, U32>: Bind.Bound{+binds, uses, scopes} = bb - encode(sent(classify(toks, Cursor{binds, uses}, binds), ee, lines, 0), 0, 0) + encode(sent(classify(toks, Cursor{binds, uses}, Kinds{by_line(binds), by_name(binds)}), ee, lines, 0), 0, 0) # a document's semantic tokens, encoded, their columns and lengths in the # negotiated encoding diff --git a/src/syntax/bind.bend b/src/syntax/bind.bend index c522eea..1b95cde 100644 --- a/src/syntax/bind.bend +++ b/src/syntax/bind.bend @@ -1031,26 +1031,3 @@ def named_sites.go(uses: List<&2, Use>, +name: String) -> List<&2, Pos>: def named_sites(bb: Bound, +name: String) -> List<&2, Pos>: Bound{binds, uses, scopes} = bb named_sites.go(uses, name) - -# the kind of the binder at a position, for what a use looks like -def kind_at(binds: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, BindKind>: - match binds: - case Nil{}: - None{} - case Con{Bind{name, +l, +c, kind, note}, rest}: - +more = kind_at(rest, line, col) - Bool.pick(Maybe<&2, BindKind>, Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)), Some{kind}, more) - -# the kind of an item or constructor of the file, by name -def kind_of_item(binds: List<&2, Bind>, +name: String) -> Maybe<&2, BindKind>: - match binds: - case Nil{}: - None{} - case Con{Bind{+n, l, c, KItem{}, note}, rest}: - +more = kind_of_item(rest, name) - Bool.pick(Maybe<&2, BindKind>, String.eq(n, name), Some{KItem{}}, more) - case Con{Bind{+n, l, c, KCtor{}, note}, rest}: - +more = kind_of_item(rest, name) - Bool.pick(Maybe<&2, BindKind>, String.eq(n, name), Some{KCtor{}}, more) - case Con{other, rest}: - kind_of_item(rest, name) From 665c36859fa637cbe340f19ee0e5a7efddbc76b3 Mon Sep 17 00:00:00 2001 From: noah-emp <182041600+noah-emp@users.noreply.github.com> Date: Sat, 26 Sep 2026 12:05:43 -0400 Subject: [PATCH 2/3] docs(spec): BOLT-LSP-8, UTF-16 columns are code points on a line with no wide char enc_narrow proves it; it was tagged BOLT-LSP-7, whose row neither named it nor states it. Co-Authored-By: Claude Opus 5.5 --- SPEC.md | 1 + src/lsp/LAWS.bend | 2 +- src/lsp/README.md | 3 ++- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/SPEC.md b/SPEC.md index 407efb4..2decf0c 100644 --- a/SPEC.md +++ b/SPEC.md @@ -131,6 +131,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-LSP-5 | The checker never runs `main`. | Proved | proved | src/lsp/LAWS.bend check_only; src/lsp/LAWS.bend followup_check_only | | BOLT-LSP-6 | Hover, definition, references and completion answer from the binder (BOLT-SYN-5) over the open text and its relative imports. | Proved | proved | src/lsp/LAWS.bend nav_open_text; src/lsp/LAWS.bend nav_definition_binder; src/lsp/LAWS.bend nav_definition_local; src/lsp/LAWS.bend nav_definition_item; src/lsp/LAWS.bend nav_definition_import; src/lsp/LAWS.bend nav_definition_free; src/lsp/LAWS.bend nav_import_open; src/lsp/LAWS.bend nav_hover_use; src/lsp/LAWS.bend nav_hover_binder; src/lsp/LAWS.bend nav_hover_item; src/lsp/LAWS.bend nav_hover_own; src/lsp/LAWS.bend nav_references; src/lsp/LAWS.bend nav_completion; src/lsp/LAWS.bend nav_completion_import | | BOLT-LSP-7 | Positions are in the encoding the client negotiated. | Proved | proved | src/lsp/LAWS.bend enc_negotiated; src/lsp/LAWS.bend enc_advertised; src/lsp/LAWS.bend enc_kept; src/lsp/LAWS.bend enc_round; src/lsp/LAWS.bend enc_sent; src/lsp/LAWS.bend enc_read; src/lsp/LAWS.bend enc_tokens; src/lsp/LAWS.bend enc_utf32 | +| BOLT-LSP-8 | On a line with no character past U+FFFF, a UTF-16 column is the code-point column, both sent and read. | Proved | proved | src/lsp/LAWS.bend enc_narrow | ### Library (BOLT-LIB) diff --git a/src/lsp/LAWS.bend b/src/lsp/LAWS.bend index 571a15d..01058f4 100644 --- a/src/lsp/LAWS.bend +++ b/src/lsp/LAWS.bend @@ -891,7 +891,7 @@ law enc_utf32: # LAW: on lines with no char past U+FFFF, UTF-16 counts every column as a # code point, both ways: why Enc.cols converts such a document as utf-32 -# BOLT-LSP-7 +# BOLT-LSP-8 law enc_narrow: for +lines: List<&2, String> for h: {Enc.wide_any(lines) == False{} : Bool} diff --git a/src/lsp/README.md b/src/lsp/README.md index 7b2435e..f411a1e 100644 --- a/src/lsp/README.md +++ b/src/lsp/README.md @@ -79,7 +79,8 @@ Positions follow LSP 3.17's `positionEncoding`: initialize answers `utf-32` when the client offers it and `utf-16` otherwise, and `enc.bend` converts every character offset read or sent between bolt's code-point columns and the negotiated encoding (a char past U+FFFF is two UTF-16 units). On a line -with no such char the two agree (BOLT-LSP-7 in `LAWS.bend`). +with no such char the two agree (BOLT-LSP-8 in `LAWS.bend`), so a document +with none converts as utf-32 and never looks a line up. Completion offers what could finish the name being typed: `Alias.pre` from the file behind the alias; anything else from the document, its aliases and (once From 646381ab7c125123edf8552baaabef667442e693 Mon Sep 17 00:00:00 2001 From: noah-emp <182041600+noah-emp@users.noreply.github.com> Date: Sat, 26 Sep 2026 12:07:49 -0400 Subject: [PATCH 3/3] docs(spec): word BOLT-LSP-8 in UTF-16 units and characters, not code points Co-Authored-By: Claude Opus 5.5 --- SPEC.md | 2 +- src/lsp/LAWS.bend | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/SPEC.md b/SPEC.md index 2decf0c..12d2683 100644 --- a/SPEC.md +++ b/SPEC.md @@ -131,7 +131,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | BOLT-LSP-5 | The checker never runs `main`. | Proved | proved | src/lsp/LAWS.bend check_only; src/lsp/LAWS.bend followup_check_only | | BOLT-LSP-6 | Hover, definition, references and completion answer from the binder (BOLT-SYN-5) over the open text and its relative imports. | Proved | proved | src/lsp/LAWS.bend nav_open_text; src/lsp/LAWS.bend nav_definition_binder; src/lsp/LAWS.bend nav_definition_local; src/lsp/LAWS.bend nav_definition_item; src/lsp/LAWS.bend nav_definition_import; src/lsp/LAWS.bend nav_definition_free; src/lsp/LAWS.bend nav_import_open; src/lsp/LAWS.bend nav_hover_use; src/lsp/LAWS.bend nav_hover_binder; src/lsp/LAWS.bend nav_hover_item; src/lsp/LAWS.bend nav_hover_own; src/lsp/LAWS.bend nav_references; src/lsp/LAWS.bend nav_completion; src/lsp/LAWS.bend nav_completion_import | | BOLT-LSP-7 | Positions are in the encoding the client negotiated. | Proved | proved | src/lsp/LAWS.bend enc_negotiated; src/lsp/LAWS.bend enc_advertised; src/lsp/LAWS.bend enc_kept; src/lsp/LAWS.bend enc_round; src/lsp/LAWS.bend enc_sent; src/lsp/LAWS.bend enc_read; src/lsp/LAWS.bend enc_tokens; src/lsp/LAWS.bend enc_utf32 | -| BOLT-LSP-8 | On a line with no character past U+FFFF, a UTF-16 column is the code-point column, both sent and read. | Proved | proved | src/lsp/LAWS.bend enc_narrow | +| BOLT-LSP-8 | On a line with no character past U+FFFF, a column counted in UTF-16 units equals the column counted in characters, both sent and read. | Proved | proved | src/lsp/LAWS.bend enc_narrow | ### Library (BOLT-LIB) diff --git a/src/lsp/LAWS.bend b/src/lsp/LAWS.bend index 01058f4..1694574 100644 --- a/src/lsp/LAWS.bend +++ b/src/lsp/LAWS.bend @@ -889,8 +889,9 @@ law enc_utf32: {Enc.out(Enc.Cols{Enc.Utf32{}, lines}, line, col) == col : U32} & {Enc.into(Enc.Cols{Enc.Utf32{}, lines}, line, col) == col : U32} -# LAW: on lines with no char past U+FFFF, UTF-16 counts every column as a -# code point, both ways: why Enc.cols converts such a document as utf-32 +# LAW: on a line with no char past U+FFFF, a column counted in UTF-16 units +# equals the column counted in characters, both ways: why Enc.cols converts +# such a document as utf-32 # BOLT-LSP-8 law enc_narrow: for +lines: List<&2, String>