0 | module IotaTime.Duration
  1 |
  2 | %default total
  3 |
  4 | ||| A fixed amount of elapsed timeline time, measured in nanoseconds.
  5 | ||| Unlike `Period`, a duration has no calendar-relative units.
  6 | export
  7 | record DurationRep where
  8 |   constructor MkDuration
  9 |   storedNanoseconds : Integer
 10 |
 11 | ||| The public opaque type of fixed elapsed durations.
 12 | public export
 13 | Duration : Type
 14 | Duration = DurationRep
 15 |
 16 | public export
 17 | Eq Duration where
 18 |   left == right = left.storedNanoseconds == right.storedNanoseconds
 19 |
 20 | public export
 21 | Ord Duration where
 22 |   compare left right = compare left.storedNanoseconds right.storedNanoseconds
 23 |
 24 | public export
 25 | Show Duration where
 26 |   show value = "fromNanoseconds " ++ show value.storedNanoseconds
 27 |
 28 | ||| Construct a duration from an exact number of nanoseconds.
 29 | export
 30 | durationFromNanoseconds : Integer -> Duration
 31 | durationFromNanoseconds = MkDuration
 32 |
 33 | ||| Construct a duration from an exact number of nanoseconds.
 34 | public export
 35 | fromNanoseconds : Integer -> Duration
 36 | fromNanoseconds = durationFromNanoseconds
 37 |
 38 | ||| Construct a duration from an exact number of microseconds.
 39 | export
 40 | durationFromMicroseconds : Integer -> Duration
 41 | durationFromMicroseconds value = MkDuration (value * 1000)
 42 |
 43 | ||| Construct a duration from an exact number of microseconds.
 44 | public export
 45 | fromMicroseconds : Integer -> Duration
 46 | fromMicroseconds = durationFromMicroseconds
 47 |
 48 | ||| Construct a duration from an exact number of milliseconds.
 49 | export
 50 | durationFromMilliseconds : Integer -> Duration
 51 | durationFromMilliseconds value = MkDuration (value * 1000000)
 52 |
 53 | ||| Construct a duration from an exact number of milliseconds.
 54 | public export
 55 | fromMilliseconds : Integer -> Duration
 56 | fromMilliseconds = durationFromMilliseconds
 57 |
 58 | ||| Construct a duration from an exact number of seconds.
 59 | export
 60 | durationFromSeconds : Integer -> Duration
 61 | durationFromSeconds value = MkDuration (value * 1000000000)
 62 |
 63 | ||| Construct a duration from an exact number of seconds.
 64 | public export
 65 | fromSeconds : Integer -> Duration
 66 | fromSeconds = durationFromSeconds
 67 |
 68 | ||| Construct a duration from fixed 60-second minutes.
 69 | export
 70 | durationFromMinutes : Integer -> Duration
 71 | durationFromMinutes value = durationFromSeconds (value * 60)
 72 |
 73 | ||| Construct a duration from fixed 60-second minutes.
 74 | public export
 75 | fromMinutes : Integer -> Duration
 76 | fromMinutes = durationFromMinutes
 77 |
 78 | ||| Construct a duration from fixed 60-minute hours.
 79 | export
 80 | durationFromHours : Integer -> Duration
 81 | durationFromHours value = durationFromMinutes (value * 60)
 82 |
 83 | ||| Construct a duration from fixed 60-minute hours.
 84 | public export
 85 | fromHours : Integer -> Duration
 86 | fromHours = durationFromHours
 87 |
 88 | ||| Construct a duration from fixed 24-hour days, independent of calendars and zones.
 89 | export
 90 | durationFromStandardDays : Integer -> Duration
 91 | durationFromStandardDays value = durationFromHours (value * 24)
 92 |
 93 | ||| Construct a duration from fixed 24-hour days, independent of calendars and zones.
 94 | public export
 95 | fromStandardDays : Integer -> Duration
 96 | fromStandardDays = durationFromStandardDays
 97 |
 98 | ||| Construct a duration from fixed seven-day weeks.
 99 | export
