0 | module System.Linux.Epoll
  1 |
  2 | import Data.Bits
  3 | import Data.Nat
  4 | import Derive.Finite
  5 | import Derive.Prelude
  6 | import public System.Linux.Error
  7 | import public System.Linux.File
  8 | import System.FFI
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- Events
 15 | --------------------------------------------------------------------------------
 16 |
 17 | export %foreign "C:ep_epollin,epoll-idris"
 18 | epollin : Bits32
 19 |
 20 | export %foreign "C:ep_epollout,epoll-idris"
 21 | epollout : Bits32
 22 |
 23 | export %foreign "C:ep_epollrdhup,epoll-idris"
 24 | epollrdhup : Bits32
 25 |
 26 | export %foreign "C:ep_epollpri,epoll-idris"
 27 | epollpri : Bits32
 28 |
 29 | export %foreign "C:ep_epollerr,epoll-idris"
 30 | epollerr : Bits32
 31 |
 32 | export %foreign "C:ep_epollhup,epoll-idris"
 33 | epollhup : Bits32
 34 |
 35 | ||| Type of events epoll can wait for.
 36 | |||
 37 | ||| For every file descriptor observed by epoll a
 38 | ||| combination of events can be watched for. Events
 39 | ||| can be combined via `(<+>)`.
 40 | export
 41 | record Events where
 42 |   constructor E
 43 |   value : Bits32
 44 |
 45 | %runElab derive "Events" [Show,Eq,Ord]
 46 |
 47 | export %inline
 48 | eventCode : Events -> Bits32
 49 | eventCode = value
 50 |
 51 | export %inline
 52 | Semigroup Events where
 53 |   E x <+> E y = E (x .|. y)
 54 |
 55 | ||| Event for observing if a file is ready for input, that is,
 56 | ||| `read` invoked with that file will not block.
 57 | export %inline
 58 | EPOLLIN : Events
 59 | EPOLLIN = E epollin
 60 |
 61 | ||| Event for observing if a file is ready for output, that is,
 62 | ||| `write` invoked with that file will not block.
 63 | export %inline
 64 | EPOLLOUT : Events
 65 | EPOLLOUT = E epollout
 66 |
 67 | export %inline
 68 | EPOLLRDHUP : Events
 69 | EPOLLRDHUP = E epollrdhup
 70 |
 71 | export %inline
 72 | EPOLLPRI : Events
 73 | EPOLLPRI = E epollpri
 74 |
 75 | export %inline
 76 | EPOLLERR : Events
 77 | EPOLLERR = E epollerr
 78 |
 79 | export %inline
 80 | EPOLLHUP : Events
 81 | EPOLLHUP = E epollhup
 82 |
 83 | --------------------------------------------------------------------------------
 84 | -- Flags
 85 | --------------------------------------------------------------------------------
 86 |
 87 | export %foreign "C:ep_epollet,epoll-idris"
 88 | epollet : Bits32
 89 |
 90 | export %foreign "C:ep_epolloneshot,epoll-idris"
 91 | epolloneshot : Bits32
 92 |
 93 | export %foreign "C:ep_epollwakeup,epoll-idris"
 94 | epollwakeup : Bits32
 95 |
 96 | export %foreign "C:ep_epollexclusive,epoll-idris"
 97 | epollexclusive : Bits32
 98 |
 99 | export
