3998c4f · Idris-dev · git.iko.soy

8||| A Dependent type to describe File Handles. File handles are

9||| parameterised with the current state of the file: Closed; Open for

10||| reading; and Open for writing.

11−|||

11+|||

12−||| @ m The file mode.

12+||| @ m The file mode.

13data OpenFile : (m : Mode) -> Type where

14 FH : File -> OpenFile m

15

21

22||| Here the protocol for resource access is defined as an effect.

23||| The state transitions diagram for the protocol is as follows:

24−|||

24+|||

25||| digraph G {

26−|||

26+|||

27||| empty; read; write; // States

28−|||

28+|||

29||| empty -> read [label="Open R"];

30||| read -> empty [label="Close"];

31||| read -> read [label="ReadLine"];

32||| read -> read [label="EOF"];

33−|||

33+|||

34||| empty -> write [label="Open W"];

35||| write -> empty [label="Close"];

36||| write -> write [label="WriteLine"];

37−|||

37+|||

38||| }

39data FileIO : Effect where

40 ||| Open a file with the specified mode.

41− |||

41+ |||

42 ||| Opening a file successful moves the state from 'empty' to the

43 ||| specified mode. If not successful the state is still 'empty'.

44− |||

44+ |||

45 ||| @ fname The file name to be opened.

46 ||| @ m The file mode.

47 Open : (fname: String)

51 False => ())

52

53 ||| Close a file.

54− |||

54+ |||

55 ||| Closing a file moves the state from Open to closed.

56− Close : sig FileIO () (OpenFile m) ()

56+ Close : sig FileIO () (OpenFile m) ()

57

58 ||| Read a line from the file.

59− |||

59+ |||

60 ||| Only files that are open for reading can be read.

61 ReadLine : sig FileIO String (OpenFile Read)

62−

62+

63 ||| Write a string to a file.

64− |||

64+ |||

65 ||| Only file that are open for writing can be written to.

66 WriteString : String -> sig FileIO () (OpenFile Write)

67

68 ||| End of file?

69− |||

69+ |||

70 ||| Only files open for reading can be tested for EOF

71 EOF : sig FileIO Bool (OpenFile Read)

72

76instance Handler FileIO IO where

77 handle () (Open fname m) k = do h <- openFile fname m

78 valid <- validFile h

79− if valid then k True (FH h)

79+ if valid then k True (FH h)

80 else k False ()

81 handle (FH h) Close k = do closeFile h

82 k () ()

112--

113

114||| Open a file with the specified mode.

115−|||

115+|||

116||| @ fname The file name to be opened.

117||| @ m The file mode.

118open : (fname : String)

119 -> (m : Mode)

120− -> Eff Bool [FILE_IO ()]

120+ -> Eff Bool [FILE_IO ()]

121 (\res => [FILE_IO (case res of

122 True => OpenFile m

123 False => ())])

144eof : Eff Bool [FILE_IO (OpenFile Read)]

145eof = call $ EOF

146

147+||| Read a complete file, returning a user defined error if

148+||| unsuccesful.

149+|||

150+readFile : (errFunc : String -> e)

151+ -> (fname : String)

152+ -> Eff (Either e String) [FILE_IO ()]

153+readFile errFunc fname = do

154+ case !(open fname Read) of

155+ False => pure $ Left (errFunc fname)

156+ True => do

157+ src <- readAcc ""

158+ close

159+ pure $ Right src

160+ where

161+ readAcc : String -> Eff String [FILE_IO (OpenFile Read)]

162+ readAcc acc = if (not !(eof))

163+ then readAcc (acc ++ !(readLine))

164+ else pure acc

165+

166+||| Write a file containing the provided string, returning a user

167+||| defined error if unsuccesful.

168+|||

169+writeFile : (errFunc : String -> e)

170+ -> (fname : String)

171+ -> (content : String)

172+ -> Eff (Either e ()) [FILE_IO ()]

173+writeFile errFunc fname content = do

174+ case !(open fname Write) of

175+ True => do

176+ writeString content

177+ close

178+ pure $ Right ()

179+ False => pure $ Left (errFunc fname)

180+

181+

182+namespace Default

183+ readFile : String -> Eff (Either String String) [FILE_IO ()]

184+ readFile = File.readFile id

185+

186+ writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]

187+ writeFile = File.writeFile id

147-- --------------------------------------------------------------------- [ EOF ]

188-- --------------------------------------------------------------------- [ EOF ]