0 | module IotaTime.TimeZone.Core

  2 | import public Data.So

  3 | import public IotaTime.Instant

  4 | import public IotaTime.Offset

  5 | import public IotaTime.OffsetDateTime

  6 | import IotaTime.Internal.Gregorian

  8 | %default total

 11 | record TransitionInfo where

 12 |   constructor MkTransitionInfo

 13 |   storedUtcOffset : Offset

 14 |   storedInDst : Bool

 15 |   storedSavings : Maybe Offset

 16 |   storedAbbreviation : String

 20 | transitionInfo : Offset -> Bool -> String -> TransitionInfo

 21 | transitionInfo valueOffset inDst valueAbbreviation =

 22 |   MkTransitionInfo valueOffset inDst

 23 |     (if inDst then Nothing else Just empty) valueAbbreviation

 27 | transitionInfoWithSavings : Offset -> Offset -> String -> TransitionInfo

 28 | transitionInfoWithSavings valueOffset valueSavings valueAbbreviation =

 29 |   MkTransitionInfo valueOffset (valueSavings /= empty)

 30 |     (Just valueSavings) valueAbbreviation

 33 | utcOffset : TransitionInfo -> Offset

 34 | utcOffset = storedUtcOffset

 37 | isDaylightSavingTime : TransitionInfo -> Bool

 38 | isDaylightSavingTime = storedInDst

 42 | transitionSavings : TransitionInfo -> Maybe Offset

 43 | transitionSavings = storedSavings

 46 | abbreviation : TransitionInfo -> String

 47 | abbreviation = storedAbbreviation

 52 | record ZoneInterval where

 53 |   constructor MkZoneInterval

 54 |   storedIntervalStart : Maybe Instant

 55 |   storedIntervalEnd : Maybe Instant

 56 |   storedIntervalInfo : TransitionInfo

 59 | intervalStart : ZoneInterval -> Maybe Instant

 60 | intervalStart = storedIntervalStart

 63 | intervalEnd : ZoneInterval -> Maybe Instant

 64 | intervalEnd = storedIntervalEnd

 67 | wallOffset : ZoneInterval -> Offset

 68 | wallOffset = utcOffset . storedIntervalInfo

 72 | savings : ZoneInterval -> Maybe Offset

 73 | savings = transitionSavings . storedIntervalInfo

 76 | intervalIsDaylightSavingTime : ZoneInterval -> Bool

 77 | intervalIsDaylightSavingTime = isDaylightSavingTime . storedIntervalInfo

 80 | intervalAbbreviation : ZoneInterval -> String

 81 | intervalAbbreviation = abbreviation . storedIntervalInfo

 84 | record ZoneTransition where

 85 |   constructor MkZoneTransition

 86 |   transitionInstant : Instant

 87 |   transitionInfo : TransitionInfo

 89 | public export

 90 | data TransitionTimeMode = WallTime | StandardTime | UniversalTime

 93 | data RecurrenceDay

 94 |   = JulianWithoutLeap Integer

 95 |   | JulianWithLeap Integer

 96 |   | MonthWeekDay Integer Integer Integer

 98 | public export

 99 | data RecurrenceRuleError

100 |   = JulianDayOutOfRange Integer

101 |   | MonthOutOfRange Integer

102 |   | WeekOutOfRange Integer

103 |   | WeekdayOutOfRange Integer

106 | record RecurrenceRule where

107 |   constructor MkRecurrenceRule

108 |   recurrenceDay : RecurrenceDay

109 |   recurrenceSeconds : Integer

110 |   recurrenceMode : TransitionTimeMode

114 | julianWithoutLeapRule : Integer -> Integer -> TransitionTimeMode ->

115 |                          Either RecurrenceRuleError RecurrenceRule

116 | julianWithoutLeapRule day seconds mode =

117 |   if day >= 1 && day <= 365

118 |     then Right (MkRecurrenceRule (JulianWithoutLeap day) seconds mode)

119 |     else Left (JulianDayOutOfRange day)

123 | julianWithLeapRule : Integer -> Integer -> TransitionTimeMode ->

124 |                       Either RecurrenceRuleError RecurrenceRule

125 | julianWithLeapRule day seconds mode =

126 |   if day >= 0 && day <= 365

