0 | module IotaTime.OffsetDateTime
  1 |
  2 | import public IotaTime.Calendar
  3 | import public IotaTime.CalendarDateTime
  4 | import public IotaTime.Instant
  5 | import public IotaTime.LocalTime
  6 | import public IotaTime.Offset
  7 |
  8 | %default total
  9 |
 10 | nanosecondsPerSecond : Integer
 11 | nanosecondsPerSecond = 1000000000
 12 |
 13 | nanosecondsPerDay : Integer
 14 | nanosecondsPerDay = 86400 * nanosecondsPerSecond
 15 |
 16 | bridgeDaysOf : {dateType : Type} -> {auto rep : HasCalendarBridge dateType} ->
 17 |                dateType -> Integer
 18 | bridgeDaysOf @{rep} = toBridgeDays @{rep}
 19 |
 20 | acceptsBridgeDay : {dateType : Type} -> {auto rep : HasCalendarBridge dateType} ->
 21 |                    Integer -> Bool
 22 | acceptsBridgeDay @{rep} = acceptsBridgeDays @{rep}
 23 |
 24 | dateFromBridgeDays : {dateType : Type} -> {auto rep : HasCalendarBridge dateType} ->
 25 |                      (days : Integer) ->
 26 |                      {auto 0 valid : So (acceptsBridgeDay @{rep} days)} ->
 27 |                      dateType
 28 | dateFromBridgeDays @{rep} days @{valid} = fromBridgeDays @{rep} days @{valid}
 29 |
 30 | bridgeDateTypeName : {dateType : Type} ->
 31 |                      {auto rep : HasCalendarBridge dateType} -> String
 32 | bridgeDateTypeName @{rep} = bridgeCalendarName @{rep}
 33 |
 34 | export
 35 | record OffsetDateTimeRep (calendar : Type) (cal : Calendar calendar) where
 36 |   constructor MkOffsetDateTime
 37 |   localValue : CalendarDateTime calendar @{cal}
 38 |   offsetValue : Offset
 39 |
 40 | public export
 41 | OffsetDateTime : (calendar : Type) -> {auto cal : Calendar calendar} -> Type
 42 | OffsetDateTime calendar @{cal} = OffsetDateTimeRep calendar cal
 43 |
 44 | public export
 45 | {calendar : Type} -> {cal : Calendar calendar} ->
 46 |   Eq (CalendarDateTime calendar @{cal}) =>
 47 |   Eq (OffsetDateTimeRep calendar cal) where
 48 |   left == right =
 49 |     left.localValue == right.localValue && left.offsetValue == right.offsetValue
 50 |
 51 | ||| Associate a calendar-local date and time with its displacement from UTC.
 52 | export
 53 | atOffset : {calendar : Type} -> {auto cal : Calendar calendar} ->
 54 |            CalendarDateTime calendar @{cal} -> Offset ->
 55 |            OffsetDateTime calendar @{cal}
 56 | atOffset = MkOffsetDateTime
 57 |
 58 | ||| HodaTime-compatible constructor from a local calendar date-time and offset.
 59 | public export
 60 | fromCalendarDateTimeWithOffset : {calendar : Type} ->
 61 |                                  {auto cal : Calendar calendar} ->
 62 |                                  CalendarDateTime calendar @{cal} -> Offset ->
 63 |                                  OffsetDateTime calendar @{cal}
 64 | fromCalendarDateTimeWithOffset = atOffset
 65 |
 66 | export
 67 | localDateTime : {calendar : Type} -> {auto cal : Calendar calendar} ->
 68 |                 OffsetDateTime calendar @{cal} ->
 69 |                 CalendarDateTime calendar @{cal}
 70 | localDateTime = localValue
 71 |
 72 | public export
 73 | toCalendarDateTime : {calendar : Type} -> {auto cal : Calendar calendar} ->
 74 |                      OffsetDateTime calendar @{cal} ->
 75 |                      CalendarDateTime calendar @{cal}
 76 | toCalendarDateTime = localDateTime
 77 |
 78 | export
 79 | offsetOf : {calendar : Type} -> {auto cal : Calendar calendar} ->
 80 |            OffsetDateTime calendar @{cal} -> Offset
 81 | offsetOf = offsetValue
 82 |
 83 | public export
 84 | offset : {calendar : Type} -> {auto cal : Calendar calendar} ->
 85 |          OffsetDateTime calendar @{cal} -> Offset
 86 | offset = offsetOf
 87 |
 88 | ||| Extracting the local date-time after construction returns the supplied value.
 89 | public export
 90 | offsetDateTimeLocalPart :
 91 |   {calendar : Type} -> {auto cal : Calendar calendar} ->
 92 |   (valueDateTime : CalendarDateTime calendar @{cal}) ->
 93 |   (valueOffset : Offset) ->
 94 |   toCalendarDateTime @{cal}
 95 |     (fromCalendarDateTimeWithOffset @{cal} valueDateTime valueOffset) = valueDateTime
 96 | offsetDateTimeLocalPart _ _ = Refl
 97 |
 98 | ||| Extracting the offset after construction returns the supplied offset.
 99 | public export
