0 | module System.Posix.Time

  2 | import Data.C.Ptr

  4 | import Derive.Prelude

  6 | import System.Posix.File.ReadRes

  7 | import public Data.C.Integer

  8 | import public System.Clock

  9 | import public System.Posix.Errno

 10 | import public System.Posix.Time.Types

 11 | import public System.Posix.Timer.Types

 13 | %default total

 14 | %language ElabReflection

 16 | export %inline

 17 | (.secs) : Clock t -> TimeT

 18 | (.secs) = cast . seconds

 20 | export %inline

 21 | (.nsecs) : Clock t -> TimeT

 22 | (.nsecs) = cast . nanoseconds

 28 | namespace Timespec

 29 |   %foreign "C:get_tv_sec, posix-idris"

 30 |   prim__get_tv_sec: AnyPtr -> PrimIO TimeT

 32 |   %foreign "C:get_tv_nsec, posix-idris"

 33 |   prim__get_tv_nsec: AnyPtr -> PrimIO NsecT

 35 |   %foreign "C:set_tv_sec, posix-idris"

 36 |   prim__set_tv_sec: AnyPtr -> TimeT -> PrimIO ()

 38 |   %foreign "C:set_tv_nsec, posix-idris"

 39 |   prim__set_tv_nsec: AnyPtr -> NsecT -> PrimIO ()

 41 |   ||| A wrapper around a `struct timespec` pointer.

 42 |   export

 43 |   record STimespec (s : Type) where

 44 |     constructor TS

 45 |     ptr : AnyPtr

 47 |   export %inline

 48 |   Struct STimespec where

 49 |     swrap   = TS

 50 |     sunwrap = ptr

 52 |   public export %inline

 53 |   SizeOf (STimespec s) where

 54 |     sizeof_ = timespec_size

 56 |   public export

 57 |   0 IOTimespec : Type

 58 |   IOTimespec = STimespec World

 60 |   ||| Reads the `tv_sec` field of a `timespec` pointer.

 61 |   export %inline

 62 |   sec : STimespec s -> F1 s TimeT

 63 |   sec (TS p) = ffi (prim__get_tv_sec p)

 65 |   ||| Reads the `tv_nsec` field of a `timespec` pointer.

 66 |   export %inline

 67 |   nsec : STimespec s -> F1 s NsecT

 68 |   nsec (TS p) = ffi (prim__get_tv_nsec p)

 70 |   ||| Sets the `tv_sec` field of a `timespec` pointer.

 71 |   export %inline

 72 |   setSec : STimespec s -> TimeT -> F1 s ()

 73 |   setSec (TS p) t = ffi (prim__set_tv_sec p t)

 75 |   ||| Sets the `tv_nsec` field of a `timespec` pointer.

 76 |   export %inline

 77 |   setNsec : STimespec s -> NsecT -> F1 s ()

 78 |   setNsec (TS p) t = ffi (prim__set_tv_nsec p t)

 80 |   ||| Convert a `STimespec` to a `Clock t`

 81 |   export %inline

 82 |   toClock : {t : _} -> STimespec s -> F1 s (Clock t)

 83 |   toClock ts t =

 84 |     let x0 # t := sec ts t

 85 |         x1 # t := nsec ts t

 86 |      in MkClock (cast x0) (cast x1) # t

 88 |   export

 89 |   withTimespec : Clock t -> (IOTimespec -> EPrim a) -> EPrim a

 90 |   withTimespec cl f =

 91 |     withStruct STimespec $ \ts,t =>

 92 |       let _ # t := setSec ts (cast $ seconds cl) t

 93 |           _ # t := setNsec ts (cast $ nanoseconds cl) t

 94 |        in f ts t

 96 | export %inline %hint

 97 | convertClock : {t : _} -> Convert (Clock t)

 98 | convertClock = convStruct STimespec toClock

104 | namespace STimeval

106 |   %foreign "C:get_timeval_tv_sec, posix-idris"

107 |   get_timeval_tv_sec: AnyPtr -> PrimIO TimeT

109 |   %foreign "C:get_timeval_tv_usec, posix-idris"

110 |   get_timeval_tv_usec: AnyPtr -> PrimIO SusecondsT

112 |   %foreign "C:set_timeval_tv_sec, posix-idris"

113 |   set_timeval_tv_sec: AnyPtr -> TimeT -> PrimIO ()

115 |   %foreign "C:set_timeval_tv_usec, posix-idris"