127 |     then Right (MkRecurrenceRule (JulianWithLeap day) seconds mode)

128 |     else Left (JulianDayOutOfRange day)

132 | monthWeekDayRule : Integer -> Integer -> Integer -> Integer ->

133 |                    TransitionTimeMode -> Either RecurrenceRuleError RecurrenceRule

134 | monthWeekDayRule month week weekday seconds mode =

135 |   if month < 1 || month > 12 then Left (MonthOutOfRange month)

136 |   else if week < 1 || week > 5 then Left (WeekOutOfRange week)

137 |   else if weekday < 0 || weekday > 6 then Left (WeekdayOutOfRange weekday)

138 |   else Right (MkRecurrenceRule (MonthWeekDay month week weekday) seconds mode)

141 | record ZoneRecurrence where

142 |   constructor MkZoneRecurrence

143 |   standardTransition : TransitionInfo

144 |   daylightTransition : TransitionInfo

145 |   daylightStart : RecurrenceRule

146 |   standardStart : RecurrenceRule

150 | zoneRecurrence : TransitionInfo -> TransitionInfo -> RecurrenceRule ->

151 |                  RecurrenceRule -> ZoneRecurrence

152 | zoneRecurrence = MkZoneRecurrence

155 | record RecurrenceEra where

156 |   constructor MkRecurrenceEra

157 |   eraStart : Maybe Instant

158 |   eraInitialTransition : TransitionInfo

159 |   eraRecurrence : Maybe ZoneRecurrence

162 | record TimeZoneRep where

163 |   constructor MkTimeZone

164 |   storedZoneId : String

165 |   initialTransition : TransitionInfo

166 |   transitions : List ZoneTransition

167 |   recurrenceEras : List RecurrenceEra

169 | public export

170 | TimeZone : Type

171 | TimeZone = TimeZoneRep

173 | public export

174 | Eq TimeZoneRep where

175 |   left == right = left.storedZoneId == right.storedZoneId

177 | public export

178 | Show TimeZoneRep where

179 |   show value = if value.storedZoneId == "UTC"

180 |     then "<TimeZone UTC>"

181 |     else "<TimeZone " ++ show value.storedZoneId ++ ">"

184 | areZoneTransitionsAfter : Integer -> List (Integer, TransitionInfo) -> Bool

185 | areZoneTransitionsAfter previous [] = True

186 | areZoneTransitionsAfter previous ((instant, _) :: rest) =

187 |   previous < instant && areZoneTransitionsAfter instant rest

191 | isValidZoneTransitions : List (Integer, TransitionInfo) -> Bool

192 | isValidZoneTransitions [] = True

193 | isValidZoneTransitions ((instant, _) :: rest) =

194 |   areZoneTransitionsAfter instant rest

196 | toTransitions : List (Integer, TransitionInfo) -> List ZoneTransition

197 | toTransitions [] = []

198 | toTransitions ((instant, valueInfo) :: rest) =

199 |   MkZoneTransition (fromNanosecondsSinceEpoch instant) valueInfo ::

200 |   toTransitions rest

204 | fixedTimeZone : String -> Offset -> TimeZone

205 | fixedTimeZone valueId valueOffset =

206 |   MkTimeZone valueId (transitionInfo valueOffset False valueId) [] []

211 | timeZoneFromTransitions : (valueId : String) ->

212 |                           (valueInitialInfo : TransitionInfo) ->

213 |                           (valueTransitions : List (Integer, TransitionInfo)) ->

214 |                           {auto 0 valid : So

215 |                             (isValidZoneTransitions valueTransitions)} ->

216 |                           TimeZone

217 | timeZoneFromTransitions valueId valueInitialInfo valueTransitions =

218 |   MkTimeZone valueId valueInitialInfo (toTransitions valueTransitions) []

220 | public export

221 | data TimeZoneError

222 |   = TransitionsNotStrictlyIncreasing

223 |   | RecurrenceErasNotStrictlyIncreasing

224 |   | MissingRecurrenceEra

226 | runtimeTransitionsValid : List (Instant, TransitionInfo) -> Bool

227 | runtimeTransitionsValid [] = True

228 | runtimeTransitionsValid ((instant, _) :: rest) = go instant rest

229 |   where

230 |     go : Instant -> List (Instant, TransitionInfo) -> Bool

