
   0 | module IotaTime.Calendar.Islamic
   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 | %hide Language.Reflection.Types.ParamTypeInfo.pattern
  11 | 
  12 | %default total
  13 | 
  14 | ||| The supported tabular Islamic 30-year leap-cycle assignments.
  15 | public export
  16 | data IslamicLeapPattern = Base15 | Base16 | Indian | HabashAlHasib
  17 | 
  18 | ||| Evidence and leap-year positions for one Islamic leap pattern.
  19 | public export
  20 | interface KnownIslamicLeapPattern (pattern : IslamicLeapPattern) where
  21 |   leapCycleYears : List Integer
  22 | 
  23 | public export
  24 | KnownIslamicLeapPattern Base15 where
  25 |   leapCycleYears = [2, 5, 7, 10, 13, 15, 18, 21, 24, 26, 29]
  26 | 
  27 | public export
  28 | KnownIslamicLeapPattern Base16 where
  29 |   leapCycleYears = [2, 5, 7, 10, 13, 16, 18, 21, 24, 26, 29]
  30 | 
  31 | public export
  32 | KnownIslamicLeapPattern Indian where
  33 |   leapCycleYears = [2, 5, 8, 10, 13, 16, 19, 21, 24, 27, 29]
  34 | 
  35 | public export
  36 | KnownIslamicLeapPattern HabashAlHasib where
  37 |   leapCycleYears = [2, 5, 8, 11, 13, 16, 19, 21, 24, 27, 0]
  38 | 
  39 | ||| The two conventional epochs used by tabular Islamic calendars.
  40 | public export
  41 | data IslamicEpoch = Astronomical | Civil
  42 | 
  43 | ||| Evidence for the first timeline day represented by an Islamic epoch.
  44 | public export
  45 | interface KnownIslamicEpoch (epoch : IslamicEpoch) where
  46 |   epochDay : Integer
  47 |   dateConstructorName : String
  48 | 
  49 | public export
  50 | KnownIslamicEpoch Astronomical where
  51 |   epochDay = -503166
  52 |   dateConstructorName = "calendarDate'"
  53 | 
  54 | public export
  55 | KnownIslamicEpoch Civil where
  56 |   epochDay = -503165
  57 |   dateConstructorName = "civilCalendarDate'"
  58 | 
  59 | islamicEpochDay : IslamicEpoch -> Integer
  60 | islamicEpochDay Astronomical = -503166
  61 | islamicEpochDay Civil = -503165
  62 | 
  63 | ||| A tabular Islamic calendar indexed by its epoch and leap-cycle pattern.
  64 | public export
  65 | data IslamicByEpoch : IslamicEpoch -> IslamicLeapPattern -> Type where
  66 |   IslamicCalendar : IslamicByEpoch epoch pattern
  67 | 
  68 | ||| The astronomical-epoch calendar retained by the original iotaTime API.
  69 | public export
  70 | Islamic : IslamicLeapPattern -> Type
  71 | Islamic = IslamicByEpoch Astronomical
  72 | 
  73 | ||| A civil-epoch tabular Islamic calendar.
  74 | public export
  75 | CivilIslamic : IslamicLeapPattern -> Type
  76 | CivilIslamic = IslamicByEpoch Civil
  77 | 
  78 | public export
  79 | IslamicBase15 : Type
  80 | IslamicBase15 = Islamic Base15
  81 | 
  82 | public export
  83 | IslamicBase16 : Type
  84 | IslamicBase16 = Islamic Base16
  85 | 
  86 | public export
  87 | IslamicIndian : Type
  88 | IslamicIndian = Islamic Indian
  89 | 
  90 | public export
  91 | IslamicHabashAlHasib : Type
  92 | IslamicHabashAlHasib = Islamic HabashAlHasib
  93 | 
  94 | public export
  95 | IslamicBcl : Type
  96 | IslamicBcl = IslamicBase16
  97 | 
  98 | public export
  99 | CivilIslamicBase15 : Type
 100 | CivilIslamicBase15 = CivilIslamic Base15
 101 | 
 102 | public export
 103 | CivilIslamicBase16 : Type
 104 | CivilIslamicBase16 = CivilIslamic Base16
 105 | 
 106 | public export
 107 | CivilIslamicIndian : Type
 108 | CivilIslamicIndian = CivilIslamic Indian
 109 | 
 110 | public export
 111 | CivilIslamicHabashAlHasib : Type
 112 | CivilIslamicHabashAlHasib = CivilIslamic HabashAlHasib
 113 | 
 114 | public export
 115 | CivilIslamicBcl : Type
 116 | CivilIslamicBcl = CivilIslamicBase16
 117 | 
 118 | namespace IslamicMonths
 119 |   public export
 120 |   data IslamicMonth
 121 |     = Muharram | Safar | RabiAlAwwal | RabiAlThani
 122 |     | JumadaAlAwwal | JumadaAlThani | Rajab | Shaban
 123 |     | Ramadan | Shawwal | DhulQadah | DhulHijjah
 124 | 
 125 |   public export
 126 |   monthNumber : IslamicMonth -> Integer
 127 |   monthNumber Muharram = 1
 128 |   monthNumber Safar = 2
 129 |   monthNumber RabiAlAwwal = 3
 130 |   monthNumber RabiAlThani = 4
 131 |   monthNumber JumadaAlAwwal = 5
 132 |   monthNumber JumadaAlThani = 6
 133 |   monthNumber Rajab = 7
 134 |   monthNumber Shaban = 8
 135 |   monthNumber Ramadan = 9
 136 |   monthNumber Shawwal = 10
 137 |   monthNumber DhulQadah = 11
 138 |   monthNumber DhulHijjah = 12
 139 | 
 140 |   public export
 141 |   Eq IslamicMonth where
 142 |     left == right = monthNumber left == monthNumber right
 143 | 
 144 |   public export
 145 |   Ord IslamicMonth where
 146 |     compare left right = compare (monthNumber left) (monthNumber right)
 147 | 
 148 |   %runElab derive `{IslamicMonth} [Show]
 149 | 
 150 | monthFromNumber : Integer -> IslamicMonth
 151 | monthFromNumber 1 = IslamicMonths.Muharram
 152 | monthFromNumber 2 = IslamicMonths.Safar
 153 | monthFromNumber 3 = IslamicMonths.RabiAlAwwal
 154 | monthFromNumber 4 = IslamicMonths.RabiAlThani
 155 | monthFromNumber 5 = IslamicMonths.JumadaAlAwwal
 156 | monthFromNumber 6 = IslamicMonths.JumadaAlThani
 157 | monthFromNumber 7 = IslamicMonths.Rajab
 158 | monthFromNumber 8 = IslamicMonths.Shaban
 159 | monthFromNumber 9 = IslamicMonths.Ramadan
 160 | monthFromNumber 10 = IslamicMonths.Shawwal
 161 | monthFromNumber 11 = IslamicMonths.DhulQadah
 162 | monthFromNumber _ = IslamicMonths.DhulHijjah
 163 | 
 164 | islamicWeekdayFromDays : Integer -> DayOfWeek
 165 | islamicWeekdayFromDays value = weekdayFromNumber (value + 3)
 166 | 
 167 | export
 168 | record IslamicDate (epoch : IslamicEpoch) (pattern : IslamicLeapPattern) where
 169 |   constructor MkIslamicDate
 170 |   daysSinceEpoch : Integer
 171 |   0 validDays : So (daysSinceEpoch >= islamicEpochDay epoch)
 172 | 
 173 | public export
 174 | Eq (IslamicDate epoch pattern) where
 175 |   left == right = left.daysSinceEpoch == right.daysSinceEpoch
 176 | 
 177 | public export
 178 | Ord (IslamicDate epoch pattern) where
 179 |   compare left right = compare left.daysSinceEpoch right.daysSinceEpoch
 180 | 
 181 | public export
 182 | isLeapYear : {pattern : IslamicLeapPattern} ->
 183 |                     KnownIslamicLeapPattern pattern => Year -> Bool
 184 | isLeapYear value =
 185 |   let cycleYear = yearValue value `mod` 30
 186 |    in elem cycleYear (leapCycleYears {pattern})
 187 | 
 188 | countCycleLeaps : Integer -> List Integer -> Integer
 189 | countCycleLeaps _ [] = 0
 190 | countCycleLeaps years (position :: rest) =
 191 |   (if position > 0 && position <= years then 1 else 0) +
 192 |   countCycleLeaps years rest
 193 | 
 194 | leapsBeforeIslamicYear : {pattern : IslamicLeapPattern} ->
 195 |                          KnownIslamicLeapPattern pattern => Year -> Integer
 196 | leapsBeforeIslamicYear value =
 197 |   let priorYears = yearValue value - 1
 198 |       cycles = priorYears `div` 30
 199 |       yearsInCycle = priorYears `mod` 30
 200 |    in cycles * 11 + countCycleLeaps yearsInCycle (leapCycleYears {pattern})
 201 | 
 202 | public export
 203 | maxDaysInMonth : {pattern : IslamicLeapPattern} ->
 204 |                         KnownIslamicLeapPattern pattern =>
 205 |                         IslamicMonth -> Year -> DayOfMonth
 206 | maxDaysInMonth IslamicMonths.DhulHijjah value =
 207 |   if isLeapYear {pattern} value then 30 else 29
 208 | maxDaysInMonth valueMonth _ =
 209 |   if IslamicMonths.monthNumber valueMonth `mod` 2 == 1 then 30 else 29
 210 | 
 211 | public export
 212 | isValidDate : {pattern : IslamicLeapPattern} ->
 213 |                      KnownIslamicLeapPattern pattern =>
 214 |                      DayOfMonth -> IslamicMonth -> Year -> Bool
 215 | isValidDate valueDay valueMonth valueYear =
 216 |   let dayNumber = dayOfMonthValue valueDay
 217 |       maxDay = dayOfMonthValue
 218 |         (maxDaysInMonth {pattern} valueMonth valueYear)
 219 |    in dayNumber >= 1 && dayNumber <= maxDay && yearValue valueYear >= 1
 220 | 
 221 | monthOffset : IslamicMonth -> Integer
 222 | monthOffset value = ((IslamicMonths.monthNumber value - 1) * 59 + 1) `div` 2
 223 | 
 224 | islamicDaysFromCivil : {epoch : IslamicEpoch} ->
 225 |                        {pattern : IslamicLeapPattern} ->
 226 |                        KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 227 |                        Year -> IslamicMonth -> DayOfMonth -> Integer
 228 | islamicDaysFromCivil valueYear valueMonth valueDay =
 229 |   epochDay {epoch} + (yearValue valueYear - 1) * 354 +
 230 |     leapsBeforeIslamicYear {pattern} valueYear + monthOffset valueMonth +
 231 |     dayOfMonthValue valueDay - 1
 232 | 
 233 | islamicYearLength : {pattern : IslamicLeapPattern} ->
 234 |                     KnownIslamicLeapPattern pattern => Integer -> Integer
 235 | islamicYearLength cycleYear =
 236 |   if elem (cycleYear `mod` 30) (leapCycleYears {pattern}) then 355 else 354
 237 | 
 238 | findIslamicYear : {pattern : IslamicLeapPattern} ->
 239 |                   KnownIslamicLeapPattern pattern =>
 240 |       Nat -> Integer -> Integer -> (Integer, Integer)
 241 | findIslamicYear Z cycleYear remaining = (cycleYear, remaining)
 242 | findIslamicYear (S fuel) cycleYear remaining =
 243 |   let length = islamicYearLength {pattern} (cycleYear + 1)
 244 |    in if remaining < length
 245 |         then (cycleYear, remaining)
 246 |   else findIslamicYear {pattern} fuel (cycleYear + 1) (remaining - length)
 247 | 
 248 | islamicCivilFromDays : {epoch : IslamicEpoch} ->
 249 |                        {pattern : IslamicLeapPattern} ->
 250 |                        KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 251 |                        Integer -> (Year, IslamicMonth, DayOfMonth)
 252 | islamicCivilFromDays value =
 253 |   let relative = value - epochDay {epoch}
 254 |       cycles = relative `div` 10631
 255 |       remaining = relative `mod` 10631
 256 |       (yearInCycle, dayOfYear) = findIslamicYear {pattern} 30 0 remaining
 257 |       yearNumber = cycles * 30 + yearInCycle + 1
 258 |       monthNumber = if dayOfYear == 354 then 12 else dayOfYear * 2 `div` 59 + 1
 259 |       offset = ((monthNumber - 1) * 59 + 1) `div` 2
 260 |       dayNumber = dayOfYear - offset + 1
 261 |    in (yearFromInteger yearNumber, monthFromNumber monthNumber,
 262 |        dayOfMonthFromInteger dayNumber)
 263 | 
 264 | checkedIslamicDate : {epoch : IslamicEpoch} ->
 265 |                      {pattern : IslamicLeapPattern} ->
 266 |                      (days : Integer) ->
 267 |                      (0 valid : So (days >= islamicEpochDay epoch)) ->
 268 |                      IslamicDate epoch pattern
 269 | checkedIslamicDate days valid = MkIslamicDate days valid
 270 | 
 271 | fromIslamicDays : {epoch : IslamicEpoch} ->
 272 |                   {pattern : IslamicLeapPattern} ->
 273 |                   (days : Integer) ->
 274 |                   {auto 0 valid : So (days >= islamicEpochDay epoch)} ->
 275 |                   IslamicDate epoch pattern
 276 | fromIslamicDays days @{valid} = checkedIslamicDate days valid
 277 | 
 278 | export
 279 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 280 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 281 |   HasCalendarBridge (IslamicDate epoch pattern) where
 282 |   toBridgeDays = daysSinceEpoch
 283 |   acceptsBridgeDays = (>= islamicEpochDay epoch)
 284 |   fromBridgeDays = fromIslamicDays {epoch} {pattern}
 285 |   bridgeCalendarName = "Islamic"
 286 | 
 287 | makeIslamicDate : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 288 |                   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 289 |                   Integer -> IslamicDate epoch pattern
 290 | makeIslamicDate {epoch} days =
 291 |   let clamped = max (islamicEpochDay epoch) days
 292 |    in case choose (clamped >= islamicEpochDay epoch) of
 293 |         Left valid => checkedIslamicDate clamped valid
 294 |         Right _ => case epoch of
 295 |           Astronomical => checkedIslamicDate (-503166) Oh
 296 |           Civil => checkedIslamicDate (-503165) Oh
 297 | 
 298 | clampToIslamic : {epoch : IslamicEpoch} -> KnownIslamicEpoch epoch =>
 299 |                  Integer -> Integer
 300 | clampToIslamic {epoch} = max (islamicEpochDay epoch)
 301 | 
 302 | shiftIslamicDays : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 303 |                    KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 304 |                    Integer -> IslamicDate epoch pattern -> IslamicDate epoch pattern
 305 | shiftIslamicDays amount date =
 306 |   makeIslamicDate {epoch} {pattern}
 307 |     (clampToIslamic {epoch} (date.daysSinceEpoch + amount))
 308 | 
 309 | shiftIslamicMonths : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 310 |                      KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 311 |                      Integer -> IslamicDate epoch pattern -> IslamicDate epoch pattern
 312 | shiftIslamicMonths amount date =
 313 |   let (valueYear, valueMonth, valueDay) =
 314 |       islamicCivilFromDays {epoch} {pattern} date.daysSinceEpoch
 315 |       monthOrdinal = IslamicMonths.monthNumber valueMonth - 1 + amount
 316 |       targetYear = yearFromInteger
 317 |         (yearValue valueYear + monthOrdinal `div` 12)
 318 |       targetMonth = monthFromNumber (monthOrdinal `mod` 12 + 1)
 319 |       targetDay = min valueDay
 320 |         (maxDaysInMonth {pattern} targetMonth targetYear)
 321 |    in makeIslamicDate {epoch} {pattern}
 322 |         (clampToIslamic {epoch}
 323 |           (islamicDaysFromCivil {epoch} {pattern}
 324 |             targetYear targetMonth targetDay))
 325 | 
 326 | shiftIslamicYears : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 327 |                     KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 328 |                     Integer -> IslamicDate epoch pattern -> IslamicDate epoch pattern
 329 | shiftIslamicYears amount date =
 330 |   let (valueYear, valueMonth, valueDay) =
 331 |       islamicCivilFromDays {epoch} {pattern} date.daysSinceEpoch
 332 |       targetYear = yearFromInteger (yearValue valueYear + amount)
 333 |       targetDay = min valueDay
 334 |         (maxDaysInMonth {pattern} valueMonth targetYear)
 335 |    in makeIslamicDate {epoch} {pattern}
 336 |         (clampToIslamic {epoch}
 337 |           (islamicDaysFromCivil {epoch} {pattern}
 338 |             targetYear valueMonth targetDay))
 339 | 
 340 | applyIslamicPeriod : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 341 |                      KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 342 |                      Period target -> IslamicDate epoch pattern -> IslamicDate epoch pattern
 343 | applyIslamicPeriod {epoch} {pattern} = applyDatePeriodWith
 344 |   (shiftIslamicYears {epoch} {pattern})
 345 |   (shiftIslamicMonths {epoch} {pattern})
 346 |   (shiftIslamicDays {epoch} {pattern})
 347 | 
 348 | islamicDayOfWeek : IslamicDate epoch pattern -> DayOfWeek
 349 | islamicDayOfWeek date = islamicWeekdayFromDays date.daysSinceEpoch
 350 | 
 351 | nextIslamic : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 352 |               KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 353 |               Integer -> DayOfWeek -> IslamicDate epoch pattern ->
 354 |               IslamicDate epoch pattern
 355 | nextIslamic count target date =
 356 |   makeIslamicDate {epoch} {pattern} (clampToIslamic {epoch}
 357 |     (date.daysSinceEpoch +
 358 |       nextWeekdayOffset count (islamicDayOfWeek date) target))
 359 | 
 360 | previousIslamic : {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 361 |                   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 362 |                   Integer -> DayOfWeek -> IslamicDate epoch pattern ->
 363 |                   IslamicDate epoch pattern
 364 | previousIslamic count target date =
 365 |   makeIslamicDate {epoch} {pattern} (clampToIslamic {epoch}
 366 |     (date.daysSinceEpoch +
 367 |       previousWeekdayOffset count (islamicDayOfWeek date) target))
 368 | 
 369 | public export
 370 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 371 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 372 |   Calendar (IslamicByEpoch epoch pattern) where
 373 |   DateRep = IslamicDate epoch pattern
 374 |   MonthRep _ = IslamicMonth
 375 | 
 376 |   isValidDays = (>= islamicEpochDay epoch)
 377 |   fromDays = fromIslamicDays {epoch} {pattern}
 378 |   toDaysFor date = date.daysSinceEpoch
 379 |   toDaysValid (MkIslamicDate _ valid) = valid
 380 |   toFromDays _ _ = Refl
 381 |   fromToDays (MkIslamicDate _ _) = Refl
 382 |   calendarName = "Islamic"
 383 | 
 384 |   year' date = let (value, _, _) =
 385 |                     islamicCivilFromDays {epoch} {pattern}
 386 |                       date.daysSinceEpoch in value
 387 |   toYmd date = let (_, valueMonth, valueDay) =
 388 |                     islamicCivilFromDays {epoch} {pattern} date.daysSinceEpoch
 389 |                 in (valueMonth, valueDay)
 390 |   day' date = let (_, _, value) =
 391 |                    islamicCivilFromDays {epoch} {pattern}
 392 |                      date.daysSinceEpoch in value
 393 |   month' date = let (_, value, _) =
 394 |                      islamicCivilFromDays {epoch} {pattern}
 395 |                        date.daysSinceEpoch in value
 396 | 
 397 |   applyCalendarPeriod' = applyIslamicPeriod {epoch} {pattern}
 398 |   shiftCalendarDays' = shiftIslamicDays {epoch} {pattern}
 399 | 
 400 |   dayOfWeekFor = islamicDayOfWeek
 401 |   nextFor = nextIslamic {epoch} {pattern}
 402 |   previousFor = previousIslamic {epoch} {pattern}
 403 | 
 404 | public export
 405 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 406 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 407 |   Show (IslamicDate epoch pattern) where
 408 |   show date = case islamicCivilFromDays {epoch} {pattern}
 409 |     date.daysSinceEpoch of
 410 |     (valueYear, valueMonth, valueDay) =>
 411 |       dateConstructorName {epoch} ++ " " ++ show valueDay ++ " " ++
 412 |       show valueMonth ++ " " ++ show valueYear
 413 | 
 414 | public export
 415 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 416 |   HasCalendar (IslamicDate epoch pattern) where
 417 |   calendarCapability = ()
 418 | 
 419 | public export
 420 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 421 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 422 |   PeriodTarget (IslamicDate epoch pattern) where
 423 |   periodTarget = ()
 424 | 
 425 | public export
 426 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 427 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 428 |   ApplyPeriod (IslamicDate epoch pattern) where
 429 |   applyPeriod = applyIslamicPeriod {epoch} {pattern}
 430 | 
 431 | public export
 432 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 433 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 434 |   CalendarValue (IslamicDate epoch pattern) where
 435 |   CalendarMonth _ = IslamicMonth
 436 |   calendarValueToDays = toDaysFor {calendar = IslamicByEpoch epoch pattern}
 437 |   calendarValueYear = yearFor {calendar = IslamicByEpoch epoch pattern}
 438 |   calendarValueMonthDay = toYmd {calendar = IslamicByEpoch epoch pattern}
 439 |   calendarValueDayOfWeek =
 440 |     dayOfWeekFor {calendar = IslamicByEpoch epoch pattern}
 441 |   calendarValueBetweenWith =
 442 |     betweenWithFor {calendar = IslamicByEpoch epoch pattern}
 443 | 
 444 | public export
 445 | {epoch : IslamicEpoch} -> {pattern : IslamicLeapPattern} ->
 446 |   KnownIslamicEpoch epoch => KnownIslamicLeapPattern pattern =>
 447 |   CalendarNavigation (IslamicDate epoch pattern) where
 448 |   calendarValueNext = nextFor {calendar = IslamicByEpoch epoch pattern}
 449 |   calendarValuePrevious = previousFor {calendar = IslamicByEpoch epoch pattern}
 450 | 
 451 | ||| Construct a statically validated Islamic date for the selected leap pattern.
 452 | public export
 453 | calendarDate' : {pattern : IslamicLeapPattern} ->
 454 |                {auto known : KnownIslamicLeapPattern pattern} ->
 455 |                (valueDay : DayOfMonth) -> (valueMonth : IslamicMonth) ->
 456 |                (valueYear : Year) ->
 457 |                {auto 0 valid : So
 458 |                  (isValidDate {pattern} valueDay valueMonth valueYear)} ->
 459 |                CalendarDate (Islamic pattern)
 460 | calendarDate' valueDay valueMonth valueYear =
 461 |   makeIslamicDate {epoch = Astronomical} {pattern}
 462 |     (islamicDaysFromCivil {epoch = Astronomical} {pattern}
 463 |       valueYear valueMonth valueDay)
 464 | 
 465 | ||| Construct a statically validated Base16/BCL Islamic date.
 466 | public export
 467 | calendarDate : (valueDay : DayOfMonth) -> (valueMonth : IslamicMonth) ->
 468 |               (valueYear : Year) ->
 469 |               {auto 0 valid : So
 470 |                 (isValidDate {pattern = Base16}
 471 |                   valueDay valueMonth valueYear)} ->
 472 |               CalendarDate IslamicBcl
 473 | calendarDate = calendarDate' {pattern = Base16}
 474 | 
 475 | ||| Failures produced while refining untrusted Islamic date data.
 476 | public export
 477 | data IslamicDateError
 478 |   = InvalidIslamicDate DayOfMonth IslamicMonth Year
 479 |   | InvalidIslamicDayCount Integer
 480 |   | InvalidIslamicNthDay DayNth DayOfWeek IslamicMonth Year
 481 |   | InvalidIslamicWeekDate WeekNumber DayOfWeek Year
 482 | 
 483 | ||| Validate runtime date components for the selected Islamic leap pattern.
 484 | public export
 485 | refineDate' : {pattern : IslamicLeapPattern} ->
 486 |                      {auto known : KnownIslamicLeapPattern pattern} ->
 487 |                      DayOfMonth -> IslamicMonth -> Year ->
 488 |                      Either IslamicDateError (CalendarDate (Islamic pattern))
 489 | refineDate' @{known} valueDay valueMonth valueYear =
 490 |   case choose (isValidDate {pattern} valueDay valueMonth valueYear) of
 491 |     Left valid => Right
 492 |       (calendarDate' {pattern} @{known}
 493 |         valueDay valueMonth valueYear @{valid})
 494 |     Right _ => Left (InvalidIslamicDate valueDay valueMonth valueYear)
 495 | 
 496 | ||| Validate runtime date components using the Base16/BCL leap pattern.
 497 | public export
 498 | refineDate : DayOfMonth -> IslamicMonth -> Year ->
 499 |                     Either IslamicDateError (CalendarDate IslamicBcl)
 500 | refineDate = refineDate' {pattern = Base16}
 501 | 
 502 | ||| Construct a date in the selected Islamic pattern from a statically valid
 503 | ||| calendar-relative day count.
 504 | public export
 505 | fromDays' : {pattern : IslamicLeapPattern} ->
 506 |                    {auto known : KnownIslamicLeapPattern pattern} ->
 507 |                    (days : Integer) ->
 508 |                    {auto 0 valid : So
 509 |                      (IotaTime.Calendar.isValidDays
 510 |                        {calendar = Islamic pattern} days)} ->
 511 |                    CalendarDate (Islamic pattern)
 512 | fromDays' {pattern} = fromIslamicDays {epoch = Astronomical} {pattern}
 513 | 
 514 | public export
 515 | fromDays : (days : Integer) ->
 516 |                   {auto 0 valid : So
 517 |                     (IotaTime.Calendar.isValidDays
 518 |                       {calendar = IslamicBcl} days)} ->
 519 |                   CalendarDate IslamicBcl
 520 | fromDays = fromDays' {pattern = Base16}
 521 | 
 522 | ||| Validate a runtime day count for the selected Islamic leap pattern.
 523 | public export
 524 | refineDays' : {pattern : IslamicLeapPattern} ->
 525 |                      {auto known : KnownIslamicLeapPattern pattern} ->
 526 |                      Integer -> Either IslamicDateError
 527 |                        (CalendarDate (Islamic pattern))
 528 | refineDays' @{known} days = case choose
 529 |   (IotaTime.Calendar.isValidDays {calendar = Islamic pattern} days) of
 530 |   Left valid => Right (fromDays' {pattern} @{known} days @{valid})
 531 |   Right _ => Left (InvalidIslamicDayCount days)
 532 | 
 533 | public export
 534 | refineDays : Integer -> Either IslamicDateError
 535 |                       (CalendarDate IslamicBcl)
 536 | refineDays = refineDays' {pattern = Base16}
 537 | 
 538 | ||| Construct a statically validated civil-epoch Islamic date for the selected
 539 | ||| leap pattern.
 540 | public export
 541 | civilCalendarDate' : {pattern : IslamicLeapPattern} ->
 542 |                     {auto known : KnownIslamicLeapPattern pattern} ->
 543 |                     (valueDay : DayOfMonth) ->
 544 |                     (valueMonth : IslamicMonth) -> (valueYear : Year) ->
 545 |                     {auto 0 valid : So
 546 |                       (isValidDate {pattern}
 547 |                         valueDay valueMonth valueYear)} ->
 548 |                     CalendarDate (CivilIslamic pattern)
 549 | civilCalendarDate' valueDay valueMonth valueYear =
 550 |   makeIslamicDate {epoch = Civil} {pattern}
 551 |     (islamicDaysFromCivil {epoch = Civil} {pattern}
 552 |       valueYear valueMonth valueDay)
 553 | 
 554 | ||| Construct a statically validated Base16 civil-epoch Islamic date.
 555 | public export
 556 | civilCalendarDate : (valueDay : DayOfMonth) ->
 557 |                    (valueMonth : IslamicMonth) -> (valueYear : Year) ->
 558 |                    {auto 0 valid : So
 559 |                      (isValidDate {pattern = Base16}
 560 |                        valueDay valueMonth valueYear)} ->
 561 |                    CalendarDate CivilIslamicBcl
 562 | civilCalendarDate = civilCalendarDate' {pattern = Base16}
 563 | 
 564 | ||| Validate runtime date components for a selected civil-epoch leap pattern.
 565 | public export
 566 | refineCivilDate' : {pattern : IslamicLeapPattern} ->
 567 |                           {auto known : KnownIslamicLeapPattern pattern} ->
 568 |                           DayOfMonth -> IslamicMonth -> Year ->
 569 |                           Either IslamicDateError
 570 |                             (CalendarDate (CivilIslamic pattern))
 571 | refineCivilDate' @{known} valueDay valueMonth valueYear =
 572 |   case choose (isValidDate {pattern}
 573 |     valueDay valueMonth valueYear) of
 574 |       Left valid => Right (civilCalendarDate' {pattern} @{known}
 575 |         valueDay valueMonth valueYear @{valid})
 576 |       Right _ => Left (InvalidIslamicDate valueDay valueMonth valueYear)
 577 | 
 578 | ||| Validate runtime civil-epoch date components using the Base16 pattern.
 579 | public export
 580 | refineCivilDate : DayOfMonth -> IslamicMonth -> Year ->
 581 |                          Either IslamicDateError
 582 |                            (CalendarDate CivilIslamicBcl)
 583 | refineCivilDate = refineCivilDate' {pattern = Base16}
 584 | 
 585 | ||| Construct a civil-epoch date from a statically valid timeline day count.
 586 | public export
 587 | civilFromDays' : {pattern : IslamicLeapPattern} ->
 588 |                         {auto known : KnownIslamicLeapPattern pattern} ->
 589 |                         (days : Integer) ->
 590 |                         {auto 0 valid : So
 591 |                           (IotaTime.Calendar.isValidDays
 592 |                             {calendar = CivilIslamic pattern} days)} ->
 593 |                         CalendarDate (CivilIslamic pattern)
 594 | civilFromDays' {pattern} = fromIslamicDays {epoch = Civil} {pattern}
 595 | 
 596 | public export
 597 | civilFromDays : (days : Integer) ->
 598 |                        {auto 0 valid : So
 599 |                          (IotaTime.Calendar.isValidDays
 600 |                            {calendar = CivilIslamicBcl} days)} ->
 601 |                        CalendarDate CivilIslamicBcl
 602 | civilFromDays = civilFromDays' {pattern = Base16}
 603 | 
 604 | ||| Validate a runtime timeline day count for a selected civil leap pattern.
 605 | public export
 606 | refineCivilDays' : {pattern : IslamicLeapPattern} ->
 607 |                           {auto known : KnownIslamicLeapPattern pattern} ->
 608 |                           Integer -> Either IslamicDateError
 609 |                             (CalendarDate (CivilIslamic pattern))
 610 | refineCivilDays' @{known} days =
 611 |   case choose
 612 |     (IotaTime.Calendar.isValidDays
 613 |       {calendar = CivilIslamic pattern} days) of
 614 |     Left valid => Right
 615 |       (civilFromDays' {pattern} @{known} days @{valid})
 616 |     Right _ => Left (InvalidIslamicDayCount days)
 617 | 
 618 | public export
 619 | refineCivilDays : Integer -> Either IslamicDateError
 620 |                            (CalendarDate CivilIslamicBcl)
 621 | refineCivilDays = refineCivilDays' {pattern = Base16}
 622 | 
 623 | nthIslamicDayOfMonthFor : {epoch : IslamicEpoch} ->
 624 |                           {pattern : IslamicLeapPattern} ->
 625 |                           KnownIslamicEpoch epoch =>
 626 |                           KnownIslamicLeapPattern pattern =>
 627 |                           DayNth -> DayOfWeek -> IslamicMonth -> Year ->
 628 |                           DayOfMonth
 629 | nthIslamicDayOfMonthFor nth target valueMonth valueYear =
 630 |   let monthLength = maxDaysInMonth {pattern} valueMonth valueYear
 631 |       firstOffset = (weekdayNumber target -
 632 |         weekdayNumber (islamicWeekdayFromDays
 633 |           (islamicDaysFromCivil {epoch} {pattern}
 634 |             valueYear valueMonth 1))) `mod` daysPerWeek
 635 |       lastOffset = (weekdayNumber (islamicWeekdayFromDays
 636 |         (islamicDaysFromCivil {epoch} {pattern}
 637 |           valueYear valueMonth monthLength)) -
 638 |         weekdayNumber target) `mod` daysPerWeek
 639 |       dayNumber = nthWeekdayDayNumber nth (dayOfMonthValue monthLength)
 640 |         firstOffset lastOffset
 641 |    in dayOfMonthFromInteger dayNumber
 642 | 
 643 | public export
 644 | nthDayOfMonth : {pattern : IslamicLeapPattern} ->
 645 |                        KnownIslamicLeapPattern pattern =>
 646 |                        DayNth -> DayOfWeek -> IslamicMonth -> Year ->
 647 |                        DayOfMonth
 648 | nthDayOfMonth =
 649 |   nthIslamicDayOfMonthFor {epoch = Astronomical} {pattern}
 650 | 
 651 | public export
 652 | civilNthDayOfMonth : {pattern : IslamicLeapPattern} ->
 653 |                             KnownIslamicLeapPattern pattern =>
 654 |                             DayNth -> DayOfWeek -> IslamicMonth ->
 655 |                             Year -> DayOfMonth
 656 | civilNthDayOfMonth =
 657 |   nthIslamicDayOfMonthFor {epoch = Civil} {pattern}
 658 | 
 659 | public export
 660 | isValidNthDay : {pattern : IslamicLeapPattern} ->
 661 |                        KnownIslamicLeapPattern pattern =>
 662 |                        DayNth -> DayOfWeek -> IslamicMonth -> Year -> Bool
 663 | isValidNthDay nth target valueMonth valueYear =
 664 |   yearValue valueYear >= 1 && case nth of
 665 |     Fifth => nthDayOfMonth {pattern} nth target valueMonth valueYear <=
 666 |       maxDaysInMonth {pattern} valueMonth valueYear
 667 |     _ => True
 668 | 
 669 | public export
 670 | isValidCivilNthDay : {pattern : IslamicLeapPattern} ->
 671 |                             KnownIslamicLeapPattern pattern =>
 672 |                             DayNth -> DayOfWeek -> IslamicMonth ->
 673 |                             Year -> Bool
 674 | isValidCivilNthDay nth target valueMonth valueYear =
 675 |   yearValue valueYear >= 1 && case nth of
 676 |     Fifth => civilNthDayOfMonth {pattern}
 677 |       nth target valueMonth valueYear <=
 678 |         maxDaysInMonth {pattern} valueMonth valueYear
 679 |     _ => True
 680 | 
 681 | ||| Construct the nth requested weekday in an Islamic month for the selected
 682 | ||| leap pattern.
 683 | public export
 684 | fromNthDay' : {pattern : IslamicLeapPattern} ->
 685 |                      {auto known : KnownIslamicLeapPattern pattern} ->
 686 |                      (nth : DayNth) -> (target : DayOfWeek) ->
 687 |                      (valueMonth : IslamicMonth) -> (valueYear : Year) ->
 688 |                      {auto 0 valid : So
 689 |                        (isValidNthDay {pattern}
 690 |                          nth target valueMonth valueYear)} ->
 691 |                      CalendarDate (Islamic pattern)
 692 | fromNthDay' nth target valueMonth valueYear =
 693 |   makeIslamicDate {epoch = Astronomical} {pattern}
 694 |     (islamicDaysFromCivil {epoch = Astronomical} {pattern}
 695 |       valueYear valueMonth
 696 |       (nthDayOfMonth {pattern} nth target valueMonth valueYear))
 697 | 
 698 | public export
 699 | fromNthDay : (nth : DayNth) -> (target : DayOfWeek) ->
 700 |                     (valueMonth : IslamicMonth) -> (valueYear : Year) ->
 701 |                     {auto 0 valid : So
 702 |                       (isValidNthDay {pattern = Base16}
 703 |                         nth target valueMonth valueYear)} ->
 704 |                     CalendarDate IslamicBcl
 705 | fromNthDay = fromNthDay' {pattern = Base16}
 706 | 
 707 | ||| Validate an nth-weekday request for the selected Islamic leap pattern.
 708 | public export
 709 | refineNthDay' : {pattern : IslamicLeapPattern} ->
 710 |                        {auto known : KnownIslamicLeapPattern pattern} ->
 711 |                        DayNth -> DayOfWeek -> IslamicMonth -> Year ->
 712 |                        Either IslamicDateError (CalendarDate (Islamic pattern))
 713 | refineNthDay' @{known} nth target valueMonth valueYear =
 714 |   case choose (isValidNthDay {pattern}
 715 |     nth target valueMonth valueYear) of
 716 |       Left valid => Right
 717 |         (fromNthDay' {pattern}
 718 |           @{known} nth target valueMonth valueYear @{valid})
 719 |       Right _ => Left (InvalidIslamicNthDay nth target valueMonth valueYear)
 720 | 
 721 | public export
 722 | refineNthDay : DayNth -> DayOfWeek -> IslamicMonth -> Year ->
 723 |                       Either IslamicDateError (CalendarDate IslamicBcl)
 724 | refineNthDay = refineNthDay' {pattern = Base16}
 725 | 
 726 | ||| Construct the nth requested weekday in a civil-epoch Islamic month.
 727 | public export
 728 | civilFromNthDay' : {pattern : IslamicLeapPattern} ->
 729 |                           {auto known : KnownIslamicLeapPattern pattern} ->
 730 |                           (nth : DayNth) -> (target : DayOfWeek) ->
 731 |                           (valueMonth : IslamicMonth) -> (valueYear : Year) ->
 732 |                           {auto 0 valid : So
 733 |                             (isValidCivilNthDay {pattern}
 734 |                               nth target valueMonth valueYear)} ->
 735 |                           CalendarDate (CivilIslamic pattern)
 736 | civilFromNthDay' nth target valueMonth valueYear =
 737 |   makeIslamicDate {epoch = Civil} {pattern}
 738 |     (islamicDaysFromCivil {epoch = Civil} {pattern}
 739 |       valueYear valueMonth
 740 |       (civilNthDayOfMonth {pattern}
 741 |         nth target valueMonth valueYear))
 742 | 
 743 | public export
 744 | civilFromNthDay : (nth : DayNth) ->
 745 |                          (target : DayOfWeek) ->
 746 |                          (valueMonth : IslamicMonth) -> (valueYear : Year) ->
 747 |                          {auto 0 valid : So
 748 |                            (isValidCivilNthDay {pattern = Base16}
 749 |                              nth target valueMonth valueYear)} ->
 750 |                          CalendarDate CivilIslamicBcl
 751 | civilFromNthDay = civilFromNthDay' {pattern = Base16}
 752 | 
 753 | public export
 754 | refineCivilNthDay' : {pattern : IslamicLeapPattern} ->
 755 |                             {auto known : KnownIslamicLeapPattern pattern} ->
 756 |                             DayNth -> DayOfWeek -> IslamicMonth -> Year ->
 757 |                             Either IslamicDateError
 758 |                               (CalendarDate (CivilIslamic pattern))
 759 | refineCivilNthDay' @{known} nth target valueMonth valueYear =
 760 |   case choose (isValidCivilNthDay {pattern}
 761 |     nth target valueMonth valueYear) of
 762 |       Left valid => Right (civilFromNthDay' {pattern} @{known}
 763 |         nth target valueMonth valueYear @{valid})
 764 |       Right _ => Left
 765 |         (InvalidIslamicNthDay nth target valueMonth valueYear)
 766 | 
 767 | public export
 768 | refineCivilNthDay : DayNth -> DayOfWeek -> IslamicMonth ->
 769 |                            Year -> Either IslamicDateError
 770 |                              (CalendarDate CivilIslamicBcl)
 771 | refineCivilNthDay = refineCivilNthDay' {pattern = Base16}
 772 | 
 773 | islamicWeekDateDaysFor : {epoch : IslamicEpoch} ->
 774 |                          {pattern : IslamicLeapPattern} ->
 775 |                          KnownIslamicEpoch epoch =>
 776 |                          KnownIslamicLeapPattern pattern =>
 777 |                          WeekNumber -> DayOfWeek -> Year -> Integer
 778 | islamicWeekDateDaysFor week target valueYear =
 779 |   let firstDay = islamicDaysFromCivil {epoch} {pattern}
 780 |         valueYear IslamicMonths.Muharram 1
 781 |       firstWeekStart = firstDay -
 782 |         ((weekdayNumber (islamicWeekdayFromDays firstDay) - 6)
 783 |           `mod` 7)
 784 |       targetOffset = (weekdayNumber target - 6) `mod` 7
 785 |    in firstWeekStart + 7 * (weekNumberValue week - 1) + targetOffset
 786 | 
 787 | public export
 788 | weekDateDays : {pattern : IslamicLeapPattern} ->
 789 |                       KnownIslamicLeapPattern pattern =>
 790 |                       WeekNumber -> DayOfWeek -> Year -> Integer
 791 | weekDateDays =
 792 |   islamicWeekDateDaysFor {epoch = Astronomical} {pattern}
 793 | 
 794 | public export
 795 | civilWeekDateDays : {pattern : IslamicLeapPattern} ->
 796 |                            KnownIslamicLeapPattern pattern =>
 797 |                            WeekNumber -> DayOfWeek -> Year -> Integer
 798 | civilWeekDateDays =
 799 |   islamicWeekDateDaysFor {epoch = Civil} {pattern}
 800 | 
 801 | public export
 802 | isValidWeekDate : {pattern : IslamicLeapPattern} ->
 803 |                   KnownIslamicLeapPattern pattern =>
 804 |                   WeekNumber -> DayOfWeek -> Year -> Bool
 805 | isValidWeekDate week target valueYear =
 806 |   (yearValue valueYear > 1 && weekNumberValue week >= 0) ||
 807 |     IotaTime.Calendar.isValidDays {calendar = Islamic pattern}
 808 |       (weekDateDays {pattern} week target valueYear)
 809 | 
 810 | public export
 811 | isValidCivilWeekDate : {pattern : IslamicLeapPattern} ->
 812 |                        KnownIslamicLeapPattern pattern =>
 813 |                        WeekNumber -> DayOfWeek -> Year -> Bool
 814 | isValidCivilWeekDate week target valueYear =
 815 |   (yearValue valueYear > 1 && weekNumberValue week >= 0) ||
 816 |     IotaTime.Calendar.isValidDays {calendar = CivilIslamic pattern}
 817 |       (civilWeekDateDays {pattern} week target valueYear)
 818 | 
 819 | ||| Construct a Saturday-based Islamic week date for the selected leap pattern.
 820 | public export
 821 | fromWeekDate' : {pattern : IslamicLeapPattern} ->
 822 |                 {auto known : KnownIslamicLeapPattern pattern} ->
 823 |                 (week : WeekNumber) -> (target : DayOfWeek) ->
 824 |                 (valueYear : Year) ->
 825 |                 {auto 0 valid : So
 826 |                   (isValidWeekDate {pattern} week target valueYear)} ->
 827 |                 CalendarDate (Islamic pattern)
 828 | fromWeekDate' week target valueYear =
 829 |   makeIslamicDate {epoch = Astronomical} {pattern}
 830 |     (weekDateDays {pattern} week target valueYear)
 831 | 
 832 | public export
 833 | fromWeekDate : (week : WeekNumber) ->
 834 |                (target : DayOfWeek) -> (valueYear : Year) ->
 835 |                {auto 0 valid : So
 836 |                  (isValidWeekDate {pattern = Base16} week target valueYear)} ->
 837 |                CalendarDate IslamicBcl
 838 | fromWeekDate = fromWeekDate' {pattern = Base16}
 839 | 
 840 | ||| Validate a runtime Islamic week date for the selected leap pattern.
 841 | public export
 842 | refineWeekDate' : {pattern : IslamicLeapPattern} ->
 843 |                   {auto known : KnownIslamicLeapPattern pattern} ->
 844 |                   WeekNumber -> DayOfWeek -> Year ->
 845 |                   Either IslamicDateError (CalendarDate (Islamic pattern))
 846 | refineWeekDate' @{known} week target valueYear =
 847 |   case choose (isValidWeekDate {pattern} week target valueYear) of
 848 |     Left valid => Right
 849 |       (fromWeekDate' {pattern} @{known} week target valueYear @{valid})
 850 |     Right _ => Left (InvalidIslamicWeekDate week target valueYear)
 851 | 
 852 | public export
 853 | refineWeekDate : WeekNumber -> DayOfWeek -> Year ->
 854 |                  Either IslamicDateError (CalendarDate IslamicBcl)
 855 | refineWeekDate = refineWeekDate' {pattern = Base16}
 856 | 
 857 | ||| Construct a Saturday-based civil-epoch Islamic week date.
 858 | public export
 859 | civilFromWeekDate' : {pattern : IslamicLeapPattern} ->
 860 |                      {auto known : KnownIslamicLeapPattern pattern} ->
 861 |                      (week : WeekNumber) -> (target : DayOfWeek) ->
 862 |                      (valueYear : Year) ->
 863 |                      {auto 0 valid : So
 864 |                        (isValidCivilWeekDate {pattern} week target valueYear)} ->
 865 |                      CalendarDate (CivilIslamic pattern)
 866 | civilFromWeekDate' week target valueYear =
 867 |   makeIslamicDate {epoch = Civil} {pattern}
 868 |     (civilWeekDateDays {pattern} week target valueYear)
 869 | 
 870 | public export
 871 | civilFromWeekDate : (week : WeekNumber) ->
 872 |                     (target : DayOfWeek) -> (valueYear : Year) ->
 873 |                     {auto 0 valid : So
 874 |                       (isValidCivilWeekDate {pattern = Base16}
 875 |                         week target valueYear)} ->
 876 |                     CalendarDate CivilIslamicBcl
 877 | civilFromWeekDate = civilFromWeekDate' {pattern = Base16}
 878 | 
 879 | public export
 880 | refineCivilWeekDate' : {pattern : IslamicLeapPattern} ->
 881 |                        {auto known : KnownIslamicLeapPattern pattern} ->
 882 |                        WeekNumber -> DayOfWeek -> Year ->
 883 |                        Either IslamicDateError
 884 |                          (CalendarDate (CivilIslamic pattern))
 885 | refineCivilWeekDate' @{known} week target valueYear =
 886 |   case choose (isValidCivilWeekDate {pattern}
 887 |     week target valueYear) of
 888 |       Left valid => Right (civilFromWeekDate' {pattern} @{known}
 889 |         week target valueYear @{valid})
 890 |       Right _ => Left (InvalidIslamicWeekDate week target valueYear)
 891 | 
 892 | public export
 893 | refineCivilWeekDate : WeekNumber -> DayOfWeek -> Year ->
 894 |                       Either IslamicDateError (CalendarDate CivilIslamicBcl)
 895 | refineCivilWeekDate = refineCivilWeekDate' {pattern = Base16}
 896 |