1	# walk/disk: an effect (CPU event loop only): the names directly in a
2	# directory, whether a path is a directory, and the working directory
3	# relative paths are named from. A name that is itself a directory ends in
4	# "/"; "." and ".." are never in the list, and a directory that cannot be
5	# opened lists as empty. Order is the file system's; the lint planner
6	# (src/lint/plan.bend) sorts what it keeps.
7	#
8	# It is the real file system, through a foreign effect (dir.c, dir.js) that
9	# lists one directory: its names, one a line, a directory's name ending in
10	# "/"; one (cwd.c, cwd.js) that names the working directory; and Base's
11	# File, which tells a directory from a file.
12	#
13	# Trusted, not proved: the listing effect returns a directory's entries,
14	# marking directories with `/`, the OS tells the truth when `is_dir` asks
15	# whether a path is a folder, and the file read returns a file's text. They
16	# are foreign code, and the planner takes their answers as given.
17	import Base
18	
19	# every name directly in the directory, one a line
20	def walkdir.entries(dir: String) -> IO(String):
21	  import "./dir.c"
22	  import "./dir.js"
23	
24	# the named lines: the text ends in a newline, so the last line is empty
25	def named(ls: List<&2, String>) -> List<&2, String>:
26	  match ls:
27	    case Nil{}:
28	      Nil{}
29	    case Con{+l, t}:
30	      +more = named(t)
31	      Bool.pick(List<&2, String>, String.is_empty(l), more, l <> more)
32	
33	# a directory's entries, a directory marked by a `/`
34	def entries(dir: String) -> IO(List<&2, String>):  # noqa: L001 disk effect
35	  do IO<List<&2, String>>:
36	    text : String <- walkdir.entries(dir)
37	    return named(String.lines(text))
38	
39	# whether a first read failed as a directory's does (EISDIR, 21, in C and
40	# in node alike)
41	def is_dir.code(rr: Result<&1, &1, U32 & String, List<&2, U32>>) -> Bool:
42	  match rr:
43	    case Fail{e}:
44	      (code, _msg) = e
45	      U32.is_eq(code, 21)
46	    case Done{_bytes}:
47	      False{}
48	
49	# the file closed, and what its first read said
50	def is_dir.got(got: File & Result<&1, &1, U32 & String, List<&2, U32>>) -> IO(Bool):
51	  (file, rr) = got
52	  do IO<Bool>:
53	    File.close(file)
54	    return is_dir.code(rr)
55	
56	# a path that opened: read one byte and see; one that did not is no directory
57	def is_dir.opened(rr: Result<&1, &1, U32 & String, File>) -> IO(Bool):
58	  match rr:
59	    case Fail{_e}:
60	      IO.pure(Bool, False{})
61	    case Done{file}:
62	      do IO<Bool>:
63	        got : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_bytes(file, 1)
64	        is_dir.got(got)
65	
66	# whether a path is a directory: it opens, and reading it fails as a
67	# directory's read does. Base's File has no stat, and a directory opens for
68	# reading on both lanes.
69	def is_dir(path: String) -> IO(Bool):  # noqa: L001 disk effect
70	  do IO<Bool>:
71	    r : Result<&1, &1, U32 & String, File> <- File.open(path, "r")
72	    is_dir.opened(r)
73	
74	# the working directory, from the root; "" when it cannot be named
75	def walkdir.cwd() -> IO(String):
76	  import "./cwd.c"
77	  import "./cwd.js"
78	
79	# the working directory, from the root ("" when it cannot be named)
80	def cwd() -> IO(String):  # noqa: L001 disk effect
81	  walkdir.cwd()