231 |     go previous [] = True

232 |     go previous ((next, _) :: remaining) =

233 |       previous < next && go next remaining

235 | toRuntimeTransitions : List (Instant, TransitionInfo) -> List ZoneTransition

236 | toRuntimeTransitions [] = []

237 | toRuntimeTransitions ((instant, valueInfo) :: rest) =

238 |   MkZoneTransition instant valueInfo :: toRuntimeTransitions rest

242 | refineTimeZone : String -> TransitionInfo -> List (Instant, TransitionInfo) ->

243 |                  Either TimeZoneError TimeZone

244 | refineTimeZone valueId valueInitialInfo valueTransitions =

245 |   if runtimeTransitionsValid valueTransitions

246 |     then Right (MkTimeZone valueId valueInitialInfo

247 |       (toRuntimeTransitions valueTransitions) [])

248 |     else Left TransitionsNotStrictlyIncreasing

252 | refineRecurringTimeZone : String -> TransitionInfo ->

253 |                           List (Instant, TransitionInfo) -> ZoneRecurrence ->

254 |                           Either TimeZoneError TimeZone

255 | refineRecurringTimeZone valueId valueInitialInfo valueTransitions recurrence =

256 |   if runtimeTransitionsValid valueTransitions

257 |     then let (boundary, initial) = finalExplicit valueInitialInfo valueTransitions

258 |           in Right (MkTimeZone valueId valueInitialInfo

259 |             (toRuntimeTransitions valueTransitions)

260 |             [MkRecurrenceEra boundary initial (Just recurrence)])

261 |     else Left TransitionsNotStrictlyIncreasing

262 |   where

263 |     finalExplicit : TransitionInfo -> List (Instant, TransitionInfo) ->

264 |                     (Maybe Instant, TransitionInfo)

265 |     finalExplicit initial [] = (Nothing, initial)

266 |     finalExplicit initial ((instant, info) :: rest) = go instant info rest

267 |       where

268 |         go : Instant -> TransitionInfo -> List (Instant, TransitionInfo) ->

269 |              (Maybe Instant, TransitionInfo)

270 |         go instant info [] = (Just instant, info)

271 |         go instant info ((next, nextInfo) :: remaining) =

272 |           go next nextInfo remaining

275 | zoneId : TimeZone -> String

276 | zoneId = storedZoneId

278 | recurrenceNanosecondsPerSecond : Integer

279 | recurrenceNanosecondsPerSecond = 1000000000

281 | recurrenceSecondsPerDay : Integer

282 | recurrenceSecondsPerDay = 86400

284 | isGregorianLeapYear : Integer -> Bool

285 | isGregorianLeapYear year =

286 |   year `mod` 400 == 0 || (year `mod` 4 == 0 && year `mod` 100 /= 0)

288 | gregorianYearFromDays : Integer -> Integer

289 | gregorianYearFromDays days =

290 |   let (year, _, _) = gregorianCivilFromDays days

291 |    in year

293 | daysInGregorianMonth : Integer -> Integer -> Integer

294 | daysInGregorianMonth year 2 = if isGregorianLeapYear year then 29 else 28

295 | daysInGregorianMonth year month =

296 |   if month == 4 || month == 6 || month == 9 || month == 11 then 30 else 31

298 | recurrenceDayInYear : Integer -> RecurrenceDay -> Integer

299 | recurrenceDayInYear year (JulianWithoutLeap day) =

300 |   gregorianDaysFromCivil year 1 1 + day - 1 +

301 |     if isGregorianLeapYear year && day >= 60 then 1 else 0

302 | recurrenceDayInYear year (JulianWithLeap day) =

303 |   gregorianDaysFromCivil year 1 1 + day

304 | recurrenceDayInYear year (MonthWeekDay month week weekday) =

305 |   let first = gregorianDaysFromCivil year month 1

306 |    in let firstWeekday = (first + 3) `mod` 7

307 |      in let candidate = first + (weekday - firstWeekday) `mod` 7 + 7 * (week - 1)

308 |        in if candidate >= first + daysInGregorianMonth year month

309 |             then candidate - 7

310 |             else candidate

312 | transitionAdjustment : ZoneRecurrence -> TransitionInfo ->

