0 | module System.Time
  1 |
  2 | import Control.Monad.Trans
  3 |
  4 | import public Data.Fin
  5 | import public Data.Nat
  6 | import Data.String
  7 |
  8 | import System       -- for `sleep` for `IO` implementations
  9 | import System.Clock -- for `clockTime` for `IO` implementations
 10 |
 11 | %default total
 12 |
 13 | ----------------------------------------------------------
 14 | --- Common stuff for absolute time and finite duration ---
 15 | ----------------------------------------------------------
 16 |
 17 | public export %inline
 18 | UntypedTime : Type
 19 | UntypedTime = Nat
 20 |
 21 | export
 22 | interface TimeValue a where
 23 |   (.millis)  : UntypedTime -> a
 24 |   (.seconds) : UntypedTime -> a
 25 |   (.minutes) : UntypedTime -> a
 26 |   (.hours)   : UntypedTime -> a
 27 |   (.days)    : UntypedTime -> a
 28 |
 29 |   -- back conversions may lose data
 30 |   (.asMillis)  : a -> UntypedTime
 31 |   (.asSeconds) : a -> UntypedTime
 32 |   (.asMinutes) : a -> UntypedTime
 33 |   (.asHours)   : a -> UntypedTime
 34 |   (.asDays)    : a -> UntypedTime
 35 |
 36 |   -- appropriate components when we represent this time value as `DD HH:MM:SS.ms`
 37 |   (.millisComponent)  : a -> Fin 1000
 38 |   (.secondsComponent) : a -> Fin 60
 39 |   (.minutesComponent) : a -> Fin 60
 40 |   (.hoursComponent)   : a -> Fin 24
 41 |   (.daysComponent)    : a -> Nat
 42 |
 43 |   x.seconds = (1000 * x).millis
 44 |   x.minutes = (60 * x).seconds
 45 |   x.hours   = (60 * x).minutes
 46 |   x.days    = (24 * x).hours
 47 |
 48 |   x.asSeconds = divNatNZ x.asMillis  1000 %search
 49 |   x.asMinutes = divNatNZ x.asSeconds 60   %search
 50 |   x.asHours   = divNatNZ x.asMinutes 60   %search
 51 |   x.asDays    = divNatNZ x.asHours   24   %search
 52 |
 53 |   x.millisComponent  = restrict _ $ cast x.asMillis
 54 |   x.secondsComponent = restrict _ $ cast x.asSeconds
 55 |   x.minutesComponent = restrict _ $ cast x.asMinutes
 56 |   x.hoursComponent   = restrict _ $ cast x.asHours
 57 |   x.daysComponent    = x.asDays
 58 |
 59 | ---------------------
 60 | --- Absolute time ---
 61 | ---------------------
 62 |
 63 | -- Well, absolute time is anyway a finite duration from some point in past...
 64 | namespace AbsTime
 65 |
 66 |   export
 67 |   record Time where
 68 |     constructor MkTime
 69 |     millis : UntypedTime
 70 |
 71 |   export
 72 |   TimeValue Time where
 73 |     (.millis)   = MkTime
 74 |     (.asMillis) = millis
 75 |
 76 |   export
 77 |   Eq Time where
 78 |     (==) = (==) `on` (.asMillis)
 79 |
 80 |   export
 81 |   Ord Time where
 82 |     compare = compare `on` (.asMillis)
 83 |
 84 | ----------------------------
 85 | --- Finite time duration ---
 86 | ----------------------------
 87 |
 88 | namespace FiniteDuration
 89 |
 90 |   export
 91 |   record FinDuration where
 92 |     constructor MkFinDuration
 93 |     millis : UntypedTime
 94 |
 95 |   export
 96 |   TimeValue FinDuration where
 97 |     (.millis) = MkFinDuration
 98 |     (.asMillis) = millis
 99 |
