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.
8	import Base
9	import ./service.bend as S
10	import ../frame.bend as Frame
11	
12	# the process's stdin and stdout, and the bytes read but not yet framed
13	type 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
17	def 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	
30	def 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	
43	def 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
53	def 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	
68	def 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
77	def recv(h2: Stdio) -> IO(Stdio & Maybe<&2, String>):  # noqa: L001 transport effect
78	  recv.loop(U32.to_nat(1000000), h2)
79	
80	def 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
85	def 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
93	def stdio.fd(nn: U32) -> IO(File):
94	  import "./fd.c"
95	  import "./fd.js"
96	
97	# the process's descriptors 0 and 1, wrapped
98	def 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
105	def new() -> S.Transport<Stdio>:  # noqa: L001 effect record
106	  S.Transport{recv, send}