0 | ||| Types and functions for reasoning about time.
  1 | module System.Clock
  2 |
  3 | import Data.Nat
  4 | import Data.String
  5 | import PrimIO
  6 |
  7 | %default total
  8 |
  9 | ||| The various types of system clock available.
 10 | public export
 11 | data ClockType
 12 |   = ||| The time elapsed since the "epoch:" 00:00:00 UTC, January 1, 1970
 13 |     UTC
 14 |   | ||| The time elapsed since some arbitrary point in the past
 15 |     Monotonic
 16 |   | ||| Representing a time duration.
 17 |     Duration
 18 |   | ||| The amount of CPU time used by the current process.
 19 |     Process
 20 |   | ||| The amount of CPU time used by the current thread.
 21 |     Thread
 22 |   | ||| The current process's CPU time consumed by the garbage collector.
 23 |     GCCPU
 24 |   | ||| The current process's real time consumed by the garbage collector.
 25 |     GCReal
 26 |
 27 | export
 28 | Show ClockType where
 29 |   show UTC       = "UTC"
 30 |   show Monotonic = "monotonic"
 31 |   show Duration  = "duration"
 32 |   show Process   = "process"
 33 |   show Thread    = "thread"
 34 |   show GCCPU     = "gcCPU"
 35 |   show GCReal    = "gcReal"
 36 |
 37 | ||| A clock recording some time in seconds and nanoseconds. The "type" of time
 38 | ||| recorded is indicated by the given `ClockType`.
 39 | public export
 40 | data Clock : (type : ClockType) -> Type where
 41 |   MkClock
 42 |     : {type : ClockType}
 43 |     -> (seconds : Integer)
 44 |     -> (nanoseconds : Integer)
 45 |     -> Clock type
 46 |
 47 | public export
 48 | Eq (Clock type) where
 49 |   (MkClock seconds1 nanoseconds1) == (MkClock seconds2 nanoseconds2) =
 50 |     seconds1 == seconds2 && nanoseconds1 == nanoseconds2
 51 |
 52 | public export
 53 | Ord (Clock type) where
 54 |   compare (MkClock seconds1 nanoseconds1) (MkClock seconds2 nanoseconds2) =
 55 |     case compare seconds1 seconds2 of
 56 |       LT => LT
 57 |       GT => GT
 58 |       EQ => compare nanoseconds1 nanoseconds2
 59 |
 60 | public export
 61 | Show (Clock type) where
 62 |   show (MkClock {type} seconds nanoseconds) =
 63 |     show type ++ ": " ++ show seconds ++ "s " ++ show nanoseconds ++ "ns"
 64 |
 65 | ||| Display a `Clock`'s content, padding the seconds and nanoseconds as
 66 | ||| appropriate.
 67 | |||
 68 | ||| @ s   the number of digits used to display the seconds
 69 | ||| @ ns  the number of digits used to display the nanoseconds
 70 | ||| @ clk the Clock whose contents to display
 71 | export
 72 | showTime : (s, ns : Nat) -> (clk : Clock type) -> String
 73 | showTime s ns (MkClock seconds nanoseconds) =
 74 |   let seconds' = show seconds
 75 |       nanoseconds' = show nanoseconds
 76 |   in concat [ padLeft s '0' seconds'
 77 |             , if ns == 0 then "" else "."
 78 |             , padRight ns '0' $ substr 0 ns $ (padLeft 9 '0' nanoseconds')
 79 |             , "s"
 80 |             ]
 81 |
 82 | ||| A helper to deconstruct a Clock.
 83 | public export
 84 | seconds : Clock type -> Integer
 85 | seconds (MkClock s _) = s
 86 |
 87 | ||| A helper to deconstruct a Clock.
 88 | public export
 89 | nanoseconds : Clock type -> Integer
 90 | nanoseconds (MkClock _ ns) = ns
 91 |
 92 | ||| Make a duration value.
 93 | |||
 94 | ||| @ s  the number of seconds in the duration
 95 | ||| @ ns the number of nanoseconds in the duration
 96 | public export
 97 | makeDuration : (s : Integer) -> (ns : Integer) -> Clock Duration
 98 | makeDuration = MkClock
 99 |
100 | ||| Opaque clock value manipulated by the back-end.
101 | data OSClock : Type where [external]
102 |
103 | ||| Note: Backends are required to implement UTC, monotonic time, CPU time in
104 | ||| current process/thread, and time duration; the rest are optional.
105 | export
106 | data ClockTypeMandatory
107 |   = Mandatory
108 |   | Optional
109 |
110 | ||| Determine whether the specified `ClockType` is required to be implemented by
111 | ||| all backends.
112 | public export
113 | isClockMandatory : ClockType -> ClockTypeMandatory
114 | isClockMandatory GCCPU  = Optional
115 | isClockMandatory GCReal = Optional
116 | isClockMandatory _      = Mandatory
117 |
118 | %foreign "scheme:blodwen-clock-time-monotonic"
119 |          "RefC:clockTimeMonotonic"
120 |          "javascript:lambda:()=>performance.now()" -- javascript clocks are represented as milliseconds
121 | prim__clockTimeMonotonic : PrimIO OSClock
122 |
123 | ||| Get the current backend's monotonic time.
124 | clockTimeMonotonic : IO OSClock
125 | clockTimeMonotonic = fromPrim prim__clockTimeMonotonic
126 |
127 | %foreign "scheme:blodwen-clock-time-utc"
128 |          "RefC:clockTimeUtc"
129 |          "javascript:lambda:()=>Date.now()"
130 | prim__clockTimeUtc : PrimIO OSClock
131 |
132 | ||| Get the current UTC time.
133 | clockTimeUtc : IO OSClock
134 | clockTimeUtc = fromPrim prim__clockTimeUtc
135 |
136 | %foreign "scheme:blodwen-clock-time-process"
137 |          "RefC:clockTimeProcess"
138 |          "javascript:support:clockTimeProcess,support_system_clock"
139 | prim__clockTimeProcess : PrimIO OSClock
140 |
141 | ||| Get the amount of time used by the current process.
142 | clockTimeProcess : IO OSClock
143 | clockTimeProcess = fromPrim prim__clockTimeProcess
144 |
145 | %foreign "scheme:blodwen-clock-time-thread"
146 |          "RefC:clockTimeThread"
147 |          "javascript:support:clockTimeThread,support_system_clock"
148 | prim__clockTimeThread : PrimIO OSClock
149 |
150 | ||| Get the amount of time used by the current thread.
151 | clockTimeThread : IO OSClock
152 | clockTimeThread = fromPrim prim__clockTimeThread
153 |
154 | %foreign "scheme:blodwen-clock-time-gccpu"
155 |          "RefC:clockTimeGcCpu"
156 |          "javascript:lambda:()=>null"
157 | prim__clockTimeGcCpu : PrimIO OSClock
158 |
159 | ||| Get the amount of the current process's CPU time consumed by the garbage
160 | ||| collector.
161 | clockTimeGcCpu : IO OSClock
162 | clockTimeGcCpu = fromPrim prim__clockTimeGcCpu
163 |
164 | %foreign "scheme:blodwen-clock-time-gcreal"
165 |          "RefC:clockTimeGcReal"
166 |          "javascript:lambda:()=>null"
167 | prim__clockTimeGcReal : PrimIO OSClock
168 |
169 | ||| Get the amount of the current process's real-time consumed by the garbage
170 | ||| collector.
171 | clockTimeGcReal : IO OSClock
172 | clockTimeGcReal = fromPrim prim__clockTimeGcReal
173 |
174 | fetchOSClock : ClockType -> IO OSClock
175 | fetchOSClock UTC       = clockTimeUtc
176 | fetchOSClock Monotonic = clockTimeMonotonic
177 | fetchOSClock Process   = clockTimeProcess
178 | fetchOSClock Thread    = clockTimeThread
179 | fetchOSClock GCCPU     = clockTimeGcCpu
180 | fetchOSClock GCReal    = clockTimeGcReal
181 | fetchOSClock Duration  = clockTimeMonotonic
182 |
183 | %foreign "scheme:blodwen-is-time?"
184 |          "RefC:clockValid"
185 |          "javascript:lambda:(x)=>x===null?0:1"
186 | prim__osClockValid : OSClock -> PrimIO Int
187 |
188 | ||| A test to determine the status of optional clocks.
189 | osClockValid : OSClock -> IO Int
190 | osClockValid clk = fromPrim (prim__osClockValid clk)
191 |
192 | %foreign "scheme:blodwen-clock-second"
193 |          "RefC:clockSecond"
194 |          "javascript:lambda:(x)=>BigInt(Math.floor(x/1000))"
195 | prim__osClockSecond : OSClock -> PrimIO Bits64
196 |
197 | ||| Get the second of time from the given `OSClock`.
198 | osClockSecond : OSClock -> IO Bits64
199 | osClockSecond clk = fromPrim (prim__osClockSecond clk)
200 |
201 | %foreign "scheme:blodwen-clock-nanosecond"
202 |          "RefC:clockNanosecond"
203 |          "javascript:lambda:(x)=>BigInt(Math.floor((x%1000)*1000*1000))"
204 | prim__osClockNanosecond : OSClock -> PrimIO Bits64
205 |
206 | ||| Get the nanosecond of time from the given `OSClock`.
207 | osClockNanosecond : OSClock -> IO Bits64
208 | osClockNanosecond clk = fromPrim (prim__osClockNanosecond clk)
209 |
210 | ||| Convert an `OSClock` to an Idris `Clock`.
211 | fromOSClock : {type : ClockType} -> OSClock -> IO (Clock type)
212 | fromOSClock clk =
213 |   pure $
214 |     MkClock
215 |       {type}
216 |       (cast !(osClockSecond clk))
217 |       (cast !(osClockNanosecond clk))
218 |
219 | ||| The return type of a function using a `Clock` depends on the type of
220 | ||| `Clock`:
221 | ||| * `Optional` clocks may not be implemented, so we might not return anything
222 | ||| * `Mandatory` clocks have to be implemented, so we _will_ return something
223 | public export
224 | clockTimeReturnType : (typ : ClockType) -> Type
225 | clockTimeReturnType typ with (isClockMandatory typ)
226 |   clockTimeReturnType typ | Optional = Maybe (Clock typ)
227 |   clockTimeReturnType typ | Mandatory = Clock typ
228 |
229 | ||| Fetch the system clock of a given kind. If the clock is mandatory,
230 | ||| we return a `Clock type` else, we return a `Maybe (Clock type)`.
231 | public export
232 | clockTime : (typ : ClockType) -> IO (clockTimeReturnType typ)
233 | clockTime clockType with (isClockMandatory clockType)
234 |   clockTime clockType | Mandatory = fetchOSClock clockType >>= fromOSClock
235 |   clockTime clockType | Optional = do
236 |     clk <- fetchOSClock clockType
237 |     valid <- map (== 1) $ osClockValid clk
238 |     if valid
239 |       then map Just $ fromOSClock clk
240 |       else pure Nothing
241 |
242 | ||| Convert the time in the given clock to nanoseconds.
243 | public export
244 | toNano : Clock type -> Integer
245 | toNano (MkClock seconds nanoseconds) =
246 |   let scale = 1000000000
247 |    in scale * seconds + nanoseconds
248 |
249 | ||| Convert some time in nanoseconds to a `Clock` containing that time.
250 | |||
251 | ||| @ n the time in nanoseconds
252 | public export
253 | fromNano : {type : ClockType} -> (n : Integer) -> Clock type
254 | fromNano n =
255 |   let scale       = 1000000000
256 |       seconds     = n `div` scale
257 |       nanoseconds = n `mod` scale
258 |    in MkClock seconds nanoseconds
259 |
260 | ||| Compute difference between two clocks of the same type.
261 | ||| @ end the end time
262 | ||| @ start the start time
263 | public export
264 | timeDifference : Clock type -> Clock type -> Clock Duration
265 | timeDifference end start = fromNano $ toNano end - toNano start
266 |
267 | ||| Add a duration to a clock value.
268 | public export
269 | addDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
270 | addDuration clock duration = fromNano $ toNano clock + toNano duration
271 |
272 | ||| Subtract a duration from a clock value.
273 | public export
274 | subtractDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
275 | subtractDuration clock duration = fromNano $ toNano clock - toNano duration
276 |