IotaTime.Pattern.Locale

Definitions

data StrftimeError : Type

  Failure to translate an operating-system `strftime` layout into a typed
  iotaTime pattern.

Totality: total
Visibility: public export
Constructors:

UnsupportedSpecifier : Char -> StrftimeError

DanglingPercent : StrftimeError

MissingOffsetSpecifier : StrftimeError

MissingZoneSpecifier : StrftimeError

Hints:

Eq StrftimeError

Show StrftimeError

localeDatePattern : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Either StrftimeError (Pattern DateFields (CalendarDate calendar))

  Compile the operating system's preferred date layout for a calendar.

Totality: total
Visibility: public export

localeTimePattern : Locale -> Either StrftimeError (Pattern TimeFields LocalTime)

  Compile the operating system's preferred local-time layout.

Totality: total
Visibility: public export

record DateTimeFieldsRep : Type

  Parser state for a combined calendar date and local-time pattern.

Totality: total
Visibility: export
Constructor: 

MkDateTimeFields : DateFields -> TimeFields -> DateTimeFieldsRep

Projections:

.parsedDateFields : DateTimeFieldsRep -> DateFields

.parsedTimeFields : DateTimeFieldsRep -> TimeFields

DateTimeFields : Type

  Opaque parser state for combined calendar date and local-time patterns.

Totality: total
Visibility: public export

dateTimeFields : DateFields -> TimeFields -> DateTimeFields

  Combine date and time seeds for `parseWith` on a partial date-time pattern.

Totality: total
Visibility: public export

localeDateTimePattern : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Either StrftimeError (Pattern DateTimeFields (CalendarDateTime calendar))

  Compile the operating system's preferred local date-time layout for a calendar.

Totality: total
Visibility: public export

localeOffsetDateTimePattern : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Locale -> Either StrftimeError (Pattern (DateTimeFields, Offset) (OffsetDateTime calendar))

  Compile the operating system's preferred offset date-time layout for a calendar.

Totality: total
Visibility: public export

data ZonedPatternError : Type -> Type -> Type

  Errors from layout compilation, local parsing, zone loading, or local-time
  resolution while parsing a zoned date-time.

Totality: total
Visibility: public export
Constructors:

ZonedLayoutError : StrftimeError -> ZonedPatternError providerError resolverError

ZonedParseError : PatternError -> ZonedPatternError providerError resolverError

ZonedProviderError : providerError -> ZonedPatternError providerError resolverError

ZonedResolutionError : resolverError -> ZonedPatternError providerError resolverError

parseZonedDateTime : {default Gregorian calendar : Type} -> {auto patterned : CalendarPattern calendar} -> Monad m => (String -> m (Either providerError TimeZone)) -> (CalendarDateTime calendar -> TimeZone -> Either resolverError (ZonedDateTime calendar)) -> Locale -> String -> m (Either (ZonedPatternError providerError resolverError) (ZonedDateTime calendar))

  Parse a locale %Z layout, load the captured zone in any `Monad`, and resolve
  local time.

Totality: total
Visibility: public export