0 | module IotaTime.Calendar.Hebrew

  2 | import IotaTime.Internal.ApplyPeriod

  3 | import IotaTime.Calendar

  4 | import IotaTime.Internal.Normalization

  5 | import IotaTime.Period

  6 | import Data.So

  8 | %default total

 11 | public export

 12 | data HebrewNumbering = Civil | Scriptural

 15 | public export

 16 | interface KnownHebrewNumbering (numbering : HebrewNumbering) where

 17 |   numberingStart : Integer

 19 | public export

 20 | KnownHebrewNumbering Civil where

 21 |   numberingStart = 0

 23 | public export

 24 | KnownHebrewNumbering Scriptural where

 25 |   numberingStart = 7

 28 | public export

 29 | data Hebrew : HebrewNumbering -> Type where

 30 |   HebrewCalendar : Hebrew numbering

 32 | public export

 33 | HebrewCivil : Type

 34 | HebrewCivil = Hebrew Civil

 36 | public export

 37 | HebrewScriptural : Type

 38 | HebrewScriptural = Hebrew Scriptural

 40 | public export

 42 | isLeapYear : Year -> Bool

 43 | isLeapYear value = (7 * yearValue value + 1) `mod` 19 < 7

 45 | namespace HebrewMonths

 46 |   public export

 47 |   data HebrewMonth : HebrewNumbering -> Year -> Type where

 48 |     Tishri : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 49 |        HebrewMonth numbering valueYear

 50 |     Cheshvan : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 51 |          HebrewMonth numbering valueYear

 52 |     Kislev : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 53 |        HebrewMonth numbering valueYear

 54 |     Tevet : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 55 |       HebrewMonth numbering valueYear

 56 |     Shevat : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 57 |        HebrewMonth numbering valueYear

 58 |     AdarI : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 59 |       {auto 0 leap : So (isLeapYear valueYear)} ->

 60 |       HebrewMonth numbering valueYear

 61 |     Adar : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 62 |      HebrewMonth numbering valueYear

 63 |     Nisan : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 64 |       HebrewMonth numbering valueYear

 65 |     Iyar : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 66 |      HebrewMonth numbering valueYear

 67 |     Sivan : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 68 |       HebrewMonth numbering valueYear

 69 |     Tammuz : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 70 |        HebrewMonth numbering valueYear

 71 |     Av : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 72 |    HebrewMonth numbering valueYear

 73 |     Elul : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 74 |      HebrewMonth numbering valueYear

 76 |   public export

 77 |   calendarIndex : {numbering : HebrewNumbering} -> {valueYear : Year} ->

 78 |       HebrewMonth numbering valueYear -> Integer

 79 |   calendarIndex Tishri = 0

 80 |   calendarIndex Cheshvan = 1

 81 |   calendarIndex Kislev = 2

 82 |   calendarIndex Tevet = 3

 83 |   calendarIndex Shevat = 4

 84 |   calendarIndex AdarI = 5

 85 |   calendarIndex Adar = 6

 86 |   calendarIndex Nisan = 7

 87 |   calendarIndex Iyar = 8

 88 |   calendarIndex Sivan = 9

 89 |   calendarIndex Tammuz = 10

 90 |   calendarIndex Av = 11

 91 |   calendarIndex Elul = 12

 93 |   public export

 94 |   {numbering : HebrewNumbering} -> {valueYear : Year} ->

 95 |     Eq (HebrewMonth numbering valueYear) where

 96 |     left == right = calendarIndex left == calendarIndex right

 98 |   public export

 99 |   {numbering : HebrewNumbering} -> {valueYear : Year} ->

100 |     Ord (HebrewMonth numbering valueYear) where

101 |     compare left right = compare (calendarIndex left) (calendarIndex right)

103 |   export

104 |   showMonth : HebrewMonth numbering valueYear -> String

105 |   showMonth Tishri = "Tishri"

106 |   showMonth Cheshvan = "Cheshvan"

107 |   showMonth Kislev = "Kislev"

108 |   showMonth Tevet = "Tevet"

109 |   showMonth Shevat = "Shevat"

110 |   showMonth AdarI = "AdarI"

111 |   showMonth Adar = "Adar"

112 |   showMonth Nisan = "Nisan"

113 |   showMonth Iyar = "Iyar"

114 |   showMonth Sivan = "Sivan"

115 |   showMonth Tammuz = "Tammuz"

116 |   showMonth Av = "Av"

117 |   showMonth Elul = "Elul"

119 |   public export

120 |   {numbering : HebrewNumbering} -> {valueYear : Year} ->

121 |     Show (HebrewMonth numbering valueYear) where

122 |     show = showMonth

125 | public export

126 | data HebrewMonthName

127 |   = TishriName | CheshvanName | KislevName | TevetName | ShevatName

128 |   | AdarIName | AdarName | NisanName | IyarName | SivanName