313 |                        TransitionTimeMode -> Integer

314 | transitionAdjustment recurrence before UniversalTime = 0

315 | transitionAdjustment recurrence before StandardTime =

316 |   totalOffsetSeconds (utcOffset recurrence.standardTransition)

317 | transitionAdjustment recurrence before WallTime =

318 |   totalOffsetSeconds (utcOffset before)

320 | ruleInstant : ZoneRecurrence -> Integer -> TransitionInfo -> RecurrenceRule -> Instant

321 | ruleInstant recurrence year before rule =

322 |   let day = recurrenceDayInYear year rule.recurrenceDay

323 |    in let adjustment = transitionAdjustment recurrence before rule.recurrenceMode

324 |      in fromNanosecondsSinceEpoch

325 |           ((day * recurrenceSecondsPerDay + rule.recurrenceSeconds - adjustment) *

326 |             recurrenceNanosecondsPerSecond)

328 | recurrenceEvents : ZoneRecurrence -> Integer -> List (Instant, TransitionInfo)

329 | recurrenceEvents recurrence year =

330 |   order

331 |     (ruleInstant recurrence year recurrence.standardTransition

332 |       recurrence.daylightStart, recurrence.daylightTransition)

333 |     (ruleInstant recurrence year recurrence.daylightTransition

334 |       recurrence.standardStart, recurrence.standardTransition)

335 |   where

336 |     order : (Instant, TransitionInfo) -> (Instant, TransitionInfo) ->

337 |             List (Instant, TransitionInfo)

338 |     order first@(firstInstant, _) second@(secondInstant, _) =

339 |       if firstInstant <= secondInstant then [first, second] else [second, first]

341 | recurringIntervalAt : ZoneRecurrence -> Maybe Instant -> Maybe Instant ->

342 |                       TransitionInfo -> Instant -> ZoneInterval

343 | recurringIntervalAt recurrence eraStart eraEnd initial query =

344 |   choose eraStart initial events

345 |   where

346 |     queryDay = toNanosecondsSinceEpoch query `div`

347 |       (recurrenceSecondsPerDay * recurrenceNanosecondsPerSecond)

348 |     queryYear = gregorianYearFromDays queryDay

349 |     events = recurrenceEvents recurrence (queryYear - 1) ++

350 |       recurrenceEvents recurrence queryYear ++

351 |       recurrenceEvents recurrence (queryYear + 1)

353 |     afterStart : Instant -> Bool

354 |     afterStart event = case eraStart of

355 |       Nothing => True

356 |       Just boundary => event > boundary

358 |     beforeEnd : Instant -> Bool

359 |     beforeEnd event = case eraEnd of

360 |       Nothing => True

361 |       Just boundary => event < boundary

363 |     choose : Maybe Instant -> TransitionInfo ->

364 |              List (Instant, TransitionInfo) -> ZoneInterval

365 |     choose start current [] = MkZoneInterval start eraEnd current

366 |     choose start current ((event, info) :: rest) =

367 |       if not (afterStart event) then choose start current rest

368 |       else if not (beforeEnd event) then MkZoneInterval start eraEnd current

369 |       else if event <= query then choose (Just event) info rest

370 |       else MkZoneInterval start (Just event) current

372 | recurringTransitionAt : ZoneRecurrence -> Maybe Instant -> TransitionInfo ->

373 |                         Instant -> TransitionInfo

374 | recurringTransitionAt recurrence cutoff initial query =

375 |   chooseLatest cutoff initial events

376 |   where

377 |     queryDay = toNanosecondsSinceEpoch query `div`

378 |       (recurrenceSecondsPerDay * recurrenceNanosecondsPerSecond)

379 |     queryYear = gregorianYearFromDays queryDay

380 |     events = recurrenceEvents recurrence (queryYear - 1) ++

381 |       recurrenceEvents recurrence queryYear ++

382 |       recurrenceEvents recurrence (queryYear + 1)

384 |     afterCutoff : Maybe Instant -> Instant -> Bool

385 |     afterCutoff Nothing event = True

386 |     afterCutoff (Just boundary) event = event > boundary

388 |     chooseLatest : Maybe Instant -> TransitionInfo ->

389 |                    List (Instant, TransitionInfo) -> TransitionInfo

390 |     chooseLatest boundary current [] = current