100 | record Flags where
101 |   constructor F
102 |   value : Bits32
103 |
104 | %runElab derive "Flags" [Show,Eq,Ord]
105 |
106 | export %inline
107 | flagCode : Flags -> Bits32
108 | flagCode = value
109 |
110 | export %inline
111 | Semigroup Flags where
112 |   F x <+> F y = F (x .|. y)
113 |
114 | export %inline
115 | Monoid Flags where
116 |   neutral = F 0
117 |
118 | export %inline
119 | EPOLLET : Flags
120 | EPOLLET = F epollet
121 |
122 | export %inline
123 | EPOLLONESHOT : Flags
124 | EPOLLONESHOT = F epolloneshot
125 |
126 | export %inline
127 | EPOLLWAKEUP : Flags
128 | EPOLLWAKEUP = F epollwakeup
129 |
130 | export %inline
131 | EPOLLEXCLUSIVE : Flags
132 | EPOLLEXCLUSIVE = F epollexclusive
133 |
134 | --------------------------------------------------------------------------------
135 | -- epoll utilities
136 | --------------------------------------------------------------------------------
137 |
138 | %foreign  "C:close,epoll-idris"
139 | prim__close : Bits32 -> PrimIO ()
140 |
141 | %foreign  "C:ep_epoll_add,epoll-idris"
142 | prim__epoll_add : Bits32 -> Bits32 -> Bits32 -> Bits32 -> PrimIO Int32
143 |
144 | %foreign  "C:ep_epoll_mod,epoll-idris"
145 | prim__epoll_mod : Bits32 -> Bits32 -> Bits32 -> Bits32 -> PrimIO Int32
146 |
147 | %foreign  "C:ep_epoll_del,epoll-idris"
148 | prim__epoll_del : Bits32 -> Bits32 -> PrimIO Int32
149 |
150 | %foreign  "C__collect_safe:epoll_wait,epoll-idris"
151 | prim__epoll_wait : Bits32 -> AnyPtr -> Bits32 -> Int32 -> PrimIO Int32
152 |
153 | %foreign  "C:epoll_create1,epoll-idris"
154 | prim__epoll_create1 : Bits32 -> PrimIO Int32
155 |
156 | %foreign  "C:ep_allocEvent,epoll-idris"
157 | prim__ep_allocEvent : PrimIO AnyPtr
158 |
159 | %foreign  "C:ep_getFile,epoll-idris"
160 | prim__ep_getFile : AnyPtr -> PrimIO Bits32
161 |
162 | %foreign  "C:ep_getEvents,epoll-idris"
163 | prim__ep_getEvents : AnyPtr -> PrimIO Bits32
164 |
165 | export
166 | record EpollEvent where
167 |   constructor EE
168 |   ptr : AnyPtr
169 |
170 | export
171 | record EpollEvents (n : Nat) where
172 |   constructor EES
173 |   ptr : AnyPtr
174 |
175 | export
176 | record EpollFD where
177 |   constructor EFD
178 |   file  : Bits32
179 |   event : AnyPtr
180 |
181 | export
182 | Show EpollFD where show = show . file
183 |
184 | parameters {0 a : Type}
185 |            {auto ef : FileDesc a}
186 |
187 |   ||| Adds, modifies, or removes interest in the given file descriptor
188 |   ||| at an epoll instance.
189 |   export %inline
190 |   epollAdd : EpollFD -> a -> Events -> Flags -> PrimIO (Either EpollErr ())
191 |   epollAdd (EFD ef _) f (E e) (F fl) w =
192 |     let MkIORes n w := prim__epoll_add ef fl (fileDesc f) e w
193 |      in checkErr n w
194 |
195 |   ||| Adds, modifies, or removes interest in the given file descriptor
196 |   ||| at an epoll instance.
197 |   export %inline
198 |   epollMod : EpollFD -> a -> Events -> Flags -> PrimIO (Either EpollErr ())
199 |   epollMod (EFD ef _) f (E e) (F fl) w =
200 |     let MkIORes n w := prim__epoll_mod ef fl (fileDesc f) e w
201 |      in checkErr n w
202 |
203 |   ||| Adds, modifies, or removes interest in the given file descriptor
204 |   ||| at an epoll instance.
205 |   export %inline
206 |   epollDel : EpollFD -> a -> PrimIO (Either EpollErr ())
207 |   epollDel (EFD ef _) f w =
208 |     let MkIORes n w := prim__epoll_del ef (fileDesc f) w
209 |      in checkErr n w
210 |
211 | ||| Creates a new epoll file descriptor that can be used to monitor
212 | ||| other file descriptors for readiness.
213 | export
214 | epollCreate : IO (Either EpollErr EpollFD)
215 | epollCreate =
216 |   fromPrim $ \w =>
217 |     let MkIORes res w := prim__epoll_create1 0 w
218 |      in case res of
219 |           -1 => getErr w
220 |           n  =>
221 |             let MkIORes ptr w := prim__ep_allocEvent w
222 |              in MkIORes (Right $ EFD (cast n) ptr) w
223 |
224 | public export
225 | data EpollRes : Type where
226 |   NoEv : EpollRes
227 |   Ev   : (file : Bits32) -> (ev : Events) -> EpollRes
228 |   Err  : EpollErr -> EpollRes
229 |
230 | %runElab derive "EpollRes" [Show,Eq]
231 |
232 | fromLeft : Either EpollErr Void -> EpollRes
233 | fromLeft (Left e) = Err e
234 | fromLeft (Right v) impossible
235 |
236 | export %inline
237 | epollClose : EpollFD -> PrimIO ()
238 | epollClose e = close e.file
239 |
240 | export
241 | epollWait : EpollFD -> (timeout : Int32) -> PrimIO EpollRes
242 | epollWait (EFD f p) timeout w=
243 |   let MkIORes n w := prim__epoll_wait f p 1 timeout w
244 |    in case n of
245 |         0 => MkIORes NoEv w
246 |         1 =>
247 |           let MkIORes f w := prim__ep_getFile p w
248 |               MkIORes e w := prim__ep_getEvents p w
249 |            in MkIORes (Ev f $ E e) w
250 |         _ =>
251 |           let MkIORes e w := getErr w
252 |            in MkIORes (fromLeft e) w
253 |
254 | export %inline
255 | epollWaitTimeout : EpollFD -> (ms : Bits32) -> PrimIO EpollRes
256 | epollWaitTimeout fd = epollWait fd . cast
257 |
258 | export %inline
259 | epollNoWait : EpollFD -> PrimIO EpollRes
260 | epollNoWait fd = epollWait fd 0
261 |