0 | module IotaTime.Calendar.Iso
  1 |
  2 | import public IotaTime.Calendar
  3 | import public IotaTime.Calendar.Gregorian
  4 | import Data.So
  5 |
  6 | %default total
  7 |
  8 | -- Kept inline (not delegated to Internal.Gregorian) so ISO week-date `So`
  9 | -- proofs reduce definitionally across module boundaries.
 10 | public export
 11 | daysFromCivil : Year -> Integer -> Integer -> Integer
 12 | daysFromCivil valueYear valueMonth valueDay =
 13 |   let yearNumber = yearValue valueYear
 14 |       shiftedYear = if valueMonth <= 2 then yearNumber - 1 else yearNumber
 15 |       era = shiftedYear `div` 400
 16 |       yearOfEra = shiftedYear - era * 400
 17 |       shiftedMonth = valueMonth + if valueMonth > 2 then -3 else 9
 18 |       dayOfYear = (153 * shiftedMonth + 2) `div` 5 + valueDay - 1
 19 |       dayOfEra = yearOfEra * 365 + yearOfEra `div` 4 -
 20 |         yearOfEra `div` 100 + dayOfYear
 21 |    in era * 146097 + dayOfEra - 730485
 22 |
 23 | public export
 24 | weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer
 25 | weekDateDays week target valueYear =
 26 |   let januaryFourth = daysFromCivil valueYear 1 4
 27 |       januaryFourthWeekday = (januaryFourth + 3) `mod` 7
 28 |       januaryFourthFromMonday =
 29 |         (januaryFourthWeekday - weekdayNumber Monday) `mod` 7
 30 |       targetFromMonday =
 31 |         (weekdayNumber target - weekdayNumber Monday) `mod` 7
 32 |    in januaryFourth - januaryFourthFromMonday +
 33 |       7 * (weekNumberValue week - 1) + targetFromMonday
 34 |
 35 | ||| Whether an ISO week-numbering year contains week 53.
 36 | public export
 37 | hasFiftyThreeWeeks : Year -> Bool
 38 | hasFiftyThreeWeeks valueYear =
 39 |   let januaryFirstWeekday = (daysFromCivil valueYear 1 1 + 3) `mod` 7
 40 |    in januaryFirstWeekday == weekdayNumber Thursday ||
 41 |       (januaryFirstWeekday == weekdayNumber Wednesday &&
 42 |        IotaTime.Calendar.Gregorian.isLeapYear valueYear)
 43 |
 44 | ||| The number of ISO weeks in a year, either 52 or 53.
 45 | public export
 46 | weeksInIsoYear : Year -> WeekNumber
 47 | weeksInIsoYear valueYear =
 48 |   if hasFiftyThreeWeeks valueYear then 53 else 52
 49 |
 50 | ||| Whether a week number belongs to the requested ISO week-numbering year.
 51 | public export
 52 | isValidIsoWeekNumber : WeekNumber -> Year -> Bool
 53 | isValidIsoWeekNumber week valueYear =
 54 |   let value = weekNumberValue week
 55 |    in value >= 1 &&
 56 |       (value <= 52 || (value == 53 && hasFiftyThreeWeeks valueYear))
 57 |
 58 | ||| Whether an unrestricted arithmetic week coordinate resolves inside the
 59 | ||| supported Gregorian range.
 60 | public export
 61 | isValidArithmeticWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool
 62 | isValidArithmeticWeekDate week target valueYear =
 63 |   IotaTime.Calendar.isValidDays {calendar = Gregorian}
 64 |     (weekDateDays week target valueYear)
 65 |
 66 | ||| Whether a standards-valid ISO week date resolves inside the supported
 67 | ||| Gregorian range.
 68 | public export
 69 | isValidWeekDate : WeekNumber -> DayOfWeek -> Year -> Bool
 70 | isValidWeekDate week target valueYear =
 71 |   isValidIsoWeekNumber week valueYear &&
 72 |   isValidArithmeticWeekDate week target valueYear
 73 |
 74 | 0 andRight : (left, right : Bool) -> So (left && right) -> So right
 75 | andRight True True Oh = Oh
 76 |
 77 | ||| Construct an unrestricted arithmetic ISO week coordinate. Unlike
 78 | ||| `fromWeekDate`, this operation deliberately permits week zero and values
 79 | ||| beyond the requested ISO year.
 80 | public export
 81 | arithmeticFromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) ->
 82 |                          (valueYear : Year) ->
 83 |                          {auto 0 valid : So
 84 |                            (isValidArithmeticWeekDate
 85 |                              week target valueYear)} ->
 86 |                          CalendarDate Gregorian
 87 | arithmeticFromWeekDate week target valueYear =
 88 |   IotaTime.Calendar.Gregorian.fromDays
 89 |     (weekDateDays week target valueYear) @{valid}
 90 |
 91 | ||| Construct a Gregorian date using ISO-8601 week numbering. Weeks start on
 92 | ||| Monday, week 1 contains January 4, and the week must belong to the requested
 93 | ||| ISO week-numbering year.
 94 | public export
 95 | fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) ->
 96 |                (valueYear : Year) ->
 97 |                {auto 0 valid : So
 98 |                  (IotaTime.Calendar.Iso.isValidWeekDate
 99 |                    week target valueYear)} ->
100 |                CalendarDate Gregorian
101 | fromWeekDate week target valueYear @{valid} =
102 |   let 0 arithmeticValid : So
103 |         (isValidArithmeticWeekDate week target valueYear)
104 |       arithmeticValid = andRight
105 |         (isValidIsoWeekNumber week valueYear)
106 |         (isValidArithmeticWeekDate week target valueYear)
107 |         valid
108 |    in arithmeticFromWeekDate week target valueYear @{arithmeticValid}
109 |
110 | public export
111 | data IsoWeekDateError
112 |   = InvalidIsoWeekDate WeekNumber DayOfWeek Year
113 |   | ArithmeticIsoWeekDateOutOfRange WeekNumber DayOfWeek Year
114 |
115 | ||| Validate an ISO week date learned at runtime.
116 | public export
117 | refineWeekDate : WeekNumber -> DayOfWeek -> Year ->
118 |                  Either IsoWeekDateError (CalendarDate Gregorian)
119 | refineWeekDate week target valueYear =
120 |   case choose
121 |     (IotaTime.Calendar.Iso.isValidWeekDate week target valueYear) of
122 |     Left valid => Right
123 |       (IotaTime.Calendar.Iso.fromWeekDate week target valueYear @{valid})
124 |     Right _ => Left (InvalidIsoWeekDate week target valueYear)
125 |
126 | ||| Validate an unrestricted arithmetic week coordinate learned at runtime.
127 | public export
128 | refineArithmeticWeekDate : WeekNumber -> DayOfWeek -> Year ->
129 |   Either IsoWeekDateError (CalendarDate Gregorian)
130 | refineArithmeticWeekDate week target valueYear =
131 |   case choose (isValidArithmeticWeekDate week target valueYear) of
132 |     Left valid => Right
133 |       (arithmeticFromWeekDate week target valueYear @{valid})
134 |     Right _ => Left
135 |       (ArithmeticIsoWeekDateOutOfRange week target valueYear)
136 |