
   0 | module IotaTime.Calendar
   1 | 
   2 | import public IotaTime.Calendar.Component
   3 | import IotaTime.Period
   4 | import Derive.Prelude
   5 | 
   6 | %language ElabReflection
   7 | 
   8 | %default total
   9 | 
  10 | ||| A weekday in the standard seven-day civil week shared by all iotaTime
  11 | ||| calendars.
  12 | public export
  13 | data DayOfWeek
  14 |   = Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday
  15 | 
  16 | ||| Zero-based weekday position from Sunday through Saturday.
  17 | public export
  18 | weekdayNumber : DayOfWeek -> Integer
  19 | weekdayNumber Sunday = 0
  20 | weekdayNumber Monday = 1
  21 | weekdayNumber Tuesday = 2
  22 | weekdayNumber Wednesday = 3
  23 | weekdayNumber Thursday = 4
  24 | weekdayNumber Friday = 5
  25 | weekdayNumber Saturday = 6
  26 | 
  27 | ||| Number of days in the standard civil week modeled by iotaTime calendars.
  28 | public export
  29 | daysPerWeek : Integer
  30 | daysPerWeek = 7
  31 | 
  32 | ||| Convert an integer weekday position to the corresponding weekday,
  33 | ||| wrapping values outside the standard zero-through-six range.
  34 | public export
  35 | weekdayFromNumber : Integer -> DayOfWeek
  36 | weekdayFromNumber value = case value `mod` 7 of
  37 |   0 => Sunday
  38 |   1 => Monday
  39 |   2 => Tuesday
  40 |   3 => Wednesday
  41 |   4 => Thursday
  42 |   5 => Friday
  43 |   _ => Saturday
  44 | 
  45 | ||| Signed day offset to the requested following weekday occurrence.
  46 | export
  47 | nextWeekdayOffset : Integer -> DayOfWeek -> DayOfWeek -> Integer
  48 | nextWeekdayOffset count current target =
  49 |   let currentNumber = weekdayNumber current
  50 |       targetNumber = weekdayNumber target
  51 |       weeks = if targetNumber > currentNumber then count - 1 else count
  52 |    in daysPerWeek * weeks + targetNumber - currentNumber
  53 | 
  54 | ||| Signed day offset to the requested preceding weekday occurrence.
  55 | export
  56 | previousWeekdayOffset : Integer -> DayOfWeek -> DayOfWeek -> Integer
  57 | previousWeekdayOffset count current target =
  58 |   let currentNumber = weekdayNumber current
  59 |       targetNumber = weekdayNumber target
  60 |       weeks = if targetNumber < currentNumber then count - 1 else count
  61 |    in -(daysPerWeek * weeks + currentNumber - targetNumber)
  62 | 
  63 | ||| Apply calendar period components from largest to smallest, preserving a
  64 | ||| separate shift for weeks before the final day shift.
  65 | export
  66 | applyDatePeriodWith :
  67 |   (shiftYears : Integer -> date -> date) ->
  68 |   (shiftMonths : Integer -> date -> date) ->
  69 |   (shiftDays : Integer -> date -> date) ->
  70 |   Period target -> date -> date
  71 | applyDatePeriodWith shiftYears shiftMonths shiftDays period =
  72 |     shiftDays (periodDays period)
  73 |   . shiftDays (daysPerWeek * periodWeeks period)
  74 |   . shiftMonths (periodMonths period)
  75 |   . shiftYears (periodYears period)
  76 | 
  77 | public export
  78 | Eq DayOfWeek where
  79 |   left == right = weekdayNumber left == weekdayNumber right
  80 | 
  81 | public export
  82 | Ord DayOfWeek where
  83 |   compare left right = compare (weekdayNumber left) (weekdayNumber right)
  84 | 
  85 | %runElab derive `{DayOfWeek} [Show]
  86 | 
  87 | ||| Selects an occurrence of a weekday within a month.
  88 | public export
  89 | data DayNth
  90 |   = FourthToLast
  91 |   | ThirdToLast
  92 |   | SecondToLast
  93 |   | Last
  94 |   | First
  95 |   | Second
  96 |   | Third
  97 |   | Fourth
  98 |   | Fifth
  99 | 
 100 | %runElab derive `{DayNth} [Eq, Show]
 101 | 
 102 | ||| Compute the raw day-of-month candidate for a weekday occurrence.
 103 | ||| Calendar implementations remain responsible for validating the candidate
 104 | ||| against their supported year and month ranges before constructing a date.
 105 | export
 106 | nthWeekdayDayNumber : DayNth -> (monthLength : Integer) ->
 107 |                       (firstOffset : Integer) -> (lastOffset : Integer) ->
 108 |                       Integer
 109 | nthWeekdayDayNumber FourthToLast monthLength _ lastOffset =
 110 |   monthLength - lastOffset - 3 * daysPerWeek
 111 | nthWeekdayDayNumber ThirdToLast monthLength _ lastOffset =
 112 |   monthLength - lastOffset - 2 * daysPerWeek
 113 | nthWeekdayDayNumber SecondToLast monthLength _ lastOffset =
 114 |   monthLength - lastOffset - daysPerWeek
 115 | nthWeekdayDayNumber Last monthLength _ lastOffset =
 116 |   monthLength - lastOffset
 117 | nthWeekdayDayNumber First _ firstOffset _ = 1 + firstOffset
 118 | nthWeekdayDayNumber Second _ firstOffset _ =
 119 |   1 + daysPerWeek + firstOffset
 120 | nthWeekdayDayNumber Third _ firstOffset _ =
 121 |   1 + 2 * daysPerWeek + firstOffset
 122 | nthWeekdayDayNumber Fourth _ firstOffset _ =
 123 |   1 + 3 * daysPerWeek + firstOffset
 124 | nthWeekdayDayNumber Fifth _ firstOffset _ =
 125 |   1 + 4 * daysPerWeek + firstOffset
 126 | 
 127 | ||| A calendar conversion failed because the target calendar cannot represent
 128 | ||| the source date's bridge day.
 129 | public export
 130 | data CalendarConversionError = TargetCalendarOutOfRange String Integer
 131 | 
 132 | ||| Calendar units used when decomposing the difference between two dates.
 133 | public export
 134 | data DateDifferenceUnits = DaysOnly | YearsMonthsDays
 135 | 
 136 | ||| Month arithmetic used while decomposing a calendar difference.
 137 | public export
 138 | data MonthArithmeticPolicy = ClampToMonth
 139 | 
 140 | ||| Controls how a difference between calendar dates is decomposed.
 141 | public export
 142 | record DateDifferencePolicy where
 143 |   constructor MkDateDifferencePolicy
 144 |   units : DateDifferenceUnits
 145 |   monthArithmetic : MonthArithmeticPolicy
 146 | 
 147 | ||| The standard largest-first, non-overshooting calendar decomposition.
 148 | public export
 149 | nodaTimePolicy : DateDifferencePolicy
 150 | nodaTimePolicy = MkDateDifferencePolicy YearsMonthsDays ClampToMonth
 151 | 
 152 | ||| Capabilities and dependent representations required of a calendar.
 153 | ||| `MonthRep` may depend on the year, allowing calendars such as Hebrew to
 154 | ||| make leap-only months unrepresentable in common years.
 155 | public export
 156 | interface Calendar calendar where
 157 |   DateRep : Type
 158 |   MonthRep : Year -> Type
 159 | 
 160 |   isValidDays : Integer -> Bool
 161 |   fromDays : (days : Integer) -> {auto 0 valid : So (isValidDays days)} -> DateRep
 162 |   toDaysFor : DateRep -> Integer
 163 |   0 toDaysValid : (date : DateRep) -> So (isValidDays (toDaysFor date))
 164 |   0 toFromDays : (days : Integer) -> (0 valid : So (isValidDays days)) ->
 165 |                  toDaysFor (fromDays days {valid}) = days
 166 |   0 fromToDays : (date : DateRep) ->
 167 |                  fromDays (toDaysFor date) {valid = toDaysValid date} = date
 168 |   calendarName : String
 169 | 
 170 |   year' : DateRep -> Year
 171 |   toYmd : (date : DateRep) -> (MonthRep (year' date), DayOfMonth)
 172 |   day' : DateRep -> DayOfMonth
 173 |   month' : (date : DateRep) -> MonthRep (year' date)
 174 | 
 175 |   applyCalendarPeriod' : Period target -> DateRep -> DateRep
 176 |   shiftCalendarDays' : Integer -> DateRep -> DateRep
 177 | 
 178 |   dayOfWeekFor : DateRep -> DayOfWeek
 179 |   nextFor : Integer -> DayOfWeek -> DateRep -> DateRep
 180 |   previousFor : Integer -> DayOfWeek -> DateRep -> DateRep
 181 | 
 182 | ||| The opaque date representation selected by a calendar implementation.
 183 | public export
 184 | CalendarDate : (calendar : Type) -> {auto cal : Calendar calendar} -> Type
 185 | CalendarDate calendar @{cal} = DateRep @{cal}
 186 | 
 187 | ||| Internal normalization implemented by iotaTime's built-in calendars for
 188 | ||| cross-calendar and instant conversion. Calendar-local APIs use
 189 | ||| `Calendar.toDaysFor` instead.
 190 | export
 191 | interface HasCalendarBridge date where
 192 |   toBridgeDays : date -> Integer
 193 |   acceptsBridgeDays : Integer -> Bool
 194 |   fromBridgeDays : (days : Integer) ->
 195 |                          {auto 0 valid : So (acceptsBridgeDays days)} -> date
 196 |   bridgeCalendarName : String
 197 | 
 198 | ||| Calendar operations determined by a concrete date representation.
 199 | ||| This lets value-oriented APIs infer the calendar from their first date
 200 | ||| argument instead of requiring a repeated `{calendar = ...}` annotation.
 201 | public export
 202 | interface HasCalendarBridge date => CalendarValue date where
 203 |   CalendarMonth : Year -> Type
 204 |   calendarValueToDays : date -> Integer
 205 |   calendarValueYear : date -> Year
 206 |   calendarValueMonthDay : (value : date) ->
 207 |     (CalendarMonth (calendarValueYear value), DayOfMonth)
 208 |   calendarValueDayOfWeek : date -> DayOfWeek
 209 |   calendarValueBetweenWith :
 210 |     DateDifferencePolicy -> date -> date -> Period date
 211 | 
 212 | ||| Weekday navigation selected by the concrete date representation.
 213 | public export
 214 | interface CalendarValue date => CalendarNavigation date where
 215 |   calendarValueNext : Integer -> DayOfWeek -> date -> date
 216 |   calendarValuePrevious : Integer -> DayOfWeek -> date -> date
 217 | 
 218 | ||| Extract the calendar year from a date.
 219 | public export
 220 | yearFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 221 |   CalendarDate calendar @{cal} -> Year
 222 | yearFor @{cal} = year' @{cal}
 223 | 
 224 | ||| Extract the year-indexed calendar month from a date.
 225 | public export
 226 | monthFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 227 |   (date : CalendarDate calendar @{cal}) ->
 228 |   MonthRep @{cal} (yearFor {calendar} @{cal} date)
 229 | monthFor @{cal} = month' @{cal}
 230 | 
 231 | ||| Extract the day of month from a date.
 232 | public export
 233 | dayFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 234 |   CalendarDate calendar @{cal} -> DayOfMonth
 235 | dayFor @{cal} = day' @{cal}
 236 | 
 237 | export
 238 | applyCalendarPeriod : {calendar : Type} -> {auto cal : Calendar calendar} ->
 239 |                       Period target -> CalendarDate calendar @{cal} ->
 240 |                       CalendarDate calendar @{cal}
 241 | applyCalendarPeriod @{cal} = applyCalendarPeriod' @{cal}
 242 | 
 243 | export
 244 | shiftCalendarDays : {calendar : Type} -> {auto cal : Calendar calendar} ->
 245 |                     Integer -> CalendarDate calendar @{cal} -> CalendarDate calendar @{cal}
 246 | shiftCalendarDays @{cal} = shiftCalendarDays' @{cal}
 247 | 
 248 | ||| Compute the exact signed day period from `start` to `end`.
 249 | public export
 250 | betweenDaysFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 251 |               {auto target : HasCalendar (CalendarDate calendar @{cal})} ->
 252 |               (start : CalendarDate calendar @{cal}) ->
 253 |               (end : CalendarDate calendar @{cal}) ->
 254 |               Period (CalendarDate calendar @{cal})
 255 | betweenDaysFor @{cal} start end = days (toDaysFor @{cal} end - toDaysFor @{cal} start)
 256 | 
 257 | yearsBetween : {calendar : Type} -> {auto cal : Calendar calendar} ->
 258 |                {auto target : HasCalendar (CalendarDate calendar @{cal})} ->
 259 |                CalendarDate calendar @{cal} -> CalendarDate calendar @{cal} -> Integer
 260 | yearsBetween @{cal} start end =
 261 |   let estimate = yearValue (yearFor @{cal} end) - yearValue (yearFor @{cal} start)
 262 |       estimatedDate = applyCalendarPeriod @{cal}
 263 |         (years {target = CalendarDate calendar @{cal}} estimate) start
 264 |       estimatedDays = toDaysFor @{cal} estimatedDate
 265 |       startDays = toDaysFor @{cal} start
 266 |       endDays = toDaysFor @{cal} end
 267 |    in if startDays <= endDays
 268 |         then if estimatedDays <= endDays then estimate else estimate - 1
 269 |         else if estimatedDays >= endDays then estimate else estimate + 1
 270 | 
 271 | monthsBetween : {calendar : Type} -> {auto cal : Calendar calendar} ->
 272 |                 {auto target : HasCalendar (CalendarDate calendar @{cal})} ->
 273 |                 CalendarDate calendar @{cal} -> CalendarDate calendar @{cal} -> Integer
 274 | monthsBetween @{cal} start end =
 275 |   let startDays = toDaysFor @{cal} start
 276 |       endDays = toDaysFor @{cal} end
 277 |       fuel = cast (abs (endDays - startDays) + 1)
 278 |    in if startDays <= endDays
 279 |         then forward fuel 0
 280 |         else backward fuel 0
 281 |   where
 282 |     forward : Nat -> Integer -> Integer
 283 |     forward Z count = count
 284 |     forward (S fuel) count =
 285 |       let candidate = count + 1
 286 |           candidateDays = toDaysFor @{cal}
 287 |             (applyCalendarPeriod @{cal}
 288 |               (months {target = CalendarDate calendar @{cal}} candidate) start)
 289 |        in if candidateDays <= toDaysFor @{cal} end
 290 |             then if candidateDays == toDaysFor @{cal} end
 291 |               then candidate
 292 |               else forward fuel candidate
 293 |             else count
 294 | 
 295 |     backward : Nat -> Integer -> Integer
 296 |     backward Z count = count
 297 |     backward (S fuel) count =
 298 |       let candidate = count - 1
 299 |           candidateDays = toDaysFor @{cal}
 300 |             (applyCalendarPeriod @{cal}
 301 |               (months {target = CalendarDate calendar @{cal}} candidate) start)
 302 |        in if candidateDays >= toDaysFor @{cal} end
 303 |             then if candidateDays == toDaysFor @{cal} end
 304 |               then candidate
 305 |               else backward fuel candidate
 306 |             else count
 307 | 
 308 | ||| Decompose the signed difference from `start` to `end` according to `policy`.
 309 | ||| Calendar units are selected largest-first without passing the endpoint.
 310 | public export
 311 | betweenWithFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 312 |               {auto target : HasCalendar (CalendarDate calendar @{cal})} ->
 313 |               DateDifferencePolicy ->
 314 |               (start : CalendarDate calendar @{cal}) ->
 315 |               (end : CalendarDate calendar @{cal}) ->
 316 |               Period (CalendarDate calendar @{cal})
 317 | betweenWithFor @{cal} (MkDateDifferencePolicy DaysOnly _) start end =
 318 |   betweenDaysFor @{cal} start end
 319 | betweenWithFor @{cal} (MkDateDifferencePolicy YearsMonthsDays ClampToMonth) start end =
 320 |   let yearCount = yearsBetween @{cal} start end
 321 |       afterYears = applyCalendarPeriod @{cal}
 322 |         (years {target = CalendarDate calendar @{cal}} yearCount) start
 323 |       monthCount = monthsBetween @{cal} afterYears end
 324 |       afterMonths = applyCalendarPeriod @{cal}
 325 |         (months {target = CalendarDate calendar @{cal}} monthCount) afterYears
 326 |       dayCount = toDaysFor @{cal} end - toDaysFor @{cal} afterMonths
 327 |    in years {target = CalendarDate calendar @{cal}} yearCount <+>
 328 |       months {target = CalendarDate calendar @{cal}} monthCount <+>
 329 |       days {target = CalendarDate calendar @{cal}} dayCount
 330 | 
 331 | ||| Decompose the signed calendar difference using `nodaTimePolicy`.
 332 | public export
 333 | betweenFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 334 |           {auto target : HasCalendar (CalendarDate calendar @{cal})} ->
 335 |           (start : CalendarDate calendar @{cal}) ->
 336 |           (end : CalendarDate calendar @{cal}) ->
 337 |           Period (CalendarDate calendar @{cal})
 338 | betweenFor @{cal} = betweenWithFor @{cal} nodaTimePolicy
 339 | 
 340 | ||| Decompose a date while preserving the dependency between its year and month.
 341 | public export
 342 | yearMonthDayFor : {calendar : Type} -> {auto cal : Calendar calendar} ->
 343 |                (date : CalendarDate calendar @{cal}) ->
 344 |                (valueYear : Year ** (MonthRep @{cal} valueYear, DayOfMonth))
 345 | yearMonthDayFor @{cal} date =
 346 |   (year' @{cal} date ** toYmd @{cal} date)
 347 | 
 348 | ||| Compute the exact signed day period from `start` to `end`.
 349 | public export
 350 | betweenDays : (start : date) -> {auto value : CalendarValue date} ->
 351 |               date -> Period date
 352 | betweenDays start @{value} =
 353 |   calendarValueBetweenWith @{value}
 354 |     (MkDateDifferencePolicy DaysOnly ClampToMonth) start
 355 | 
 356 | ||| Decompose a difference according to `policy`, inferring the calendar from
 357 | ||| the first date argument.
 358 | public export
 359 | betweenWith : DateDifferencePolicy ->
 360 |               (start : date) -> {auto value : CalendarValue date} ->
 361 |               date -> Period date
 362 | betweenWith policy start @{value} =
 363 |   calendarValueBetweenWith @{value} policy start
 364 | 
 365 | ||| Decompose a signed date difference using `nodaTimePolicy`.
 366 | public export
 367 | between : (start : date) -> {auto value : CalendarValue date} ->
 368 |           date -> Period date
 369 | between = betweenWith nodaTimePolicy
 370 | 
 371 | ||| Decompose a date while preserving its year-indexed month type.
 372 | public export
 373 | yearMonthDay : (value : date) -> {auto rep : CalendarValue date} ->
 374 |                (valueYear : Year **
 375 |                  (CalendarMonth @{rep} valueYear, DayOfMonth))
 376 | yearMonthDay value @{rep} =
 377 |   (calendarValueYear @{rep} value ** calendarValueMonthDay @{rep} value)
 378 | 
 379 | ||| Return the calendar-relative day count for a concrete date value.
 380 | public export
 381 | toDays : (value : date) -> {auto rep : CalendarValue date} -> Integer
 382 | toDays value @{rep} = calendarValueToDays @{rep} value
 383 | 
 384 | ||| Extract the calendar year from a concrete date value.
 385 | public export
 386 | year : (value : date) -> {auto rep : CalendarValue date} -> Year
 387 | year value @{rep} = calendarValueYear @{rep} value
 388 | 
 389 | ||| Extract the year-indexed calendar month from a concrete date value.
 390 | public export
 391 | month : (value : date) -> {auto rep : CalendarValue date} ->
 392 |   CalendarMonth @{rep} (year value @{rep})
 393 | month value @{rep} = fst (calendarValueMonthDay @{rep} value)
 394 | 
 395 | ||| Extract the day of month from a concrete date value.
 396 | public export
 397 | day : (value : date) -> {auto rep : CalendarValue date} -> DayOfMonth
 398 | day value @{rep} = snd (calendarValueMonthDay @{rep} value)
 399 | 
 400 | ||| Combined and projected civil-date observations are definitionally coherent.
 401 | public export
 402 | calendarComponentsCoherent :
 403 |   (value : date) -> {auto rep : CalendarValue date} ->
 404 |   yearMonthDay value @{rep} =
 405 |     (year value @{rep} ** (month value @{rep}, day value @{rep}))
 406 | calendarComponentsCoherent value @{rep} with
 407 |   (calendarValueMonthDay @{rep} value)
 408 |   _ | (_, _) = Refl
 409 | 
 410 | ||| Extract the weekday from a concrete date value.
 411 | public export
 412 | dayOfWeek : (value : date) -> {auto rep : CalendarValue date} -> DayOfWeek
 413 | dayOfWeek value @{rep} = calendarValueDayOfWeek @{rep} value
 414 | 
 415 | ||| Find a matching weekday relative to a concrete date value.
 416 | public export
 417 | next : {auto navigation : CalendarNavigation date} ->
 418 |   Integer -> DayOfWeek -> (value : date) -> date
 419 | next count weekday value @{navigation} =
 420 |   calendarValueNext @{navigation} count weekday value
 421 | 
 422 | ||| Find a preceding matching weekday relative to a concrete date value.
 423 | public export
 424 | previous : {auto navigation : CalendarNavigation date} ->
 425 |            Integer -> DayOfWeek -> (value : date) -> date
 426 | previous count weekday value @{navigation} =
 427 |   calendarValuePrevious @{navigation} count weekday value
 428 | 
 429 | ||| Convert a date to another calendar through their shared bridge day.
 430 | ||| Returns `TargetCalendarOutOfRange` when the target cannot represent it.
 431 | public export
 432 | withCalendar : {sourceDate : Type} -> {targetDate : Type} ->
 433 |                {auto sourceRep : HasCalendarBridge sourceDate} ->
 434 |                {auto targetRep : HasCalendarBridge targetDate} ->
 435 |                sourceDate ->
 436 |                Either CalendarConversionError targetDate
 437 | withCalendar @{sourceRep} @{targetRep} date =
 438 |   let valueDays = toBridgeDays @{sourceRep} date
 439 |    in case choose (acceptsBridgeDays @{targetRep} valueDays) of
 440 |         Left valid => Right (fromBridgeDays @{targetRep} valueDays @{valid})
 441 |         Right _ => Left
 442 |           (TargetCalendarOutOfRange (bridgeCalendarName @{targetRep}) valueDays)