0 | module IotaTime.CalendarDateTime
  1 |
  2 | import IotaTime.Calendar
  3 | import IotaTime.Internal.ApplyPeriod
  4 | import IotaTime.LocalTime
  5 | import IotaTime.Period
  6 |
  7 | %default total
  8 |
  9 | nanosecondsPerDay : Integer
 10 | nanosecondsPerDay = 86400 * 1000000000
 11 |
 12 | ||| A calendar date paired with a local time of day.
 13 | public export
 14 | record CalendarDateTimeRep (calendar : Type) (cal : Calendar calendar) where
 15 |   constructor MkCalendarDateTime
 16 |   date : CalendarDate calendar @{cal}
 17 |   time : LocalTime
 18 |
 19 | ||| The date-time representation selected by a calendar implementation.
 20 | public export
 21 | CalendarDateTime : (calendar : Type) -> {auto cal : Calendar calendar} -> Type
 22 | CalendarDateTime calendar @{cal} = CalendarDateTimeRep calendar cal
 23 |
 24 | public export
 25 | {calendar : Type} -> {cal : Calendar calendar} ->
 26 |   Eq (CalendarDate calendar @{cal}) =>
 27 |   Eq (CalendarDateTimeRep calendar cal) where
 28 |   MkCalendarDateTime leftDate leftTime ==
 29 |     MkCalendarDateTime rightDate rightTime =
 30 |       leftDate == rightDate && leftTime == rightTime
 31 |
 32 | public export
 33 | {calendar : Type} -> {cal : Calendar calendar} ->
 34 |   Ord (CalendarDate calendar @{cal}) =>
 35 |   Ord (CalendarDateTimeRep calendar cal) where
 36 |   compare left right = case compare left.date right.date of
 37 |     EQ => compare left.time right.time
 38 |     ordering => ordering
 39 |
 40 | public export
 41 | {calendar : Type} -> {cal : Calendar calendar} ->
 42 |   Show (CalendarDate calendar @{cal}) =>
 43 |   Show (CalendarDateTimeRep calendar cal) where
 44 |   show value = "at (" ++ show value.date ++ ") (" ++ show value.time ++ ")"
 45 |
 46 | ||| Associate a local time with a date, using time-first argument order.
 47 | public export
 48 | on : {calendar : Type} -> {auto cal : Calendar calendar} ->
 49 |      LocalTime -> CalendarDate calendar @{cal} -> CalendarDateTime calendar @{cal}
 50 | on valueTime valueDate = MkCalendarDateTime valueDate valueTime
 51 |
 52 | ||| Associate a date with a local time, using date-first argument order.
 53 | public export
 54 | at : {calendar : Type} -> {auto cal : Calendar calendar} ->
 55 |   CalendarDate calendar @{cal} -> LocalTime -> CalendarDateTime calendar @{cal}
 56 | at valueDate valueTime = on valueTime valueDate
 57 |
 58 | ||| Associate a date with midnight at the start of that day.
 59 | public export
 60 | atStartOfDay : {calendar : Type} -> {auto cal : Calendar calendar} ->
 61 |       CalendarDate calendar @{cal} -> CalendarDateTime calendar @{cal}
 62 | atStartOfDay valueDate = at valueDate (localTime 0 0 0 0)
 63 |
 64 | ||| Extract the calendar date component.
 65 | public export
 66 | datePart : {calendar : Type} -> {auto cal : Calendar calendar} ->
 67 |            CalendarDateTime calendar @{cal} -> CalendarDate calendar @{cal}
 68 | datePart = date
 69 |
 70 | ||| Extract the local time-of-day component.
 71 | public export
 72 | localTimeOfDay : {calendar : Type} -> {auto cal : Calendar calendar} ->
 73 |                  CalendarDateTime calendar @{cal} -> LocalTime
 74 | localTimeOfDay = time
 75 |
 76 | ||| Extracting the date after construction returns the supplied date.
 77 | public export
 78 | atDatePart : {calendar : Type} -> {auto cal : Calendar calendar} ->
 79 |              (valueDate : CalendarDate calendar @{cal}) ->
 80 |              (valueTime : LocalTime) ->
 81 |              datePart @{cal} (at @{cal} valueDate valueTime) = valueDate
 82 | atDatePart _ _ = Refl
 83 |
 84 | ||| Extracting the local time after construction returns the supplied time.
 85 | public export
 86 | atLocalTimeOfDay : {calendar : Type} -> {auto cal : Calendar calendar} ->
 87 |                    (valueDate : CalendarDate calendar @{cal}) ->
 88 |                    (valueTime : LocalTime) ->
 89 |                    localTimeOfDay @{cal} (at @{cal} valueDate valueTime) = valueTime
 90 | atLocalTimeOfDay _ _ = Refl
 91 |
 92 | ||| Reconstructing a calendar date-time from its projections is exact.
 93 | public export
 94 | calendarDateTimeRoundTrip :
 95 |   {calendar : Type} -> {auto cal : Calendar calendar} ->
 96 |   (value : CalendarDateTime calendar @{cal}) ->
 97 |   at @{cal} (datePart @{cal} value) (localTimeOfDay @{cal} value) = value
 98 | calendarDateTimeRoundTrip (MkCalendarDateTime _ _) = Refl
 99 |
