1	import Base
2	
3	# Files for the credential and roster stores. Base has no rename, chmod,
4	# unlink, readdir or mkdir, so those run /bin tools through Process.run
5	# (absolute path, literal argv, no shell). Failures are `(code, message)`
6	# like Base's own effects.
7	
8	def Res(-A: Type) -> Type:
9	  Result<&1, &1, U32 & String, A>
10	
11	def proc.timeout() -> U32:
12	  10000
13	
14	def proc.max() -> U32:
15	  1048576
16	
17	def tool.status(ok: Bool, status: U32, out: String, err: String) -> Res(String):
18	  match ok:
19	    case True{}:
20	      Done{out}
21	    case False{}:
22	      Fail{(status, err)}
23	
24	# Run a tool; Done{stdout} on exit status 0, else Fail{(status, stderr)}.
25	def tool.out(r: Result<&1, &1, U32 & String, U32 & (String & String)>) -> Res(String):
26	  match r:
27	    case Fail{e}:
28	      Fail{e}
29	    case Done{(+status, (out, err))}:
30	      tool.status(U32.is_eq(status, 0), status, out, err)
31	
32	def tool.unit(r: Res(String)) -> Res(Unit):
33	  match r:
34	    case Fail{e}:
35	      Fail{e}
36	    case Done{out}:
37	      Done{Unit{}}
38	
39	def tool(program: String, args: List<String>) -> IO(Res(String)):
40	  IO.bind(Result<&1, &1, U32 & String, U32 & (String & String)>, Res(String),
41	    Process.run(program, args, "", proc.max(), proc.timeout()),
42	    r => IO.pure(Res(String), tool.out(r)))
43	
44	def tool_unit(program: String, args: List<String>) -> IO(Res(Unit)):
45	  IO.bind(Res(String), Res(Unit), tool(program, args), r => IO.pure(Res(Unit), tool.unit(r)))
46	
47	# Run `next` only when the previous step worked.
48	def then(r: Res(Unit), next: IO(Res(Unit))) -> IO(Res(Unit)):
49	  match r:
50	    case Fail{e}:
51	      IO.pure(Res(Unit), Fail{e})
52	    case Done{u}:
53	      next
54	
55	# ---- read ----------------------------------------------------------------------
56	
57	def read.done(fr: File & Res(String)) -> IO(Res(String)):
58	  (f, r) = fr
59	  IO.bind(Unit, Res(String), File.close(f), u => IO.pure(Res(String), r))
60	
61	def read.sized2(f: File, r: Res(U32)) -> IO(Res(String)):
62	  match r:
63	    case Fail{e}:
64	      IO.bind(Unit, Res(String), File.close(f), u => IO.pure(Res(String), Fail{e}))
65	    case Done{n}:
66	      IO.bind(File & Res(String), Res(String), File.read(f, n), read.done)
67	
68	def read.sized(fr: File & Res(U32)) -> IO(Res(String)):
69	  (f, r) = fr
70	  read.sized2(f, r)
71	
72	def read.open(r: Res(File)) -> IO(Res(String)):
73	  match r:
74	    case Fail{e}:
75	      IO.pure(Res(String), Fail{e})
76	    case Done{f}:
77	      IO.bind(File & Res(U32), Res(String), File.size(f), read.sized)
78	
79	# The whole file as text. Fail{(errno, message)} when it cannot be read.
80	def read_file(path: String) -> IO(Res(String)):
81	  IO.bind(Res(File), Res(String), File.open(path, "r"), read.open)
82	
83	# ---- exists, list ----------------------------------------------------------------
84	
85	def exists.of(r: Result<&1, &1, U32 & String, U32 & (String & String)>) -> Bool:
86	  match r:
87	    case Fail{e}:
88	      False{}
89	    case Done{(+status, rest)}:
90	      U32.is_eq(status, 0)
91	
92	# Does the path exist (a file, directory or the target of a symlink)?
93	def exists(path: String) -> IO(Bool):
94	  IO.bind(Result<&1, &1, U32 & String, U32 & (String & String)>, Bool,
95	    Process.run("/bin/test", ["-e", path], "", proc.max(), proc.timeout()),
96	    r => IO.pure(Bool, exists.of(r)))
97	
98	def names.keep(empty: Bool, h: String, rest: List<&2, String>) -> List<&2, String>:
99	  match empty:
100	    case True{}:
101	      rest
102	    case False{}:
103	      h <> rest
104	
105	def names(ls: List<&2, String>) -> List<&2, String>:
106	  match ls:
107	    case Nil{}:
108	      []
109	    case Con{+h, t}:
110	      names.keep(String.is_empty(h), h, names(t))
111	
112	def list.of(r: Res(String)) -> Res(List<&2, String>):
113	  match r:
114	    case Fail{e}:
115	      Fail{e}
116	    case Done{out}:
117	      Done{names(String.lines(out))}
118	
119	# Entry names of a directory (hidden ones included, `.` and `..` not),
120	# in `ls` order. A name holding a newline is not representable.
121	def list_dir(path: String) -> IO(Res(List<&2, String>)):
122	  IO.bind(Res(String), Res(List<&2, String>), tool("/bin/ls", ["-1A", "--", path]),
123	    r => IO.pure(Res(List<&2, String>), list.of(r)))
124	
125	# ---- paths -------------------------------------------------------------------------
126	
127	def sel.s(c: Bool, x: String, y: String) -> String:
128	  match c:
129	    case True{}:
130	      x
131	    case False{}:
132	      y
133	
134	def slash.pick(hit: Bool, t: String, rest: String) -> String:
135	  match hit:
136	    case True{}:
137	      t
138	    case False{}:
139	      rest
140	
141	# Drop through the first `/` (the input is a reversed path).
142	def slash.drop(s: String) -> String:
143	  match s:
144	    case SNil{}:
145	      SNil{}
146	    case SCon{+c, +t}:
147	      slash.pick(Char.is_eq(c, '/'), t, slash.drop(t))
148	
149	def dirname.fin(s: String, absolute: Bool) -> String:
150	  match s:
151	    case SNil{}:
152	      sel.s(absolute, "/", ".")
153	    case _:
154	      s
155	
156	# Everything before the last `/`: "a/b/c" is "a/b", "/x" is "/", "x" is ".".
157	def dirname(+p: String) -> String:
158	  dirname.fin(String.reverse(slash.drop(String.reverse(p))), String.starts_with(p, "/"))
159	
160	
161	# ---- stdin -------------------------------------------------------------------------------
162	
163	def read.stdin(r: Res(File)) -> IO(Res(String)):
164	  match r:
165	    case Fail{e}:
166	      IO.pure(Res(String), Fail{e})
167	    case Done{f}:
168	      IO.bind(File & Res(String), Res(String), File.read(f, 1048576), read.done)
169	
170	# What is on standard input, up to 1 MiB, in one read: "" at end of file. The
171	# CLI reads stdin once (a token, a confirmation), so one read is enough.
172	def read_stdin() -> IO(Res(String)):
173	  IO.bind(Res(File), Res(String), File.open("/dev/stdin", "r"), read.stdin)