129 |   | TammuzName | AvName | ElulName

131 | public export

132 | Eq HebrewMonthName where

133 |   TishriName == TishriName = True

134 |   CheshvanName == CheshvanName = True

135 |   KislevName == KislevName = True

136 |   TevetName == TevetName = True

137 |   ShevatName == ShevatName = True

138 |   AdarIName == AdarIName = True

139 |   AdarName == AdarName = True

140 |   NisanName == NisanName = True

141 |   IyarName == IyarName = True

142 |   SivanName == SivanName = True

143 |   TammuzName == TammuzName = True

144 |   AvName == AvName = True

145 |   ElulName == ElulName = True

146 |   _ == _ = False

148 | public export

149 | monthName : {numbering : HebrewNumbering} -> {valueYear : Year} ->

150 |             HebrewMonth numbering valueYear -> HebrewMonthName

151 | monthName HebrewMonths.Tishri = TishriName

152 | monthName HebrewMonths.Cheshvan = CheshvanName

153 | monthName HebrewMonths.Kislev = KislevName

154 | monthName HebrewMonths.Tevet = TevetName

155 | monthName HebrewMonths.Shevat = ShevatName

156 | monthName HebrewMonths.AdarI = AdarIName

157 | monthName HebrewMonths.Adar = AdarName

158 | monthName HebrewMonths.Nisan = NisanName

159 | monthName HebrewMonths.Iyar = IyarName

160 | monthName HebrewMonths.Sivan = SivanName

161 | monthName HebrewMonths.Tammuz = TammuzName

162 | monthName HebrewMonths.Av = AvName

163 | monthName HebrewMonths.Elul = ElulName

165 | public export

166 | monthNumber : {numbering : HebrewNumbering} -> {year : Year} ->

167 |                     KnownHebrewNumbering numbering =>

168 |                     HebrewMonth numbering year -> Integer

169 | monthNumber value =

170 |   (HebrewMonths.calendarIndex value - numberingStart {numbering} + 13) `mod` 13 + 1

172 | monthsInHebrewYear : Year -> Integer

173 | monthsInHebrewYear value = if isLeapYear value then 13 else 12

175 | public export

177 | monthsElapsed : Year -> Integer

178 | monthsElapsed value =

179 |   let number = yearValue value

180 |       cycles = (number - 1) `div` 19

181 |       inCycle = (number - 1) `mod` 19

182 |    in 235 * cycles + 12 * inCycle + (7 * inCycle + 1) `div` 19

184 | public export

186 | elapsedDays : Year -> Integer

187 | elapsedDays value =

188 |   let elapsedMonths = monthsElapsed value

189 |       partsElapsed = 204 + 793 * (elapsedMonths `mod` 1080)

190 |       hoursElapsed = 5 + 12 * elapsedMonths + 793 * (elapsedMonths `div` 1080) +

191 |         partsElapsed `div` 1080

192 |       moladDay = 1 + 29 * elapsedMonths + hoursElapsed `div` 24

193 |       moladParts = 1080 * (hoursElapsed `mod` 24) + partsElapsed `mod` 1080

194 |       postponed = if moladParts >= 19440

195 |         then moladDay + 1

196 |         else if moladDay `mod` 7 == 2 && moladParts >= 9924 && not (isLeapYear value)

197 |           then moladDay + 1

198 |           else if moladDay `mod` 7 == 1 && moladParts >= 16789 &&

199 |               isLeapYear (Year.fromInteger (yearValue value - 1))

200 |             then moladDay + 1

201 |             else moladDay

202 |    in if postponed `mod` 7 == 0 || postponed `mod` 7 == 3 || postponed `mod` 7 == 5

203 |         then postponed + 1

204 |         else postponed

206 | public export

208 | firstDayOfYear : Year -> Integer

209 | firstDayOfYear value = -2103608 + elapsedDays value

211 | public export

213 | daysInYear : Year -> Integer

214 | daysInYear value =

215 |   firstDayOfYear (Year.fromInteger (yearValue value + 1)) -

216 |   firstDayOfYear value

218 | public export

220 | isCheshvanLong : Year -> Bool

221 | isCheshvanLong value = daysInYear value `mod` 10 == 5

223 | public export

225 | isKislevShort : Year -> Bool

226 | isKislevShort value = daysInYear value `mod` 10 == 3

228 | public export

230 | monthLengthByIndex : Year -> Integer -> Integer

231 | monthLengthByIndex _ 0 = 30

232 | monthLengthByIndex value 1 = if isCheshvanLong value then 30 else 29

233 | monthLengthByIndex value 2 = if isKislevShort value then 29 else 30

234 | monthLengthByIndex _ 3 = 29

235 | monthLengthByIndex _ 4 = 30

236 | monthLengthByIndex value 5 = if isLeapYear value then 30 else 0

237 | monthLengthByIndex _ 6 = 29

238 | monthLengthByIndex _ 7 = 30

