git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
d732dedEdwin Brady
libs/effects/Effect/File.idr+85−14
compare with master
unifiedsplit
@@ -1,24 +1,78 @@
1+-- -------------------------------------------------------- [ Effectful FileIO ]
1module Effect.File
2module Effect.File
2
3
3import Effects
4import Effects
4import Control.IOExcept
5import Control.IOExcept
5
6
7+
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+|||
12+||| @ m The file mode.
6−data OpenFile : Mode -> Type where
13+data OpenFile : (m : Mode) -> Type where
7 FH : File -> OpenFile m
14 FH : File -> OpenFile m
8
15
9openOK : Mode -> Bool -> Type
16openOK : Mode -> Bool -> Type
10openOK m True = OpenFile m
17openOK m True = OpenFile m
11openOK m False = ()
18openOK m False = ()
12
19
20+-- ------------------------------------------------------------ [ The Protocol ]
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+|||
25+||| digraph G {
26+|||
27+||| empty; read; write; // States
28+|||
29+||| empty -> read [label="Open R"];
30+||| read -> empty [label="Close"];
31+||| read -> read [label="ReadLine"];
32+||| read -> read [label="EOF"];
33+|||
34+||| empty -> write [label="Open W"];
35+||| write -> empty [label="Close"];
36+||| write -> write [label="WriteLine"];
37+|||
38+||| }
13data FileIO : Effect where
39data FileIO : Effect where
40+ ||| Open a file with the specified mode.
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+ |||
45+ ||| @ fname The file name to be opened.
46+ ||| @ m The file mode.
47+ Open : (fname: String)
14− Open : String -> (m : Mode) ->
48+ -> (m : Mode)
49+ -> {() ==> {res} if res
50+ then OpenFile m
15− {() ==> {res} if res then OpenFile m else ()} FileIO Bool
51+ else ()} FileIO Bool
52+
53+ ||| Close a file.
54+ |||
55+ ||| Closing a file moves the state from Open to closed.
16− Close : {OpenFile m ==> ()} FileIO ()
56+ Close : {OpenFile m ==> ()} FileIO ()
17−
57+
58+ ||| Read a line from the file.
59+ |||
60+ ||| Only files that are open for reading can be read.
18− ReadLine : {OpenFile Read} FileIO String
61+ ReadLine : {OpenFile Read} FileIO String
62+
63+ ||| Write a line to a file.
64+ |||
65+ ||| Only file that are open for writing can be written to.
19− WriteLine : String -> {OpenFile Write} FileIO ()
66+ WriteLine : String -> {OpenFile Write} FileIO ()
67+
68+ ||| End of file?
69+ |||
70+ ||| Only files open for reading can be tested for EOF
20− EOF : {OpenFile Read} FileIO Bool
71+ EOF : {OpenFile Read} FileIO Bool
21−
72+
73+-- ------------------------------------------------------------ [ The Handlers ]
74+
75+--- An implementation of the resource access protocol for the IO Context.
22instance Handler FileIO IO where
76instance Handler FileIO IO where
23 handle () (Open fname m) k = do h <- openFile fname m
77 handle () (Open fname m) k = do h <- openFile fname m
24 valid <- validFile h
78 valid <- validFile h
@@ -33,30 +87,47 @@ instance Handler FileIO IO where
33 handle (FH h) EOF k = do e <- feof h
87 handle (FH h) EOF k = do e <- feof h
34 k e (FH h)
88 k e (FH h)
35
89
90+-- -------------------------------------------------------------- [ The Effect ]
36FILE_IO : Type -> EFFECT
91FILE_IO : Type -> EFFECT
37FILE_IO t = MkEff t FileIO
92FILE_IO t = MkEff t FileIO
38
93
94+-- ------------------------------------------------------------ [ The Bindings ]
95+--
96+-- Bind the IO context handlers to functions. These functions will run
97+-- in the IO context.
98+--
99+
100+||| Open a file with the specified mode.
101+|||
102+||| @ fname The file name to be opened.
103+||| @ m The file mode.
39open : Handler FileIO e =>
104open : Handler FileIO e =>
105+ (fname : String)
40− String -> (m : Mode) ->
106+ -> (m : Mode)
41− { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool
107+ -> { [FILE_IO ()] ==> [FILE_IO (if result
108+ then OpenFile m
109+ else ())] } Eff e Bool
42open f m = Open f m
110open f m = Open f m
43
111
112+
113+||| Close a file.
44close : Handler FileIO e =>
114close : Handler FileIO e =>
45 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
46close = Close
116close = Close
47
117
118+||| Read a line from the file.
48readLine : Handler FileIO e =>
119readLine : Handler FileIO e =>
49 { [FILE_IO (OpenFile Read)] } Eff e String
120 { [FILE_IO (OpenFile Read)] } Eff e String
50readLine = ReadLine
121readLine = ReadLine
51
122
123+||| Write a line to a file.
52writeLine : Handler FileIO e =>
124writeLine : Handler FileIO e =>
53 String -> { [FILE_IO (OpenFile Write)] } Eff e ()
125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()
54writeLine str = WriteLine str
126writeLine str = WriteLine str
55
127
128+||| End of file?
56eof : Handler FileIO e =>
129eof : Handler FileIO e =>
57 { [FILE_IO (OpenFile Read)] } Eff e Bool
130 { [FILE_IO (OpenFile Read)] } Eff e Bool
58eof = EOF
131eof = EOF
59
132
60−
133+-- --------------------------------------------------------------------- [ EOF ]
61−
62−
libs/prelude/Prelude/Fin.idr+6
@@ -98,6 +98,12 @@ instance MaxBound (Fin (S n)) where
98(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
98(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
99(+) (fS f) f' = fS (f + f')
99(+) (fS f) f' = fS (f + f')
100
100
101+||| Substract two Fins, keeping the bound of the minuend
102+(-) : Fin n -> Fin m -> Fin n
103+fZ - _ = fZ
104+f - fZ = f
105+(fS f) - (fS f') = weaken $ f - f'
106+
101||| Multiply two Fins, extending the bound
107||| Multiply two Fins, extending the bound
102(*) : Fin n -> Fin m -> Fin (n * m)
108(*) : Fin n -> Fin m -> Fin (n * m)
103(*) {n=Z} f f' = FinZElim f
109(*) {n=Z} f f' = FinZElim f
libs/prelude/Prelude/Vect.idr+8
@@ -381,6 +381,14 @@ nub = nubBy (==)
381-- Splitting and breaking lists
381-- Splitting and breaking lists
382--------------------------------------------------------------------------------
382--------------------------------------------------------------------------------
383
383
384+||| A tuple where the first element is a Vect of the n first elements and
385+||| the second element is a Vect of the remaining elements of the original Vect
386+||| It is equivalent to (take n xs, drop n xs)
387+||| @ m the index to split at
388+||| @ xs the Vect to split in two
389+splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)
390+splitAt n xs = (take n xs, drop n xs)
391+
384--------------------------------------------------------------------------------
392--------------------------------------------------------------------------------
385-- Predicates
393-- Predicates
386--------------------------------------------------------------------------------
394--------------------------------------------------------------------------------