116 |   set_timeval_tv_usec: AnyPtr -> SusecondsT -> PrimIO ()

118 |   %foreign "C:li_timeval, posix-idris"

119 |   prim__timeval : TimeT -> SusecondsT -> PrimIO AnyPtr

121 |   export

122 |   record STimeval (s : Type) where

123 |     constructor STV

124 |     ptr : AnyPtr

126 |   export %inline

127 |   Struct STimeval where

128 |     swrap   = STV

129 |     sunwrap = ptr

131 |   export %inline

132 |   SizeOf (STimeval s) where

133 |     sizeof_ = timeval_size

135 |   public export

136 |   0 IOTimeval : Type

137 |   IOTimeval = STimeval World

139 |   export %inline

140 |   sec : STimeval s -> F1 s TimeT

141 |   sec s = ffi $ get_timeval_tv_sec s.ptr

143 |   export %inline

144 |   usec : STimeval s -> F1 s SusecondsT

145 |   usec s = ffi $ get_timeval_tv_usec s.ptr

147 |   export %inline

148 |   setsec : STimeval s -> TimeT -> F1 s ()

149 |   setsec s v = ffi $ set_timeval_tv_sec s.ptr v

151 |   export %inline

152 |   setusec : STimeval s -> SusecondsT -> F1 s ()

153 |   setusec s v = ffi $ set_timeval_tv_usec s.ptr v

155 |   ||| Pure alternative to the `STimeval` struct.

156 |   public export

157 |   record Timeval where

158 |     constructor TV

159 |     sec  : TimeT

160 |     usec : SusecondsT

162 |   %runElab derive "Timeval" [Show,Eq]

164 |   export %inline

165 |   stimeval : Timeval -> F1 s (STimeval s)

166 |   stimeval (TV s u) t = let p # t := ffi (prim__timeval s u) t in STV p # t

168 |   export

169 |   timeval : STimeval s -> F1 s Timeval

170 |   timeval stv t =

171 |     let sec  # t := STimeval.sec stv t

172 |         usec # t := STimeval.usec stv t

173 |      in TV sec usec # t

175 | export %inline %hint

176 | convertTimeval : Convert Timeval

177 | convertTimeval = convStruct STimeval timeval

183 | namespace Itimerval

184 |   %foreign "C:get_itimerval_it_interval, posix-idris"

185 |   get_itimerval_it_interval: AnyPtr -> PrimIO AnyPtr

187 |   %foreign "C:get_itimerval_it_value, posix-idris"

188 |   get_itimerval_it_value: AnyPtr -> PrimIO AnyPtr

190 |   %foreign "C:set_itimerval_it_interval, posix-idris"

191 |   set_itimerval_it_interval: AnyPtr -> AnyPtr -> PrimIO ()

193 |   %foreign "C:set_itimerval_it_value, posix-idris"

194 |   set_itimerval_it_value: AnyPtr -> AnyPtr -> PrimIO ()

196 |   %foreign "C:li_itimerval, posix-idris"

197 |   prim__itimerval : TimeT -> SusecondsT -> TimeT -> SusecondsT -> PrimIO AnyPtr

199 |   export

200 |   record Itimerval (s : Type) where

201 |     constructor ITV

202 |     ptr : AnyPtr

204 |   export %inline

205 |   Struct Itimerval where

206 |     swrap   = ITV

207 |     sunwrap = ptr

209 |   export %inline

210 |   SizeOf (Itimerval s) where

211 |     sizeof_ = itimerval_size

213 |   public export

214 |   0 IOTimerval : Type

215 |   IOTimerval = Itimerval World

217 |   export %inline

218 |   interval : Itimerval s -> F1 s (STimeval s)

219 |   interval s t = mapR1 STV $ ffi (get_itimerval_it_interval s.ptr) t

221 |   export %inline

222 |   value : Itimerval s -> F1 s (STimeval s)

223 |   value s t = mapR1 STV $ ffi (get_itimerval_it_value s.ptr) t

225 |   export %inline

226 |   setinterval : Itimerval s -> STimeval s -> F1 s ()

227 |   setinterval s v = ffi $ set_itimerval_it_interval s.ptr v.ptr

229 |   export %inline

230 |   setvalue : Itimerval s -> STimeval s -> F1 s ()

231 |   setvalue s v = ffi $ set_itimerval_it_value s.ptr v.ptr

233 |   ||| Pure alternative to the `Itimerval` struct.