391 |     chooseLatest boundary current ((event, info) :: rest) =

392 |       if afterCutoff boundary event && event <= query

393 |         then chooseLatest (Just event) info rest

394 |         else chooseLatest boundary current rest

396 | eraInitial : Maybe Instant -> ZoneRecurrence -> TransitionInfo

397 | eraInitial Nothing recurrence = recurrence.standardTransition

398 | eraInitial (Just start) recurrence = recurringTransitionAt recurrence Nothing

399 |   recurrence.standardTransition start

401 | eraSpecsValid : List (Maybe Instant, ZoneRecurrence) -> Bool

402 | eraSpecsValid [] = False

403 | eraSpecsValid ((start, _) :: rest) = go start rest

404 |   where

405 |     go : Maybe Instant -> List (Maybe Instant, ZoneRecurrence) -> Bool

406 |     go previous [] = True

407 |     go previous ((next, _) :: remaining) = case (previous, next) of

408 |       (_, Nothing) => False

409 |       (Nothing, Just next) => go (Just next) remaining

410 |       (Just previous, Just next) =>

411 |         previous < next && go (Just next) remaining

413 | toRecurrenceEras : List (Maybe Instant, ZoneRecurrence) -> List RecurrenceEra

414 | toRecurrenceEras [] = []

415 | toRecurrenceEras ((start, recurrence) :: rest) =

416 |   MkRecurrenceEra start (eraInitial start recurrence) (Just recurrence) ::

417 |   toRecurrenceEras rest

419 | zoneEraSpecsValid : List (Maybe Instant, TransitionInfo, Maybe ZoneRecurrence) -> Bool

420 | zoneEraSpecsValid [] = False

421 | zoneEraSpecsValid ((start, _, _) :: rest) = go start rest

422 |   where

423 |     go : Maybe Instant ->

424 |          List (Maybe Instant, TransitionInfo, Maybe ZoneRecurrence) -> Bool

425 |     go previous [] = True

426 |     go previous ((next, _, _) :: remaining) = case (previous, next) of

427 |       (_, Nothing) => False

428 |       (Nothing, Just next) => go (Just next) remaining

429 |       (Just previous, Just next) =>

430 |         previous < next && go (Just next) remaining

432 | toZoneEras : List (Maybe Instant, TransitionInfo, Maybe ZoneRecurrence) ->

433 |              List RecurrenceEra

434 | toZoneEras [] = []

435 | toZoneEras ((start, initial, recurrence) :: rest) =

436 |   MkRecurrenceEra start computed recurrence :: toZoneEras rest

437 |   where

438 |     computed : TransitionInfo

439 |     computed = case recurrence of

440 |       Nothing => initial

441 |       Just value => case start of

442 |         Nothing => initial

443 |         Just boundary => recurringTransitionAt value Nothing initial boundary

447 | refineTimeZoneEras : String ->

448 |   List (Maybe Instant, TransitionInfo, Maybe ZoneRecurrence) ->

449 |   Either TimeZoneError TimeZone

450 | refineTimeZoneEras valueId specs =

451 |   if zoneEraSpecsValid specs

452 |     then case toZoneEras specs of

453 |       [] => Left MissingRecurrenceEra

454 |       first :: eras => Right (MkTimeZone valueId

455 |         first.eraInitialTransition [] (first :: eras))

456 |     else case specs of

457 |       [] => Left MissingRecurrenceEra

458 |       _ => Left RecurrenceErasNotStrictlyIncreasing

463 | refineRecurrenceErasTimeZone : String ->

464 |   List (Maybe Instant, ZoneRecurrence) -> Either TimeZoneError TimeZone

465 | refineRecurrenceErasTimeZone valueId specs =

466 |   if eraSpecsValid specs

467 |     then case toRecurrenceEras specs of

468 |       [] => Left MissingRecurrenceEra

469 |       first :: eras => Right (MkTimeZone valueId

470 |         first.eraInitialTransition [] (first :: eras))

471 |     else case specs of

472 |       [] => Left MissingRecurrenceEra

473 |       _ => Left RecurrenceErasNotStrictlyIncreasing

475 | recurrenceIntervalAt : List RecurrenceEra -> Instant -> Maybe ZoneInterval

