@@ -31,6 +31,22 @@ data FileHandle : (mode : Mode) -> Type where
3131 FH : File -> FileHandle mode
3232
3333||| Description of state transition operations on a file.
34+|||
35+||| +------------+-------------+----------------+----------------+----------------+
36+||| | Operation | State in | Mode in | State out | Mode out |
37+||| +------------+-------------+----------------+----------------+----------------+
38+||| | open | - | - | file handle | input paramater|
39+||| | close | file handle | any | - | - |
40+||| | eof | file handle | ValidModeRead | file handle | ValidModeRead |
41+||| | flush | file handle | any | file handle | unchanged |
42+||| | readLine | file handle | ValidModeRead | file handle | ValidModeRead |
43+||| | readChar | file handle | ValidModeRead | file handle | ValidModeRead |
44+||| | readFile | - | - | - | - |
45+||| | writeString| file handle | ValidModeWrite | file handle | ValidModeWrite |
46+||| | writeLine | file handle | ValidModeWrite | file handle | ValidModeWrite |
47+||| | writeFile | - | - | - | - |
48+||| +------------+-------------+----------------+----------------+----------------+
49+|||
3450public export
3551interface File (m : Type -> Type) where
3652 FileHandleI : Mode -> Type