239 | monthLengthByIndex _ 8 = 29

240 | monthLengthByIndex _ 9 = 30

241 | monthLengthByIndex _ 10 = 29

242 | monthLengthByIndex _ 11 = 30

243 | monthLengthByIndex _ 12 = 29

244 | monthLengthByIndex _ _ = 0

246 | public export

248 | maxDaysInMonth : {numbering : HebrewNumbering} -> {year : Year} ->

249 |                        (value : HebrewMonth numbering year) -> DayOfMonth

250 | maxDaysInMonth {year} value =

251 |   dayOfMonthFromInteger (monthLengthByIndex year (HebrewMonths.calendarIndex value))

253 | public export

255 | isValidDay : DayOfMonth -> (valueYear : Year) ->

256 |                    HebrewMonth numbering valueYear -> Bool

257 | isValidDay valueDay valueYear HebrewMonths.Cheshvan =

258 |   valueDay <= if isCheshvanLong valueYear then 30 else 29

259 | isValidDay valueDay valueYear HebrewMonths.Kislev =

260 |   valueDay <= if isKislevShort valueYear then 29 else 30

261 | isValidDay valueDay _ HebrewMonths.Tevet = valueDay <= 29

262 | isValidDay valueDay _ HebrewMonths.Adar = valueDay <= 29

263 | isValidDay valueDay _ HebrewMonths.Iyar = valueDay <= 29

264 | isValidDay valueDay _ HebrewMonths.Tammuz = valueDay <= 29

265 | isValidDay valueDay _ HebrewMonths.Elul = valueDay <= 29

266 | isValidDay valueDay _ _ = valueDay <= 30

269 | daysBeforeHebrewMonth : Year -> Integer -> Integer

270 | daysBeforeHebrewMonth _ 0 = 0

271 | daysBeforeHebrewMonth _ 1 = 30

272 | daysBeforeHebrewMonth value 2 = 30 + monthLengthByIndex value 1

273 | daysBeforeHebrewMonth value target =

274 |   let variableDays = monthLengthByIndex value 1 +

275 |         monthLengthByIndex value 2

276 |       adarIDays = monthLengthByIndex value 5

277 |    in case target of

278 |         3 => 30 + variableDays

279 |         4 => 59 + variableDays

280 |         5 => 89 + variableDays

281 |         6 => 89 + variableDays + adarIDays

282 |         7 => 118 + variableDays + adarIDays

283 |         8 => 148 + variableDays + adarIDays

284 |         9 => 177 + variableDays + adarIDays

285 |         10 => 207 + variableDays + adarIDays

286 |         11 => 236 + variableDays + adarIDays

287 |         12 => 266 + variableDays + adarIDays

288 |         _ => 295 + variableDays + adarIDays

291 | hebrewYearMonthDayToDays : {numbering : HebrewNumbering} ->

292 |                            (valueYear : Year) -> HebrewMonth numbering valueYear ->

293 |                            DayOfMonth -> Integer

294 | hebrewYearMonthDayToDays valueYear valueMonth valueDay =

295 |   firstDayOfYear valueYear +

296 |   daysBeforeHebrewMonth valueYear (HebrewMonths.calendarIndex valueMonth) +

297 |   dayOfMonthValue valueDay - 1

299 | monthFromCalendarIndex : {numbering : HebrewNumbering} ->

300 |                          (valueYear : Year) -> Integer -> HebrewMonth numbering valueYear

301 | monthFromCalendarIndex _ 0 = HebrewMonths.Tishri

302 | monthFromCalendarIndex _ 1 = HebrewMonths.Cheshvan

303 | monthFromCalendarIndex _ 2 = HebrewMonths.Kislev

304 | monthFromCalendarIndex _ 3 = HebrewMonths.Tevet

305 | monthFromCalendarIndex _ 4 = HebrewMonths.Shevat

306 | monthFromCalendarIndex valueYear 5 = case choose (isLeapYear valueYear) of

307 |   Left leap => HebrewMonths.AdarI @{leap}

308 |   Right _ => HebrewMonths.Adar

309 | monthFromCalendarIndex _ 6 = HebrewMonths.Adar

310 | monthFromCalendarIndex _ 7 = HebrewMonths.Nisan

311 | monthFromCalendarIndex _ 8 = HebrewMonths.Iyar

312 | monthFromCalendarIndex _ 9 = HebrewMonths.Sivan

313 | monthFromCalendarIndex _ 10 = HebrewMonths.Tammuz

314 | monthFromCalendarIndex _ 11 = HebrewMonths.Av

315 | monthFromCalendarIndex _ _ = HebrewMonths.Elul

317 | findHebrewYear : Nat -> Integer -> Year -> Year

318 | findHebrewYear Z days candidate = candidate

319 | findHebrewYear (S fuel) days candidate =

320 |   if firstDayOfYear candidate > days

