1	# src/file: a file's text, read whole, or None when it cannot be opened.
2	import Base
3	
4	# the handle closed, and whatever was gathered
5	def file.slurp.end(file: File, acc: String) -> IO(String):
6	  do IO<String>:
7	    File.close(file)
8	    return acc
9	
10	# an empty chunk means the end of the file
11	def file.slurp.cut(chunk: String, file: File, acc: String, rest: File -> String -> IO(String)) -> IO(String):
12	  match chunk:
13	    case SNil{}:
14	      file.slurp.end(file, acc)
15	    case SCon{c, t}:
16	      rest(file, acc ++ SCon{c, t})
17	
18	# a failed read ends the file as surely as an empty one
19	def file.slurp.more(
20	  res: Result<&1, &1, U32 & String, String>,
21	  file: File,
22	  acc: String,
23	  rest: File -> String -> IO(String)
24	) -> IO(String):
25	  match res:
26	    case Fail{_e}:
27	      file.slurp.end(file, acc)
28	    case Done{chunk}:
29	      file.slurp.cut(chunk, file, acc, rest)
30	
31	# the handle comes back paired with what it read
32	def file.slurp.next(
33	  got: File & Result<&1, &1, U32 & String, String>,
34	  acc: String,
35	  rest: File -> String -> IO(String)
36	) -> IO(String):
37	  (file, res) = got
38	  file.slurp.more(res, file, acc, rest)
39	
40	# the whole file, read in chunks until one is empty, or the fuel is
41	def file.slurp(fuel: Nat, file: File, acc: String) -> IO(String):
42	  match fuel:
43	    case 0n:
44	      file.slurp.end(file, acc)
45	    case 1n+f:
46	      do IO<String>:
47	        got : File & Result<&1, &1, U32 & String, String> <- File.read(file, 65536)
48	        file.slurp.next(got, acc, fl => a => file.slurp(f, fl, a))
49	
50	# what an opened file holds, or nothing when it would not open
51	def file.read.opened(res: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
52	  match res:
53	    case Fail{_e}:
54	      IO.pure(Maybe<&2, String>, None{})
55	    case Done{file}:
56	      do IO<Maybe<&2, String>>:
57	        text : String <- file.slurp(U32.to_nat(100000), file, "")
58	        return Some{text}
59	
60	# a file's text, or None when it cannot be opened
61	def file.read(path: String) -> IO(Maybe<&2, String>):
62	  do IO<Maybe<&2, String>>:
63	    res : Result<&1, &1, U32 & String, File> <- File.open(path, "r")
64	    file.read.opened(res)
65	
66	# a file's text, or "" when there is none
67	def file.text_of(got: Maybe<&2, String>) -> String:
68	  match got:
69	    case None{}:
70	      ""
71	    case Some{s}:
72	      s