234 |   public export

235 |   record Timerval where

236 |     constructor TRV

237 |     interval : Timeval

238 |     value    : Timeval

240 |   %runElab derive "Timerval" [Show,Eq]

242 |   ||| Creates and sets the fields of a `Itimerval` pointer.

245 |   export %inline

246 |   itimerval : Timerval -> F1 s (Itimerval s)

247 |   itimerval (TRV (TV si ui) (TV sv uv)) t =

248 |     mapR1 ITV $ ffi (prim__itimerval si ui sv uv) t

250 |   export

251 |   timerval : Itimerval s -> F1 s Timerval

252 |   timerval itv t =

253 |     let siv  # t := Itimerval.interval itv t

254 |         iv   # t := timeval siv t

255 |         sval # t := Itimerval.value itv t

256 |         val  # t := timeval sval t

257 |      in TRV iv val # t

259 | export %inline %hint

260 | convertTimerval : Convert Timerval

261 | convertTimerval = convStruct Itimerval timerval

267 | namespace Itimerspec

268 |   export %foreign "C:get_itimerspec_it_interval, posix-idris"

269 |   get_itimerspec_it_interval: AnyPtr -> PrimIO AnyPtr

271 |   export %foreign "C:get_itimerspec_it_value, posix-idris"

272 |   get_itimerspec_it_value: AnyPtr -> PrimIO AnyPtr

274 |   export %foreign "C:set_itimerspec_it_interval, posix-idris"

275 |   set_itimerspec_it_interval: AnyPtr -> AnyPtr -> PrimIO ()

277 |   export %foreign "C:set_itimerspec_it_value, posix-idris"

278 |   set_itimerspec_it_value: AnyPtr -> AnyPtr -> PrimIO ()

280 |   %foreign "C:li_itimerspec, posix-idris"

281 |   prim__itimerspec : TimeT -> NsecT -> TimeT -> NsecT -> PrimIO AnyPtr

283 |   ||| Note: Also this is POSIX compliant, it is not available on

286 |   export

287 |   record Itimerspec (s : Type) where

288 |     constructor ITS

289 |     ptr : AnyPtr

291 |   export %inline

292 |   Struct Itimerspec where

293 |     swrap   = ITS

294 |     sunwrap = ptr

296 |   export %inline

297 |   SizeOf (Itimerspec s) where

298 |     sizeof_ = itimerspec_size

300 |   public export

301 |   0 IOTimerspec : Type

302 |   IOTimerspec = Itimerspec World

304 |   namespace Itimerspec

305 |     export %inline

306 |     interval : Itimerspec s -> F1 s (STimespec s)

307 |     interval s t = mapR1 wrap $ ffi (get_itimerspec_it_interval s.ptr) t

309 |     export %inline

310 |     value : Itimerspec s -> F1 s (STimespec s)

311 |     value s t = mapR1 wrap $ ffi (get_itimerspec_it_value s.ptr) t

313 |     export %inline

314 |     setinterval : Itimerspec s -> STimespec s -> F1 s ()

315 |     setinterval s v = ffi $ set_itimerspec_it_interval s.ptr (unwrap v)

317 |     export %inline

318 |     setvalue : Itimerspec s -> STimespec s -> F1 s ()

319 |     setvalue s v = ffi $ set_itimerspec_it_value s.ptr (unwrap v)

321 |   ||| Creates and sets the fields of a `Itimerspec` pointer.

324 |   export %inline

325 |   itimerspec :

326 |        (secInterval  : TimeT)

327 |     -> (usecInterval : NsecT)

328 |     -> (secValue     : TimeT)

329 |     -> (usecValue    : NsecT)

330 |     -> F1 s (Itimerspec s)

331 |   itimerspec si ni sv nv t =

332 |     mapR1 ITS $ ffi (prim__itimerspec si ni sv nv) t

334 |   ||| Pure alternative to the `Itimerspec` struct.

335 |   public export

336 |   record Timerspec where

337 |     constructor TS

338 |     interval : Clock Duration

339 |     value    : Clock Duration

341 |   %runElab derive "Timerspec" [Show,Eq]

343 |   export

344 |   timerspec : Itimerspec s -> F1 s Timerspec

345 |   timerspec its t =

346 |     let siv  # t := Itimerspec.interval its t

347 |         iv   # t := toClock siv t

348 |         sval # t := Itimerspec.value its t