100 |   export %defaulthint
101 |   DefaultTimeValue : TimeValue FinDuration
102 |   DefaultTimeValue = %search
103 |
104 |   export
105 |   Eq FinDuration where
106 |     (==) = (==) `on` (.asMillis)
107 |
108 |   export
109 |   Ord FinDuration where
110 |     compare = compare `on` (.asMillis)
111 |
112 |   export
113 |   Semigroup FinDuration where
114 |     (<+>) = MkFinDuration .: (+) `on` (.asMillis)
115 |
116 |   export
117 |   Monoid FinDuration where
118 |     neutral = MkFinDuration 0
119 |
120 |   export
121 |   (*) : Nat -> FinDuration -> FinDuration
122 |   n * d = (n * d.asMillis).millis
123 |
124 |   -- May lose data! `z * (d / z)` may be less than `d`
125 |   export
126 |   (/) : FinDuration -> (z : Nat) -> (0 _ : NonZero z) => FinDuration
127 |   d / z = (divNatNZ d.asMillis z %search).millis
128 |
129 |   -- Gives a zero length duration if longer duration is subtracted from a smaller one
130 |   export
131 |   (-) : FinDuration -> FinDuration -> FinDuration
132 |   x - y = (x.asMillis `minus` y.asMillis).millis
133 |
134 | ------------------------------------------------------------
135 | --- Operations between absolute time and finite duration ---
136 | ------------------------------------------------------------
137 |
138 | -- This is an absolute difference. `y + (x - y)` may be more than `x` if `x < y`
139 | export
140 | (-) : Time -> Time -> FinDuration
141 | x - y = ((x `max` y).asMillis `minus` (x `min` y).asMillis).millis
142 |
143 | export
144 | (+) : Time -> FinDuration -> Time
145 | t + d = (t.asMillis + d.asMillis).millis
146 |
147 | ----------------------
148 | --- Interpolations ---
149 | ----------------------
150 |
151 | timeComponent : Cast v Nat => v -> (pre, descSg, descPl : String) -> List String
152 | timeComponent d pre descSg descPl = let d : Nat := cast d in if d == 0 then [] else
153 |   ["\{pre}\{show d}\{if d == 1 then descSg else descPl}"]
154 |
155 | joinOr : (ifEmpty : String) -> List (List String) -> List String
156 | joinOr ifEmpty [] = [ ifEmpty ]
157 | joinOr _       xs = join xs
158 |
159 | ifNotNull : (List a -> List a) -> List a -> List a
160 | ifNotNull _ [] = []
161 | ifNotNull f xs = f xs
162 |
163 | stripFinZeros : String -> String
164 | stripFinZeros = pack . reverse . dropWhile (== '0') . reverse . unpack
165 |
166 | namespace FiniteDuration
167 |
168 |   export
169 |   [Wrds] Interpolation FinDuration where
170 |     interpolate tv = joinBy " " $ joinOr "0 sec"
171 |       [ timeComponent tv.daysComponent    "" " day"  " days"
172 |       , timeComponent tv.hoursComponent   "" " hr"   " hr"
173 |       , timeComponent tv.minutesComponent "" " min"  " min"
174 |       , timeComponent tv.secondsComponent "" " sec"  " sec"
175 |       , timeComponent tv.millisComponent  "" " ms"   " ms"
176 |       ]
177 |
178 |   export
179 |   [Words] Interpolation FinDuration where
180 |     interpolate tv = joinBy ", " $ joinOr "0 seconds"
181 |       [ timeComponent tv.daysComponent    "" " day"         " days"
182 |       , timeComponent tv.hoursComponent   "" " hour"        " hours"
183 |       , timeComponent tv.minutesComponent "" " minute"      " minutes"
184 |       , timeComponent tv.secondsComponent "" " second"      " seconds"
185 |       , timeComponent tv.millisComponent  "" " millisecond" " milliseconds"
186 |       ]
187 |
188 |   export
189 |   [Semicoloned] Interpolation FinDuration where
190 |     interpolate tv = concat $ do
191 |       let s  = tv.secondsComponent
192 |           ms = tv.millisComponent
193 |       timeComponent tv.daysComponent "" "d" "d" ++
194 |         [ padLeft 2 '0' $ show tv.hoursComponent
195 |         , ":"
196 |         , padLeft 2 '0' $ show tv.minutesComponent
197 |         ] ++ if s == 0 && ms == 0 then [] else
198 |           ":" :: padLeft 2 '0' (show s) :: (("." ++) . padLeft 3 '0' <$> timeComponent ms "" "" "")
199 |
200 |   export
201 |   [ISO8601] Interpolation FinDuration where
202 |     interpolate d = do
203 |       let date = [ timeComponent d.daysComponent "" "D" "D" ]
204 |       let time = ifNotNull (["T"]::)
205 |                    [ timeComponent d.hoursComponent   "" "H" "H"
206 |                    , timeComponent d.minutesComponent "" "M" "M"
207 |                    , let s  = d.secondsComponent
208 |                          ms = d.millisComponent
209 |                      in if s == 0 && ms == 0 then [] else
210 |                           show s :: (("." ++) . stripFinZeros . padLeft 3 '0'<$> timeComponent ms "" "" "") ++ ["S"]
211 |                    ]
212 |       strCons 'P' . concat . joinOr "T0S" $ date ++ time
213 |
214 |   export %defaulthint %inline
215 |   DefaultFinDurationInterpolation : Interpolation FinDuration
216 |   DefaultFinDurationInterpolation = Wrds
217 |
218 | ------------------
219 | --- Interfaces ---
220 | ------------------
221 |
222 | public export
223 | interface Timed m where
224 |   currentTime : m Time
225 |
226 | public export
227 | interface Timed m => Monad m => CanSleep m where
228 |   sleepTill : Time -> m Unit
229 |   sleepTill t = sleepFor $ t - !currentTime
230 |
231 |   sleepFor : FinDuration -> m Unit
232 |   sleepFor d = sleepTill $ !currentTime + d
233 |
234 | ----------------------------------------
235 | --- Implementations for `MonadTrans` ---
236 | ----------------------------------------
237 |
238 | namespace Timed
239 |
240 |   export
241 |   [Trans] Timed m => MonadTrans t => Monad m => Timed (t m) where
242 |     currentTime = lift currentTime
243 |
244 | namespace CanSleep
245 |
246 |   export
247 |   [Trans] CanSleep m => MonadTrans t => Monad m => Monad (t m) => CanSleep (t m) using Timed.Trans where
248 |     sleepFor  = lift . sleepFor
249 |     sleepTill = lift . sleepTill
250 |
251 | --------------------------------
252 | --- Implementations for `IO` ---
253 | --------------------------------
254 |
255 | namespace Timed
256 |
257 |   export
258 |   [HasIO] HasIO io => Timed io where
259 |     currentTime = liftIO $ (.millis) . fromInteger . millisOfClock <$> clockTime UTC where
260 |       millisOfClock : Clock _ -> Integer
261 |       millisOfClock (MkClock secs nanos) = secs * 1000 + nanos `div` 1000000
262 |
263 | namespace CanSleep
264 |
265 |   export
266 |   [HasIO] HasIO io => CanSleep io using Timed.HasIO where
267 |     sleepFor d = do
268 |       sleep $ cast d.asSeconds
269 |       let (msComp ** _) = toIntWithPrf d.millisComponent
270 |       usleep msComp
271 |       where
272 |         %inline
273 |         toIntWithPrf : Fin 1000 -> (x : Int ** So (x >= 0))
274 |         toIntWithPrf k = (cast $ finToNat k ** believe_me {- we are converting from `Nat` -} Oh)
275 |
276 | export
277 | Timed IO where
278 |   currentTime = currentTime @{HasIO}
279 |
280 | export
281 | CanSleep IO where
282 |   sleepFor = sleepFor @{HasIO}
283 |