@@ -153,7 +153,7 @@ file management follows a resource usage protocol with the following
154- When a file is closed, its handle should no longer be used
154- When a file is closed, its handle should no longer be used
156−These requirements can be expressed formally in , by creating a
156+These requirements can be expressed formally by creating a
157``FILE_IO`` effect parameterised over a file handle state, which is
157``FILE_IO`` effect parameterised over a file handle state, which is
158either empty, open for reading, or open for writing. The ``FILE_IO``
158either empty, open for reading, or open for writing. The ``FILE_IO``
159effect’s definition is given below. Note that this
159effect’s definition is given below. Note that this
@@ -173,7 +173,7 @@ to support random access files and better reporting of error conditions.
174 open : (fname : String)
174 open : (fname : String)
175 -> (m : Mode)
175 -> (m : Mode)
176− -> Eff Bool [FILE_IO ()]
176+ -> Eff Bool [FILE_IO ()]
177 (\res => [FILE_IO (case res of
177 (\res => [FILE_IO (case res of
178 True => OpenFile m
178 True => OpenFile m
179 False => ())])
179 False => ())])
@@ -191,7 +191,7 @@ In particular, consider the type of ``open``:
192 open : (fname : String)
192 open : (fname : String)
193 -> (m : Mode)
193 -> (m : Mode)
194− -> Eff Bool [FILE_IO ()]
194+ -> Eff Bool [FILE_IO ()]
195 (\res => [FILE_IO (case res of
195 (\res => [FILE_IO (case res of
196 True => OpenFile m
196 True => OpenFile m
197 False => ())])
197 False => ())])
@@ -207,7 +207,7 @@ we continue the protocol accordingly.
208 readFile : Eff (List String) [FILE_IO (OpenFile Read)]
208 readFile : Eff (List String) [FILE_IO (OpenFile Read)]
209 readFile = readAcc [] where
209 readFile = readAcc [] where
210− readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]
210+ readAcc : List String -> Eff (List String) [FILE_IO (OpenFile Read)]
211 readAcc acc = if (not !eof)
211 readAcc acc = if (not !eof)
212 then readAcc (!readLine :: acc)
212 then readAcc (!readLine :: acc)
213 else pure (reverse acc)
213 else pure (reverse acc)