files.bend
bend-kit-files@0.1.0.0 · 254 lines · 0 definitions
1# POSIX paths plus directory and metadata effects. Source: https://github.com/paymog/bend-kit/tree/main/files
2import Base
3
4# The path.* defs are pure and lexical: they never touch the disk.
5# The effects are thin OS calls; each failure is (errno, text).
6# import ./files/files.bend as Fs
7
8def path.is_absolute(p: String) -> Bool:
9 String.starts_with(p, "/")
10
11def path.join.rel(bare: Bool, a: String, b: String) -> String:
12 match bare:
13 case True{}:
14 a ++ b
15 case False{}:
16 a ++ "/" ++ b
17
18def path.join.if(abs: Bool, +a: String, b: String) -> String:
19 match abs:
20 case True{}:
21 b
22 case False{}:
23 path.join.rel(String.is_empty(a) || String.ends_with(a, "/"), a, b)
24
25# b when b is absolute; otherwise b under a.
26def path.join(a: String, +b: String) -> String:
27 path.join.if(path.is_absolute(b), a, b)
28
29def path.norm.pop.if(up: Bool, h: String, t: List<&2, String>) ->
30 List<&2, String>:
31 match up:
32 case True{}:
33 ".." <> (h <> t)
34 case False{}:
35 t
36
37# A ".." above the root is dropped; above a relative start it is kept.
38def path.norm.pop(stack: List<&2, String>, abs: Bool) -> List<&2, String>:
39 match stack:
40 case Nil{}:
41 Bool.pick(List<&2, String>, abs, Nil{}, [".."])
42 case Con{+h, t}:
43 path.norm.pop.if(String.eq(h, ".."), h, t)
44
45def path.norm.step(
46 skip: Bool, up: Bool, s: String, stack: List<&2, String>, abs: Bool
47) -> List<&2, String>:
48 match skip:
49 case True{}:
50 stack
51 case False{}:
52 match up:
53 case True{}:
54 path.norm.pop(stack, abs)
55 case False{}:
56 s <> stack
57
58# The kept segments, last first.
59def path.norm.go(segs: List<&2, String>, stack: List<&2, String>, +abs: Bool) ->
60 List<&2, String>:
61 match segs:
62 case Nil{}:
63 stack
64 case Con{+s, t}:
65 path.norm.go(t,
66 path.norm.step(String.eq(s, "") || String.eq(s, "."), String.eq(s, ".."),
67 s, stack, abs),
68 abs)
69
70def path.norm.fin(abs: Bool, body: String) -> String:
71 match abs:
72 case True{}:
73 "/" ++ body
74 case False{}:
75 match body:
76 case SNil{}:
77 "."
78 case SCon{h, t}:
79 SCon{h, t}
80
81# Drops empty and "." segments and resolves "..", as POSIX normpath does
82# (RFC 3986 §5.2.4 for paths), but always to one leading "/".
83def path.normalize(+p: String) -> String:
84 +abs = path.is_absolute(p)
85 path.norm.fin(abs,
86 String.join(List.reverse(&2, String,
87 path.norm.go(String.split(p, '/'), Nil{}, abs)), "/"))
88
89def path.parent(p: String) -> String:
90 +n = path.normalize(p)
91 path.norm.fin(path.is_absolute(n),
92 String.join(List.reverse(&2, String,
93 List.tail(&2, String, List.reverse(&2, String, String.split(n, '/')))), "/"))
94
95def path.file_name.fin(m: Maybe<&2, String>) -> String:
96 match m:
97 case None{}:
98 ""
99 case Some{+s}:
100 Bool.pick(String, String.eq(s, "."), "", s)
101
102# The last segment of the normalized path; "" for "/" and ".".
103def path.file_name(p: String) -> String:
104 path.file_name.fin(List.last(&2, String, String.split(path.normalize(p), '/')))
105
106def path.extension.fin(bare: Bool, ext: String) -> String:
107 match bare:
108 case True{}:
109 ""
110 case False{}:
111 ext
112
113def path.extension.go(rev: List<&2, String>) -> String:
114 match rev:
115 case Nil{}:
116 ""
117 case Con{ext, Nil{}}:
118 ""
119 case Con{ext, Con{prev, rest}}:
120 path.extension.fin(String.is_empty(prev) && List.is_empty(&2, String, rest),
121 ext)
122
123# The text after the file name's last ".", without the dot. A leading dot
124# does not start one: ".bashrc" has none.
125def path.extension(p: String) -> String:
126 path.extension.go(List.reverse(&2, String, String.split(path.file_name(p), '.')))
127
128type FileType is Data:
129 Regular{}
130 Directory{}
131 Other{}
132
133# mtime is whole seconds since the Unix epoch. size and mtime wrap at 2^32.
134type Info is Data:
135 Info{kind: FileType, size: U32, mtime: U32}
136
137# Entry names, NUL-separated, in the order the OS gives them.
138def list_dir.raw(path: String) -> IO(Result<&1, &1, U32 & String, String>):
139 import "./effs/files.c"
140 import "./effs/files.js"
141
142# (kind, size, mtime); kind 0 is a regular file, 1 a directory, 2 other.
143# Symbolic links are followed.
144def stat.raw(path: String) ->
145 IO(Result<&1, &1, U32 & String, U32 & U32 & U32>):
146 import "./effs/files.c"
147 import "./effs/files.js"
148
149def mkdir(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
150 import "./effs/files.c"
151 import "./effs/files.js"
152
153# Removes a file or an empty directory.
154def remove(path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
155 import "./effs/files.c"
156 import "./effs/files.js"
157
158def rename(from: String, to: String) ->
159 IO(Result<&1, &1, U32 & String, Unit>):
160 import "./effs/files.c"
161 import "./effs/files.js"
162
163# Creates a new, empty, private directory under the system temp dir.
164def temp_dir() -> IO(Result<&1, &1, U32 & String, String>):
165 import "./effs/files.c"
166 import "./effs/files.js"
167
168def list_dir.fin(r: Result<&1, &1, U32 & String, String>) ->
169 Result<&1, &1, U32 & String, List<&2, String>>:
170 match r:
171 case Fail{e}:
172 Fail{e}
173 case Done{s}:
174 Done{List.sort(~String, ~String.is_le,
175 List.filter(~String, ~(n => Bool.not(String.is_empty(n))),
176 String.split(s, Chr{0})))}
177
178# Entry names, without "." and "..", sorted.
179def list_dir(path: String) ->
180 IO(Result<&1, &1, U32 & String, List<&2, String>>):
181 do IO<Result<&1, &1, U32 & String, List<&2, String>>>:
182 r : Result<&1, &1, U32 & String, String> <- list_dir.raw(path)
183 return list_dir.fin(r)
184
185def stat.kind(+k: U32) -> FileType:
186 Bool.pick(FileType, U32.is_eq(k, 0), Regular{},
187 Bool.pick(FileType, U32.is_eq(k, 1), Directory{}, Other{}))
188
189def stat.fin(r: Result<&1, &1, U32 & String, U32 & U32 & U32>) ->
190 Result<&1, &1, U32 & String, Info>:
191 match r:
192 case Fail{e}:
193 Fail{e}
194 case Done{(k, size, mtime)}:
195 Done{Info{stat.kind(k), size, mtime}}
196
197def stat(path: String) -> IO(Result<&1, &1, U32 & String, Info>):
198 do IO<Result<&1, &1, U32 & String, Info>>:
199 r : Result<&1, &1, U32 & String, U32 & U32 & U32> <- stat.raw(path)
200 return stat.fin(r)
201
202def exists(path: String) -> IO(Bool):
203 do IO<Bool>:
204 r : Result<&1, &1, U32 & String, U32 & U32 & U32> <- stat.raw(path)
205 return Result.is_done(&1, &1, U32 & String, U32 & U32 & U32, r)
206
207def mkdir_all.dir(r: Result<&1, &1, U32 & String, Info>) ->
208 Result<&1, &1, U32 & String, Unit>:
209 match r:
210 case Fail{e}:
211 Fail{e}
212 case Done{Info{Directory{}, size, mtime}}:
213 Done{Unit{}}
214 case Done{i}:
215 Fail{(17, "File exists")}
216
217def mkdir_all.fail(exists: Bool, e: U32 & String,
218 k: IO(Result<&1, &1, U32 & String, Unit>)) ->
219 IO(Result<&1, &1, U32 & String, Unit>):
220 match exists:
221 case True{}:
222 k
223 case False{}:
224 IO.pure(Result<&1, &1, U32 & String, Unit>, Fail{e})
225
226def mkdir_all.step(r: Result<&1, &1, U32 & String, Unit>,
227 k: IO(Result<&1, &1, U32 & String, Unit>)) ->
228 IO(Result<&1, &1, U32 & String, Unit>):
229 match r:
230 case Fail{(+code, text)}:
231 mkdir_all.fail(U32.is_eq(code, 17), (code, text), k)
232 case Done{u}:
233 k
234
235def mkdir_all.go(segs: List<&2, String>, +at: String) ->
236 IO(Result<&1, &1, U32 & String, Unit>):
237 match segs:
238 case Nil{}:
239 do IO<Result<&1, &1, U32 & String, Unit>>:
240 r : Result<&1, &1, U32 & String, Info> <- stat(at)
241 return mkdir_all.dir(r)
242 case Con{s, t}:
243 +next = path.join(at, s)
244 do IO<Result<&1, &1, U32 & String, Unit>>:
245 r : Result<&1, &1, U32 & String, Unit> <- mkdir(next)
246 mkdir_all.step(r, mkdir_all.go(t, next))
247
248# Creates the directory and any missing parents. Succeeds when it is
249# already a directory; fails if a component is not a directory.
250def mkdir_all(+path: String) -> IO(Result<&1, &1, U32 & String, Unit>):
251 mkdir_all.go(
252 List.filter(~String, ~(n => Bool.not(String.eq(n, ""))),
253 String.split(path, '/')),
254 Bool.pick(String, path.is_absolute(path), "/", "."))