0 | module IotaTime.Pattern.Calendar

  2 | import Data.Fin

  3 | import Data.Vect

  4 | import IotaTime.Calendar

  5 | import IotaTime.Calendar.Coptic

  6 | import IotaTime.Calendar.Gregorian

  7 | import IotaTime.Calendar.Hebrew

  8 | import IotaTime.Calendar.Islamic

  9 | import IotaTime.Calendar.Julian

 10 | import IotaTime.Calendar.Persian

 11 | import IotaTime.Pattern

 13 | %default total

 17 | public export

 18 | data PatternMonthNameSource : Nat -> Type where

 19 |   GregorianLocaleMonthNames : {monthCount : Nat} ->

 20 |     (0 countIsTwelve : monthCount = 12) ->

 21 |     PatternMonthNameSource monthCount

 22 |   CanonicalCalendarMonthNames : {monthCount : Nat} ->

 23 |     PatternMonthNameSource monthCount

 26 | public export

 27 | interface Calendar calendar => CalendarPattern calendar where

 28 |   patternMonthCount : Nat

 29 |   patternMonthNames : Vect patternMonthCount String

 30 |   patternMonthAbbreviations : Vect patternMonthCount String

 31 |   patternMonthNameSource : PatternMonthNameSource patternMonthCount

 32 |   patternMonthNameSource = CanonicalCalendarMonthNames

 33 |   patternMonthIndex : CalendarDate calendar -> Fin patternMonthCount

 34 |   patternWeekdayIndex : CalendarDate calendar -> Fin 7

 35 |   refinePatternDate : Integer -> Integer -> Integer ->

 36 |     Either PatternError (CalendarDate calendar)

 38 | refineDay : Integer -> Either PatternError DayOfMonth

 39 | refineDay value = case refineDayOfMonth value of

 40 |   Left _ => Left (InvalidValue "day is outside 1-31")

 41 |   Right day => Right day

 43 | refineMonth : Nat -> Integer -> Either PatternError Integer

 44 | refineMonth monthCount value =

 45 |   let maximum = cast monthCount

 46 |   in if value >= 1 && value <= maximum

 47 |     then Right value

 48 |     else Left (ValueOutOfRange "month" 1 maximum value)

 50 | invalidDate : String -> Either PatternError value

 51 | invalidDate name = Left (InvalidValue ("invalid " ++ name ++ " date"))

 53 | refineTwelveMonthDate : String ->

 54 |   (Integer -> monthType) ->

 55 |   (DayOfMonth -> monthType -> Year -> Either error result) ->

 56 |   Integer -> Integer -> Integer -> Either PatternError result

 57 | refineTwelveMonthDate calendarName toMonth refineDate year month day = do

 58 |   valueMonth <- refineMonth 12 month

 59 |   valueDay <- refineDay day

 60 |   case refineDate valueDay (toMonth valueMonth) (yearFromInteger year) of

 61 |     Left _ => invalidDate calendarName

 62 |     Right date => Right date

 64 | abbreviate : String -> String

 65 | abbreviate = substr 0 3

 67 | abbreviateAll : {monthCount : Nat} ->

 68 |                 Vect monthCount String -> Vect monthCount String

 69 | abbreviateAll = map abbreviate

 71 | gregorianMonthNames : Vect 12 String

 72 | gregorianMonthNames =

 73 |   [ "January", "February", "March", "April", "May", "June"

 74 |   , "July", "August", "September", "October", "November", "December"

 75 |   ]

 77 | monthIndex12 : Integer -> Fin 12

 78 | monthIndex12 value = restrict 11 (value - 1)

 80 | monthIndex13 : Integer -> Fin 13

 81 | monthIndex13 value = restrict 12 (value - 1)

 83 | weekdayIndex7 : Integer -> Fin 7

 84 | weekdayIndex7 value = restrict 6 value

 86 | gregorianMonth : Integer -> Month

 87 | gregorianMonth 1 = January

 88 | gregorianMonth 2 = February

 89 | gregorianMonth 3 = March

 90 | gregorianMonth 4 = April

 91 | gregorianMonth 5 = May

 92 | gregorianMonth 6 = June

 93 | gregorianMonth 7 = July

 94 | gregorianMonth 8 = August

 95 | gregorianMonth 9 = September

 96 | gregorianMonth 10 = October

 97 | gregorianMonth 11 = November

 98 | gregorianMonth _ = December

100 | public export

101 | CalendarPattern Gregorian where

102 |   patternMonthCount = 12

103 |   patternMonthNames = gregorianMonthNames

104 |   patternMonthAbbreviations = abbreviateAll gregorianMonthNames

105 |   patternMonthNameSource = GregorianLocaleMonthNames Refl

106 |   patternMonthIndex date = monthIndex12

