src/lsp/transport/stdio.bend
bolt@1.19.0.0 · 102 lines · 0 definitions
1# transport/stdio: LSP's base protocol over stdin and stdout. Reads bytes (a
2# read may end inside a UTF-8 char, and Content-Length counts bytes), keeps
3# what is past the current message in buf.
4import Base
5import bolt@1.19.0.0/src/lsp/transport/service.bend as S
6import bolt@1.19.0.0/src/lsp/frame.bend as Frame
7
8# the process's stdin and stdout, and the bytes read but not yet framed
9type Stdio is Type: # noqa: L001 transport effect
10 Stdio{inp: File, out: File, buf: List<&2, U32>}
11
12# no bytes means the peer closed the pipe
13def recv.grown(
14 bytes: List<&2, U32>,
15 inp: File,
16 out: File,
17 buf: List<&2, U32>,
18 rest: Stdio -> IO(Stdio & Maybe<&2, String>)
19) -> IO(Stdio & Maybe<&2, String>):
20 match bytes:
21 case Nil{}:
22 IO.pure(Stdio & Maybe<&2, String>, (Stdio{inp, out, []}, None{}))
23 case Con{b, t}:
24 rest(Stdio{inp, out, List.append(&2, U32, buf, b <> t)})
25
26def recv.fed(
27 rr: Result<&1, &1, U32 & String, List<&2, U32>>,
28 inp: File,
29 out: File,
30 buf: List<&2, U32>,
31 rest: Stdio -> IO(Stdio & Maybe<&2, String>)
32) -> IO(Stdio & Maybe<&2, String>):
33 match rr:
34 case Fail{e}:
35 IO.pure(Stdio & Maybe<&2, String>, (Stdio{inp, out, []}, None{}))
36 case Done{bytes}:
37 recv.grown(bytes, inp, out, buf, rest)
38
39def recv.read(
40 got: File & Result<&1, &1, U32 & String, List<&2, U32>>,
41 out: File,
42 buf: List<&2, U32>,
43 rest: Stdio -> IO(Stdio & Maybe<&2, String>)
44) -> IO(Stdio & Maybe<&2, String>):
45 (inp, r) = got
46 recv.fed(r, inp, out, buf, rest)
47
48# a whole message is cut off the buffer; short of one, read and look again
49def recv.on(
50 cc: Frame.Cut,
51 inp: File,
52 out: File,
53 buf: List<&2, U32>,
54 rest: Stdio -> IO(Stdio & Maybe<&2, String>)
55) -> IO(Stdio & Maybe<&2, String>):
56 match cc:
57 case Frame.Whole{body, left}:
58 IO.pure(Stdio & Maybe<&2, String>, (Stdio{inp, out, left}, Some{Frame.decode(body)}))
59 case Frame.More{}:
60 do IO<Stdio & Maybe<&2, String>>:
61 got : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_bytes(inp, 65536)
62 recv.read(got, out, buf, rest)
63
64def recv.loop(fuel: Nat, h2: Stdio) -> IO(Stdio & Maybe<&2, String>):
65 match fuel:
66 case 0n:
67 IO.pure(Stdio & Maybe<&2, String>, (h2, None{}))
68 case 1n+f:
69 Stdio{inp, out, +buf} = h2
70 recv.on(Frame.cut(buf), inp, out, buf, hh => recv.loop(f, hh))
71
72# the fuel bounds the reads one message may take
73def recv(h2: Stdio) -> IO(Stdio & Maybe<&2, String>): # noqa: L001 transport effect
74 recv.loop(U32.to_nat(1000000), h2)
75
76def send.done(ww: File & Result<&1, &1, U32 & String, Unit>, inp: File, buf: List<&2, U32>) -> IO(Stdio):
77 (out, r) = ww
78 IO.pure(Stdio, Stdio{inp, out, buf})
79
80# a body, framed and written
81def send(h2: Stdio, body: String) -> IO(Stdio): # noqa: L001 transport effect
82 Stdio{inp, out, buf} = h2
83 do IO<Stdio>:
84 w : File & Result<&1, &1, U32 & String, Unit> <- File.write(out, Frame.wrap(body))
85 send.done(w, inp, buf)
86
87# a File for a descriptor the process already holds. Not File.open on
88# /dev/stdin: an editor may hand the server sockets, which no path opens
89def stdio.fd(nn: U32) -> IO(File):
90 import "./fd.c"
91 import "./fd.js"
92
93# the process's descriptors 0 and 1, wrapped
94def open() -> IO(Stdio): # noqa: L001 transport effect
95 do IO<Stdio>:
96 inp : File <- stdio.fd(0)
97 out : File <- stdio.fd(1)
98 return Stdio{inp, out, []}
99
100# the transport over stdio
101def new() -> S.Transport<Stdio>: # noqa: L001 effect record
102 S.Transport{recv, send}