IotaTime.TimeZone.Core

Reexports

Definitions

record TransitionInfo : Type

Totality: total
Visibility: export
Constructor: 

MkTransitionInfo : Offset -> Bool -> Maybe Offset -> String -> TransitionInfo

Projections:

.storedAbbreviation : TransitionInfo -> String

.storedInDst : TransitionInfo -> Bool

.storedSavings : TransitionInfo -> Maybe Offset

.storedUtcOffset : TransitionInfo -> Offset

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

  Describe the zone state effective over a timeline segment.

Totality: total
Visibility: export

transitionInfoWithSavings : Offset -> Offset -> String -> TransitionInfo

  Describe zone state with an exact daylight-saving adjustment.

Totality: total
Visibility: export

utcOffset : TransitionInfo -> Offset

Totality: total
Visibility: export

isDaylightSavingTime : TransitionInfo -> Bool

Totality: total
Visibility: export

transitionSavings : TransitionInfo -> Maybe Offset

  The daylight-saving adjustment, when the source data identifies it.

Totality: total
Visibility: export

abbreviation : TransitionInfo -> String

Totality: total
Visibility: export

record ZoneInterval : Type

  The zone state and timeline bounds effective at an instant. `Nothing`
  denotes an unbounded endpoint.

Totality: total
Visibility: export
Constructor: 

MkZoneInterval : Maybe Instant -> Maybe Instant -> TransitionInfo -> ZoneInterval

Projections:

.storedIntervalEnd : ZoneInterval -> Maybe Instant

.storedIntervalInfo : ZoneInterval -> TransitionInfo

.storedIntervalStart : ZoneInterval -> Maybe Instant

intervalStart : ZoneInterval -> Maybe Instant

Totality: total
Visibility: export

intervalEnd : ZoneInterval -> Maybe Instant

Totality: total
Visibility: export

wallOffset : ZoneInterval -> Offset

Totality: total
Visibility: export

savings : ZoneInterval -> Maybe Offset

  The daylight-saving adjustment, when the zone source identifies it.

Totality: total
Visibility: export

intervalIsDaylightSavingTime : ZoneInterval -> Bool

Totality: total
Visibility: export

intervalAbbreviation : ZoneInterval -> String

Totality: total
Visibility: export

record ZoneTransition : Type

Totality: total
Visibility: export
Constructor: 

MkZoneTransition : Instant -> TransitionInfo -> ZoneTransition

Projections:

.transitionInfo : ZoneTransition -> TransitionInfo

.transitionInstant : ZoneTransition -> Instant

data TransitionTimeMode : Type

Totality: total
Visibility: public export
Constructors:

WallTime : TransitionTimeMode

StandardTime : TransitionTimeMode

UniversalTime : TransitionTimeMode

data RecurrenceDay : Type

Totality: total
Visibility: export
Constructors:

JulianWithoutLeap : Integer -> RecurrenceDay

JulianWithLeap : Integer -> RecurrenceDay

MonthWeekDay : Integer -> Integer -> Integer -> RecurrenceDay

data RecurrenceRuleError : Type

Totality: total
Visibility: public export
Constructors:

JulianDayOutOfRange : Integer -> RecurrenceRuleError

MonthOutOfRange : Integer -> RecurrenceRuleError

WeekOutOfRange : Integer -> RecurrenceRuleError

WeekdayOutOfRange : Integer -> RecurrenceRuleError

record RecurrenceRule : Type

Totality: total
Visibility: export
Constructor: 

MkRecurrenceRule : RecurrenceDay -> Integer -> TransitionTimeMode -> RecurrenceRule

Projections:

.recurrenceDay : RecurrenceRule -> RecurrenceDay

.recurrenceMode : RecurrenceRule -> TransitionTimeMode

.recurrenceSeconds : RecurrenceRule -> Integer

julianWithoutLeapRule : Integer -> Integer -> TransitionTimeMode -> Either RecurrenceRuleError RecurrenceRule

  Validate a one-based Julian day that omits February 29.

Totality: total
Visibility: export

julianWithLeapRule : Integer -> Integer -> TransitionTimeMode -> Either RecurrenceRuleError RecurrenceRule

  Validate a zero-based Julian day that includes February 29.

Totality: total
Visibility: export

monthWeekDayRule : Integer -> Integer -> Integer -> Integer -> TransitionTimeMode -> Either RecurrenceRuleError RecurrenceRule

  Validate an Mm.w.d POSIX transition day.

Totality: total
Visibility: export

