IotaTime.Pattern.ZonedDateTime

Definitions

record ZonedDateTimePattern : Type -> Type -> Type

  A format-only ZonedDateTime pattern. Parsing requires loading a zone and
  choosing how skipped or ambiguous local times are resolved.

Totality: total
Visibility: export
Constructor: 

MkZonedDateTimePattern : (value -> String) -> ZonedDateTimePattern state value

Projection: 

.zonedFormatPart : ZonedDateTimePattern state value -> value -> String

zonedDateTimePattern : {auto patterned : CalendarPattern calendar} -> Pattern state (CalendarDateTime calendar) -> (ZonedDateTime calendar -> String) -> ZonedDateTimePattern state (ZonedDateTime calendar)

  Build a format-only ZonedDateTime pattern from a local date-time pattern
  and a function that renders the zone suffix.

Totality: total
Visibility: public export

formatZonedDateTime : ZonedDateTimePattern state value -> value -> String

  Format a zoned value using its local date-time and rendered zone suffix.

Totality: total
Visibility: public export

pZonedDateTime : {auto patterned : CalendarPattern calendar} -> ZonedDateTimePattern (DateFields, TimeFields) (ZonedDateTime calendar)

  ISO local date-time followed by a space and the zone ID.

Totality: total
Visibility: public export

pZonedDateTimeQuoted : {auto patterned : CalendarPattern calendar} -> ZonedDateTimePattern (DateFields, TimeFields) (ZonedDateTime calendar)

  ISO local date-time followed by a quoted, escaped zone ID. This form can
  represent Windows identifiers containing spaces.

Totality: total
Visibility: public export

data ZonedDateTimePatternError : Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

ZonedDateTimeParseError : PatternError -> ZonedDateTimePatternError providerError resolverError

ZonedDateTimeProviderError : providerError -> ZonedDateTimePatternError providerError resolverError

ZonedDateTimeResolutionError : resolverError -> ZonedDateTimePatternError providerError resolverError

parseZonedDateTimePatternWith : Monad m => {auto patterned : CalendarPattern calendar} -> Pattern state (CalendarDateTime calendar) -> Pattern zoneState String -> (String -> m (Either providerError TimeZone)) -> (CalendarDateTime calendar -> TimeZone -> Either resolverError (ZonedDateTime calendar)) -> String -> m (Either (ZonedDateTimePatternError providerError resolverError) (ZonedDateTime calendar))

  Parse using explicit local date-time and zone-ID patterns, then load and
  resolve the captured zone. This lets protocols choose token or quoted zone
  syntax in advance.

Totality: total
Visibility: public export

parseZonedDateTimeWith : Monad m => {auto patterned : CalendarPattern calendar} -> Pattern state (CalendarDateTime calendar) -> (String -> m (Either providerError TimeZone)) -> (CalendarDateTime calendar -> TimeZone -> Either resolverError (ZonedDateTime calendar)) -> String -> m (Either (ZonedDateTimePatternError providerError resolverError) (ZonedDateTime calendar))

  Parse using a local date-time pattern, load the captured zone ID, and
  resolve the local value according to the caller's chosen policy.
  The provider effect is any `Monad`, allowing use from `IO`, effect
  interpreters, or pure test monads.

Totality: total
Visibility: public export

parseStandardZonedDateTime : Monad m => {auto patterned : CalendarPattern calendar} -> (String -> m (Either providerError TimeZone)) -> (CalendarDateTime calendar -> TimeZone -> Either resolverError (ZonedDateTime calendar)) -> String -> m (Either (ZonedDateTimePatternError providerError resolverError) (ZonedDateTime calendar))

  Parse the standard ISO local date-time and zone-ID layout in the provider's
  monad.

Totality: total
Visibility: public export