100 | durationFromStandardWeeks : Integer -> Duration
101 | durationFromStandardWeeks value = durationFromStandardDays (value * 7)
102 |
103 | ||| Construct a duration from fixed seven-day weeks.
104 | public export
105 | fromStandardWeeks : Integer -> Duration
106 | fromStandardWeeks = durationFromStandardWeeks
107 |
108 | ||| Return the exact signed nanosecond count represented by a duration.
109 | public export
110 | toDurationNanoseconds : Duration -> Integer
111 | toDurationNanoseconds = storedNanoseconds
112 |
113 | ||| Return the number of whole microseconds in a duration.
114 | public export
115 | toMicroseconds : Duration -> Integer
116 | toMicroseconds value = toDurationNanoseconds value `div` 1000
117 |
118 | ||| Return the number of whole milliseconds in a duration.
119 | public export
120 | toMilliseconds : Duration -> Integer
121 | toMilliseconds value = toMicroseconds value `div` 1000
122 |
123 | ||| Return the number of whole seconds in a duration, truncated toward negative infinity.
124 | public export
125 | toSeconds : Duration -> Integer
126 | toSeconds value = toMilliseconds value `div` 1000
127 |
128 | ||| Return the number of whole fixed 60-second minutes in a duration.
129 | public export
130 | toMinutes : Duration -> Integer
131 | toMinutes value = toSeconds value `div` 60
132 |
133 | ||| Return the number of whole fixed 60-minute hours in a duration.
134 | public export
135 | toHours : Duration -> Integer
136 | toHours value = toMinutes value `div` 60
137 |
138 | ||| Return the number of whole fixed 24-hour days in a duration.
139 | public export
140 | toStandardDays : Duration -> Integer
141 | toStandardDays value = toHours value `div` 24
142 |
143 | ||| Return the number of whole fixed seven-day weeks in a duration.
144 | public export
145 | toStandardWeeks : Duration -> Integer
146 | toStandardWeeks value = toStandardDays value `div` 7
147 |
148 | ||| The duration containing no elapsed time.
149 | export
150 | zeroDuration : Duration
151 | zeroDuration = MkDuration 0
152 |
153 | ||| Add two elapsed durations.
154 | export
155 | addDurations : Duration -> Duration -> Duration
156 | addDurations left right =
157 |   MkDuration (left.storedNanoseconds + right.storedNanoseconds)
158 |
159 | ||| Add two elapsed durations.
160 | public export
161 | add : Duration -> Duration -> Duration
162 | add = addDurations
163 |
164 | ||| Subtract the second duration from the first.
165 | export
166 | subtractDurations : Duration -> Duration -> Duration
167 | subtractDurations left right =
168 |   MkDuration (left.storedNanoseconds - right.storedNanoseconds)
169 |
170 | ||| Subtract the second duration from the first.
171 | public export
172 | minus : Duration -> Duration -> Duration
173 | minus = subtractDurations
174 |
175 | ||| Reverse the direction of a duration.
176 | export
177 | negateDuration : Duration -> Duration
178 | negateDuration value = MkDuration (negate value.storedNanoseconds)
179 |
180 | ||| Multiply a duration by an integer factor.
181 | export
182 | scaleDuration : Integer -> Duration -> Duration
183 | scaleDuration factor value = MkDuration (factor * value.storedNanoseconds)
184 |
185 | ||| Proof that constructing then observing a nanosecond count is lossless.
186 | public export
187 | durationNanosecondsRoundTrip : (value : Integer) ->
188 |   toDurationNanoseconds (fromNanoseconds value) = value
189 | durationNanosecondsRoundTrip value = Refl
190 |
191 | ||| Proof that observing then reconstructing a duration preserves it.
192 | public export
193 | durationRoundTrip : (value : Duration) ->
194 |   fromNanoseconds (toDurationNanoseconds value) = value
195 | durationRoundTrip (MkDuration value) = Refl
196 |