src/io/file.bend
ezx@1.4.0.0 · 104 lines · 0 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# what an opened file holds, or nothing when it would not open
52def read.opened(res: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
53 match res:
54 case Fail{_e}:
55 IO.pure(Maybe<&2, String>, None{})
56 case Done{file}:
57 do IO<Maybe<&2, String>>:
58 text : String <- slurp(U32.to_nat(100000), file, "")
59 return Some{text}
60
61# a file's text, or None when it cannot be opened
62def read(path: String) -> IO(Maybe<&2, String>):
63 do IO<Maybe<&2, String>>:
64 r : Result<&1, &1, U32 & String, File> <- File.open(path, "r")
65 read.opened(r)
66
67# whether a write reported success
68def write.ok(res: Result<&1, &1, U32 & String, Unit>) -> Bool:
69 match res:
70 case Fail{_e}:
71 False{}
72 case Done{_u}:
73 True{}
74
75# a write's outcome, once the handle is shut
76def write.done(written: File & Result<&1, &1, U32 & String, Unit>) -> IO(Bool):
77 (file, r) = written
78 do IO<Bool>:
79 File.close(file)
80 return write.ok(r)
81
82# the text written to an opened file
83def write.opened(res: Result<&1, &1, U32 & String, File>, text: String) -> IO(Bool):
84 match res:
85 case Fail{_e}:
86 IO.pure(Bool, False{})
87 case Done{file}:
88 do IO<Bool>:
89 w : File & Result<&1, &1, U32 & String, Unit> <- File.write(file, text)
90 write.done(w)
91
92# a file replaced with this text; False when it could not be written
93def write(path: String, text: String) -> IO(Bool):
94 do IO<Bool>:
95 r : Result<&1, &1, U32 & String, File> <- File.open(path, "w")
96 write.opened(r, text)
97
98# a file's text, or "" when there is none
99def text_of(got: Maybe<&2, String>) -> String:
100 match got:
101 case None{}:
102 ""
103 case Some{s}:
104 s