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