0 | module System.Linux.TimerFD
  1 |
  2 | import Data.Bits
  3 | import Derive.Finite
  4 | import Derive.Prelude
  5 | import System.Linux.Error
  6 | import System.Linux.File
  7 | import public System.Clock
  8 |
  9 | %default total
 10 | %language ElabReflection
 11 |
 12 | --------------------------------------------------------------------------------
 13 | -- FFI
 14 | --------------------------------------------------------------------------------
 15 |
 16 | %foreign "C:ep_clock_realtime,epoll-idris"
 17 | ep_clock_realtime : Bits32
 18 |
 19 | %foreign "C:ep_clock_monotonic,epoll-idris"
 20 | ep_clock_monotonic : Bits32
 21 |
 22 | %foreign "C:ep_clock_boottime,epoll-idris"
 23 | ep_clock_boottime : Bits32
 24 |
 25 | %foreign "C:ep_clock_realtime_alarm,epoll-idris"
 26 | ep_clock_realtime_alarm : Bits32
 27 |
 28 | %foreign "C:ep_clock_boottime_alarm,epoll-idris"
 29 | ep_clock_boottime_alarm : Bits32
 30 |
 31 | %foreign "C:ep_tfd_cloexec,epoll-idris"
 32 | ep_tfd_cloexec : Bits32
 33 |
 34 | %foreign "C:ep_tfd_nonblock,epoll-idris"
 35 | ep_tfd_nonblock : Bits32
 36 |
 37 | %foreign "C:timerfd_create,epoll-idris"
 38 | prim__timerfd_create : Bits32 -> Bits32 -> PrimIO Bits32
 39 |
 40 | %foreign "C:ep_readTimer,epoll-idris"
 41 | prim__ep_readTimer : Bits32 -> PrimIO Bits64
 42 |
 43 | %foreign "C:ep_setTime,epoll-idris"
 44 | prim__ep_setTime : Bits32 -> Int64 -> Bits32 -> PrimIO ()
 45 |
 46 | --------------------------------------------------------------------------------
 47 | -- API
 48 | --------------------------------------------------------------------------------
 49 |
 50 | public export
 51 | data ClockTpe : Type where
 52 |   REALTIME       : ClockTpe
 53 |   MONOTONIC      : ClockTpe
 54 |   BOOTTIME       : ClockTpe
 55 |   REALTIME_ALARM : ClockTpe
 56 |   BOOTTIME_ALARM : ClockTpe
 57 |
 58 | %runElab derive "ClockTpe" [Show,Eq,Finite]
 59 |
 60 | export
 61 | clockCode : ClockTpe -> Bits32
 62 | clockCode REALTIME       = ep_clock_realtime
 63 | clockCode MONOTONIC      = ep_clock_monotonic
 64 | clockCode BOOTTIME       = ep_clock_boottime
 65 | clockCode REALTIME_ALARM = ep_clock_realtime_alarm
 66 | clockCode BOOTTIME_ALARM = ep_clock_boottime_alarm
 67 |
 68 | ||| Flags describing the behavior of an timer file descriptor.
 69 | |||
 70 | ||| Several flags can be combined using `(<+>)`.
 71 | export
 72 | record Flags where
 73 |   constructor F
 74 |   value : Bits32
 75 |
 76 | %runElab derive "Flags" [Show,Eq,Ord]
 77 |
 78 | export %inline
 79 | flagCode : Flags -> Bits32
 80 | flagCode = value
 81 |
 82 | export %inline
 83 | Semigroup Flags where
 84 |   F x <+> F y = F (x .|. y)
 85 |
 86 | export %inline
 87 | Monoid Flags where neutral = F 0
 88 |
 89 | export %inline
 90 | TFD_CLOEXEC : Flags
 91 | TFD_CLOEXEC = F ep_tfd_cloexec
 92 |
 93 | ||| Sets the file descriptor to non-blocking: Reading from
 94 | ||| an `TimerFD` via `readTimer` will usually block the calling thread
 95 | ||| unless the file descriptor's timer has already expired at least
 96 | ||| once.
 97 | |||
 98 | ||| With this flag being set, `readTimer` will never block but will return
 99 | ||| `Left EAGAIN` in case of a still running timer.
100 | export %inline
101 | TFD_NONBLOCK : Flags
102 | TFD_NONBLOCK = F ep_tfd_nonblock
103 |
104 | ||| A timer file descriptor that can be monitored via `epoll`.
105 | public export
106 | record TimerFD where
107 |   constructor TFD
108 |   file : Bits32
109 |
110 | export %inline
111 | FileDesc TimerFD where fileDesc = file
112 |
113 | ||| Creates a new `TimerFD` with the given initial value a flags set.
114 | export %inline
115 | timerCreate : ClockTpe -> Flags -> PrimIO TimerFD
116 | timerCreate c (F f) w =
117 |   let MkIORes file w := prim__timerfd_create (clockCode c) f w
118 |    in MkIORes (TFD file) w
119 |
120 | ||| Reads the current value from a timer file descriptor, returning the
121 | ||| number of times the timer has expired since the last read.
122 | |||
123 | ||| This will block the calling thread unless the `TFD_NONBLOCK` flag
124 | ||| was set.
125 | export %inline
126 | readTimer : TimerFD -> PrimIO (Either EpollErr Bits64)
127 | readTimer (TFD f) w =
128 |   let MkIORes v w := prim__ep_readTimer f w
129 |    in case v of
130 |         0 => getErr w
131 |         n => MkIORes (Right n) w
132 |
133 | export %inline
134 | setTime : TimerFD -> Clock Duration -> PrimIO ()
135 | setTime (TFD f) c =
136 |   prim__ep_setTime f (cast $ seconds c) (cast $ nanoseconds c)
137 |
138 | ||| Creates and finally closes and event file descriptor.
139 | export
140 | withTimer : ClockTpe -> Flags -> (TimerFD -> PrimIO a) -> PrimIO a
141 | withTimer ct fs f w =
142 |   let MkIORes tf  w := timerCreate ct fs w
143 |       MkIORes res w := f tf w
144 |       MkIORes _   w := close tf w
145 |    in MkIORes res w
146 |
147 | --------------------------------------------------------------------------------
148 | -- Syntax
149 | --------------------------------------------------------------------------------
150 |
151 | ||| The zero duration.
152 | export %inline
153 | zero : Clock Duration
154 | zero = makeDuration 0 0
155 |
156 | ||| Creates a duration of `n` seconds
157 | export
158 | (.s) : (n : Nat) -> Clock Duration
159 | n.s = makeDuration (cast n) 0
160 |
161 | ||| Creates a duration of `n` nanoseconds
162 | export
163 | (.ns) : (n : Nat) -> Clock Duration
164 | n.ns = makeDuration 0 (cast n)
165 |
166 | ||| Creates a duration of `n` microseconds
167 | export
168 | (.us) : (n : Nat) -> Clock Duration
169 | n.us = (n * 1_000).ns
170 |
171 | ||| Creates a duration of `n` milliseconds
172 | export
173 | (.ms) : (n : Nat) -> Clock Duration
174 | n.ms = (n * 1_000_000).ns
175 |