diff --git a/SPEC.md b/SPEC.md index 407efb4..12d2683 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 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 c6cfa8f..1694574 100644 --- a/src/lsp/LAWS.bend +++ b/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} 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/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 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)