349 |         val  # t := toClock sval t

350 |      in TS iv val # t

352 |   export

353 |   duration : TimeT -> NsecT -> Clock Duration

354 |   duration s ns = makeDuration (cast s) (cast ns)

356 | export %inline %hint

357 | convTimerspec : Convert Timerspec

358 | convTimerspec = convStruct Itimerspec timerspec

364 | namespace STm

365 |   export %foreign "C:get_tm_sec, posix-idris"

366 |   get_tm_sec: AnyPtr -> PrimIO Bits8

368 |   export %foreign "C:get_tm_min, posix-idris"

369 |   get_tm_min: AnyPtr -> PrimIO Bits8

371 |   export %foreign "C:get_tm_hour, posix-idris"

372 |   get_tm_hour: AnyPtr -> PrimIO Bits8

374 |   export %foreign "C:get_tm_mday, posix-idris"

375 |   get_tm_mday: AnyPtr -> PrimIO Bits8

377 |   export %foreign "C:get_tm_mon, posix-idris"

378 |   get_tm_mon: AnyPtr -> PrimIO Bits8

380 |   export %foreign "C:get_tm_year, posix-idris"

381 |   get_tm_year: AnyPtr -> PrimIO Int32

383 |   export %foreign "C:get_tm_wday, posix-idris"

384 |   get_tm_wday: AnyPtr -> PrimIO Bits8

386 |   export %foreign "C:get_tm_yday, posix-idris"

387 |   get_tm_yday: AnyPtr -> PrimIO Bits16

389 |   export %foreign "C:get_tm_isdst, posix-idris"

390 |   get_tm_isdst: AnyPtr -> PrimIO Int8

392 |   export %foreign "C:li_gmtime_r, posix-idris"

393 |   prim__gmtime_r: TimeT -> AnyPtr -> PrimIO ()

395 |   export %foreign "C:li_localtime_r, posix-idris"

396 |   prim__localtime_r: TimeT -> AnyPtr -> PrimIO ()

398 |   ||| Converts time to a nicely formatted string.

399 |   export %foreign "C:li_ctime_r, posix-idris"

400 |   ctime: TimeT -> String

402 |   export %foreign "C:li_asctime_r, posix-idris"

403 |   prim__asctime_r: (sec,min,hour,mday,mon : Bits8) -> (year : Int32) -> (wday : Bits8) -> (yday : Bits16) -> (isdst : Int8) -> String

405 |   export %foreign "C:li_mktime, posix-idris"

406 |   prim__mktime: (sec,min,hour,mday,mon : Bits8) -> (year : Int32) -> (wday : Bits8) -> (yday : Bits16) -> (isdst : Int8) -> TimeT

408 |   ||| Note: Although this is POSIX compliant, it is not available on

411 |   export

412 |   record STm s where

413 |     constructor STM

414 |     ptr : AnyPtr

416 |   export %inline

417 |   Struct STm where

418 |     swrap   = STM

419 |     sunwrap = ptr

421 |   export %inline

422 |   SizeOf (STm s) where

423 |     sizeof_ = tm_size

425 |   export %inline

426 |   getsec: STm s -> F1 s Bits8

427 |   getsec (STM ptr) = ffi $ get_tm_sec ptr

429 |   export %inline

430 |   getmin: STm s -> F1 s Bits8

431 |   getmin (STM ptr) = ffi $ get_tm_min ptr

433 |   export %inline

434 |   gethour: STm s -> F1 s Bits8

435 |   gethour (STM ptr) = ffi $ get_tm_hour ptr

437 |   export %inline

438 |   getmday: STm s -> F1 s Bits8

439 |   getmday (STM ptr) = ffi $ get_tm_mday ptr

441 |   export %inline

442 |   getmon: STm s -> F1 s Bits8

443 |   getmon (STM ptr) = ffi $ get_tm_mon ptr

445 |   export %inline

446 |   getyear: STm s -> F1 s Int32

447 |   getyear (STM ptr) = ffi $ get_tm_year ptr

449 |   export %inline

450 |   getwday: STm s -> F1 s Bits8

451 |   getwday (STM ptr) = ffi $ get_tm_wday ptr

453 |   export %inline

454 |   getyday: STm s -> F1 s Bits16

455 |   getyday (STM ptr) = ffi $ get_tm_yday ptr

457 |   export %inline

458 |   getisdst: STm s -> F1 s Int8

459 |   getisdst (STM ptr) = ffi $ get_tm_isdst ptr