100 | ||| Convert the date component to another calendar through their shared bridge
101 | ||| day while preserving the local time of day.
102 | public export
103 | withCalendar : {source : Type} -> {target : Type} ->
104 |                {auto sourceCal : Calendar source} ->
105 |                {auto targetCal : Calendar target} ->
106 |                {auto sourceRep : HasCalendarBridge (CalendarDate source @{sourceCal})} ->
107 |                {auto targetRep : HasCalendarBridge (CalendarDate target @{targetCal})} ->
108 |                CalendarDateTime source @{sourceCal} ->
109 |                Either CalendarConversionError (CalendarDateTime target @{targetCal})
110 | withCalendar @{sourceCal} @{targetCal} @{sourceRep} @{targetRep} value =
111 |   map (\convertedDate => MkCalendarDateTime convertedDate value.time)
112 |     (IotaTime.Calendar.withCalendar @{sourceRep} @{targetRep} value.date)
113 |
114 | public export
115 | implementation {calendar : Type} -> {cal : Calendar calendar} ->
116 |   HasCalendar (CalendarDateTime calendar @{cal}) where
117 |   calendarCapability = ()
118 |
119 | public export
120 | implementation {calendar : Type} -> {cal : Calendar calendar} ->
121 |   HasTime (CalendarDateTime calendar @{cal}) where
122 |   timeCapability = ()
123 |
124 | public export
125 | implementation {calendar : Type} -> {cal : Calendar calendar} ->
126 |   PeriodTarget (CalendarDateTime calendar @{cal}) where
127 |   periodTarget = ()
128 |
129 | public export
130 | implementation {calendar : Type} -> {cal : Calendar calendar} ->
131 |   ApplyPeriod (CalendarDateTime calendar @{cal}) where
132 |   applyPeriod period value =
133 |     let dateAfterPeriod = applyCalendarPeriod @{cal} period value.date
134 |         (carry, timeAfterPeriod) = applyTimePeriodWithCarry period value.time
135 |      in MkCalendarDateTime (shiftCalendarDays @{cal} carry dateAfterPeriod) timeAfterPeriod
136 |
137 | ||| Compute the exact signed period from `start` to `end`, treating each civil
138 | ||| calendar day as 24 hours.
139 | public export
140 | between : {calendar : Type} -> {auto cal : Calendar calendar} ->
141 |           (start : CalendarDateTime calendar @{cal}) ->
142 |           (end : CalendarDateTime calendar @{cal}) ->
143 |           Period (CalendarDateTime calendar @{cal})
144 | between @{cal} start end = nanoseconds
145 |   ((toDaysFor @{cal} end.date - toDaysFor @{cal} start.date) * nanosecondsPerDay +
146 |    toNanosecondsSinceMidnight end.time - toNanosecondsSinceMidnight start.time)