107 |     (IotaTime.Calendar.Gregorian.monthNumber

108 |       (month date))

109 |   patternWeekdayIndex date = weekdayIndex7

110 |     (weekdayNumber (dayOfWeek date))

111 |   refinePatternDate year month day = do

112 |     valueMonth <- refineMonth 12 month

113 |     valueDay <- refineDay day

114 |     case IotaTime.Calendar.Gregorian.refineDate

115 |       valueDay (gregorianMonth valueMonth)

116 |       (yearFromInteger year) of

117 |       Left _ => invalidDate "Gregorian"

118 |       Right date => Right date

120 | julianMonth : Integer -> JulianMonth

121 | julianMonth 1 = JulianMonths.January

122 | julianMonth 2 = JulianMonths.February

123 | julianMonth 3 = JulianMonths.March

124 | julianMonth 4 = JulianMonths.April

125 | julianMonth 5 = JulianMonths.May

126 | julianMonth 6 = JulianMonths.June

127 | julianMonth 7 = JulianMonths.July

128 | julianMonth 8 = JulianMonths.August

129 | julianMonth 9 = JulianMonths.September

130 | julianMonth 10 = JulianMonths.October

131 | julianMonth 11 = JulianMonths.November

132 | julianMonth _ = JulianMonths.December

134 | public export

135 | CalendarPattern Julian where

136 |   patternMonthCount = 12

137 |   patternMonthNames = gregorianMonthNames

138 |   patternMonthAbbreviations = abbreviateAll gregorianMonthNames

139 |   patternMonthNameSource = GregorianLocaleMonthNames Refl

140 |   patternMonthIndex date = monthIndex12

141 |     (JulianMonths.monthNumber (month date))

142 |   patternWeekdayIndex date = weekdayIndex7

143 |     (weekdayNumber (dayOfWeek date))

144 |   refinePatternDate year month day = do

145 |     valueMonth <- refineMonth 12 month

146 |     valueDay <- refineDay day

147 |     case IotaTime.Calendar.Julian.refineDate

148 |       valueDay (julianMonth valueMonth)

149 |       (yearFromInteger year) of

150 |       Left _ => invalidDate "Julian"

151 |       Right date => Right date

153 | copticMonth : Integer -> CopticMonth

154 | copticMonth 1 = CopticMonths.Thout

155 | copticMonth 2 = CopticMonths.Paopi

156 | copticMonth 3 = CopticMonths.Hathor

157 | copticMonth 4 = CopticMonths.Koiak

158 | copticMonth 5 = CopticMonths.Tobi

159 | copticMonth 6 = CopticMonths.Meshir

160 | copticMonth 7 = CopticMonths.Paremhat

161 | copticMonth 8 = CopticMonths.Paremoude

162 | copticMonth 9 = CopticMonths.Pashons

163 | copticMonth 10 = CopticMonths.Paoni

164 | copticMonth 11 = CopticMonths.Epip

165 | copticMonth 12 = CopticMonths.Mesori

166 | copticMonth _ = CopticMonths.PiKogiEnavot

168 | public export

169 | CalendarPattern Coptic where

170 |   patternMonthCount = 13

171 |   patternMonthNames =

172 |     [ "Thout", "Paopi", "Hathor", "Koiak", "Tobi", "Meshir"

173 |     , "Paremhat", "Paremoude", "Pashons", "Paoni", "Epip", "Mesori"

174 |     , "PiKogiEnavot"

175 |     ]

176 |   patternMonthAbbreviations =

177 |     [ "Tho", "Pao", "Hat", "Koi", "Tob", "Mes", "Par", "Pmd"

178 |     , "Pas", "Pni", "Epi", "Mso", "PKN"

179 |     ]

180 |   patternMonthIndex date = monthIndex13

181 |     (CopticMonths.monthNumber (month date))

182 |   patternWeekdayIndex date = weekdayIndex7

183 |     (weekdayNumber (dayOfWeek date))

184 |   refinePatternDate year month day = do

185 |     valueMonth <- refineMonth 13 month

186 |     valueDay <- refineDay day

187 |     case IotaTime.Calendar.Coptic.refineDate

188 |       valueDay (copticMonth valueMonth)

189 |       (yearFromInteger year) of

190 |       Left _ => invalidDate "Coptic"

191 |       Right date => Right date

193 | islamicMonth : Integer -> IslamicMonth

194 | islamicMonth 1 = IslamicMonths.Muharram

195 | islamicMonth 2 = IslamicMonths.Safar

196 | islamicMonth 3 = IslamicMonths.RabiAlAwwal

197 | islamicMonth 4 = IslamicMonths.RabiAlThani

198 | islamicMonth 5 = IslamicMonths.JumadaAlAwwal

199 | islamicMonth 6 = IslamicMonths.JumadaAlThani

