
  0 | module IotaTime.Pattern.Instant
  1 | 
  2 | import IotaTime.Calendar
  3 | import IotaTime.Calendar.Gregorian
  4 | import IotaTime.CalendarDateTime
  5 | import IotaTime.Instant
  6 | import IotaTime.Offset
  7 | import IotaTime.OffsetDateTime
  8 | import IotaTime.Pattern
  9 | import IotaTime.Pattern.Calendar
 10 | import IotaTime.Pattern.CalendarDate
 11 | import IotaTime.Pattern.CalendarDateTime
 12 | import IotaTime.Pattern.LocalTime
 13 | 
 14 | %default total
 15 | 
 16 | ||| A Gregorian date-time pattern adapted to parse and format UTC instants.
 17 | export
 18 | record InstantPattern state where
 19 |   constructor MkInstantPattern
 20 |   calendarPattern : Pattern state (CalendarDateTime Gregorian)
 21 | 
 22 | calendarDateTimeToInstant : CalendarDateTime Gregorian -> Instant
 23 | calendarDateTimeToInstant value = IotaTime.OffsetDateTime.toInstant
 24 |   (fromCalendarDateTimeWithOffset value empty)
 25 | 
 26 | ||| Build an Instant pattern from a Gregorian CalendarDateTime pattern.
 27 | public export
 28 | instantPattern : Pattern state (CalendarDateTime Gregorian) ->
 29 |                  InstantPattern state
 30 | instantPattern = MkInstantPattern
 31 | 
 32 | ||| Parse an Instant, treating the underlying Gregorian date-time as UTC.
 33 | public export
 34 | parseInstant : InstantPattern state -> String -> Either PatternError Instant
 35 | parseInstant pattern source =
 36 |   map calendarDateTimeToInstant
 37 |     (IotaTime.Pattern.parse pattern.calendarPattern source)
 38 | 
 39 | ||| Format an Instant in UTC. Instants outside the Gregorian calendar's
 40 | ||| supported range return the existing typed calendar conversion error.
 41 | public export
 42 | formatInstant : InstantPattern state -> Instant ->
 43 |                 Either CalendarConversionError String
 44 | formatInstant pattern value = do
 45 |   offsetValue <- IotaTime.OffsetDateTime.fromInstant
 46 |     {calendar = Gregorian} empty value
 47 |   Right (IotaTime.Pattern.format pattern.calendarPattern
 48 |     (toCalendarDateTime offsetValue))
 49 | 
 50 | ||| ISO-8601 UTC at whole-second precision: yyyy-MM-ddTHH:mm:ssZ.
 51 | public export
 52 | pInstant : InstantPattern (DateFields, TimeFields)
 53 | pInstant = instantPattern (ps {calendar = Gregorian} <% char 'Z')
 54 | 
 55 | ||| ISO-8601 UTC with nine fractional digits:
 56 | ||| yyyy-MM-ddTHH:mm:ss.fffffffffZ.
 57 | public export
 58 | pInstantNano : InstantPattern (DateFields, TimeFields)
 59 | pInstantNano = instantPattern (po {calendar = Gregorian} <% char 'Z')