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