200 | islamicMonth 7 = IslamicMonths.Rajab

201 | islamicMonth 8 = IslamicMonths.Shaban

202 | islamicMonth 9 = IslamicMonths.Ramadan

203 | islamicMonth 10 = IslamicMonths.Shawwal

204 | islamicMonth 11 = IslamicMonths.DhulQadah

205 | islamicMonth _ = IslamicMonths.DhulHijjah

207 | islamicMonthNames : Vect 12 String

208 | islamicMonthNames =

209 |   [ "Muharram", "Safar", "RabiAlAwwal", "RabiAlThani"

210 |   , "JumadaAlAwwal", "JumadaAlThani", "Rajab", "Shaban"

211 |   , "Ramadan", "Shawwal", "DhulQadah", "DhulHijjah"

212 |   ]

214 | islamicMonthAbbreviations : Vect 12 String

215 | islamicMonthAbbreviations =

216 |   [ "Muh", "Saf", "RaA", "RaT", "JuA", "JuT"

217 |   , "Raj", "Sha", "Ram", "Shw", "DhQ", "DhH"

218 |   ]

220 | public export

221 | {pattern : IslamicLeapPattern} -> KnownIslamicLeapPattern pattern =>

222 |   CalendarPattern (Islamic pattern) where

223 |   patternMonthCount = 12

224 |   patternMonthNames = islamicMonthNames

225 |   patternMonthAbbreviations = islamicMonthAbbreviations

226 |   patternMonthIndex date = monthIndex12 (IslamicMonths.monthNumber

227 |     (month date))

228 |   patternWeekdayIndex date = weekdayIndex7 (weekdayNumber

229 |     (dayOfWeek date))

230 |   refinePatternDate = refineTwelveMonthDate "Islamic" islamicMonth