321 |     then findHebrewYear fuel days (yearFromInteger (yearValue candidate - 1))

322 |     else let following = yearFromInteger (yearValue candidate + 1)

323 |           in if firstDayOfYear following <= days

324 |                then findHebrewYear fuel days following

325 |                else candidate

327 | findHebrewMonth : Nat -> Year -> Integer -> Integer -> (Integer, DayOfMonth)

328 | findHebrewMonth Z valueYear index remaining =

329 |   (index, dayOfMonthFromInteger (remaining + 1))

330 | findHebrewMonth (S fuel) valueYear index remaining =

331 |   let monthLength = monthLengthByIndex valueYear index

332 |    in if remaining < monthLength

333 |         then (index, dayOfMonthFromInteger (remaining + 1))

334 |         else findHebrewMonth fuel valueYear (index + 1) (remaining - monthLength)

336 | hebrewCivilFromDays : {numbering : HebrewNumbering} -> Integer ->

337 |   (valueYear : Year ** (HebrewMonth numbering valueYear, DayOfMonth))

338 | hebrewCivilFromDays days =

339 |   let firstYearDay = firstDayOfYear 1

340 |       estimate = max 1 ((days - firstYearDay) `div` 366 + 1)

341 |       valueYear = findHebrewYear (cast (abs estimate + 2)) days

342 |         (yearFromInteger estimate)

343 |       (monthIndex, valueDay) = findHebrewMonth 13 valueYear 0

344 |         (days - firstDayOfYear valueYear)

345 |   in (valueYear ** (monthFromCalendarIndex {numbering} valueYear monthIndex, valueDay))

348 | public export

349 | epochDay : Integer

350 | epochDay = -2103607

353 | record HebrewDate (numbering : HebrewNumbering) where

354 |   constructor MkHebrewDate

355 |   daysSinceEpoch : Integer

356 |   0 validDays : So (daysSinceEpoch >= -2103607)

358 | hebrewDateParts : {numbering : HebrewNumbering} -> HebrewDate numbering ->

359 |   (valueYear : Year ** (HebrewMonth numbering valueYear, DayOfMonth))

360 | hebrewDateParts {numbering} date =

361 |   normalizationBarrier (hebrewCivilFromDays {numbering}) date.daysSinceEpoch

363 | public export

364 | Eq (HebrewDate numbering) where

365 |   left == right = left.daysSinceEpoch == right.daysSinceEpoch

367 | public export

368 | Ord (HebrewDate numbering) where

369 |   compare left right = compare left.daysSinceEpoch right.daysSinceEpoch

371 | public export

372 | {numbering : HebrewNumbering} -> Show (HebrewDate numbering) where

373 |   show date = case hebrewDateParts date of

374 |     (valueYear ** (valueMonth, valueDay)) =>

375 |       "calendarDate' " ++ show valueDay ++ " " ++

376 |       show valueYear ++ " " ++ HebrewMonths.showMonth valueMonth

378 | checkedHebrewDate : {numbering : HebrewNumbering} -> (days : Integer) ->

379 |                     (0 valid : So (days >= -2103607)) -> HebrewDate numbering

380 | checkedHebrewDate days valid = MkHebrewDate days valid

382 | fromHebrewDays : {numbering : HebrewNumbering} -> (days : Integer) ->

383 |                  {auto 0 valid : So (days >= -2103607)} -> HebrewDate numbering

384 | fromHebrewDays days @{valid} = checkedHebrewDate days valid

386 | makeHebrewDate : {numbering : HebrewNumbering} -> Integer -> HebrewDate numbering

387 | makeHebrewDate days =

388 |   let clamped = max epochDay days

389 |    in case choose (clamped >= -2103607) of

390 |         Left valid => checkedHebrewDate clamped valid

391 |         Right _ => checkedHebrewDate epochDay Oh

394 | {numbering : HebrewNumbering} -> HasCalendarBridge (HebrewDate numbering) where

395 |   toBridgeDays = daysSinceEpoch

396 |   acceptsBridgeDays = (>= epochDay)

397 |   fromBridgeDays = fromHebrewDays {numbering}

398 |   bridgeCalendarName = "Hebrew"

400 | public export

402 | isValidDate : (valueDay : DayOfMonth) -> (valueYear : Year) ->

403 |                     HebrewMonth numbering valueYear -> Bool

404 | isValidDate valueDay valueYear valueMonth =

405 |   let dayNumber = dayOfMonthValue valueDay

406 |       yearNumber = yearValue valueYear

407 |       maxDay = case valueMonth of

408 |         HebrewMonths.Cheshvan => if isCheshvanLong valueYear then 30 else 29

409 |         HebrewMonths.Kislev => if isKislevShort valueYear then 29 else 30

410 |         HebrewMonths.Tevet => 29

411 |         HebrewMonths.Adar => 29

412 |         HebrewMonths.Iyar => 29

413 |         HebrewMonths.Tammuz => 29

