0 | module System.Posix.Poll.Struct
  1 |
  2 | import Data.C.Ptr
  3 | import Derive.Prelude
  4 | import System.Posix.File.FileDesc
  5 | import System.Posix.Poll.Types
  6 |
  7 | %default total
  8 | %language ElabReflection
  9 |
 10 | --------------------------------------------------------------------------------
 11 | -- FFI
 12 | --------------------------------------------------------------------------------
 13 |
 14 | %foreign "C:get_pollfd_fd, posix-idris"
 15 | prim__get_pollfd_fd: AnyPtr -> PrimIO Bits32
 16 |
 17 | %foreign "C:set_pollfd_fd, posix-idris"
 18 | prim__set_pollfd_fd: AnyPtr -> Bits32 -> PrimIO ()
 19 |
 20 | %foreign "C:get_pollfd_events, posix-idris"
 21 | prim__get_pollfd_events: AnyPtr -> PrimIO Bits32
 22 |
 23 | %foreign "C:set_pollfd_events, posix-idris"
 24 | prim__set_pollfd_events: AnyPtr -> Bits32 -> PrimIO ()
 25 |
 26 | %foreign "C:get_pollfd_revents, posix-idris"
 27 | prim__get_pollfd_revents: AnyPtr -> PrimIO Bits32
 28 |
 29 | %foreign "C:set_pollfd_revents, posix-idris"
 30 | prim__set_pollfd_revents: AnyPtr -> Bits32 -> PrimIO ()
 31 |
 32 | --------------------------------------------------------------------------------
 33 | -- SPollFD
 34 | --------------------------------------------------------------------------------
 35 |
 36 | ||| A wrapper around a `struct pollfd` pointer.
 37 | export
 38 | record SPollFD (s : Type) where
 39 |   constructor PF
 40 |   ptr : AnyPtr
 41 |
 42 | export %inline
 43 | Struct SPollFD where
 44 |   swrap   = PF
 45 |   sunwrap = ptr
 46 |
 47 | public export %inline
 48 | SizeOf (SPollFD s) where
 49 |   sizeof_ = pollfd_size
 50 |
 51 | public export
 52 | 0 PollFD : Type
 53 | PollFD = SPollFD World
 54 |
 55 | ||| Reads the `fd` field of a `struct pollfd` pointer.
 56 | export %inline
 57 | pollfd : SPollFD s -> F1 s Fd
 58 | pollfd (PF p) t =
 59 |   let v # t := ffi (prim__get_pollfd_fd p) t
 60 |    in MkFd v # t
 61 |
 62 | ||| Sets the `fd` field of a `struct pollfd` pointer.
 63 | export %inline
 64 | setPollfd : SPollFD s -> Fd -> F1' s
 65 | setPollfd (PF p) (MkFd v) = ffi (prim__set_pollfd_fd p v)
 66 |
 67 | ||| Reads the `events` field of a `struct pollfd` pointer.
 68 | export %inline
 69 | events : SPollFD s -> F1 s PollEvent
 70 | events (PF p) t =
 71 |   let v # t := ffi (prim__get_pollfd_events p) t
 72 |    in PE v # t
 73 |
 74 | ||| Sets the `events` field of a `struct pollfd` pointer.
 75 | export %inline
 76 | setEvents : SPollFD s -> PollEvent -> F1' s
 77 | setEvents (PF p) (PE v) = ffi (prim__set_pollfd_events p v)
 78 |
 79 | ||| Reads the `revents` field of a `struct pollfd` pointer.
 80 | export %inline
 81 | revents : SPollFD s -> F1 s PollEvent
 82 | revents (PF p) t =
 83 |   let v # t := ffi (prim__get_pollfd_revents p) t
 84 |    in PE v # t
 85 |
 86 | ||| Sets the `revents` field of a `struct pollfd` pointer.
 87 | export %inline
 88 | setRevents : SPollFD s -> PollEvent -> F1' s
 89 | setRevents (PF p) (PE v) = ffi (prim__set_pollfd_revents p v)
 90 |
 91 | --------------------------------------------------------------------------------
 92 | -- PollPair
 93 | --------------------------------------------------------------------------------
 94 |
 95 | public export
 96 | record PollPair where
 97 |   constructor PP
 98 |   fd     : Fd
 99 |   events : PollEvent
100 |
101 | %runElab derive "PollPair" [Show,Eq]
102 |
103 | export
104 | pollResults : {n : _} -> CArray s n (SPollFD s) -> F1 s (List PollPair)
105 | pollResults arr = go [] n
106 |   where
107 |     go : List PollPair -> (m : Nat) -> (0 p : LTE m n) => F1 s (List PollPair)
108 |     go xs 0     t = xs # t
109 |     go xs (S k) t =
110 |       let spfd # t := getStructNat arr k t
111 |           fd   # t := pollfd spfd t
112 |           evs  # t := revents spfd t
113 |        in if evs == 0 then go xs k t else go (PP fd evs :: xs) k t
114 |
115 | export
116 | writeFiles : {n : _} -> CArray s n (SPollFD s) -> List PollPair -> F1' s
117 | writeFiles arr = go n
118 |   where
119 |     go : (m : Nat) -> (ix : Ix m n) => List PollPair -> F1' s
120 |     go (S k) (x::xs) t =
121 |       let spfd # t := getStructIx arr k t
122 |           _    # t := setPollfd spfd x.fd t
123 |           _    # t := setEvents spfd x.events t
124 |        in go k xs t
125 |     go _     _       t = () # t
126 |