100 | offsetDateTimeOffsetPart :
101 |   {calendar : Type} -> {auto cal : Calendar calendar} ->
102 |   (valueDateTime : CalendarDateTime calendar @{cal}) ->
103 |   (valueOffset : Offset) ->
104 |   offset @{cal}
105 |     (fromCalendarDateTimeWithOffset @{cal} valueDateTime valueOffset) = valueOffset
106 | offsetDateTimeOffsetPart _ _ = Refl
107 |
108 | ||| Reconstructing an offset date-time from its projections is exact.
109 | public export
110 | offsetDateTimeRoundTrip :
111 |   {calendar : Type} -> {auto cal : Calendar calendar} ->
112 |   (value : OffsetDateTime calendar @{cal}) ->
113 |   fromCalendarDateTimeWithOffset @{cal}
114 |     (toCalendarDateTime @{cal} value) (offset @{cal} value) = value
115 | offsetDateTimeRoundTrip (MkOffsetDateTime _ _) = Refl
116 |
117 | localNanoseconds : LocalTime -> Integer
118 | localNanoseconds value =
119 |   (((hourValue (hour value) * 60 + minuteValue (minute value)) * 60 +
120 |     secondValue (second value)) * nanosecondsPerSecond) +
121 |     nanosecondValue (nanosecond value)
122 |
123 | localTimeFromNanoseconds : Integer -> LocalTime
124 | localTimeFromNanoseconds value = localTime
125 |   (either (const 0) id (refineHour (value `div` (3600 * nanosecondsPerSecond))))
126 |   (either (const 0) id (refineMinute (value `div` (60 * nanosecondsPerSecond) `mod` 60)))
127 |   (either (const 0) id (refineSecond (value `div` nanosecondsPerSecond `mod` 60)))
128 |   (either (const 0) id (refineNanosecond (value `mod` nanosecondsPerSecond)))
129 |
130 | ||| Resolve an offset date-time to its unique point on the global timeline.
131 | public export
132 | toInstant : {calendar : Type} -> {auto cal : Calendar calendar} ->
133 |             {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
134 |             OffsetDateTime calendar @{cal} -> Instant
135 | toInstant @{cal} @{rep} value = fromNanosecondsSinceEpoch
136 |   (bridgeDaysOf @{rep} (datePart value.localValue) * nanosecondsPerDay +
137 |    localNanoseconds (localTimeOfDay value.localValue) -
138 |    totalOffsetSeconds value.offsetValue * nanosecondsPerSecond)
139 |
140 | public export
141 | {calendar : Type} -> {cal : Calendar calendar} ->
142 |   HasCalendarBridge (CalendarDate calendar @{cal}) =>
143 |   Eq (CalendarDate calendar @{cal}) =>
144 |   Ord (OffsetDateTimeRep calendar cal) where
145 |   compare left right =
146 |     compare (toInstant left) (toInstant right) <+>
147 |     compare left.offsetValue right.offsetValue
148 |
149 | public export
150 | {calendar : Type} -> {cal : Calendar calendar} ->
151 |   HasCalendarBridge (CalendarDate calendar @{cal}) =>
152 |   Show (OffsetDateTimeRep calendar cal) where
153 |   show value = "fromInstantWithOffset (" ++
154 |     show (toInstant value) ++ ") (" ++
155 |     show value.offsetValue ++ ")"
156 |
157 | ||| Display an instant using a calendar and offset. Conversion can fail only
158 | ||| when the resulting local day lies outside the calendar's supported range.
159 | export
160 | fromInstant : {calendar : Type} -> {auto cal : Calendar calendar} ->
161 |               {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
162 |               Offset -> Instant ->
163 |               Either CalendarConversionError (OffsetDateTime calendar @{cal})
164 | fromInstant @{cal} @{rep} valueOffset valueInstant =
165 |   let localNanos = toNanosecondsSinceEpoch valueInstant +
166 |         totalOffsetSeconds valueOffset * nanosecondsPerSecond
167 |       valueDays = localNanos `div` nanosecondsPerDay
168 |       nanosWithinDay = localNanos `mod` nanosecondsPerDay
169 |    in case choose (acceptsBridgeDay @{rep} valueDays) of
170 |         Left valid => Right (MkOffsetDateTime
171 |           (on (localTimeFromNanoseconds nanosWithinDay)
172 |             (dateFromBridgeDays @{rep} valueDays @{valid}))
173 |           valueOffset)
174 |         Right _ => Left
175 |           (TargetCalendarOutOfRange (bridgeDateTypeName @{rep}) valueDays)
176 |
177 | ||| HodaTime-compatible constructor with instant-first argument order.
178 | public export
179 | fromInstantWithOffset : {calendar : Type} -> {auto cal : Calendar calendar} ->
180 |                         {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
181 |                         Instant -> Offset ->
182 |                         Either CalendarConversionError
183 |                           (OffsetDateTime calendar @{cal})
184 | fromInstantWithOffset valueInstant valueOffset =
185 |   fromInstant valueOffset valueInstant
186 |
187 | ||| Change the displayed offset while preserving the represented instant.
188 | public export
189 | withOffset : {calendar : Type} -> {auto cal : Calendar calendar} ->
190 |              {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
191 |              Offset -> OffsetDateTime calendar @{cal} ->
192 |              Either CalendarConversionError (OffsetDateTime calendar @{cal})
193 | withOffset valueOffset value = fromInstant valueOffset (toInstant value)
194 |
195 | ||| Change the calendar while preserving the local time, offset, and instant.
196 | public export
197 | withCalendar : {source : Type} -> {target : Type} ->
198 |                {auto sourceCal : Calendar source} ->
199 |                {auto targetCal : Calendar target} ->
200 |                {auto sourceRep : HasCalendarBridge (CalendarDate source @{sourceCal})} ->
201 |                {auto targetRep : HasCalendarBridge (CalendarDate target @{targetCal})} ->
202 |                OffsetDateTime source @{sourceCal} ->
203 |                Either CalendarConversionError (OffsetDateTime target @{targetCal})
204 | withCalendar @{sourceCal} @{targetCal} @{sourceRep} @{targetRep} value =
205 |   map (\converted => MkOffsetDateTime converted value.offsetValue)
206 |     (IotaTime.CalendarDateTime.withCalendar
207 |       @{sourceCal} @{targetCal} @{sourceRep} @{targetRep} value.localValue)
208 |