476 | recurrenceIntervalAt eras query = case select Nothing eras of

477 |   (Nothing, _) => Nothing

478 |   (Just era, nextStart) => case era.eraRecurrence of

479 |     Nothing => Just (MkZoneInterval era.eraStart nextStart

480 |       era.eraInitialTransition)

481 |     Just recurrence => Just (recurringIntervalAt recurrence era.eraStart

482 |       nextStart era.eraInitialTransition query)

483 |   where

484 |     startsBy : Maybe Instant -> Instant -> Bool

485 |     startsBy Nothing value = True

486 |     startsBy (Just start) value = start <= value

488 |     select : Maybe RecurrenceEra -> List RecurrenceEra ->

489 |              (Maybe RecurrenceEra, Maybe Instant)

490 |     select selected [] = (selected, Nothing)

491 |     select selected (era :: rest) =

492 |       if startsBy era.eraStart query

493 |         then select (Just era) rest

494 |         else (selected, era.eraStart)

496 | firstEraStart : List RecurrenceEra -> Maybe Instant

497 | firstEraStart [] = Nothing

498 | firstEraStart (era :: _) = era.eraStart

502 | zoneIntervalAt : TimeZone -> Instant -> ZoneInterval

503 | zoneIntervalAt valueZone valueInstant = go Nothing

504 |   valueZone.initialTransition valueZone.transitions

505 |   where

506 |     go : Maybe Instant -> TransitionInfo -> List ZoneTransition -> ZoneInterval

507 |     go start current [] = case recurrenceIntervalAt

508 |       valueZone.recurrenceEras valueInstant of

509 |         Just interval => interval

510 |         Nothing => MkZoneInterval start

511 |           (firstEraStart valueZone.recurrenceEras) current

512 |     go start current (transition :: rest) =

513 |       if valueInstant < transition.transitionInstant

514 |         then MkZoneInterval start (Just transition.transitionInstant) current

515 |         else go (Just transition.transitionInstant) transition.transitionInfo rest

518 | activeTransitionAt : TimeZone -> Instant -> TransitionInfo

519 | activeTransitionAt valueZone valueInstant =

520 |   (zoneIntervalAt valueZone valueInstant).storedIntervalInfo

523 | zoneOffsetAt : TimeZone -> Instant -> Offset

524 | zoneOffsetAt valueZone = utcOffset . activeTransitionAt valueZone

526 | addUnique : Offset -> List Offset -> List Offset

527 | addUnique value [] = [value]

528 | addUnique value (current :: rest) =

529 |   if value == current then current :: rest

530 |   else current :: addUnique value rest

532 | zoneOffsets : TimeZone -> List Offset

533 | zoneOffsets valueZone =

534 |   recurrenceOffsets valueZone.recurrenceEras valueZone.transitions

535 |   where

536 |     go : List Offset -> List ZoneTransition -> List Offset

537 |     go values [] = values

538 |     go values (transition :: rest) =

539 |       go (addUnique (utcOffset transition.transitionInfo) values) rest

541 |     addEraOffsets : List Offset -> List RecurrenceEra -> List Offset

542 |     addEraOffsets offsets [] = offsets

543 |     addEraOffsets offsets (era :: eras) = case era.eraRecurrence of

544 |       Nothing => addEraOffsets

545 |         (addUnique (utcOffset era.eraInitialTransition) offsets) eras

546 |       Just recurrence => addEraOffsets

547 |         (addUnique (utcOffset recurrence.daylightTransition)

548 |           (addUnique (utcOffset recurrence.standardTransition) offsets)) eras

550 |     recurrenceOffsets : List RecurrenceEra -> List ZoneTransition -> List Offset

551 |     recurrenceOffsets [] transitions =

552 |       go [utcOffset valueZone.initialTransition] transitions

553 |     recurrenceOffsets eras transitions =

554 |       go (addEraOffsets [utcOffset valueZone.initialTransition] eras) transitions

556 | insertByInstant : {calendar : Type} -> {auto cal : Calendar calendar} ->

