src/io/file.bend

ezx@1.11.0.0 · 137 lines · 17 definitions

1# io/file: a whole file read or written in one call. Base gives an open handle
2# and chunked reads; this is the loop over them.
3import Base
4
5# the handle closed, and whatever was gathered
6def slurp.end(file: File, acc: String) -> IO(String):
7  do IO<String>:
8    File.close(file)
9    return acc
10
11# an empty chunk means the end of the file
12def slurp.cut(chunk: String, file: File, acc: String, rest: File -> String -> IO(String)) -> IO(String):
13  match chunk:
14    case SNil{}:
15      slurp.end(file, acc)
16    case SCon{c, t}:
17      rest(file, acc ++ SCon{c, t})
18
19# a failed read ends the file as surely as an empty one
20def slurp.more(
21  res: Result<&1, &1, U32 & String, String>,
22  file: File,
23  acc: String,
24  rest: File -> String -> IO(String)
25) -> IO(String):
26  match res:
27    case Fail{_e}:
28      slurp.end(file, acc)
29    case Done{chunk}:
30      slurp.cut(chunk, file, acc, rest)
31
32# the handle comes back paired with what it read
33def slurp.next(
34  got: File & Result<&1, &1, U32 & String, String>,
35  acc: String,
36  rest: File -> String -> IO(String)
37) -> IO(String):
38  (file, r) = got
39  slurp.more(r, file, acc, rest)
40
41# the whole file, read in chunks until one is empty, or the fuel is
42def slurp(fuel: Nat, file: File, acc: String) -> IO(String):
43  match fuel:
44    case 0n:
45      slurp.end(file, acc)
46    case 1n+f:
47      do IO<String>:
48        got : File & Result<&1, &1, U32 & String, String> <- File.read(file, 65536)
49        slurp.next(got, acc, fl => a => slurp(f, fl, a))
50
51# the reads a file with no size to go by may take: a pipe, a device or a
52# /proc file reports 0 bytes and a file past 4 GiB fails to report, so these
53# are read until they end, up to 100000 reads of 64 KiB, past any file ez reads
54def unsized() -> Nat:
55  U32.to_nat(100000)
56
57# a size of 0 is no size to go by; any other is read to
58def reads.given(none: Bool, bytes: U32) -> Nat:
59  match none:
60    case True{}:
61      unsized()
62    case False{}:
63      U32.to_nat(U32.add(U32.div(bytes, 65536), 2))
64
65# the reads a file of this many bytes takes: one for every 64 KiB, one for
66# the part past the last whole 64 KiB, and one to spare for a short read
67def reads(+bytes: U32) -> Nat:
68  reads.given(U32.is_zero(bytes), bytes)
69
70# the reads the size the host reported allows
71def reads.of(res: Result<&1, &1, U32 & String, U32>) -> Nat:
72  match res:
73    case Fail{_e}:
74      unsized()
75    case Done{bytes}:
76      reads(bytes)
77
78# a file read whole, with fuel enough for the size it reported
79def read.sized(got: File & Result<&1, &1, U32 & String, U32>) -> IO(String):
80  (file, r) = got
81  slurp(reads.of(r), file, "")
82
83# what an opened file holds, or nothing when it would not open
84def read.opened(res: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
85  match res:
86    case Fail{_e}:
87      IO.pure(Maybe<&2, String>, None{})
88    case Done{file}:
89      do IO<Maybe<&2, String>>:
90        got : File & Result<&1, &1, U32 & String, U32> <- File.size(file)
91        text : String <- read.sized(got)
92        return Some{text}
93
94# a file's text, or None when it cannot be opened
95def read(path: String) -> IO(Maybe<&2, String>):
96  do IO<Maybe<&2, String>>:
97    r : Result<&1, &1, U32 & String, File> <- File.open(path, "r")
98    read.opened(r)
99
100# whether a write reported success
101def write.ok(res: Result<&1, &1, U32 & String, Unit>) -> Bool:
102  match res:
103    case Fail{_e}:
104      False{}
105    case Done{_u}:
106      True{}
107
108# a write's outcome, once the handle is shut
109def write.done(written: File & Result<&1, &1, U32 & String, Unit>) -> IO(Bool):
110  (file, r) = written
111  do IO<Bool>:
112    File.close(file)
113    return write.ok(r)
114
115# the text written to an opened file
116def write.opened(res: Result<&1, &1, U32 & String, File>, text: String) -> IO(Bool):
117  match res:
118    case Fail{_e}:
119      IO.pure(Bool, False{})
120    case Done{file}:
121      do IO<Bool>:
122        w : File & Result<&1, &1, U32 & String, Unit> <- File.write(file, text)
123        write.done(w)
124
125# a file replaced with this text; False when it could not be written
126def write(path: String, text: String) -> IO(Bool):
127  do IO<Bool>:
128    r : Result<&1, &1, U32 & String, File> <- File.open(path, "w")
129    write.opened(r, text)
130
131# a file's text, or "" when there is none
132def text_of(got: Maybe<&2, String>) -> String:
133  match got:
134    case None{}:
135      ""
136    case Some{s}:
137      s