414 |         HebrewMonths.Elul => 29

415 |         _ => 30

416 |    in yearNumber >= 1 && dayNumber <= maxDay

418 | clampToHebrew : Integer -> Integer

419 | clampToHebrew = max epochDay

421 | shiftHebrewDays : {numbering : HebrewNumbering} ->

422 |                   Integer -> HebrewDate numbering -> HebrewDate numbering

423 | shiftHebrewDays amount date = makeHebrewDate (clampToHebrew (date.daysSinceEpoch + amount))

425 | calendarIndexToPosition : Year -> Integer -> Integer

426 | calendarIndexToPosition valueYear index =

427 |   if isLeapYear valueYear || index < 5 then index else index - 1

429 | positionToCalendarIndex : Year -> Integer -> Integer

430 | positionToCalendarIndex valueYear position =

431 |   if isLeapYear valueYear || position < 5 then position else position + 1

433 | addHebrewMonths : Year -> Integer -> Integer -> (Year, Integer)

434 | addHebrewMonths valueYear index amount =

435 |   go (cast (abs amount + 2)) valueYear

436 |     (calendarIndexToPosition valueYear index + amount)

437 |   where

438 |     go : Nat -> Year -> Integer -> (Year, Integer)

439 |     go Z currentYear position =

440 |       (currentYear, positionToCalendarIndex currentYear

441 |         (max 0 (min (monthsInHebrewYear currentYear - 1) position)))

442 |     go (S fuel) currentYear position =

443 |       if position < 0

444 |         then if yearValue currentYear <= 1

445 |           then (1, 0)

446 |           else let previousYear = yearFromInteger (yearValue currentYear - 1)

447 |                 in go fuel previousYear

448 |                   (position + monthsInHebrewYear previousYear)

449 |         else if position >= monthsInHebrewYear currentYear

450 |           then go fuel (yearFromInteger (yearValue currentYear + 1))

451 |             (position - monthsInHebrewYear currentYear)

452 |           else (currentYear, positionToCalendarIndex currentYear position)

454 | shiftHebrewMonths : {numbering : HebrewNumbering} ->

455 |                     Integer -> HebrewDate numbering -> HebrewDate numbering

456 | shiftHebrewMonths amount date = case hebrewDateParts date of

457 |   (valueYear ** (valueMonth, valueDay)) =>

458 |     let (targetYear, targetIndex) = addHebrewMonths valueYear

459 |           (HebrewMonths.calendarIndex valueMonth) amount

460 |         targetMonth = monthFromCalendarIndex {numbering} targetYear targetIndex

461 |         targetDay = min valueDay (maxDaysInMonth targetMonth)

462 |      in makeHebrewDate (hebrewYearMonthDayToDays targetYear targetMonth targetDay)

464 | shiftHebrewYears : {numbering : HebrewNumbering} ->

465 |                    Integer -> HebrewDate numbering -> HebrewDate numbering

466 | shiftHebrewYears amount date = case hebrewDateParts date of

467 |   (valueYear ** (valueMonth, valueDay)) =>

468 |     let targetYear = yearFromInteger (max 1 (yearValue valueYear + amount))

469 |         sourceIndex = HebrewMonths.calendarIndex valueMonth

470 |         targetIndex = if sourceIndex == 5 && not (isLeapYear targetYear) then 6 else sourceIndex

471 |         targetMonth = monthFromCalendarIndex {numbering} targetYear targetIndex

472 |         targetDay = min valueDay (maxDaysInMonth targetMonth)

473 |      in makeHebrewDate (hebrewYearMonthDayToDays targetYear targetMonth targetDay)

475 | applyHebrewPeriod : {numbering : HebrewNumbering} ->

476 |                     Period target -> HebrewDate numbering -> HebrewDate numbering

477 | applyHebrewPeriod = applyDatePeriodWith

478 |   shiftHebrewYears shiftHebrewMonths shiftHebrewDays

480 | hebrewDayOfWeek : HebrewDate numbering -> DayOfWeek

481 | hebrewDayOfWeek date = weekdayFromNumber (date.daysSinceEpoch + 3)

483 | nextHebrew : {numbering : HebrewNumbering} ->

484 |              Integer -> DayOfWeek ->

485 |              HebrewDate numbering -> HebrewDate numbering

486 | nextHebrew count target date =

487 |   makeHebrewDate (clampToHebrew (date.daysSinceEpoch +

488 |     nextWeekdayOffset count (hebrewDayOfWeek date) target))

490 | previousHebrew : {numbering : HebrewNumbering} ->

491 |                  Integer -> DayOfWeek ->

492 |                  HebrewDate numbering -> HebrewDate numbering

493 | previousHebrew count target date =

494 |   makeHebrewDate (clampToHebrew (date.daysSinceEpoch +

495 |     previousWeekdayOffset count (hebrewDayOfWeek date) target))

497 | public export

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

