0 | module IotaTime.Internal.Gregorian
  1 |
  2 | %default total
  3 |
  4 | yearsPerLeapCycle : Integer
  5 | yearsPerLeapCycle = 4
  6 |
  7 | yearsPerCentury : Integer
  8 | yearsPerCentury = 100
  9 |
 10 | yearsPerEra : Integer
 11 | yearsPerEra = 4 * yearsPerCentury
 12 |
 13 | daysPerCommonYear : Integer
 14 | daysPerCommonYear = 365
 15 |
 16 | leapDaysPerEra : Integer
 17 | leapDaysPerEra = yearsPerEra `div` yearsPerLeapCycle -
 18 |   yearsPerEra `div` yearsPerCentury + 1
 19 |
 20 | daysPerEra : Integer
 21 | daysPerEra = yearsPerEra * daysPerCommonYear + leapDaysPerEra
 22 |
 23 | daysPerFourCommonYears : Integer
 24 | daysPerFourCommonYears = yearsPerLeapCycle * daysPerCommonYear
 25 |
 26 | daysPerCentury : Integer
 27 | daysPerCentury = yearsPerCentury * daysPerCommonYear +
 28 |   yearsPerCentury `div` yearsPerLeapCycle - 1
 29 |
 30 | erasBeforeEpoch : Integer
 31 | erasBeforeEpoch = 5
 32 |
 33 | -- Day zero is March 1, 2000, after five complete 400-year Gregorian eras.
 34 | daysBeforeEpoch : Integer
 35 | daysBeforeEpoch = erasBeforeEpoch * daysPerEra
 36 |
 37 | monthsPerMarchCycle : Integer
 38 | monthsPerMarchCycle = 5
 39 |
 40 | monthsPerYear : Integer
 41 | monthsPerYear = 12
 42 |
 43 | marchMonthNumber : Integer
 44 | marchMonthNumber = 3
 45 |
 46 | monthsBeforeMarch : Integer
 47 | monthsBeforeMarch = marchMonthNumber - 1
 48 |
 49 | monthsFromMarchThroughDecember : Integer
 50 | monthsFromMarchThroughDecember = monthsPerYear - monthsBeforeMarch
 51 |
 52 | -- A March-based five-month block has three 31-day and two 30-day months.
 53 | daysPerMarchCycle : Integer
 54 | daysPerMarchCycle = 3 * 31 + 2 * 30
 55 |
 56 | monthCalculationOffset : Integer
 57 | monthCalculationOffset = 2
 58 |
 59 | public export %inline
 60 | gregorianDaysFromCivil : Integer -> Integer -> Integer -> Integer
 61 | gregorianDaysFromCivil year month day =
 62 |   let shiftedYear = if month <= monthsBeforeMarch then year - 1 else year
 63 |       era = shiftedYear `div` yearsPerEra
 64 |       yearOfEra = shiftedYear - era * yearsPerEra
 65 |       shiftedMonth = month + if month > monthsBeforeMarch
 66 |         then -marchMonthNumber
 67 |         else monthsPerYear - marchMonthNumber
 68 |       dayOfYear = (daysPerMarchCycle * shiftedMonth + monthCalculationOffset)
 69 |         `div` monthsPerMarchCycle + day - 1
 70 |       dayOfEra = yearOfEra * daysPerCommonYear +
 71 |         yearOfEra `div` yearsPerLeapCycle -
 72 |         yearOfEra `div` yearsPerCentury + dayOfYear
 73 |    in era * daysPerEra + dayOfEra - daysBeforeEpoch
 74 |
 75 | public export %inline
 76 | gregorianCivilFromDays : Integer -> (Integer, Integer, Integer)
 77 | gregorianCivilFromDays value =
 78 |   let shifted = value + daysBeforeEpoch
 79 |       era = shifted `div` daysPerEra
 80 |       dayOfEra = shifted - era * daysPerEra
 81 |       yearOfEra =
 82 |         (dayOfEra - dayOfEra `div` daysPerFourCommonYears +
 83 |           dayOfEra `div` daysPerCentury -
 84 |           dayOfEra `div` (daysPerEra - 1)) `div` daysPerCommonYear
 85 |       partialYear = yearOfEra + era * yearsPerEra
 86 |       dayOfYear = dayOfEra -
 87 |         (daysPerCommonYear * yearOfEra +
 88 |           yearOfEra `div` yearsPerLeapCycle -
 89 |           yearOfEra `div` yearsPerCentury)
 90 |       shiftedMonth = (monthsPerMarchCycle * dayOfYear + monthCalculationOffset)
 91 |         `div` daysPerMarchCycle
 92 |       day = dayOfYear -
 93 |         (daysPerMarchCycle * shiftedMonth + monthCalculationOffset)
 94 |           `div` monthsPerMarchCycle + 1
 95 |       month = shiftedMonth + if shiftedMonth < monthsFromMarchThroughDecember
 96 |         then marchMonthNumber
 97 |         else -(monthsPerYear - marchMonthNumber)
 98 |       year = partialYear + if month <= monthsBeforeMarch then 1 else 0
 99 |    in (year, month, day)
100 |