git.iko.soy/Idris-dev
on master help sign in
Updated comments according to review comments:
b4b4641Xefias
CHANGELOG.md+2
compare with master
unifiedsplit
@@ -66,6 +66,8 @@
66+ Removed several deprecated items from the libraries shipped with Idris.
66+ Removed several deprecated items from the libraries shipped with Idris.
67+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
67+ Moved `abs` from the `Neg` interface into its own `Abs` interface. `Nat`
68 implements `Abs` with `abs = id`.
68 implements `Abs` with `abs = id`.
69++ Added `Control.ST.File`, an ST based implementation of the same behaviour
70+ implemented by `Effect.File` in the effects package.
69
71
70## Tool Updates
72## Tool Updates
71
73
libs/contrib/Control/ST/File.idr+23−7
@@ -21,19 +21,25 @@ data ValidModeWrite : Mode -> Type where
21 VMWReadW : ValidModeWrite ReadWrite
21 VMWReadW : ValidModeWrite ReadWrite
22 VMWReadWT : ValidModeWrite ReadWriteTruncate
22 VMWReadWT : ValidModeWrite ReadWriteTruncate
23
23
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+|||
24public export
29public export
25data FileHandle : (mode : Mode) -> Type where
30data FileHandle : (mode : Mode) -> Type where
26 FH : File -> FileHandle mode
31 FH : File -> FileHandle mode
27
32
33+||| Description of state transition operations on a file.
28public export
34public export
29interface File (m : Type -> Type) where
35interface File (m : Type -> Type) where
30 FileHandleI : Mode -> Type
36 FileHandleI : Mode -> Type
31
37
32 ||| Open a file.
38 ||| Open a file.
33 |||
39 |||
34− ||| @ fname the filename.
40+ ||| @fname the filename.
35− ||| @ mode the mode; either Read, WriteTruncate, Append, ReadWrite,
41+ ||| @mode the mode; either Read, WriteTruncate, Append, ReadWrite,
36− ||| ReadWriteTruncate, or ReadAppend
42+ ||| ReadWriteTruncate, or ReadAppend
37 |||
43 |||
38 open : (fname : String)
44 open : (fname : String)
39 -> (mode : Mode)
45 -> (mode : Mode)
@@ -70,25 +76,35 @@ interface File (m : Type -> Type) where
70 ||| to while being read.
76 ||| to while being read.
71 |||
77 |||
72 ||| Returns an error if fname is not a normal file.
78 ||| Returns an error if fname is not a normal file.
79+ |||
73 readFile : (fileName : String)
80 readFile : (fileName : String)
74 -> ST m (Either FileError String) []
81 -> ST m (Either FileError String) []
75
82
76 ||| Write a complete line to the file.
83 ||| Write a complete line to the file.
84+ |||
85+ ||| @string The string to be written to file.
86+ |||
77 writeString : (fileHandle : Var)
87 writeString : (fileHandle : Var)
78 -> (string : String)
88 -> (string : String)
79 -> {auto prf : ValidModeWrite mode}
89 -> {auto prf : ValidModeWrite mode}
80 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
90 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
81
91
82 ||| Write a complete line to the file.
92 ||| Write a complete line to the file.
93+ |||
94+ ||| @string The text to be written to file.
95+ |||
83 writeLine : (fileHandle : Var)
96 writeLine : (fileHandle : Var)
84 -> (string : String)
97 -> (string : String)
85 -> {auto prf : ValidModeWrite mode}
98 -> {auto prf : ValidModeWrite mode}
86 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
99 -> ST m (Either FileError ()) [ fileHandle ::: (FileHandleI mode) ]
87
100
88− -- ||| Create a file and write contents to the file.
101+ ||| Create a file and write contents to the file.
89− -- writeFile
102+ |||
90− writeFile : (fileName : String)
103+ ||| @fname The fileName of the file.
104+ ||| @string The text to be written to file.
105+ |||
106+ writeFile : (fname : String)
91− -> (string : String)
107+ -> (string : String)
92 -> ST m (Either FileError ()) []
108 -> ST m (Either FileError ()) []
93
109
94public export
110public export
test/st001/test001.idr−11
@@ -10,17 +10,6 @@ increment : (x : Var) -> STrans m () [ x ::: State Int ]
10increment x = do num <- read x
10increment x = do num <- read x
11 write x (num + 1)
11 write x (num + 1)
12
12
13−{-TestFileIO : Type -> (ConsoleIO m, STFile m) => ST m () []-}
14−{-TestFileIO x = ?TestFileIO_rhs-}
15−
16−{-TestFileIO : Type -> Type-}
17−{-TestFileIO : (ConsoleIO m, STFile m) => ST m () []-}
18−
19−{-TestFileCount : Type-}
20−{-TestFileCount : ST m (Either FileError (List String)) -}
21− {-[ count ::: (State Int), -}
22− {-fileHandle ::: FileHandleI {m} mode ]-}
23−
24readFileCount : (ConsoleIO m, File m) =>
13readFileCount : (ConsoleIO m, File m) =>
25 (fileHandle : Var)
14 (fileHandle : Var)
26 -> (count : Var)
15 -> (count : Var)