499 |   Calendar (Hebrew numbering) where

500 |   DateRep = HebrewDate numbering

501 |   MonthRep valueYear = HebrewMonth numbering valueYear

503 |   isValidDays = (>= epochDay)

504 |   fromDays = fromHebrewDays {numbering}

505 |   toDaysFor date = date.daysSinceEpoch

506 |   toDaysValid (MkHebrewDate _ valid) = valid

507 |   toFromDays _ _ = Refl

508 |   fromToDays (MkHebrewDate _ _) = Refl

509 |   calendarName = "Hebrew"

511 |   year' date = fst (hebrewDateParts date)

512 |   toYmd date = snd (hebrewDateParts date)

513 |   day' date = snd (snd (hebrewDateParts date))

514 |   month' date = fst (snd (hebrewDateParts date))

516 |   applyCalendarPeriod' = applyHebrewPeriod

517 |   shiftCalendarDays' = shiftHebrewDays

519 |   dayOfWeekFor = hebrewDayOfWeek

520 |   nextFor = nextHebrew

521 |   previousFor = previousHebrew

523 | public export

524 | {numbering : HebrewNumbering} -> HasCalendar (HebrewDate numbering) where

525 |   calendarCapability = ()

527 | public export

528 | {numbering : HebrewNumbering} ->

529 |   PeriodTarget (HebrewDate numbering) where

530 |   periodTarget = ()

532 | public export

533 | {numbering : HebrewNumbering} -> ApplyPeriod (HebrewDate numbering) where

534 |   applyPeriod = applyHebrewPeriod

536 | public export

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

538 |   CalendarValue (HebrewDate numbering) where

539 |   CalendarMonth valueYear = HebrewMonth numbering valueYear

540 |   calendarValueToDays = toDaysFor {calendar = Hebrew numbering}

541 |   calendarValueYear = yearFor {calendar = Hebrew numbering}

542 |   calendarValueMonthDay = toYmd {calendar = Hebrew numbering}

543 |   calendarValueDayOfWeek = dayOfWeekFor {calendar = Hebrew numbering}

544 |   calendarValueBetweenWith = betweenWithFor {calendar = Hebrew numbering}

546 | public export

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

548 |   CalendarNavigation (HebrewDate numbering) where

549 |   calendarValueNext = nextFor {calendar = Hebrew numbering}

550 |   calendarValuePrevious = previousFor {calendar = Hebrew numbering}

554 | public export

555 | calendarDate' : {numbering : HebrewNumbering} ->

556 |               {auto known : KnownHebrewNumbering numbering} ->

557 |               (valueDay : DayOfMonth) -> (valueYear : Year) ->

558 |               (valueMonth : HebrewMonth numbering valueYear) ->

559 |               {auto 0 valid : So (isValidDate valueDay valueYear valueMonth)} ->

560 |               CalendarDate (Hebrew numbering)

561 | calendarDate' valueDay valueYear valueMonth =

562 |   makeHebrewDate (hebrewYearMonthDayToDays valueYear valueMonth valueDay)

565 | public export

566 | calendarDate : (valueDay : DayOfMonth) -> (valueYear : Year) ->

567 |              (valueMonth : HebrewMonth Civil valueYear) ->

568 |              {auto 0 valid : So (isValidDate valueDay valueYear valueMonth)} ->

569 |              CalendarDate HebrewCivil

570 | calendarDate = calendarDate'

573 | public export

574 | data HebrewDateError

575 |   = InvalidHebrewMonth HebrewMonthName Year

576 |   | InvalidHebrewDate DayOfMonth HebrewMonthName Year

577 |   | InvalidHebrewDayCount Integer

578 |   | InvalidHebrewNthDay DayNth HebrewMonthName Year

579 |   | InvalidHebrewWeekDate WeekNumber Year

583 | public export

584 | refineMonth : {numbering : HebrewNumbering} -> (valueYear : Year) -> HebrewMonthName ->

585 |                     Either HebrewDateError (HebrewMonth numbering valueYear)

586 | refineMonth _ TishriName = Right HebrewMonths.Tishri

587 | refineMonth _ CheshvanName = Right HebrewMonths.Cheshvan

588 | refineMonth _ KislevName = Right HebrewMonths.Kislev

589 | refineMonth _ TevetName = Right HebrewMonths.Tevet

590 | refineMonth _ ShevatName = Right HebrewMonths.Shevat

591 | refineMonth valueYear AdarIName = case choose (isLeapYear valueYear) of

592 |   Left leap => Right (HebrewMonths.AdarI @{leap})

593 |   Right _ => Left (InvalidHebrewMonth AdarIName valueYear)

594 | refineMonth _ AdarName = Right HebrewMonths.Adar

595 | refineMonth _ NisanName = Right HebrewMonths.Nisan

596 | refineMonth _ IyarName = Right HebrewMonths.Iyar

