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	import Base
5	import ./service.bend as S
6	import ../frame.bend as Frame
7	
8	# the process's stdin and stdout, and the bytes read but not yet framed
9	type 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
13	def 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	
26	def 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	
39	def 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
49	def 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.Ready{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	
64	def 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
73	def recv(h2: Stdio) -> IO(Stdio & Maybe<&2, String>):  # noqa: L001 transport effect
74	  recv.loop(U32.to_nat(1000000), h2)
75	
76	def 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
81	def 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
89	def stdio.fd(nn: U32) -> IO(File):
90	  import "./fd.c"
91	  import "./fd.js"
92	
93	# the process's descriptors 0 and 1, wrapped
94	def 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
101	def new() -> S.Transport<Stdio>:  # noqa: L001 effect record
102	  S.Transport{recv, send}