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.
3	import Base
4	
5	# the handle closed, and whatever was gathered
6	def 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
12	def 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
20	def 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
33	def 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
42	def 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
52	def 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
62	def 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
68	def 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
76	def 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
83	def 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
93	def 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
99	def text_of(got: Maybe<&2, String>) -> String:
100	  match got:
101	    case None{}:
102	      ""
103	    case Some{s}:
104	      s