597 | refineMonth _ SivanName = Right HebrewMonths.Sivan

598 | refineMonth _ TammuzName = Right HebrewMonths.Tammuz

599 | refineMonth _ AvName = Right HebrewMonths.Av

600 | refineMonth _ ElulName = Right HebrewMonths.Elul

603 | public export

604 | refineDate' : {numbering : HebrewNumbering} ->

605 |                     {auto known : KnownHebrewNumbering numbering} ->

606 |                     DayOfMonth -> HebrewMonthName -> Year ->

607 |                     Either HebrewDateError (CalendarDate (Hebrew numbering))

608 | refineDate' @{known} valueDay valueMonthName valueYear =

609 |   case refineMonth {numbering} valueYear valueMonthName of

610 |     Left error => Left error

611 |     Right valueMonth => case choose (isValidDate valueDay valueYear valueMonth) of

612 |       Left valid => Right

613 |         (calendarDate' @{known} valueDay valueYear valueMonth @{valid})

614 |       Right _ => Left (InvalidHebrewDate valueDay valueMonthName valueYear)

617 | public export

618 | refineDate : DayOfMonth -> HebrewMonthName -> Year ->

619 |                    Either HebrewDateError (CalendarDate HebrewCivil)

620 | refineDate = refineDate'

624 | public export

625 | fromDays' : {numbering : HebrewNumbering} ->

626 |                   {auto known : KnownHebrewNumbering numbering} ->

627 |                   (days : Integer) -> {auto 0 valid : So

628 |                     (IotaTime.Calendar.isValidDays

629 |                       {calendar = Hebrew numbering} days)} ->

630 |                   CalendarDate (Hebrew numbering)

631 | fromDays' {numbering} = fromHebrewDays {numbering}

633 | public export

634 | fromDays : (days : Integer) -> {auto 0 valid : So

635 |   (IotaTime.Calendar.isValidDays {calendar = HebrewCivil} days)} ->

636 |                  CalendarDate HebrewCivil

637 | fromDays = fromDays'

640 | public export

641 | refineDays' : {numbering : HebrewNumbering} ->

642 |                     {auto known : KnownHebrewNumbering numbering} ->

643 |                     Integer -> Either HebrewDateError (CalendarDate (Hebrew numbering))

644 | refineDays' @{known} days = case choose

645 |   (IotaTime.Calendar.isValidDays {calendar = Hebrew numbering} days) of

646 |   Left valid => Right (fromDays' @{known} days @{valid})

647 |   Right _ => Left (InvalidHebrewDayCount days)

649 | public export

650 | refineDays : Integer -> Either HebrewDateError (CalendarDate HebrewCivil)

651 | refineDays = refineDays'

653 | public export

655 | nthDayOfMonth : {numbering : HebrewNumbering} -> DayNth -> DayOfWeek ->

656 |                       (valueYear : Year) -> HebrewMonth numbering valueYear -> DayOfMonth

657 | nthDayOfMonth nth target valueYear valueMonth =

658 |   let monthLength = maxDaysInMonth valueMonth

659 |       firstDays = hebrewYearMonthDayToDays valueYear valueMonth 1

660 |       firstOffset =

661 |         (weekdayNumber target -

662 |          (firstDays + 3) `mod` daysPerWeek) `mod` daysPerWeek

663 |       lastDays = hebrewYearMonthDayToDays valueYear valueMonth monthLength

664 |       lastOffset =

665 |         ((lastDays + 3) `mod` daysPerWeek -

666 |          weekdayNumber target) `mod` daysPerWeek

667 |       dayNumber = nthWeekdayDayNumber nth (dayOfMonthValue monthLength)

668 |         firstOffset lastOffset

669 |    in dayOfMonthFromInteger dayNumber

671 | public export

673 | isValidNthDay : {numbering : HebrewNumbering} -> DayNth -> DayOfWeek ->

674 |                       (valueYear : Year) -> HebrewMonth numbering valueYear -> Bool

675 | isValidNthDay First _ valueYear _ = yearValue valueYear >= 1

676 | isValidNthDay Second _ valueYear _ = yearValue valueYear >= 1

677 | isValidNthDay Third _ valueYear _ = yearValue valueYear >= 1

678 | isValidNthDay Fourth _ valueYear _ = yearValue valueYear >= 1

679 | isValidNthDay Last _ valueYear _ = yearValue valueYear >= 1

680 | isValidNthDay SecondToLast _ valueYear _ = yearValue valueYear >= 1

681 | isValidNthDay ThirdToLast _ valueYear _ = yearValue valueYear >= 1

682 | isValidNthDay FourthToLast _ valueYear _ = yearValue valueYear >= 1

683 | isValidNthDay Fifth target valueYear valueMonth =

684 |   yearValue valueYear >= 1 &&

685 |   dayOfMonthValue (nthDayOfMonth Fifth target valueYear valueMonth) <=

686 |     dayOfMonthValue (maxDaysInMonth valueMonth)

690 | public export

691 | fromNthDay' : {numbering : HebrewNumbering} -> KnownHebrewNumbering numbering =>

692 |                      (nth : DayNth) -> (target : DayOfWeek) ->

693 |                      (valueYear : Year) -> (valueMonth : HebrewMonth numbering valueYear) ->

694 |                      {auto 0 valid : So

695 |                        (isValidNthDay nth target valueYear valueMonth)} ->

696 |                      CalendarDate (Hebrew numbering)

697 | fromNthDay' nth target valueYear valueMonth =

698 |   makeHebrewDate

699 |     (hebrewYearMonthDayToDays valueYear valueMonth

700 |       (nthDayOfMonth nth target valueYear valueMonth))

702 | public export

703 | fromNthDay : (nth : DayNth) -> (target : DayOfWeek) ->

704 |                    (valueYear : Year) -> (valueMonth : HebrewMonth Civil valueYear) ->

705 |                    {auto 0 valid : So

706 |                      (isValidNthDay nth target valueYear valueMonth)} ->

707 |                    CalendarDate HebrewCivil

708 | fromNthDay = fromNthDay'

711 | public export

712 | refineNthDay' : {numbering : HebrewNumbering} ->

713 |                       {auto known : KnownHebrewNumbering numbering} ->

714 |                       DayNth -> DayOfWeek -> Year -> HebrewMonthName ->

715 |                       Either HebrewDateError (CalendarDate (Hebrew numbering))

716 | refineNthDay' @{known} nth target valueYear valueMonthName =

717 |   case refineMonth {numbering} valueYear valueMonthName of

718 |     Left error => Left error

719 |     Right valueMonth =>

720 |       case choose (isValidNthDay nth target valueYear valueMonth) of

721 |         Left valid => Right

722 |           (fromNthDay' @{known} nth target valueYear valueMonth @{valid})

723 |         Right _ => Left (InvalidHebrewNthDay nth valueMonthName valueYear)

725 | public export

726 | refineNthDay : DayNth -> DayOfWeek -> Year -> HebrewMonthName ->

727 |                      Either HebrewDateError (CalendarDate HebrewCivil)

728 | refineNthDay = refineNthDay'

730 | public export

732 | weekDateDays : WeekNumber -> DayOfWeek -> Year -> Integer

733 | weekDateDays week target valueYear =

734 |   let firstDay = firstDayOfYear valueYear

735 |       firstWeekStart = firstDay - (firstDay + 3) `mod` 7

736 |    in firstWeekStart + 7 * (weekNumberValue week - 1) +

737 |     weekdayNumber target

739 | public export

741 | isValidWeekDate : {numbering : HebrewNumbering} ->

742 |                   KnownHebrewNumbering numbering =>

743 |                   WeekNumber -> DayOfWeek -> Year -> Bool

744 | isValidWeekDate week target valueYear =

745 |   (yearValue valueYear > 1 && weekNumberValue week >= 0) ||

746 |     IotaTime.Calendar.isValidDays {calendar = Hebrew numbering}

747 |       (weekDateDays week target valueYear)

750 | public export

751 | fromWeekDate' : {numbering : HebrewNumbering} -> KnownHebrewNumbering numbering =>

752 |                 (week : WeekNumber) -> (target : DayOfWeek) ->

753 |                 (valueYear : Year) ->

754 |                 {auto 0 valid : So

755 |                   (isValidWeekDate {numbering} week target valueYear)} ->

756 |                 CalendarDate (Hebrew numbering)

757 | fromWeekDate' week target valueYear =

758 |   makeHebrewDate (weekDateDays week target valueYear)

760 | public export

761 | fromWeekDate : (week : WeekNumber) -> (target : DayOfWeek) ->

762 |                (valueYear : Year) ->

763 |                {auto 0 valid : So

764 |                  (isValidWeekDate {numbering = Civil} week target valueYear)} ->

765 |                CalendarDate HebrewCivil

766 | fromWeekDate = fromWeekDate'

769 | public export

770 | refineWeekDate' : {numbering : HebrewNumbering} ->

771 |                   {auto known : KnownHebrewNumbering numbering} ->

772 |                   WeekNumber -> DayOfWeek -> Year ->

773 |                   Either HebrewDateError (CalendarDate (Hebrew numbering))

774 | refineWeekDate' @{known} week target valueYear =

775 |   case choose (isValidWeekDate {numbering} week target valueYear) of

776 |     Left valid => Right

777 |       (fromWeekDate' {numbering} @{known} week target valueYear @{valid})

778 |     Right _ => Left (InvalidHebrewWeekDate week valueYear)

780 | public export

781 | refineWeekDate : WeekNumber -> DayOfWeek -> Year ->

782 |                  Either HebrewDateError (CalendarDate HebrewCivil)

783 | refineWeekDate = refineWeekDate'