
   0 | module IotaTime.Calendar.Gregorian
   1 | 
   2 | import IotaTime.Calendar
   3 | import IotaTime.Internal.ApplyPeriod
   4 | import IotaTime.Internal.Gregorian
   5 | import IotaTime.Period
   6 | import Data.So
   7 | import Derive.Prelude
   8 | 
   9 | %language ElabReflection
  10 | 
  11 | %default total
  12 | 
  13 | ||| The Gregorian calendar, supported from October 15, 1582 onward.
  14 | public export
  15 | data Gregorian = GregorianCalendar
  16 | 
  17 | public export
  18 | data Month
  19 |   = January
  20 |   | February
  21 |   | March
  22 |   | April
  23 |   | May
  24 |   | June
  25 |   | July
  26 |   | August
  27 |   | September
  28 |   | October
  29 |   | November
  30 |   | December
  31 | 
  32 | public export
  33 | monthNumber : Month -> Integer
  34 | monthNumber January = 1
  35 | monthNumber February = 2
  36 | monthNumber March = 3
  37 | monthNumber April = 4
  38 | monthNumber May = 5
  39 | monthNumber June = 6
  40 | monthNumber July = 7
  41 | monthNumber August = 8
  42 | monthNumber September = 9
  43 | monthNumber October = 10
  44 | monthNumber November = 11
  45 | monthNumber December = 12
  46 | 
  47 | public export
  48 | Eq Month where
  49 |   left == right = monthNumber left == monthNumber right
  50 | 
  51 | public export
  52 | Ord Month where
  53 |   compare left right = compare (monthNumber left) (monthNumber right)
  54 | 
  55 | %runElab derive `{Month} [Show]
  56 | 
  57 | export
  58 | record GregorianDate where
  59 |   constructor MkGregorianDate
  60 |   daysSinceEpoch : Integer
  61 |   0 validDays : So (daysSinceEpoch >= -152444)
  62 | 
  63 | public export
  64 | Eq GregorianDate where
  65 |   left == right = left.daysSinceEpoch == right.daysSinceEpoch
  66 | 
  67 | public export
  68 | Ord GregorianDate where
  69 |   compare left right = compare left.daysSinceEpoch right.daysSinceEpoch
  70 | 
  71 | monthFromNumber : Integer -> Month
  72 | monthFromNumber 1 = January
  73 | monthFromNumber 2 = February
  74 | monthFromNumber 3 = March
  75 | monthFromNumber 4 = April
  76 | monthFromNumber 5 = May
  77 | monthFromNumber 6 = June
  78 | monthFromNumber 7 = July
  79 | monthFromNumber 8 = August
  80 | monthFromNumber 9 = September
  81 | monthFromNumber 10 = October
  82 | monthFromNumber 11 = November
  83 | monthFromNumber _ = December
  84 | 
  85 | ||| Whether a Gregorian year contains February 29.
  86 | public export
  87 | isLeapYear : Year -> Bool
  88 | isLeapYear value =
  89 |   let number = yearValue value
  90 |    in number `mod` 400 == 0 || (number `mod` 4 == 0 && number `mod` 100 /= 0)
  91 | 
  92 | public export
  93 | maxDaysInMonth : Month -> Year -> DayOfMonth
  94 | maxDaysInMonth February value = if isLeapYear value then 29 else 28
  95 | maxDaysInMonth April _ = 30
  96 | maxDaysInMonth June _ = 30
  97 | maxDaysInMonth September _ = 30
  98 | maxDaysInMonth November _ = 30
  99 | maxDaysInMonth _ _ = 31
 100 | 
 101 | public export
 102 | isValidDate : DayOfMonth -> Month -> Year -> Bool
 103 | isValidDate valueDay valueMonth valueYear =
 104 |   let dayNumber = dayOfMonthValue valueDay
 105 |       yearNumber = yearValue valueYear
 106 |    in dayNumber >= 1 &&
 107 |     dayNumber <= dayOfMonthValue (maxDaysInMonth valueMonth valueYear) &&
 108 |     (yearNumber > 1582 ||
 109 |       (yearNumber == 1582 &&
 110 |       (monthNumber valueMonth > monthNumber October ||
 111 |         (valueMonth == October && dayNumber >= 15))))
 112 | 
 113 | daysFromCivil : Year -> Month -> DayOfMonth -> Integer
 114 | daysFromCivil valueYear valueMonth valueDay =
 115 |   gregorianDaysFromCivil
 116 |     (yearValue valueYear)
 117 |     (monthNumber valueMonth)
 118 |     (dayOfMonthValue valueDay)
 119 | 
 120 | civilFromDays : Integer -> (Year, Month, DayOfMonth)
 121 | civilFromDays value =
 122 |   let (valueYear, valueMonth, valueDay) = gregorianCivilFromDays value
 123 |    in (yearFromInteger valueYear,
 124 |        monthFromNumber valueMonth,
 125 |        dayOfMonthFromInteger valueDay)
 126 | 
 127 | ||| The Gregorian calendar epoch day relative to March 1, 2000.
 128 | public export
 129 | epochDay : Integer
 130 | epochDay = -152444
 131 | 
 132 | checkedGregorianDate : (days : Integer) ->
 133 |                        (0 valid : So
 134 |                          (days >= IotaTime.Calendar.Gregorian.epochDay)) ->
 135 |                        GregorianDate
 136 | checkedGregorianDate days valid = MkGregorianDate days valid
 137 | 
 138 | makeGregorianDate : Integer -> GregorianDate
 139 | makeGregorianDate days =
 140 |   let clamped = max epochDay days
 141 |    in case choose (clamped >= epochDay) of
 142 |         Left valid => checkedGregorianDate clamped valid
 143 |         Right _ => checkedGregorianDate epochDay Oh
 144 | 
 145 | export
 146 | HasCalendarBridge GregorianDate where
 147 |   toBridgeDays = daysSinceEpoch
 148 |   acceptsBridgeDays = (>= epochDay)
 149 |   fromBridgeDays days @{valid} = checkedGregorianDate days valid
 150 |   bridgeCalendarName = "Gregorian"
 151 | 
 152 | makeDate : Year -> Month -> DayOfMonth -> GregorianDate
 153 | makeDate valueYear valueMonth valueDay =
 154 |   makeGregorianDate (daysFromCivil valueYear valueMonth valueDay)
 155 | 
 156 | normalizeGregorianDay : Integer -> GregorianDate -> GregorianDate
 157 | normalizeGregorianDay targetDay date =
 158 |   let (valueYear, valueMonth, valueDay) = civilFromDays date.daysSinceEpoch
 159 |       firstOfMonth = daysFromCivil valueYear valueMonth 1
 160 |   in makeGregorianDate (firstOfMonth + targetDay - 1)
 161 | 
 162 | shiftGregorianDays : Integer -> GregorianDate -> GregorianDate
 163 | shiftGregorianDays amount date =
 164 |   makeGregorianDate (date.daysSinceEpoch + amount)
 165 | 
 166 | normalizeGregorianMonth : Integer -> GregorianDate -> GregorianDate
 167 | normalizeGregorianMonth targetMonth date =
 168 |   let (valueYear, valueMonth, valueDay) = civilFromDays date.daysSinceEpoch
 169 |       targetYear = yearFromInteger (yearValue valueYear + targetMonth `div` 12)
 170 |       normalizedMonth = monthFromNumber (targetMonth `mod` 12 + 1)
 171 |       targetDay = min valueDay (maxDaysInMonth normalizedMonth targetYear)
 172 |    in makeDate targetYear normalizedMonth targetDay
 173 | 
 174 | shiftGregorianMonths : Integer -> GregorianDate -> GregorianDate
 175 | shiftGregorianMonths amount date =
 176 |   let (_, valueMonth, _) = civilFromDays date.daysSinceEpoch
 177 |    in normalizeGregorianMonth (monthNumber valueMonth - 1 + amount) date
 178 | 
 179 | modifyGregorianYear : (Year -> Year) -> GregorianDate -> GregorianDate
 180 | modifyGregorianYear transform date =
 181 |   let (valueYear, valueMonth, valueDay) = civilFromDays date.daysSinceEpoch
 182 |       targetYear = transform valueYear
 183 |       targetDay = min valueDay (maxDaysInMonth valueMonth targetYear)
 184 |    in makeDate targetYear valueMonth targetDay
 185 | 
 186 | applyGregorianPeriod : Period target -> GregorianDate -> GregorianDate
 187 | applyGregorianPeriod = applyDatePeriodWith
 188 |   (\amount => modifyGregorianYear
 189 |     (\valueYear => yearFromInteger (yearValue valueYear + amount)))
 190 |   shiftGregorianMonths
 191 |   shiftGregorianDays
 192 | 
 193 | public export
 194 | HasCalendar GregorianDate where
 195 |   calendarCapability = ()
 196 | 
 197 | public export
 198 | PeriodTarget GregorianDate where
 199 |   periodTarget = ()
 200 | 
 201 | public export
 202 | ApplyPeriod GregorianDate where
 203 |   applyPeriod = applyGregorianPeriod
 204 | 
 205 | gregorianDayOfWeek : GregorianDate -> DayOfWeek
 206 | gregorianDayOfWeek date = weekdayFromNumber (date.daysSinceEpoch + 3)
 207 | 
 208 | nextGregorian : Integer -> DayOfWeek -> GregorianDate -> GregorianDate
 209 | nextGregorian count target date =
 210 |   makeGregorianDate (date.daysSinceEpoch +
 211 |     nextWeekdayOffset count (gregorianDayOfWeek date) target)
 212 | 
 213 | previousGregorian : Integer -> DayOfWeek -> GregorianDate -> GregorianDate
 214 | previousGregorian count target date =
 215 |   makeGregorianDate (date.daysSinceEpoch +
 216 |     previousWeekdayOffset count (gregorianDayOfWeek date) target)
 217 | 
 218 | public export
 219 | Calendar Gregorian where
 220 |   DateRep = GregorianDate
 221 |   MonthRep _ = Month
 222 | 
 223 |   isValidDays = (>= epochDay)
 224 |   fromDays days @{valid} = checkedGregorianDate days valid
 225 |   toDaysFor date = date.daysSinceEpoch
 226 |   toDaysValid (MkGregorianDate _ valid) = valid
 227 |   toFromDays _ _ = Refl
 228 |   fromToDays (MkGregorianDate _ _) = Refl
 229 |   calendarName = "Gregorian"
 230 | 
 231 |   year' date = let (value, _, _) = civilFromDays date.daysSinceEpoch in value
 232 |   toYmd date = let (_, valueMonth, valueDay) = civilFromDays date.daysSinceEpoch
 233 |                 in (valueMonth, valueDay)
 234 |   day' date = let (_, _, value) = civilFromDays date.daysSinceEpoch in value
 235 |   month' date = let (_, value, _) = civilFromDays date.daysSinceEpoch in value
 236 | 
 237 |   applyCalendarPeriod' = applyGregorianPeriod
 238 |   shiftCalendarDays' = shiftGregorianDays
 239 | 
 240 |   dayOfWeekFor = gregorianDayOfWeek
 241 |   nextFor = nextGregorian
 242 |   previousFor = previousGregorian
 243 | 
 244 | public export
 245 | CalendarValue GregorianDate where
 246 |   CalendarMonth _ = Month
 247 |   calendarValueToDays = toDaysFor {calendar = Gregorian}
 248 |   calendarValueYear = yearFor {calendar = Gregorian}
 249 |   calendarValueMonthDay = toYmd {calendar = Gregorian}
 250 |   calendarValueDayOfWeek = dayOfWeekFor {calendar = Gregorian}
 251 |   calendarValueBetweenWith = betweenWithFor {calendar = Gregorian}
 252 | 
 253 | public export
 254 | CalendarNavigation GregorianDate where
 255 |   calendarValueNext = nextFor {calendar = Gregorian}
 256 |   calendarValuePrevious = previousFor {calendar = Gregorian}
 257 | 
 258 | public export
 259 | Show GregorianDate where
 260 |   show date = case civilFromDays date.daysSinceEpoch of
 261 |     (valueYear, valueMonth, valueDay) =>
 262 |       "calendarDate " ++ show valueDay ++ " " ++
 263 |       show valueMonth ++ " " ++ show valueYear
 264 | 
 265 | ||| Construct a Gregorian date whose validity is known statically.
 266 | ||| Use `refineDate` for values learned at runtime.
 267 | public export
 268 | calendarDate : (valueDay : DayOfMonth) -> (valueMonth : Month) -> (valueYear : Year) ->
 269 |                {auto 0 valid : So (isValidDate valueDay valueMonth valueYear)} ->
 270 |                CalendarDate Gregorian
 271 | calendarDate valueDay valueMonth valueYear =
 272 |   makeGregorianDate (daysFromCivil valueYear valueMonth valueDay)
 273 | 
 274 | ||| Failures produced while refining untrusted Gregorian date data.
 275 | public export
 276 | data GregorianDateError
 277 |   = InvalidGregorianDate DayOfMonth Month Year
 278 |   | InvalidGregorianDayCount Integer
 279 |   | InvalidGregorianNthDay DayNth DayOfWeek Month Year
 280 |   | InvalidGregorianWeekDate WeekNumber DayOfWeek Year
 281 | 
 282 | ||| Validate runtime day, month, and year components as a Gregorian date.
 283 | public export
 284 | refineDate : DayOfMonth -> Month -> Year ->
 285 |                       Either GregorianDateError (CalendarDate Gregorian)
 286 | refineDate valueDay valueMonth valueYear =
 287 |   case choose (isValidDate valueDay valueMonth valueYear) of
 288 |     Left valid => Right (calendarDate valueDay valueMonth valueYear @{valid})
 289 |     Right _ => Left (InvalidGregorianDate valueDay valueMonth valueYear)
 290 | 
 291 | ||| Construct a Gregorian date from a statically valid day count relative to
 292 | ||| March 1, 2000.
 293 | public export
 294 | fromDays : (days : Integer) ->
 295 |                     {auto 0 valid : So
 296 |                       (IotaTime.Calendar.isValidDays {calendar = Gregorian} days)} ->
 297 |                     CalendarDate Gregorian
 298 | fromDays days @{valid} = checkedGregorianDate days valid
 299 | 
 300 | ||| Validate a runtime day count relative to March 1, 2000.
 301 | public export
 302 | refineDays : (days : Integer) -> Either GregorianDateError (CalendarDate Gregorian)
 303 | refineDays days =
 304 |   case choose (IotaTime.Calendar.isValidDays {calendar = Gregorian} days) of
 305 |     Left valid => Right (fromDays days @{valid})
 306 |     Right _ => Left (InvalidGregorianDayCount days)
 307 | 
 308 | nthDayOfMonth : DayNth -> DayOfWeek -> Month -> Year -> DayOfMonth
 309 | nthDayOfMonth nth target valueMonth valueYear =
 310 |   let monthLength = maxDaysInMonth valueMonth valueYear
 311 |       firstDate = makeGregorianDate (daysFromCivil valueYear valueMonth 1)
 312 |       firstOffset = (weekdayNumber target -
 313 |         weekdayNumber (gregorianDayOfWeek firstDate)) `mod` daysPerWeek
 314 |       lastDate = makeGregorianDate (daysFromCivil valueYear valueMonth monthLength)
 315 |       lastOffset = (weekdayNumber (gregorianDayOfWeek lastDate) -
 316 |         weekdayNumber target) `mod` daysPerWeek
 317 |       dayNumber = nthWeekdayDayNumber nth (dayOfMonthValue monthLength)
 318 |         firstOffset lastOffset
 319 |    in dayOfMonthFromInteger dayNumber
 320 | 
 321 | public export
 322 | isValidNthDay : DayNth -> DayOfWeek -> Month -> Year -> Bool
 323 | isValidNthDay nth target valueMonth valueYear =
 324 |   if yearValue valueYear > 1582
 325 |     then case nth of
 326 |       Fifth => nthDayOfMonth nth target valueMonth valueYear <= maxDaysInMonth valueMonth valueYear
 327 |       _ => True
 328 |     else isValidDate
 329 |       (nthDayOfMonth nth target valueMonth valueYear) valueMonth valueYear
 330 | 
 331 | ||| Construct the nth requested weekday in a Gregorian month under static
 332 | ||| validity evidence.
 333 | public export
 334 | fromNthDay : (nth : DayNth) -> (target : DayOfWeek) ->
 335 |              (valueMonth : Month) -> (valueYear : Year) ->
 336 |              {auto 0 valid : So (isValidNthDay nth target valueMonth valueYear)} ->
 337 |              CalendarDate Gregorian
 338 | fromNthDay nth target valueMonth valueYear =
 339 |   makeGregorianDate
 340 |     (daysFromCivil valueYear valueMonth (nthDayOfMonth nth target valueMonth valueYear))
 341 | 
 342 | ||| Validate an nth-weekday request for a Gregorian month.
 343 | public export
 344 | refineNthDay : DayNth -> DayOfWeek -> Month -> Year ->
 345 |                         Either GregorianDateError (CalendarDate Gregorian)
 346 | refineNthDay nth target valueMonth valueYear =
 347 |   case choose (isValidNthDay nth target valueMonth valueYear) of
 348 |     Left valid => Right (fromNthDay nth target valueMonth valueYear @{valid})
 349 |     Right _ => Left (InvalidGregorianNthDay nth target valueMonth valueYear)
 350 | 
 351 | weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer
 352 | weekDateDays week target valueYear =
 353 |   let firstDay = daysFromCivil valueYear January 1
 354 |       firstWeekStart = firstDay - weekdayNumber
 355 |         (gregorianDayOfWeek (makeGregorianDate firstDay))
 356 |   in firstWeekStart + 7 * (weekNumberValue week - 1) + weekdayNumber target
 357 | 
 358 | public export
 359 | isValidWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool
 360 | isValidWeekDate week target valueYear =
 361 |   (yearValue valueYear > 1582 && weekNumberValue week >= 0) ||
 362 |     IotaTime.Calendar.isValidDays {calendar = Gregorian}
 363 |       (weekDateDays week target valueYear)
 364 | 
 365 | ||| Construct a Gregorian Sunday-based week date under static validity evidence.
 366 | public export
 367 | fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) ->
 368 |                {auto 0 valid : So (isValidWeekDate week target valueYear)} ->
 369 |                CalendarDate Gregorian
 370 | fromWeekDate week target valueYear =
 371 |   makeGregorianDate (weekDateDays week target valueYear)
 372 | 
 373 | ||| Validate a runtime Gregorian Sunday-based week date.
 374 | public export
 375 | refineWeekDate : WeekNumber -> DayOfWeek -> Year ->
 376 |                  Either GregorianDateError (CalendarDate Gregorian)
 377 | refineWeekDate week target valueYear =
 378 |   case choose (isValidWeekDate week target valueYear) of
 379 |     Left valid => Right (fromWeekDate week target valueYear @{valid})
 380 |     Right _ => Left (InvalidGregorianWeekDate week target valueYear)