@@ -21,19 +21,25 @@ data ValidModeWrite : Mode -> Type where
2121 VMWReadW : ValidModeWrite ReadWrite
2222 VMWReadWT : ValidModeWrite ReadWriteTruncate
2323
24+||| The file handle which will be used as a State Transition
25+||| resource in the `IO` and `IOExcept` implementations of `File`.
26+|||
27+||| @mode The `Mode` that the handle was generated under.
28+|||
2429public export
2530data FileHandle : (mode : Mode) -> Type where
2631 FH : File -> FileHandle mode
2732
33+||| Description of state transition operations on a file.
2834public export
2935interface File (m : Type -> Type) where
3036 FileHandleI : Mode -> Type
3137
3238 ||| Open a file.
3339 |||
34− ||| @ fname the filename.
35− ||| @ mode the mode; either Read, WriteTruncate, Append, ReadWrite,
36− ||| ReadWriteTruncate, or ReadAppend
40+ ||| @fname the filename.
41+ ||| @mode the mode; either Read, WriteTruncate, Append, ReadWrite,
42+ ||| ReadWriteTruncate, or ReadAppend
3743 |||
3844 open : (fname : String)
3945 -> (mode : Mode)
@@ -70,25 +76,35 @@ interface File (m : Type -> Type) where
7076 ||| to while being read.
7177 |||
7278 ||| Returns an error if fname is not a normal file.
79+ |||
7380 readFile : (fileName : String)
7481 -> ST m (Either FileError String) []
7582
7683 ||| Write a complete line to the file.
84+ |||
85+ ||| @string The string to be written to file.
86+ |||
7787 writeString : (fileHandle : Var)
7888 -> (string : String)
7989 -> {auto prf : ValidModeWrite mode}
8090 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
8191
8292 ||| Write a complete line to the file.
93+ |||
94+ ||| @string The text to be written to file.
95+ |||
8396 writeLine : (fileHandle : Var)
8497 -> (string : String)
8598 -> {auto prf : ValidModeWrite mode}
8699 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
87100
88− -- ||| Create a file and write contents to the file.
89− -- writeFile
90− writeFile : (fileName : String)
91− -> (string : String)
101+ ||| Create a file and write contents to the file.
102+ |||
103+ ||| @fname The fileName of the file.
104+ ||| @string The text to be written to file.
105+ |||
106+ writeFile : (fname : String)
107+ -> (string : String)
92108 -> ST m (Either FileError ()) []
93109
94110public export