1 # ezsys/src/sys: the effects. Every decision these make is src/step.bend's, 2 # src/clock.bend's or src/dir.bend's; this module runs the effects in order 3 # and acts on the answers (SYS-TRUST-4). The three effects of its own are 4 # foreign code, a C file and its JS twin each: a flush-and-rename 5 # (SYS-TRUST-1), the wall clock (SYS-TRUST-2) and a directory's names 6 # (SYS-TRUST-5). 7 import Base 8 import ./step.bend as Step 9 import ./clock.bend as Clock 10 import ./dir.bend as Dir 11 12 # flush `from` to disk, then rename it over `to` 13 def ezsys.rename( 14 from: String, 15 to: String 16 ) -> IO(Result<&1, &1, U32 & String, Unit>): 17 import "./effs/rename.c" 18 import "./effs/rename.js" 19 20 # whole seconds since 1970-01-01T00:00:00Z and the milliseconds past them 21 def ezsys.clock() -> IO(U32 & U32): 22 import "./effs/clock.c" 23 import "./effs/clock.js" 24 25 # the names in a directory as the host lists them, in its order 26 def ezsys.list( 27 path: String 28 ) -> IO(Result<&1, &1, U32 & String, List<&2, String>>): 29 import "./effs/dir.c" 30 import "./effs/dir.js" 31 32 # reads one file.read makes at most 33 def sys.read.fuel() -> Nat: 34 65536n 35 36 # close the file, then answer 37 def sys.read.end( 38 file: File, 39 answer: Result<&1, &1, U32 & String, String> 40 ) -> IO(Result<&1, &1, U32 & String, String>): 41 IO.bind(Unit, Result<&1, &1, U32 & String, String>, File.close(file), 42 _u => IO.pure(Result<&1, &1, U32 & String, String>, answer)) 43 44 # act on one read's step: read on, or close and answer 45 def sys.read.next( 46 file: File, 47 step: Step.Read, 48 rest: File -> String -> IO(Result<&1, &1, U32 & String, String>) 49 ) -> IO(Result<&1, &1, U32 & String, String>): 50 match step: 51 case Step.ReadMore{text}: 52 rest(file)(text) 53 case Step.ReadStop{answer}: 54 sys.read.end(file, answer) 55 56 # unpack a read's file and answer 57 def sys.read.un( 58 got: String, 59 rest: File -> String -> IO(Result<&1, &1, U32 & String, String>), 60 pair: File & Result<&1, &1, U32 & String, String> 61 ) -> IO(Result<&1, &1, U32 & String, String>): 62 (file, res) = pair 63 sys.read.next(file, Step.read.step(res, got), rest) 64 65 # read chunks until an empty one; fuel first, so the call is a decreasing one 66 def sys.read.go( 67 fuel: Nat, 68 file: File, 69 got: String, 70 +chunk: U32 71 ) -> IO(Result<&1, &1, U32 & String, String>): 72 match fuel: 73 case 0n: 74 sys.read.end(file, Step.read.spent()) 75 case 1n+f: 76 IO.bind(File & Result<&1, &1, U32 & String, String>, 77 Result<&1, &1, U32 & String, String>, 78 File.read(file, chunk), 79 pair => sys.read.un(got, fl => g => sys.read.go(f, fl, g, chunk), pair)) 80 81 # the file's size decides the chunk; a failed size is the answer 82 def sys.read.sized( 83 pair: File & Result<&1, &1, U32 & String, U32> 84 ) -> IO(Result<&1, &1, U32 & String, String>): 85 (file, res) = pair 86 match res: 87 case Fail{error}: 88 sys.read.end(file, Fail{error}) 89 case Done{size}: 90 sys.read.go(sys.read.fuel(), file, "", Step.read.chunk(size)) 91 92 # an opened file is sized and read; a failed open is the answer 93 def sys.read.opened( 94 res: Result<&1, &1, U32 & String, File> 95 ) -> IO(Result<&1, &1, U32 & String, String>): 96 match res: 97 case Fail{error}: 98 IO.pure(Result<&1, &1, U32 & String, String>, Fail{error}) 99 case Done{file}: 100 IO.bind(File & Result<&1, &1, U32 & String, U32>, 101 Result<&1, &1, U32 & String, String>, File.size(file), sys.read.sized) 102 103 # a whole file's text 104 def sys.read(path: String) -> IO(Result<&1, &1, U32 & String, String>): 105 IO.bind(Result<&1, &1, U32 & String, File>, 106 Result<&1, &1, U32 & String, String>, File.open(path, "r"), 107 sys.read.opened) 108 109 # close the file, then answer the write's result 110 def sys.write.done( 111 pair: File & Result<&1, &1, U32 & String, Unit> 112 ) -> IO(Result<&1, &1, U32 & String, Unit>): 113 (file, res) = pair 114 IO.bind(Unit, Result<&1, &1, U32 & String, Unit>, File.close(file), 115 _u => IO.pure(Result<&1, &1, U32 & String, Unit>, res)) 116 117 # write to an opened file; a failed open is the answer 118 def sys.write.opened( 119 text: String, 120 res: Result<&1, &1, U32 & String, File> 121 ) -> IO(Result<&1, &1, U32 & String, Unit>): 122 match res: 123 case Fail{error}: 124 IO.pure(Result<&1, &1, U32 & String, Unit>, Fail{error}) 125 case Done{file}: 126 IO.bind(File & Result<&1, &1, U32 & String, Unit>, 127 Result<&1, &1, U32 & String, Unit>, File.write(file, text), 128 sys.write.done) 129 130 # a file's whole text replaced (created when missing) 131 def sys.write( 132 path: String, 133 text: String 134 ) -> IO(Result<&1, &1, U32 & String, Unit>): 135 IO.bind(Result<&1, &1, U32 & String, File>, 136 Result<&1, &1, U32 & String, Unit>, File.open(path, "w"), 137 res => sys.write.opened(text, res)) 138 139 # rename the written temporary file, or answer the write's failure 140 def sys.save.next( 141 +path: String, 142 step: Step.Save 143 ) -> IO(Result<&1, &1, U32 & String, Unit>): 144 match step: 145 case Step.SaveMove{}: 146 ezsys.rename(Step.save.tmp(path), path) 147 case Step.SaveStop{error}: 148 IO.pure(Result<&1, &1, U32 & String, Unit>, Fail{error}) 149 150 # write `.tmp`, then rename it over path 151 def sys.save( 152 +path: String, 153 text: String 154 ) -> IO(Result<&1, &1, U32 & String, Unit>): 155 IO.bind(Result<&1, &1, U32 & String, Unit>, 156 Result<&1, &1, U32 & String, Unit>, sys.write(Step.save.tmp(path), text), 157 res => sys.save.next(path, Step.save.step(res))) 158 159 # an environment variable, or the fallback when it is unset 160 def sys.env(name: String, fallback: String) -> IO(String): 161 IO.bind(Result<&1, &1, U32 & String, String>, String, IO.get_env(name), 162 res => IO.pure(String, Step.env.pick(res, fallback))) 163 164 # the wall clock's ISO 8601 UTC text 165 def sys.now_iso() -> IO(String): 166 IO.bind(U32 & U32, String, ezsys.clock(), 167 now => IO.pure(String, Clock.time.iso.of(now))) 168 169 # a directory's names, less "." and "..", sorted; a failed read is the answer 170 def sys.list( 171 path: String 172 ) -> IO(Result<&1, &1, U32 & String, List<&2, String>>): 173 IO.bind(Result<&1, &1, U32 & String, List<&2, String>>, 174 Result<&1, &1, U32 & String, List<&2, String>>, ezsys.list(path), 175 res => IO.pure(Result<&1, &1, U32 & String, List<&2, String>>, 176 Dir.dir.step(res)))