@@ -31,6 +31,22 @@ data FileHandle : (mode : Mode) -> Type where
31 FH : File -> FileHandle mode
31 FH : File -> FileHandle mode
33||| Description of state transition operations on a file.
33||| Description of state transition operations on a file.
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+||| +------------+-------------+----------------+----------------+----------------+
34public export
50public export
35interface File (m : Type -> Type) where
51interface File (m : Type -> Type) where
36 FileHandleI : Mode -> Type
52 FileHandleI : Mode -> Type