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