461 |   ||| Pure alternative to the `STm` struct.

464 |   public export

465 |   record Tm where

466 |     constructor TM

467 |     ||| Second of minute (0 - 60; could be a leap second)

468 |     sec:   Bits8

470 |     ||| Minute of hour (0 - 59)

471 |     min:   Bits8

473 |     ||| Hour of day (0 - 23)

474 |     hour:  Bits8

476 |     ||| Day of month (1 - 31)

477 |     mday:  Bits8

479 |     ||| Month (0 - 11)

480 |     mon:   Bits8

482 |     ||| Year since 1900

483 |     year:  Int32

485 |     ||| Day of week (Sunday = 0)

486 |     wday:  Bits8

488 |     ||| Day of year (0 - 365; 1 Jan = 0)

489 |     yday:  Bits16

491 |     ||| `True` if daylight safing time is active

492 |     isdst: Bool

494 |   %runElab derive "Tm" [Show,Eq]

496 |   ||| A broken down time value with all fields set to zero (and `False`).

499 |   export

500 |   blank : Tm

501 |   blank = TM 0 0 0 1 0 0 0 0 False

503 |   ||| Unix Epoch (00:00:00 on Thursday 1 January 1970)

504 |   export

505 |   epoch : Tm

506 |   epoch = TM 0 0 0 1 0 70 4 0 False

508 |   export

509 |   tm : STm s -> F1 s Tm

510 |   tm stm t =

511 |     let s  # t := getsec stm t

512 |         m  # t := getmin stm t

513 |         h  # t := gethour stm t

514 |         md # t := getmday stm t

515 |         mo # t := getmon stm t

516 |         y  # t := getyear stm t

517 |         wd # t := getwday stm t

518 |         yd # t := getyday stm t

519 |         id # t := getisdst stm t

520 |      in TM s m h md mo y wd yd (id > 0) # t

522 |   export %inline %hint

523 |   convTm : Convert Tm

524 |   convTm = convStruct STm tm

526 |   withSTm : (forall s . STm s -> F1 s a) -> a

527 |   withSTm f =

528 |     run1 $ \t =>

529 |      let stm # t := allocStruct1 STm t

530 |          res # t := f stm t

531 |          _   # t := freeStruct1 stm t

532 |       in res # t

534 |   ||| Converts time in seconds since the Epoch to broken down UTC time.

535 |   export

536 |   gmtime : TimeT -> Tm

537 |   gmtime secs =

538 |     withSTm $ \stm,t =>

539 |      let _   # t := ffi (prim__gmtime_r secs (sunwrap stm)) t

540 |       in tm stm t

542 |   ||| Converts time in seconds since the Epoch to broken down local time.

543 |   export

544 |   localtime : TimeT -> Tm

545 |   localtime secs =

546 |     withSTm $ \stm,t =>

547 |      let _   # t := ffi (prim__localtime_r secs (sunwrap stm)) t

548 |       in tm stm t

550 |   ||| Converts a UTC clock value to broken down local time.

551 |   export %inline

552 |   fromUTC : Clock UTC -> Tm

553 |   fromUTC = localtime . cast . seconds

555 |   ||| Converts time to a nicely formatted string.

556 |   export

557 |   asctime : Tm -> String

558 |   asctime (TM sec min hour mday mon year wday yday isdst) =

559 |     prim__asctime_r sec min hour mday mon year wday yday (if isdst then 1 else 0)

561 |   ||| Converts a broken down time to seconds since the Epoch.

562 |   export

563 |   mktime : Tm -> TimeT

564 |   mktime (TM sec min hour mday mon year wday yday isdst) =

565 |     prim__mktime sec min hour mday mon year wday yday (if isdst then 1 else 0)

567 |   ||| Converts broken down local time to a UTC clock time.

568 |   export %inline

569 |   toUTC : Tm -> Clock UTC

570 |   toUTC = fromNano . (* 1_000_000_000) . cast . mktime

572 |   ||| Keeps only the hours, seconds, and minutes of a broken down time.

573 |   export

574 |   seconds : Tm -> Integer

575 |   seconds tm = cast tm.sec + cast tm.min * 60 + cast tm.hour * 3600

577 |   ||| Drops the hours, seconds, and minutes from a broken down time.

578 |   export

579 |   dateOnly : Tm -> Tm

580 |   dateOnly = {sec := 0, min := 0, hour := 0}