231 |     (IotaTime.Calendar.Islamic.refineDate' {pattern})

233 | public export

234 | {pattern : IslamicLeapPattern} -> KnownIslamicLeapPattern pattern =>

235 |   CalendarPattern (CivilIslamic pattern) where

236 |   patternMonthCount = 12

237 |   patternMonthNames = islamicMonthNames

238 |   patternMonthAbbreviations = islamicMonthAbbreviations

239 |   patternMonthIndex date = monthIndex12 (IslamicMonths.monthNumber

240 |     (month date))

241 |   patternWeekdayIndex date = weekdayIndex7 (weekdayNumber

242 |     (dayOfWeek date))

243 |   refinePatternDate = refineTwelveMonthDate "Civil Islamic" islamicMonth

244 |     (refineCivilDate' {pattern})

246 | persianMonth : Integer -> PersianMonth

247 | persianMonth 1 = PersianMonths.Farvardin

248 | persianMonth 2 = PersianMonths.Ordibehesht

249 | persianMonth 3 = PersianMonths.Khordad

250 | persianMonth 4 = PersianMonths.Tir

251 | persianMonth 5 = PersianMonths.Mordad

252 | persianMonth 6 = PersianMonths.Shahrivar

253 | persianMonth 7 = PersianMonths.Mehr

254 | persianMonth 8 = PersianMonths.Aban

255 | persianMonth 9 = PersianMonths.Azar

256 | persianMonth 10 = PersianMonths.Dey

257 | persianMonth 11 = PersianMonths.Bahman

258 | persianMonth _ = PersianMonths.Esfand

260 | persianMonthNames : Vect 12 String

261 | persianMonthNames =

262 |   [ "Farvardin", "Ordibehesht", "Khordad", "Tir", "Mordad", "Shahrivar"

263 |   , "Mehr", "Aban", "Azar", "Dey", "Bahman", "Esfand"

264 |   ]

266 | persianMonthAbbreviations : Vect 12 String

267 | persianMonthAbbreviations =

268 |   [ "Far", "Ord", "Kho", "Tir", "Mor", "Sha"

269 |   , "Meh", "Aba", "Aza", "Dey", "Bah", "Esf"

270 |   ]

272 | public export

273 | CalendarPattern Persian where

274 |   patternMonthCount = 12

275 |   patternMonthNames = persianMonthNames

276 |   patternMonthAbbreviations = persianMonthAbbreviations

277 |   patternMonthIndex date = monthIndex12

278 |     (PersianMonths.monthNumber (month date))

279 |   patternWeekdayIndex date = weekdayIndex7

280 |     (weekdayNumber (dayOfWeek date))

281 |   refinePatternDate = refineTwelveMonthDate "Persian" persianMonth

282 |     IotaTime.Calendar.Persian.refineDate

284 | public export

285 | {rule : PersianArithmeticRule} ->

286 |   CalendarPattern (ArithmeticPersian rule) where

287 |   patternMonthCount = 12

288 |   patternMonthNames = persianMonthNames

289 |   patternMonthAbbreviations = persianMonthAbbreviations

290 |   patternMonthIndex date = monthIndex12 (PersianMonths.monthNumber

291 |     (month date))

292 |   patternWeekdayIndex date = weekdayIndex7 (weekdayNumber

293 |     (dayOfWeek date))

294 |   refinePatternDate = refineTwelveMonthDate

295 |     (arithmeticRuleName rule) persianMonth

296 |     (refineArithmeticRuleDate {rule})

298 | hebrewMonthName : {numbering : HebrewNumbering} ->

299 |                   KnownHebrewNumbering numbering => Integer -> HebrewMonthName

300 | hebrewMonthName {numbering} value =

301 |   case (value - 1 + numberingStart {numbering}) `mod` 13 of

302 |     0 => TishriName

303 |     1 => CheshvanName

304 |     2 => KislevName

305 |     3 => TevetName

306 |     4 => ShevatName

307 |     5 => AdarIName

308 |     6 => AdarName

309 |     7 => NisanName

310 |     8 => IyarName

311 |     9 => SivanName

312 |     10 => TammuzName

313 |     11 => AvName

314 |     _ => ElulName

316 | hebrewMonthLabel : HebrewMonthName -> String

317 | hebrewMonthLabel TishriName = "Tishri"

318 | hebrewMonthLabel CheshvanName = "Cheshvan"

319 | hebrewMonthLabel KislevName = "Kislev"

320 | hebrewMonthLabel TevetName = "Tevet"

321 | hebrewMonthLabel ShevatName = "Shevat"

322 | hebrewMonthLabel AdarIName = "AdarI"

323 | hebrewMonthLabel AdarName = "Adar"

324 | hebrewMonthLabel NisanName = "Nisan"

325 | hebrewMonthLabel IyarName = "Iyar"

326 | hebrewMonthLabel SivanName = "Sivan"

327 | hebrewMonthLabel TammuzName = "Tammuz"

328 | hebrewMonthLabel AvName = "Av"

329 | hebrewMonthLabel ElulName = "Elul"

331 | hebrewNames : {numbering : HebrewNumbering} ->

332 |               KnownHebrewNumbering numbering => Vect 13 String

333 | hebrewNames {numbering} =

334 |   [ hebrewMonthLabel (hebrewMonthName {numbering} 1)

335 |   , hebrewMonthLabel (hebrewMonthName {numbering} 2)

336 |   , hebrewMonthLabel (hebrewMonthName {numbering} 3)

337 |   , hebrewMonthLabel (hebrewMonthName {numbering} 4)

338 |   , hebrewMonthLabel (hebrewMonthName {numbering} 5)

339 |   , hebrewMonthLabel (hebrewMonthName {numbering} 6)

340 |   , hebrewMonthLabel (hebrewMonthName {numbering} 7)

341 |   , hebrewMonthLabel (hebrewMonthName {numbering} 8)

342 |   , hebrewMonthLabel (hebrewMonthName {numbering} 9)

343 |   , hebrewMonthLabel (hebrewMonthName {numbering} 10)

344 |   , hebrewMonthLabel (hebrewMonthName {numbering} 11)

345 |   , hebrewMonthLabel (hebrewMonthName {numbering} 12)

346 |   , hebrewMonthLabel (hebrewMonthName {numbering} 13)

347 |   ]

349 | public export

350 | {numbering : HebrewNumbering} -> KnownHebrewNumbering numbering =>

351 |   CalendarPattern (Hebrew numbering) where

352 |   patternMonthCount = 13

353 |   patternMonthNames = hebrewNames {numbering}

354 |   patternMonthAbbreviations = case numberingStart {numbering} of

355 |     0 => [ "Tis", "Che", "Kis", "Tev", "She", "AdI", "Ada"

356 |       , "Nis", "Iya", "Siv", "Tam", "Av", "Elu" ]

357 |     _ => [ "Nis", "Iya", "Siv", "Tam", "Av", "Elu", "Tis"

358 |       , "Che", "Kis", "Tev", "She", "AdI", "Ada" ]

359 |   patternMonthIndex date = case yearMonthDayFor {calendar = Hebrew numbering} date of

360 |     (_ ** (valueMonth, _)) => monthIndex13

361 |       (IotaTime.Calendar.Hebrew.monthNumber valueMonth)

362 |   patternWeekdayIndex date = weekdayIndex7 (weekdayNumber

363 |     (dayOfWeek date))

364 |   refinePatternDate year month day = do

365 |     valueMonth <- refineMonth 13 month

366 |     valueDay <- refineDay day

367 |     case IotaTime.Calendar.Hebrew.refineDate' {numbering} valueDay

368 |       (hebrewMonthName {numbering} valueMonth) (yearFromInteger year) of

369 |         Left _ => invalidDate "Hebrew"

370 |         Right date => Right date