perf(lsp): semantic tokens up to 10x faster, symbols up to 2.8x on large files

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 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)
 

src/lsp/LAWS.bend

@@ -888,3 +888,15 @@ 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 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>
+  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}

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))
+

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

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)