557 |                   {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->

558 |                   OffsetDateTime calendar @{cal} ->

559 |                   List (OffsetDateTime calendar @{cal}) ->

560 |                   List (OffsetDateTime calendar @{cal})

561 | insertByInstant value [] = [value]

562 | insertByInstant value (current :: rest) =

563 |   if toInstant value <= toInstant current

564 |     then value :: current :: rest

565 |     else current :: insertByInstant value rest

568 | mappingCandidates : {calendar : Type} -> {auto cal : Calendar calendar} ->

569 |                     {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->

570 |                     TimeZone -> CalendarDateTime calendar @{cal} ->

571 |                     List (OffsetDateTime calendar @{cal})

572 | mappingCandidates valueZone local = go (zoneOffsets valueZone)

573 |   where

574 |     go : List Offset -> List (OffsetDateTime calendar @{cal})

575 |     go [] = []

576 |     go (valueOffset :: rest) =

577 |       let candidate = atOffset local valueOffset

578 |           remaining = go rest

579 |        in if zoneOffsetAt valueZone (toInstant candidate) == valueOffset

580 |             then insertByInstant candidate remaining

581 |             else remaining

583 | nanosecondsPerSecond : Integer

584 | nanosecondsPerSecond = 1000000000

586 | findLenientGapMapping : {calendar : Type} -> {auto cal : Calendar calendar} ->

587 |                         {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->

588 |                         CalendarDateTime calendar @{cal} -> TransitionInfo ->

589 |                         List ZoneTransition ->

590 |                         Either CalendarConversionError

591 |                           (Maybe (OffsetDateTime calendar @{cal}))

592 | findLenientGapMapping local current [] = Right Nothing

593 | findLenientGapMapping local current (transition :: rest) =

594 |   let beforeOffset = utcOffset current

595 |       afterOffset = utcOffset transition.transitionInfo

596 |       beforeSeconds = totalOffsetSeconds beforeOffset

597 |       afterSeconds = totalOffsetSeconds afterOffset

598 |       candidate = atOffset local beforeOffset

599 |       candidateInstant = toInstant candidate

600 |       transitionNanos = toNanosecondsSinceEpoch transition.transitionInstant

601 |       gapNanos = (afterSeconds - beforeSeconds) * nanosecondsPerSecond

602 |       candidateNanos = toNanosecondsSinceEpoch candidateInstant

603 |    in if afterSeconds > beforeSeconds &&

604 |          candidateNanos >= transitionNanos &&

605 |          candidateNanos < transitionNanos + gapNanos

606 |         then map Just shifted

607 |         else findLenientGapMapping local transition.transitionInfo rest

608 |   where

609 |     shifted : Either CalendarConversionError (OffsetDateTime calendar @{cal})

610 |     shifted = IotaTime.OffsetDateTime.fromInstant

611 |       (utcOffset transition.transitionInfo) (toInstant (atOffset local (utcOffset current)))

613 | findLenientGapByOffsets : {calendar : Type} -> {auto cal : Calendar calendar} ->

614 |                           {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->

615 |                           TimeZone -> CalendarDateTime calendar @{cal} -> List Offset ->

616 |                           Either CalendarConversionError

617 |                             (Maybe (OffsetDateTime calendar @{cal}))

618 | findLenientGapByOffsets valueZone local [] = Right Nothing

619 | findLenientGapByOffsets valueZone local (before :: rest) =

620 |   let candidate = atOffset local before

621 |       candidateInstant = toInstant candidate

622 |       after = zoneOffsetAt valueZone candidateInstant

623 |    in if totalOffsetSeconds after > totalOffsetSeconds before

624 |         then map Just (IotaTime.OffsetDateTime.fromInstant after candidateInstant)

625 |         else findLenientGapByOffsets valueZone local rest

628 | lenientLocalMapping : {calendar : Type} -> {auto cal : Calendar calendar} ->

629 |                       {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->

630 |                       TimeZone -> CalendarDateTime calendar @{cal} ->

631 |                       Either CalendarConversionError

632 |                         (Maybe (OffsetDateTime calendar @{cal}))

633 | lenientLocalMapping valueZone local = case mappingCandidates valueZone local of

634 |   [] => do

635 |     explicit <- findLenientGapMapping local valueZone.initialTransition

636 |       valueZone.transitions

637 |     case explicit of

638 |       Just value => Right (Just value)

639 |       Nothing => findLenientGapByOffsets valueZone local (zoneOffsets valueZone)

640 |   first :: _ => Right (Just first)