record ZoneRecurrence : Type

Totality: total
Visibility: export
Constructor: 

MkZoneRecurrence : TransitionInfo -> TransitionInfo -> RecurrenceRule -> RecurrenceRule -> ZoneRecurrence

Projections:

.daylightStart : ZoneRecurrence -> RecurrenceRule

.daylightTransition : ZoneRecurrence -> TransitionInfo

.standardStart : ZoneRecurrence -> RecurrenceRule

.standardTransition : ZoneRecurrence -> TransitionInfo

zoneRecurrence : TransitionInfo -> TransitionInfo -> RecurrenceRule -> RecurrenceRule -> ZoneRecurrence

  Construct recurring standard/daylight rules from validated transition days.

Totality: total
Visibility: export

record RecurrenceEra : Type

Totality: total
Visibility: export
Constructor: 

MkRecurrenceEra : Maybe Instant -> TransitionInfo -> Maybe ZoneRecurrence -> RecurrenceEra

Projections:

.eraInitialTransition : RecurrenceEra -> TransitionInfo

.eraRecurrence : RecurrenceEra -> Maybe ZoneRecurrence

.eraStart : RecurrenceEra -> Maybe Instant

record TimeZoneRep : Type

Totality: total
Visibility: export
Constructor: 

MkTimeZone : String -> TransitionInfo -> List ZoneTransition -> List RecurrenceEra -> TimeZoneRep

Projections:

.initialTransition : TimeZoneRep -> TransitionInfo

.recurrenceEras : TimeZoneRep -> List RecurrenceEra

.storedZoneId : TimeZoneRep -> String

.transitions : TimeZoneRep -> List ZoneTransition

Hints:

Eq TimeZoneRep

Show TimeZoneRep

TimeZone : Type

Totality: total
Visibility: public export

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

Totality: total
Visibility: export

isValidZoneTransitions : List (Integer, TransitionInfo) -> Bool

  Whether transition instants are strictly increasing.

Totality: total
Visibility: export

fixedTimeZone : String -> Offset -> TimeZone

  Construct a fixed-offset zone.

Totality: total
Visibility: export

timeZoneFromTransitions : String -> TransitionInfo -> (valueTransitions : List (Integer, TransitionInfo)) -> {auto 0 _ : So (isValidZoneTransitions valueTransitions)} -> TimeZone

  Construct a transition zone from statically known, strictly increasing
  nanosecond instants and the offsets effective from those instants onward.

Totality: total
Visibility: export

data TimeZoneError : Type

Totality: total
Visibility: public export
Constructors:

TransitionsNotStrictlyIncreasing : TimeZoneError

RecurrenceErasNotStrictlyIncreasing : TimeZoneError

MissingRecurrenceEra : TimeZoneError

refineTimeZone : String -> TransitionInfo -> List (Instant, TransitionInfo) -> Either TimeZoneError TimeZone

  Validate transition data learned at runtime.

Totality: total
Visibility: export

refineRecurringTimeZone : String -> TransitionInfo -> List (Instant, TransitionInfo) -> ZoneRecurrence -> Either TimeZoneError TimeZone

  Validate explicit transitions and attach recurring rules used after them.

Totality: total
Visibility: export

zoneId : TimeZone -> String

Totality: total
Visibility: export

refineTimeZoneEras : String -> List (Maybe Instant, (TransitionInfo, Maybe ZoneRecurrence)) -> Either TimeZoneError TimeZone

  Validate ordered fixed or recurring eras for a platform adapter.

Totality: total
Visibility: export

refineRecurrenceErasTimeZone : String -> List (Maybe Instant, ZoneRecurrence) -> Either TimeZoneError TimeZone

  Validate ordered recurrence eras. An initial `Nothing` boundary applies
  without a lower timeline bound; subsequent boundaries must increase.

Totality: total
Visibility: export

zoneIntervalAt : TimeZone -> Instant -> ZoneInterval

  Query the complete zone interval effective at an instant.

Totality: total
Visibility: export

activeTransitionAt : TimeZone -> Instant -> TransitionInfo

Totality: total
Visibility: export

zoneOffsetAt : TimeZone -> Instant -> Offset

Totality: total
Visibility: export

mappingCandidates : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => TimeZone -> CalendarDateTime calendar -> List (OffsetDateTime calendar)

Totality: total
Visibility: export

lenientLocalMapping : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => TimeZone -> CalendarDateTime calendar -> Either CalendarConversionError (Maybe (OffsetDateTime calendar))

Totality: total
Visibility: export