
   0 | module IotaTime.Calendar.Persian
   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 astronomical Persian calendar over its vouched year range 1-1500.
  13 | public export
  14 | data Persian = PersianCalendar
  15 | 
  16 | namespace PersianMonths
  17 |   public export
  18 |   data PersianMonth
  19 |     = Farvardin | Ordibehesht | Khordad | Tir | Mordad | Shahrivar
  20 |     | Mehr | Aban | Azar | Dey | Bahman | Esfand
  21 | 
  22 |   public export
  23 |   monthNumber : PersianMonth -> Integer
  24 |   monthNumber Farvardin = 1
  25 |   monthNumber Ordibehesht = 2
  26 |   monthNumber Khordad = 3
  27 |   monthNumber Tir = 4
  28 |   monthNumber Mordad = 5
  29 |   monthNumber Shahrivar = 6
  30 |   monthNumber Mehr = 7
  31 |   monthNumber Aban = 8
  32 |   monthNumber Azar = 9
  33 |   monthNumber Dey = 10
  34 |   monthNumber Bahman = 11
  35 |   monthNumber Esfand = 12
  36 | 
  37 |   public export
  38 |   Eq PersianMonth where
  39 |     left == right = monthNumber left == monthNumber right
  40 | 
  41 |   public export
  42 |   Ord PersianMonth where
  43 |     compare left right = compare (monthNumber left) (monthNumber right)
  44 | 
  45 |   %runElab derive `{PersianMonth} [Show]
  46 | 
  47 | monthFromNumber : Integer -> PersianMonth
  48 | monthFromNumber 1 = PersianMonths.Farvardin
  49 | monthFromNumber 2 = PersianMonths.Ordibehesht
  50 | monthFromNumber 3 = PersianMonths.Khordad
  51 | monthFromNumber 4 = PersianMonths.Tir
  52 | monthFromNumber 5 = PersianMonths.Mordad
  53 | monthFromNumber 6 = PersianMonths.Shahrivar
  54 | monthFromNumber 7 = PersianMonths.Mehr
  55 | monthFromNumber 8 = PersianMonths.Aban
  56 | monthFromNumber 9 = PersianMonths.Azar
  57 | monthFromNumber 10 = PersianMonths.Dey
  58 | monthFromNumber 11 = PersianMonths.Bahman
  59 | monthFromNumber _ = PersianMonths.Esfand
  60 | 
  61 | public export
  62 | weekdayFromDays : Integer -> DayOfWeek
  63 | weekdayFromDays value = weekdayFromNumber (value + 3)
  64 | 
  65 | public export
  66 | minimumYear : Integer
  67 | minimumYear = 1
  68 | 
  69 | public export
  70 | maximumYear : Integer
  71 | maximumYear = 1500
  72 | 
  73 | public export
  74 | epoch : Integer
  75 | epoch = -503284
  76 | 
  77 | public export
  78 | leapYears : List Integer
  79 | leapYears =
  80 |   [ 5, 9, 13, 17, 21, 25, 29, 33, 38, 42, 46, 50, 54, 58, 62, 66
  81 |   , 71, 75, 79, 83, 87, 91, 95, 99, 104, 108, 112, 116, 120, 124, 128, 132
  82 |   , 137, 141, 145, 149, 153, 157, 161, 166, 170, 174, 178, 182, 186, 190, 194
  83 |   , 199, 203, 207, 211, 215, 219, 223, 227, 232, 236, 240, 244, 248, 252, 256
  84 |   , 260, 265, 269, 273, 277, 281, 285, 289, 293, 298, 302, 306, 310, 314, 318
  85 |   , 322, 326, 331, 335, 339, 343, 347, 351, 355, 359, 364, 368, 372, 376, 380
  86 |   , 384, 388, 392, 397, 401, 405, 409, 413, 417, 421, 426, 430, 434, 438, 442
  87 |   , 446, 450, 454, 459, 463, 467, 471, 475, 479, 483, 487, 492, 496, 500, 504
  88 |   , 508, 512, 516, 520, 525, 529, 533, 537, 541, 545, 549, 553, 558, 562, 566
  89 |   , 570, 574, 578, 582, 586, 591, 595, 599, 603, 607, 611, 615, 619, 624, 628
  90 |   , 632, 636, 640, 644, 648, 652, 657, 661, 665, 669, 673, 677, 681, 686, 690
  91 |   , 694, 698, 702, 706, 710, 714, 719, 723, 727, 731, 735, 739, 743, 747, 752
  92 |   , 756, 760, 764, 768, 772, 776, 780, 784, 789, 793, 797, 801, 805, 809, 813
  93 |   , 818, 822, 826, 830, 834, 838, 842, 846, 851, 855, 859, 863, 867, 871, 875
  94 |   , 879, 884, 888, 892, 896, 900, 904, 908, 912, 917, 921, 925, 929, 933, 937
  95 |   , 941, 945, 950, 954, 958, 962, 966, 970, 974, 978, 983, 987, 991, 995, 999
  96 |   , 1003, 1007, 1011, 1016, 1020, 1024, 1028, 1032, 1036, 1040, 1044, 1049
  97 |   , 1053, 1057, 1061, 1065, 1069, 1073, 1077, 1082, 1086, 1090, 1094, 1098
  98 |   , 1102, 1106, 1111, 1115, 1119, 1123, 1127, 1131, 1135, 1139, 1144, 1148
  99 |   , 1152, 1156, 1160, 1164, 1168, 1172, 1176, 1181, 1185, 1189, 1193, 1197
 100 |   , 1201, 1205, 1210, 1214, 1218, 1222, 1226, 1230, 1234, 1238, 1243, 1247
 101 |   , 1251, 1255, 1259, 1263, 1267, 1271, 1276, 1280, 1284, 1288, 1292, 1296
 102 |   , 1300, 1304, 1309, 1313, 1317, 1321, 1325, 1329, 1333, 1337, 1342, 1346
 103 |   , 1350, 1354, 1358, 1362, 1366, 1370, 1375, 1379, 1383, 1387, 1391, 1395
 104 |   , 1399, 1403, 1408, 1412, 1416, 1420, 1424, 1428, 1432, 1436, 1441, 1445
 105 |   , 1449, 1453, 1457, 1461, 1465, 1469, 1474, 1478, 1482, 1486, 1490, 1494
 106 |   , 1498
 107 |   ]
 108 | 
 109 | ||| Whether a supported Persian year contains Esfand 30.
 110 | public export
 111 | isLeapYear : Year -> Bool
 112 | isLeapYear value = elem (yearValue value) leapYears
 113 | 
 114 | public export
 115 | countLeapsBefore : Integer -> List Integer -> Integer
 116 | countLeapsBefore _ [] = 0
 117 | countLeapsBefore year (leapYear :: rest) =
 118 |   if leapYear < year then 1 + countLeapsBefore year rest else 0
 119 | 
 120 | public export
 121 | newYearDay : Year -> Integer
 122 | newYearDay value =
 123 |   epoch + (yearValue value - 1) * 365 +
 124 |     countLeapsBefore (yearValue value) leapYears
 125 | 
 126 | public export
 127 | lastDay : Integer
 128 | lastDay = newYearDay 1501 - 1
 129 | 
 130 | export
 131 | record PersianDate where
 132 |   constructor MkPersianDate
 133 |   daysSinceEpoch : Integer
 134 |   0 validDays : So
 135 |     (daysSinceEpoch >= IotaTime.Calendar.Persian.epoch &&
 136 |      daysSinceEpoch <= IotaTime.Calendar.Persian.lastDay)
 137 | 
 138 | public export
 139 | Eq PersianDate where
 140 |   left == right = left.daysSinceEpoch == right.daysSinceEpoch
 141 | 
 142 | public export
 143 | Ord PersianDate where
 144 |   compare left right = compare left.daysSinceEpoch right.daysSinceEpoch
 145 | 
 146 | checkedPersianDate : (days : Integer) ->
 147 |                      (0 valid : So
 148 |                        (days >= IotaTime.Calendar.Persian.epoch &&
 149 |                         days <= IotaTime.Calendar.Persian.lastDay)) ->
 150 |                      PersianDate
 151 | checkedPersianDate days valid = MkPersianDate days valid
 152 | 
 153 | public export
 154 | maxDaysInMonth : PersianMonth -> Year -> DayOfMonth
 155 | maxDaysInMonth PersianMonths.Esfand value =
 156 |   if isLeapYear value then 30 else 29
 157 | maxDaysInMonth valueMonth _ =
 158 |   if PersianMonths.monthNumber valueMonth <= 6 then 31 else 30
 159 | 
 160 | public export
 161 | isValidDate : DayOfMonth -> PersianMonth -> Year -> Bool
 162 | isValidDate valueDay valueMonth valueYear =
 163 |   let dayNumber = dayOfMonthValue valueDay
 164 |       yearNumber = yearValue valueYear
 165 |       maxDay = dayOfMonthValue (maxDaysInMonth valueMonth valueYear)
 166 |    in dayNumber >= 1 && dayNumber <= maxDay &&
 167 |       yearNumber >= minimumYear && yearNumber <= maximumYear
 168 | 
 169 | public export
 170 | monthOffset : PersianMonth -> Integer
 171 | monthOffset value =
 172 |   let number = PersianMonths.monthNumber value
 173 |    in if number <= 6 then (number - 1) * 31
 174 |       else 186 + (number - 7) * 30
 175 | 
 176 | public export
 177 | daysFromCivil : Year -> PersianMonth -> DayOfMonth -> Integer
 178 | daysFromCivil valueYear valueMonth valueDay =
 179 |   newYearDay valueYear + monthOffset valueMonth +
 180 |     dayOfMonthValue valueDay - 1
 181 | 
 182 | findPersianYear : Nat -> Integer -> Integer -> Integer
 183 | findPersianYear Z estimate days = estimate
 184 | findPersianYear (S fuel) estimate days =
 185 |   if days < newYearDay (yearFromInteger estimate)
 186 |     then findPersianYear fuel (estimate - 1) days
 187 |     else if days >= newYearDay (yearFromInteger (estimate + 1))
 188 |       then findPersianYear fuel (estimate + 1) days
 189 |       else estimate
 190 | 
 191 | persianCivilFromDays : Integer -> (Year, PersianMonth, DayOfMonth)
 192 | persianCivilFromDays value =
 193 |   let estimate = max minimumYear (min maximumYear
 194 |         ((value - epoch) `div` 365 + 1))
 195 |       yearNumber = findPersianYear 1500 estimate value
 196 |       valueYear = yearFromInteger yearNumber
 197 |       dayOfYear = value - newYearDay valueYear
 198 |       monthNumber = if dayOfYear == 365 then 12
 199 |         else if dayOfYear < 186 then dayOfYear `div` 31 + 1
 200 |         else (dayOfYear - 186) `div` 30 + 7
 201 |       offset = if monthNumber <= 6 then (monthNumber - 1) * 31
 202 |         else 186 + (monthNumber - 7) * 30
 203 |       dayNumber = dayOfYear - offset + 1
 204 |    in (valueYear, monthFromNumber monthNumber,
 205 |        dayOfMonthFromInteger dayNumber)
 206 | 
 207 | export
 208 | HasCalendarBridge PersianDate where
 209 |   toBridgeDays = daysSinceEpoch
 210 |   acceptsBridgeDays value = value >= epoch && value <= lastDay
 211 |   fromBridgeDays days @{valid} = checkedPersianDate days valid
 212 |   bridgeCalendarName = "Persian"
 213 | 
 214 | clampToPersian : Integer -> Integer
 215 | clampToPersian = max epoch . min lastDay
 216 | 
 217 | makePersianDate : Integer -> PersianDate
 218 | makePersianDate days =
 219 |   let clamped = clampToPersian days
 220 |    in case choose (clamped >= epoch && clamped <= lastDay) of
 221 |         Left valid => checkedPersianDate clamped valid
 222 |         Right _ => checkedPersianDate epoch Oh
 223 | 
 224 | shiftPersianDays : Integer -> PersianDate -> PersianDate
 225 | shiftPersianDays amount date =
 226 |   makePersianDate (date.daysSinceEpoch + amount)
 227 | 
 228 | shiftPersianMonths : Integer -> PersianDate -> PersianDate
 229 | shiftPersianMonths amount date =
 230 |   let (valueYear, valueMonth, valueDay) =
 231 |         persianCivilFromDays date.daysSinceEpoch
 232 |       monthOrdinal = PersianMonths.monthNumber valueMonth - 1 + amount
 233 |       targetYear = yearFromInteger (yearValue valueYear + monthOrdinal `div` 12)
 234 |       targetMonth = monthFromNumber (monthOrdinal `mod` 12 + 1)
 235 |       targetDay = min valueDay (maxDaysInMonth targetMonth targetYear)
 236 |   in makePersianDate (daysFromCivil targetYear targetMonth targetDay)
 237 | 
 238 | shiftPersianYears : Integer -> PersianDate -> PersianDate
 239 | shiftPersianYears amount date =
 240 |   let (valueYear, valueMonth, valueDay) =
 241 |         persianCivilFromDays date.daysSinceEpoch
 242 |       targetYear = yearFromInteger (yearValue valueYear + amount)
 243 |       targetDay = min valueDay (maxDaysInMonth valueMonth targetYear)
 244 |   in makePersianDate (daysFromCivil targetYear valueMonth targetDay)
 245 | 
 246 | applyPersianPeriod : Period target -> PersianDate -> PersianDate
 247 | applyPersianPeriod = applyDatePeriodWith
 248 |   shiftPersianYears shiftPersianMonths shiftPersianDays
 249 | 
 250 | persianDayOfWeek : PersianDate -> DayOfWeek
 251 | persianDayOfWeek date = weekdayFromDays date.daysSinceEpoch
 252 | 
 253 | nextPersian : Integer -> DayOfWeek -> PersianDate -> PersianDate
 254 | nextPersian count target date =
 255 |   makePersianDate (date.daysSinceEpoch +
 256 |     nextWeekdayOffset count (persianDayOfWeek date) target)
 257 | 
 258 | previousPersian : Integer -> DayOfWeek -> PersianDate -> PersianDate
 259 | previousPersian count target date =
 260 |   makePersianDate (date.daysSinceEpoch +
 261 |     previousWeekdayOffset count (persianDayOfWeek date) target)
 262 | 
 263 | public export
 264 | Calendar Persian where
 265 |   DateRep = PersianDate
 266 |   MonthRep _ = PersianMonth
 267 | 
 268 |   isValidDays value = value >= epoch && value <= lastDay
 269 |   fromDays days @{valid} = checkedPersianDate days valid
 270 |   toDaysFor date = date.daysSinceEpoch
 271 |   toDaysValid (MkPersianDate _ valid) = valid
 272 |   toFromDays _ _ = Refl
 273 |   fromToDays (MkPersianDate _ _) = Refl
 274 |   calendarName = "Persian"
 275 | 
 276 |   year' date = let (value, _, _) = persianCivilFromDays date.daysSinceEpoch in value
 277 |   toYmd date = let (_, valueMonth, valueDay) =
 278 |                     persianCivilFromDays date.daysSinceEpoch
 279 |                 in (valueMonth, valueDay)
 280 |   day' date = let (_, _, value) = persianCivilFromDays date.daysSinceEpoch in value
 281 |   month' date = let (_, value, _) = persianCivilFromDays date.daysSinceEpoch in value
 282 | 
 283 |   applyCalendarPeriod' = applyPersianPeriod
 284 |   shiftCalendarDays' = shiftPersianDays
 285 | 
 286 |   dayOfWeekFor = persianDayOfWeek
 287 |   nextFor = nextPersian
 288 |   previousFor = previousPersian
 289 | 
 290 | public export
 291 | Show PersianDate where
 292 |   show date = case persianCivilFromDays date.daysSinceEpoch of
 293 |     (valueYear, valueMonth, valueDay) =>
 294 |       "calendarDate " ++ show valueDay ++ " " ++
 295 |       show valueMonth ++ " " ++ show valueYear
 296 | 
 297 | public export
 298 | HasCalendar PersianDate where
 299 |   calendarCapability = ()
 300 | 
 301 | public export
 302 | PeriodTarget PersianDate where
 303 |   periodTarget = ()
 304 | 
 305 | public export
 306 | ApplyPeriod PersianDate where
 307 |   applyPeriod = applyPersianPeriod
 308 | 
 309 | public export
 310 | CalendarValue PersianDate where
 311 |   CalendarMonth _ = PersianMonth
 312 |   calendarValueToDays = toDaysFor {calendar = Persian}
 313 |   calendarValueYear = yearFor {calendar = Persian}
 314 |   calendarValueMonthDay = toYmd {calendar = Persian}
 315 |   calendarValueDayOfWeek = dayOfWeekFor {calendar = Persian}
 316 |   calendarValueBetweenWith = betweenWithFor {calendar = Persian}
 317 | 
 318 | public export
 319 | CalendarNavigation PersianDate where
 320 |   calendarValueNext = nextFor {calendar = Persian}
 321 |   calendarValuePrevious = previousFor {calendar = Persian}
 322 | 
 323 | ||| Construct a statically validated Persian date in years 1-1500.
 324 | public export
 325 | calendarDate : (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) ->
 326 |               (valueYear : Year) ->
 327 |               {auto 0 valid : So
 328 |                 (isValidDate valueDay valueMonth valueYear)} ->
 329 |               CalendarDate Persian
 330 | calendarDate valueDay valueMonth valueYear =
 331 |   makePersianDate (daysFromCivil valueYear valueMonth valueDay)
 332 | 
 333 | ||| Failures produced while refining untrusted Persian date data.
 334 | public export
 335 | data PersianDateError
 336 |   = InvalidPersianDate DayOfMonth PersianMonth Year
 337 |   | InvalidPersianDayCount Integer
 338 |   | InvalidPersianNthDay DayNth DayOfWeek PersianMonth Year
 339 |   | InvalidPersianWeekDate WeekNumber DayOfWeek Year
 340 | 
 341 | ||| Validate runtime day, month, and year components as a Persian date.
 342 | public export
 343 | refineDate : DayOfMonth -> PersianMonth -> Year ->
 344 |                     Either PersianDateError (CalendarDate Persian)
 345 | refineDate valueDay valueMonth valueYear =
 346 |   case choose (isValidDate valueDay valueMonth valueYear) of
 347 |     Left valid => Right (calendarDate valueDay valueMonth valueYear @{valid})
 348 |     Right _ => Left (InvalidPersianDate valueDay valueMonth valueYear)
 349 | 
 350 | ||| Construct a Persian date from a statically valid calendar-relative day count.
 351 | public export
 352 | fromDays : (days : Integer) ->
 353 |                   {auto 0 valid : So
 354 |                     (IotaTime.Calendar.isValidDays {calendar = Persian} days)} ->
 355 |                   CalendarDate Persian
 356 | fromDays days @{valid} = checkedPersianDate days valid
 357 | 
 358 | ||| Validate a runtime Persian day count within the supported year range.
 359 | public export
 360 | refineDays : Integer -> Either PersianDateError (CalendarDate Persian)
 361 | refineDays days = case choose
 362 |   (IotaTime.Calendar.isValidDays {calendar = Persian} days) of
 363 |   Left valid => Right (fromDays days @{valid})
 364 |   Right _ => Left (InvalidPersianDayCount days)
 365 | 
 366 | public export
 367 | nthDayOfMonth : DayNth -> DayOfWeek -> PersianMonth -> Year ->
 368 |                        DayOfMonth
 369 | nthDayOfMonth nth target valueMonth valueYear =
 370 |   let monthLength = maxDaysInMonth valueMonth valueYear
 371 |       firstOffset = (weekdayNumber target -
 372 |         weekdayNumber (weekdayFromDays
 373 |           (daysFromCivil valueYear valueMonth 1))) `mod` daysPerWeek
 374 |       lastOffset = (weekdayNumber (weekdayFromDays
 375 |         (daysFromCivil valueYear valueMonth monthLength)) -
 376 |         weekdayNumber target) `mod` daysPerWeek
 377 |       dayNumber = nthWeekdayDayNumber nth (dayOfMonthValue monthLength)
 378 |         firstOffset lastOffset
 379 |    in dayOfMonthFromInteger dayNumber
 380 | 
 381 | public export
 382 | isValidNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year -> Bool
 383 | isValidNthDay nth target valueMonth valueYear =
 384 |   yearValue valueYear >= minimumYear &&
 385 |   yearValue valueYear <= maximumYear && case nth of
 386 |     Fifth => nthDayOfMonth nth target valueMonth valueYear <=
 387 |       maxDaysInMonth valueMonth valueYear
 388 |     _ => True
 389 | 
 390 | ||| Construct the nth requested weekday in a Persian month.
 391 | public export
 392 | fromNthDay : (nth : DayNth) -> (target : DayOfWeek) ->
 393 |                     (valueMonth : PersianMonth) -> (valueYear : Year) ->
 394 |                     {auto 0 valid : So
 395 |                       (isValidNthDay nth target valueMonth valueYear)} ->
 396 |                     CalendarDate Persian
 397 | fromNthDay nth target valueMonth valueYear =
 398 |   makePersianDate (daysFromCivil valueYear valueMonth
 399 |     (nthDayOfMonth nth target valueMonth valueYear))
 400 | 
 401 | ||| Validate an nth-weekday request for a Persian month.
 402 | public export
 403 | refineNthDay : DayNth -> DayOfWeek -> PersianMonth -> Year ->
 404 |                       Either PersianDateError (CalendarDate Persian)
 405 | refineNthDay nth target valueMonth valueYear =
 406 |   case choose (isValidNthDay nth target valueMonth valueYear) of
 407 |     Left valid => Right
 408 |       (fromNthDay nth target valueMonth valueYear @{valid})
 409 |     Right _ => Left (InvalidPersianNthDay nth target valueMonth valueYear)
 410 | 
 411 | public export
 412 | weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer
 413 | weekDateDays week target valueYear =
 414 |   let firstDay = daysFromCivil valueYear PersianMonths.Farvardin 1
 415 |       firstWeekStart = firstDay -
 416 |         ((weekdayNumber (weekdayFromDays firstDay) - 6)
 417 |           `mod` 7)
 418 |       targetOffset = (weekdayNumber target - 6) `mod` 7
 419 |    in firstWeekStart + 7 * (weekNumberValue week - 1) + targetOffset
 420 | 
 421 | public export
 422 | isValidWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool
 423 | isValidWeekDate week target valueYear =
 424 |   let days = weekDateDays week target valueYear
 425 |    in yearValue valueYear >= minimumYear &&
 426 |       yearValue valueYear <= maximumYear &&
 427 |       IotaTime.Calendar.isValidDays {calendar = Persian} days
 428 | 
 429 | ||| Construct a Persian Saturday-based week date under static validity evidence.
 430 | public export
 431 | fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) ->
 432 |                (valueYear : Year) ->
 433 |                {auto 0 valid : So (isValidWeekDate week target valueYear)} ->
 434 |                CalendarDate Persian
 435 | fromWeekDate week target valueYear =
 436 |   makePersianDate (weekDateDays week target valueYear)
 437 | 
 438 | ||| Validate a runtime Persian Saturday-based week date.
 439 | public export
 440 | refineWeekDate : WeekNumber -> DayOfWeek -> Year ->
 441 |                  Either PersianDateError (CalendarDate Persian)
 442 | refineWeekDate week target valueYear =
 443 |   case choose (isValidWeekDate week target valueYear) of
 444 |     Left valid => Right (fromWeekDate week target valueYear @{valid})
 445 |     Right _ => Left (InvalidPersianWeekDate week target valueYear)
 446 | 
 447 | ||| Exact arithmetic rules available for the Solar Hijri calendar.
 448 | public export
 449 | data PersianArithmeticRule = Simple | Birashk
 450 | 
 451 | ||| A Persian calendar whose leap years are fixed by an arithmetic rule.
 452 | public export
 453 | data ArithmeticPersian : PersianArithmeticRule -> Type where
 454 |   MkArithmeticPersian : ArithmeticPersian rule
 455 | 
 456 | ||| The legacy 33-year Persian cycle used by the BCL before .NET 4.6.
 457 | public export
 458 | PersianSimple : Type
 459 | PersianSimple = ArithmeticPersian Simple
 460 | 
 461 | ||| Ahmad Birashk's nested 2820-year arithmetic Persian cycle.
 462 | public export
 463 | PersianArithmetic : Type
 464 | PersianArithmetic = ArithmeticPersian Birashk
 465 | 
 466 | simpleLeapPositions : List Integer
 467 | simpleLeapPositions = [1, 5, 9, 13, 17, 22, 26, 30]
 468 | 
 469 | countAtMost : Integer -> List Integer -> Integer
 470 | countAtMost _ [] = 0
 471 | countAtMost limit (value :: rest) =
 472 |   if value <= limit then 1 + countAtMost limit rest else 0
 473 | 
 474 | simpleLeapsBefore : Integer -> Integer
 475 | simpleLeapsBefore year =
 476 |   let elapsed = year - 1
 477 |    in (elapsed `div` 33) * 8 +
 478 |       countAtMost (elapsed `mod` 33) simpleLeapPositions
 479 | 
 480 | simpleNewYear : Integer -> Integer
 481 | simpleNewYear year = -503285 + (year - 1) * 365 + simpleLeapsBefore year
 482 | 
 483 | arithmeticNewYear : Integer -> Integer
 484 | arithmeticNewYear year =
 485 |   let base = year - 474
 486 |       cycleYear = 474 + base `mod` 2820
 487 |    in -503284 + ((cycleYear * 682 - 110) `div` 2816) +
 488 |       (cycleYear - 1) * 365 + (base `div` 2820) * 1029983
 489 | 
 490 | arithmeticRuleEpoch : PersianArithmeticRule -> Integer
 491 | arithmeticRuleEpoch Simple = -503285
 492 | arithmeticRuleEpoch Birashk = -503284
 493 | 
 494 | arithmeticRuleLastDay : PersianArithmeticRule -> Integer
 495 | arithmeticRuleLastDay Simple = simpleNewYear 9378 - 1
 496 | arithmeticRuleLastDay Birashk = arithmeticNewYear 9378 - 1
 497 | 
 498 | export
 499 | arithmeticRuleName : PersianArithmeticRule -> String
 500 | arithmeticRuleName Simple = "Persian Simple"
 501 | arithmeticRuleName Birashk = "Persian Arithmetic"
 502 | 
 503 | arithmeticRuleConstructorName : PersianArithmeticRule -> String
 504 | arithmeticRuleConstructorName Simple = "simpleCalendarDate"
 505 | arithmeticRuleConstructorName Birashk = "arithmeticCalendarDate"
 506 | 
 507 | arithmeticRuleIsLeapYear : PersianArithmeticRule -> Integer -> Bool
 508 | arithmeticRuleIsLeapYear Simple year =
 509 |   simpleNewYear (year + 1) - simpleNewYear year == 366
 510 | arithmeticRuleIsLeapYear Birashk year =
 511 |     let cycleYear = (year - 474) `mod` 2820 + 474
 512 |      in ((cycleYear + 38) * 31) `mod` 128 < 31
 513 | 
 514 | arithmeticRuleNewYearDay : PersianArithmeticRule -> Integer -> Integer
 515 | arithmeticRuleNewYearDay Simple = simpleNewYear
 516 | arithmeticRuleNewYearDay Birashk = arithmeticNewYear
 517 | 
 518 | export
 519 | record ArithmeticPersianDate (rule : PersianArithmeticRule) where
 520 |   constructor MkArithmeticPersianDate
 521 |   arithmeticDaysSinceEpoch : Integer
 522 |   0 validDays : So
 523 |     (arithmeticDaysSinceEpoch >= arithmeticRuleEpoch rule &&
 524 |      arithmeticDaysSinceEpoch <= arithmeticRuleLastDay rule)
 525 | 
 526 | public export
 527 | Eq (ArithmeticPersianDate rule) where
 528 |   left == right = left.arithmeticDaysSinceEpoch == right.arithmeticDaysSinceEpoch
 529 | 
 530 | public export
 531 | Ord (ArithmeticPersianDate rule) where
 532 |   compare left right = compare left.arithmeticDaysSinceEpoch right.arithmeticDaysSinceEpoch
 533 | 
 534 | checkedArithmeticPersianDate : {rule : PersianArithmeticRule} ->
 535 |   (days : Integer) ->
 536 |   (0 valid : So
 537 |     (days >= arithmeticRuleEpoch rule &&
 538 |      days <= arithmeticRuleLastDay rule)) ->
 539 |   ArithmeticPersianDate rule
 540 | checkedArithmeticPersianDate days valid = MkArithmeticPersianDate days valid
 541 | 
 542 | fromArithmeticPersianDays : {rule : PersianArithmeticRule} ->
 543 |   (days : Integer) ->
 544 |   {auto 0 valid : So
 545 |     (days >= arithmeticRuleEpoch rule &&
 546 |      days <= arithmeticRuleLastDay rule)} ->
 547 |   ArithmeticPersianDate rule
 548 | fromArithmeticPersianDays days @{valid} =
 549 |   checkedArithmeticPersianDate days valid
 550 | 
 551 | public export
 552 | minimumArithmeticYear : Integer
 553 | minimumArithmeticYear = 1
 554 | 
 555 | public export
 556 | maximumArithmeticYear : Integer
 557 | maximumArithmeticYear = 9377
 558 | 
 559 | public export
 560 | isArithmeticLeapYear : {rule : PersianArithmeticRule} ->
 561 |   Year -> Bool
 562 | isArithmeticLeapYear {rule} value =
 563 |   arithmeticRuleIsLeapYear rule (yearValue value)
 564 | 
 565 | public export
 566 | arithmeticNewYearDay : {rule : PersianArithmeticRule} ->
 567 |   Year -> Integer
 568 | arithmeticNewYearDay {rule} value =
 569 |   arithmeticRuleNewYearDay rule (yearValue value)
 570 | 
 571 | ||| The final supported day under the selected arithmetic Persian rule.
 572 | public export
 573 | arithmeticLastDay : {rule : PersianArithmeticRule} ->
 574 |   Integer
 575 | arithmeticLastDay {rule} =
 576 |   arithmeticRuleNewYearDay rule (maximumArithmeticYear + 1) - 1
 577 | 
 578 | public export
 579 | maxArithmeticDaysInMonth : {rule : PersianArithmeticRule} ->
 580 |   PersianMonth -> Year -> DayOfMonth
 581 | maxArithmeticDaysInMonth {rule} PersianMonths.Esfand value =
 582 |   if isArithmeticLeapYear {rule} value then 30 else 29
 583 | maxArithmeticDaysInMonth valueMonth _ =
 584 |   if PersianMonths.monthNumber valueMonth <= 6 then 31 else 30
 585 | 
 586 | public export
 587 | isValidArithmeticDate : {rule : PersianArithmeticRule} ->
 588 |   DayOfMonth -> PersianMonth -> Year -> Bool
 589 | isValidArithmeticDate {rule} valueDay valueMonth valueYear =
 590 |   let dayNumber = dayOfMonthValue valueDay
 591 |       yearNumber = yearValue valueYear
 592 |       maxDay = dayOfMonthValue
 593 |         (maxArithmeticDaysInMonth {rule} valueMonth valueYear)
 594 |    in dayNumber >= 1 && dayNumber <= maxDay &&
 595 |       yearNumber >= minimumArithmeticYear &&
 596 |       yearNumber <= maximumArithmeticYear
 597 | 
 598 | public export
 599 | arithmeticDaysFromCivil : {rule : PersianArithmeticRule} ->
 600 |   Year -> PersianMonth -> DayOfMonth -> Integer
 601 | arithmeticDaysFromCivil {rule} valueYear valueMonth valueDay =
 602 |   arithmeticNewYearDay {rule} valueYear + monthOffset valueMonth +
 603 |     dayOfMonthValue valueDay - 1
 604 | 
 605 | findArithmeticPersianYear : {rule : PersianArithmeticRule} ->
 606 |   Nat -> Integer -> Integer -> Integer
 607 | findArithmeticPersianYear {rule} Z estimate _ = estimate
 608 | findArithmeticPersianYear {rule} (S fuel) estimate days =
 609 |   if days < arithmeticRuleNewYearDay rule estimate
 610 |     then findArithmeticPersianYear {rule} fuel (estimate - 1) days
 611 |     else if days >= arithmeticRuleNewYearDay rule (estimate + 1)
 612 |       then findArithmeticPersianYear {rule} fuel (estimate + 1) days
 613 |       else estimate
 614 | 
 615 | arithmeticPersianCivilFromDays : {rule : PersianArithmeticRule} ->
 616 |   Integer -> (Year, PersianMonth, DayOfMonth)
 617 | arithmeticPersianCivilFromDays {rule} value =
 618 |   let epoch = arithmeticRuleEpoch rule
 619 |       estimate = max minimumArithmeticYear
 620 |         (min maximumArithmeticYear ((value - epoch) `div` 365 + 1))
 621 |       yearNumber = findArithmeticPersianYear {rule} 9377 estimate value
 622 |       valueYear = yearFromInteger yearNumber
 623 |       dayOfYear = value - arithmeticNewYearDay {rule} valueYear
 624 |       monthNumber = if dayOfYear == 365 then 12
 625 |         else if dayOfYear < 186 then dayOfYear `div` 31 + 1
 626 |         else (dayOfYear - 186) `div` 30 + 7
 627 |       offset = if monthNumber <= 6 then (monthNumber - 1) * 31
 628 |         else 186 + (monthNumber - 7) * 30
 629 |    in (valueYear, monthFromNumber monthNumber,
 630 |        dayOfMonthFromInteger (dayOfYear - offset + 1))
 631 | 
 632 | export
 633 | {rule : PersianArithmeticRule} ->
 634 |   HasCalendarBridge (ArithmeticPersianDate rule) where
 635 |   toBridgeDays = arithmeticDaysSinceEpoch
 636 |   acceptsBridgeDays value = value >= arithmeticRuleEpoch rule &&
 637 |     value <= arithmeticRuleLastDay rule
 638 |   fromBridgeDays = fromArithmeticPersianDays {rule}
 639 |   bridgeCalendarName = arithmeticRuleName rule
 640 | 
 641 | clampToArithmeticPersian : {rule : PersianArithmeticRule} ->
 642 |   Integer -> Integer
 643 | clampToArithmeticPersian {rule} =
 644 |   max (arithmeticRuleEpoch rule) . min (arithmeticRuleLastDay rule)
 645 | 
 646 | makeArithmeticPersianDate : {rule : PersianArithmeticRule} ->
 647 |   Integer -> ArithmeticPersianDate rule
 648 | makeArithmeticPersianDate {rule} days =
 649 |   let clamped = clampToArithmeticPersian {rule} days
 650 |    in case choose
 651 |         (clamped >= arithmeticRuleEpoch rule &&
 652 |          clamped <= arithmeticRuleLastDay rule) of
 653 |         Left valid => checkedArithmeticPersianDate clamped valid
 654 |         Right _ => case rule of
 655 |           Simple => checkedArithmeticPersianDate (-503285) Oh
 656 |           Birashk => checkedArithmeticPersianDate (-503284) Oh
 657 | 
 658 | shiftArithmeticPersianDays : {rule : PersianArithmeticRule} ->
 659 |   Integer -> ArithmeticPersianDate rule ->
 660 |   ArithmeticPersianDate rule
 661 | shiftArithmeticPersianDays {rule} amount date =
 662 |   makeArithmeticPersianDate {rule} (date.arithmeticDaysSinceEpoch + amount)
 663 | 
 664 | shiftArithmeticPersianMonths : {rule : PersianArithmeticRule} ->
 665 |   Integer -> ArithmeticPersianDate rule ->
 666 |   ArithmeticPersianDate rule
 667 | shiftArithmeticPersianMonths {rule} amount date =
 668 |   let (valueYear, valueMonth, valueDay) =
 669 |         arithmeticPersianCivilFromDays {rule} date.arithmeticDaysSinceEpoch
 670 |       monthOrdinal = PersianMonths.monthNumber valueMonth - 1 + amount
 671 |       targetYear = yearFromInteger (yearValue valueYear + monthOrdinal `div` 12)
 672 |       targetMonth = monthFromNumber (monthOrdinal `mod` 12 + 1)
 673 |       targetDay = min valueDay
 674 |         (maxArithmeticDaysInMonth {rule} targetMonth targetYear)
 675 |      in makeArithmeticPersianDate {rule}
 676 |        (arithmeticDaysFromCivil {rule} targetYear targetMonth targetDay)
 677 | 
 678 | shiftArithmeticPersianYears : {rule : PersianArithmeticRule} ->
 679 |   Integer -> ArithmeticPersianDate rule ->
 680 |   ArithmeticPersianDate rule
 681 | shiftArithmeticPersianYears {rule} amount date =
 682 |   let (valueYear, valueMonth, valueDay) =
 683 |         arithmeticPersianCivilFromDays {rule} date.arithmeticDaysSinceEpoch
 684 |       targetYear = yearFromInteger (yearValue valueYear + amount)
 685 |       targetDay = min valueDay
 686 |         (maxArithmeticDaysInMonth {rule} valueMonth targetYear)
 687 |      in makeArithmeticPersianDate {rule}
 688 |        (arithmeticDaysFromCivil {rule} targetYear valueMonth targetDay)
 689 | 
 690 | applyArithmeticPersianPeriod : {rule : PersianArithmeticRule} ->
 691 |   Period target -> ArithmeticPersianDate rule ->
 692 |   ArithmeticPersianDate rule
 693 | applyArithmeticPersianPeriod {rule} = applyDatePeriodWith
 694 |   (shiftArithmeticPersianYears {rule})
 695 |   (shiftArithmeticPersianMonths {rule})
 696 |   (shiftArithmeticPersianDays {rule})
 697 | 
 698 | arithmeticPersianDayOfWeek : ArithmeticPersianDate rule -> DayOfWeek
 699 | arithmeticPersianDayOfWeek date =
 700 |   weekdayFromDays date.arithmeticDaysSinceEpoch
 701 | 
 702 | nextArithmeticPersian : {rule : PersianArithmeticRule} ->
 703 |   Integer -> DayOfWeek ->
 704 |   ArithmeticPersianDate rule -> ArithmeticPersianDate rule
 705 | nextArithmeticPersian {rule} count target date =
 706 |   makeArithmeticPersianDate {rule} (date.arithmeticDaysSinceEpoch +
 707 |     nextWeekdayOffset count (arithmeticPersianDayOfWeek date) target)
 708 | 
 709 | previousArithmeticPersian : {rule : PersianArithmeticRule} ->
 710 |   Integer -> DayOfWeek ->
 711 |   ArithmeticPersianDate rule -> ArithmeticPersianDate rule
 712 | previousArithmeticPersian {rule} count target date =
 713 |   makeArithmeticPersianDate {rule} (date.arithmeticDaysSinceEpoch +
 714 |     previousWeekdayOffset count
 715 |       (arithmeticPersianDayOfWeek date) target)
 716 | 
 717 | public export
 718 | {rule : PersianArithmeticRule} ->
 719 |   Calendar (ArithmeticPersian rule) where
 720 |   DateRep = ArithmeticPersianDate rule
 721 |   MonthRep _ = PersianMonth
 722 | 
 723 |   isValidDays value = value >= arithmeticRuleEpoch rule &&
 724 |     value <= arithmeticRuleLastDay rule
 725 |   fromDays = fromArithmeticPersianDays {rule}
 726 |   toDaysFor date = date.arithmeticDaysSinceEpoch
 727 |   toDaysValid (MkArithmeticPersianDate _ valid) = valid
 728 |   toFromDays _ _ = Refl
 729 |   fromToDays (MkArithmeticPersianDate _ _) = Refl
 730 |   calendarName = arithmeticRuleName rule
 731 | 
 732 |   year' date = let (value, _, _) = arithmeticPersianCivilFromDays {rule}
 733 |                     date.arithmeticDaysSinceEpoch in value
 734 |   toYmd date = let (_, valueMonth, valueDay) =
 735 |                     arithmeticPersianCivilFromDays {rule}
 736 |                       date.arithmeticDaysSinceEpoch
 737 |                 in (valueMonth, valueDay)
 738 |   day' date = let (_, _, value) = arithmeticPersianCivilFromDays {rule}
 739 |                    date.arithmeticDaysSinceEpoch in value
 740 |   month' date = let (_, value, _) = arithmeticPersianCivilFromDays {rule}
 741 |                      date.arithmeticDaysSinceEpoch in value
 742 | 
 743 |   applyCalendarPeriod' = applyArithmeticPersianPeriod {rule}
 744 |   shiftCalendarDays' = shiftArithmeticPersianDays {rule}
 745 |   dayOfWeekFor = arithmeticPersianDayOfWeek
 746 |   nextFor = nextArithmeticPersian {rule}
 747 |   previousFor = previousArithmeticPersian {rule}
 748 | 
 749 | public export
 750 | {rule : PersianArithmeticRule} ->
 751 |   Show (ArithmeticPersianDate rule) where
 752 |   show date = case arithmeticPersianCivilFromDays {rule}
 753 |     date.arithmeticDaysSinceEpoch of
 754 |       (valueYear, valueMonth, valueDay) =>
 755 |         arithmeticRuleConstructorName rule ++ " " ++ show valueDay ++
 756 |         " " ++ show valueMonth ++ " " ++ show valueYear
 757 | 
 758 | public export
 759 | HasCalendar (ArithmeticPersianDate rule) where
 760 |   calendarCapability = ()
 761 | 
 762 | public export
 763 | {rule : PersianArithmeticRule} ->
 764 |   PeriodTarget (ArithmeticPersianDate rule) where
 765 |   periodTarget = ()
 766 | 
 767 | public export
 768 | {rule : PersianArithmeticRule} ->
 769 |   ApplyPeriod (ArithmeticPersianDate rule) where
 770 |   applyPeriod = applyArithmeticPersianPeriod {rule}
 771 | 
 772 | public export
 773 | {rule : PersianArithmeticRule} ->
 774 |   CalendarValue (ArithmeticPersianDate rule) where
 775 |   CalendarMonth _ = PersianMonth
 776 |   calendarValueToDays = toDaysFor {calendar = ArithmeticPersian rule}
 777 |   calendarValueYear = yearFor {calendar = ArithmeticPersian rule}
 778 |   calendarValueMonthDay = toYmd {calendar = ArithmeticPersian rule}
 779 |   calendarValueDayOfWeek = dayOfWeekFor {calendar = ArithmeticPersian rule}
 780 |   calendarValueBetweenWith =
 781 |     betweenWithFor {calendar = ArithmeticPersian rule}
 782 | 
 783 | public export
 784 | {rule : PersianArithmeticRule} ->
 785 |   CalendarNavigation (ArithmeticPersianDate rule) where
 786 |   calendarValueNext = nextFor {calendar = ArithmeticPersian rule}
 787 |   calendarValuePrevious = previousFor {calendar = ArithmeticPersian rule}
 788 | 
 789 | ||| Construct a statically validated Persian date under an arithmetic rule.
 790 | public export
 791 | arithmeticRuleCalendarDate : {rule : PersianArithmeticRule} ->
 792 |   (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) ->
 793 |   (valueYear : Year) ->
 794 |   {auto 0 valid : So
 795 |     (isValidArithmeticDate {rule} valueDay valueMonth valueYear)} ->
 796 |   CalendarDate (ArithmeticPersian rule)
 797 | arithmeticRuleCalendarDate {rule} valueDay valueMonth valueYear =
 798 |   makeArithmeticPersianDate {rule}
 799 |     (arithmeticDaysFromCivil {rule} valueYear valueMonth valueDay)
 800 | 
 801 | ||| Construct a date in the legacy 33-year Persian cycle.
 802 | public export
 803 | simpleCalendarDate : (valueDay : DayOfMonth) -> (valueMonth : PersianMonth) ->
 804 |   (valueYear : Year) ->
 805 |   {auto 0 valid : So
 806 |     (isValidArithmeticDate {rule = Simple}
 807 |       valueDay valueMonth valueYear)} -> CalendarDate PersianSimple
 808 | simpleCalendarDate = arithmeticRuleCalendarDate {rule = Simple}
 809 | 
 810 | ||| Construct a date in Birashk's 2820-year arithmetic Persian cycle.
 811 | public export
 812 | arithmeticCalendarDate : (valueDay : DayOfMonth) ->
 813 |   (valueMonth : PersianMonth) -> (valueYear : Year) ->
 814 |   {auto 0 valid : So
 815 |     (isValidArithmeticDate {rule = Birashk}
 816 |       valueDay valueMonth valueYear)} -> CalendarDate PersianArithmetic
 817 | arithmeticCalendarDate = arithmeticRuleCalendarDate {rule = Birashk}
 818 | 
 819 | ||| Validate runtime components under a selected arithmetic Persian rule.
 820 | public export
 821 | refineArithmeticRuleDate : {rule : PersianArithmeticRule} ->
 822 |   DayOfMonth -> PersianMonth -> Year ->
 823 |   Either PersianDateError (CalendarDate (ArithmeticPersian rule))
 824 | refineArithmeticRuleDate {rule} valueDay valueMonth valueYear =
 825 |   case choose (isValidArithmeticDate {rule}
 826 |     valueDay valueMonth valueYear) of
 827 |       Left valid => Right (arithmeticRuleCalendarDate {rule}
 828 |         valueDay valueMonth valueYear {valid = valid})
 829 |       Right _ => Left (InvalidPersianDate valueDay valueMonth valueYear)
 830 | 
 831 | public export
 832 | refineSimpleDate : DayOfMonth -> PersianMonth -> Year ->
 833 |   Either PersianDateError (CalendarDate PersianSimple)
 834 | refineSimpleDate = refineArithmeticRuleDate {rule = Simple}
 835 | 
 836 | public export
 837 | refineArithmeticDate : DayOfMonth -> PersianMonth -> Year ->
 838 |   Either PersianDateError (CalendarDate PersianArithmetic)
 839 | refineArithmeticDate = refineArithmeticRuleDate {rule = Birashk}
 840 | 
 841 | ||| Validate a day count under a selected arithmetic Persian rule.
 842 | public export
 843 | refineArithmeticDays : {rule : PersianArithmeticRule} ->
 844 |   Integer ->
 845 |   Either PersianDateError (CalendarDate (ArithmeticPersian rule))
 846 | refineArithmeticDays {rule} days =
 847 |   case choose
 848 |     (IotaTime.Calendar.isValidDays
 849 |       {calendar = ArithmeticPersian rule} days) of
 850 |     Left valid => Right (fromDays {calendar = ArithmeticPersian rule}
 851 |       days {valid = valid})
 852 |     Right _ => Left (InvalidPersianDayCount days)
 853 | 
 854 | arithmeticNthDayOfMonth : {rule : PersianArithmeticRule} ->
 855 |   DayNth -> DayOfWeek ->
 856 |   PersianMonth -> Year -> DayOfMonth
 857 | arithmeticNthDayOfMonth {rule} nth target valueMonth valueYear =
 858 |   let monthLength = maxArithmeticDaysInMonth {rule} valueMonth valueYear
 859 |       firstOffset = (weekdayNumber target -
 860 |         weekdayNumber (weekdayFromDays
 861 |           (arithmeticDaysFromCivil {rule} valueYear valueMonth 1)))
 862 |             `mod` daysPerWeek
 863 |       lastOffset = (weekdayNumber (weekdayFromDays
 864 |         (arithmeticDaysFromCivil {rule}
 865 |           valueYear valueMonth monthLength)) -
 866 |         weekdayNumber target) `mod` daysPerWeek
 867 |       dayNumber = nthWeekdayDayNumber nth (dayOfMonthValue monthLength)
 868 |         firstOffset lastOffset
 869 |    in dayOfMonthFromInteger dayNumber
 870 | 
 871 | public export
 872 | isValidArithmeticNthDay : {rule : PersianArithmeticRule} ->
 873 |   DayNth -> DayOfWeek ->
 874 |   PersianMonth -> Year -> Bool
 875 | isValidArithmeticNthDay {rule} nth target valueMonth valueYear =
 876 |   yearValue valueYear >= minimumArithmeticYear &&
 877 |   yearValue valueYear <= maximumArithmeticYear && case nth of
 878 |     Fifth => arithmeticNthDayOfMonth {rule}
 879 |       nth target valueMonth valueYear <=
 880 |       maxArithmeticDaysInMonth {rule} valueMonth valueYear
 881 |     _ => True
 882 | 
 883 | ||| Construct an nth weekday under a selected arithmetic Persian rule.
 884 | public export
 885 | arithmeticFromNthDay : {rule : PersianArithmeticRule} ->
 886 |   (nth : DayNth) -> (target : DayOfWeek) ->
 887 |   (valueMonth : PersianMonth) -> (valueYear : Year) ->
 888 |   {auto 0 valid : So
 889 |     (isValidArithmeticNthDay {rule}
 890 |       nth target valueMonth valueYear)} ->
 891 |   CalendarDate (ArithmeticPersian rule)
 892 | arithmeticFromNthDay {rule} nth target valueMonth valueYear =
 893 |   makeArithmeticPersianDate {rule} (arithmeticDaysFromCivil {rule}
 894 |     valueYear valueMonth
 895 |     (arithmeticNthDayOfMonth {rule} nth target valueMonth valueYear))
 896 | 
 897 | ||| Validate an nth-weekday request under an arithmetic Persian rule.
 898 | public export
 899 | refineArithmeticNthDay : {rule : PersianArithmeticRule} ->
 900 |   DayNth -> DayOfWeek ->
 901 |   PersianMonth -> Year ->
 902 |   Either PersianDateError (CalendarDate (ArithmeticPersian rule))
 903 | refineArithmeticNthDay {rule} nth target valueMonth valueYear =
 904 |   case choose (isValidArithmeticNthDay {rule}
 905 |     nth target valueMonth valueYear) of
 906 |       Left valid => Right (arithmeticFromNthDay {rule}
 907 |         nth target valueMonth valueYear {valid = valid})
 908 |       Right _ => Left (InvalidPersianNthDay nth target valueMonth valueYear)
 909 | 
 910 | arithmeticWeekDateDays : {rule : PersianArithmeticRule} ->
 911 |   WeekNumber -> DayOfWeek ->
 912 |   Year -> Integer
 913 | arithmeticWeekDateDays {rule} week target valueYear =
 914 |   let firstDay = arithmeticDaysFromCivil {rule}
 915 |         valueYear PersianMonths.Farvardin 1
 916 |       firstWeekStart = firstDay -
 917 |         ((weekdayNumber (weekdayFromDays firstDay) - 6)
 918 |           `mod` 7)
 919 |       targetOffset = (weekdayNumber target - 6) `mod` 7
 920 |    in firstWeekStart + 7 * (weekNumberValue week - 1) + targetOffset
 921 | 
 922 | public export
 923 | isValidArithmeticWeekDate : {rule : PersianArithmeticRule} ->
 924 |   WeekNumber -> DayOfWeek ->
 925 |   Year -> Bool
 926 | isValidArithmeticWeekDate {rule} week target valueYear =
 927 |   let days = arithmeticWeekDateDays {rule} week target valueYear
 928 |    in yearValue valueYear >= minimumArithmeticYear &&
 929 |       yearValue valueYear <= maximumArithmeticYear &&
 930 |       IotaTime.Calendar.isValidDays
 931 |         {calendar = ArithmeticPersian rule} days
 932 | 
 933 | ||| Construct a Saturday-based week date under an arithmetic Persian rule.
 934 | public export
 935 | arithmeticFromWeekDate : {rule : PersianArithmeticRule} ->
 936 |   (week : WeekNumber) -> (target : DayOfWeek) -> (valueYear : Year) ->
 937 |   {auto 0 valid : So
 938 |     (isValidArithmeticWeekDate {rule} week target valueYear)} ->
 939 |   CalendarDate (ArithmeticPersian rule)
 940 | arithmeticFromWeekDate {rule} week target valueYear =
 941 |   makeArithmeticPersianDate {rule}
 942 |     (arithmeticWeekDateDays {rule} week target valueYear)
 943 | 
 944 | ||| Validate a Saturday-based week date under an arithmetic Persian rule.
 945 | public export
 946 | refineArithmeticWeekDate : {rule : PersianArithmeticRule} ->
 947 |   WeekNumber -> DayOfWeek -> Year ->
 948 |   Either PersianDateError (CalendarDate (ArithmeticPersian rule))
 949 | refineArithmeticWeekDate {rule} week target valueYear =
 950 |   case choose (isValidArithmeticWeekDate {rule}
 951 |     week target valueYear) of
 952 |       Left valid => Right (arithmeticFromWeekDate {rule}
 953 |         week target valueYear {valid = valid})
 954 |       Right _ => Left (InvalidPersianWeekDate week target valueYear)
 955 |