0 | module Utils.Time

  2 | import Utils.Num

  3 | import Data.Fin

  4 | import Data.String.Parser

  5 | import Data.Vect

  6 | import Data.String

  7 | import Data.Fin.Extra

  8 | import Utils.Misc

  9 | import Decidable.Equality

 10 | import Derive.Prelude

 11 | import Generics.Derive

 13 | %hide Generics.Derive.Eq

 14 | %hide Generics.Derive.Ord

 15 | %hide Generics.Derive.Show

 17 | %language ElabReflection

 19 | public export

 20 | data Month : Type where

 21 |   January : Month

 22 |   February : Month

 23 |   March : Month

 24 |   April : Month

 25 |   May : Month

 26 |   June : Month

 27 |   July : Month

 28 |   August : Month

 29 |   September : Month

 30 |   October : Month

 31 |   November : Month

 32 |   December : Month

 35 | next_month : Month -> Month

 36 | next_month January    = February

 37 | next_month February   = March

 38 | next_month March      = April

 39 | next_month April      = May

 40 | next_month May        = June

 41 | next_month June       = July

 42 | next_month July       = August

 43 | next_month August     = September

 44 | next_month September  = October

 45 | next_month October    = November

 46 | next_month November   = December

 47 | next_month December   = January

 50 | prev_month : Month -> Month

 51 | prev_month January    = December

 52 | prev_month February   = January

 53 | prev_month March      = February

 54 | prev_month April      = March

 55 | prev_month May        = April

 56 | prev_month June       = May

 57 | prev_month July       = June

 58 | prev_month August     = July

 59 | prev_month September  = August

 60 | prev_month October    = September

 61 | prev_month November   = October

 62 | prev_month December   = November

 64 | public export

 65 | next_prev_month : (m : Month) -> (next_month $ prev_month m) = m

 66 | next_prev_month January    = Refl

 67 | next_prev_month February   = Refl

 68 | next_prev_month March      = Refl

 69 | next_prev_month April      = Refl

 70 | next_prev_month May        = Refl

 71 | next_prev_month June       = Refl

 72 | next_prev_month July       = Refl

 73 | next_prev_month August     = Refl

 74 | next_prev_month September  = Refl

 75 | next_prev_month October    = Refl

 76 | next_prev_month November   = Refl

 77 | next_prev_month December   = Refl

 79 | public export

 80 | prev_next_month : (m : Month) -> (prev_month $ next_month m) = m

 81 | prev_next_month January    = Refl

 82 | prev_next_month February   = Refl

 83 | prev_next_month March      = Refl

 84 | prev_next_month April      = Refl

 85 | prev_next_month May        = Refl

 86 | prev_next_month June       = Refl

 87 | prev_next_month July       = Refl

 88 | prev_next_month August     = Refl

 89 | prev_next_month September  = Refl

 90 | prev_next_month October    = Refl

 91 | prev_next_month November   = Refl

 92 | prev_next_month December   = Refl

 95 | nat_to_month : Nat -> Maybe Month

 96 | nat_to_month 1  = Just January

 97 | nat_to_month 2  = Just February

 98 | nat_to_month 3  = Just March

 99 | nat_to_month 4  = Just April

100 | nat_to_month 5  = Just May

101 | nat_to_month 6  = Just June

102 | nat_to_month 7  = Just July

103 | nat_to_month 8  = Just August

104 | nat_to_month 9  = Just September

105 | nat_to_month 10 = Just October

106 | nat_to_month 11 = Just November

107 | nat_to_month 12 = Just December

108 | nat_to_month _ = Nothing

111 | fin_to_month : Fin 12 -> Month

112 | fin_to_month 0  = January

113 | fin_to_month 1  = February

114 | fin_to_month 2  = March

115 | fin_to_month 3  = April

116 | fin_to_month 4  = May

117 | fin_to_month 5  = June

118 | fin_to_month 6  = July

119 | fin_to_month 7  = August

120 | fin_to_month 8  = September

121 | fin_to_month 9  = October

122 | fin_to_month 10 = November

123 | fin_to_month 11 = December

126 | month_to_nat : Month -> Nat

127 | month_to_nat January   = 1

128 | month_to_nat February  = 2

129 | month_to_nat March     = 3

130 | month_to_nat April     = 4

131 | month_to_nat May       = 5

132 | month_to_nat June      = 6

133 | month_to_nat July      = 7

134 | month_to_nat August    = 8

135 | month_to_nat September = 9

136 | month_to_nat October   = 10

137 | month_to_nat November  = 11

138 | month_to_nat December  = 12

141 | month_num_of_dates : Integer -> Month -> Nat

142 | month_num_of_dates _ January = 31

143 | month_num_of_dates year February =

144 |   if year `mod` 4 /= 0 then 28

145 |     else if year `mod` 100 /= 0 then 29

146 |     else if year `mod` 400 /= 0 then 28

147 |     else 29

148 | month_num_of_dates _ March = 31

149 | month_num_of_dates _ April = 30

150 | month_num_of_dates _ May = 31

151 | month_num_of_dates _ June = 30

152 | month_num_of_dates _ July = 31

153 | month_num_of_dates _ August = 31

154 | month_num_of_dates _ September = 30

155 | month_num_of_dates _ October = 31

156 | month_num_of_dates _ November = 30

157 | month_num_of_dates _ December = 31

159 | %runElab derive "Month" [Generic, Meta, DecEq, Eq, Ord, Show]

161 | public export

162 | data FinNonZero : Fin n -> Type where

163 |   FSIsNonZero : FinNonZero (FS x)

165 | show_nat_pad : Nat -> Nat -> String

166 | show_nat_pad p n =

167 |   let str = show n

168 |       pad_len = minus p $ length str

169 |       pad = replicate pad_len '0'

170 |   in pad <+> str

172 | show_fin_pad : Nat -> Fin n -> String

173 | show_fin_pad p n = show_nat_pad p $ finToNat n

175 | public export

176 | record Date where

177 |   constructor MkDate

178 |   year : Integer

179 |   month : Month

180 |   day : Fin (S (month_num_of_dates year month))

181 |   day_non_zero : FinNonZero day

184 | epoch_date : Date

185 | epoch_date = MkDate 1970 January 1 FSIsNonZero

188 | Eq Date where

189 |   a == b =

190 |     case decEq a.year b.year of

191 |       Yes prf0 =>

192 |         case decEq a.month b.month of

193 |           Yes prf1 => a.day == (rewrite prf0 in rewrite prf1 in b.day)

194 |           No _ => False

195 |       No _ => False

198 | Ord Date where

199 |   a `compare` b =

200 |     case decEq a.year b.year of

201 |       Yes prf0 =>

202 |         case decEq a.month b.month of

203 |           Yes prf1 =>

204 |             let b_day = rewrite prf0 in rewrite prf1 in b.day

205 |             in a.day `compare` b_day

206 |           No _ => a.month `compare` b.month

207 |       No _ => a.year `compare` b.year

210 | Show Date where

211 |   show date =

212 |     (show $ date.year)

213 |     <+> "/"

214 |     <+> (show $ month_to_nat date.month)

215 |     <+> "/"

216 |     <+> (show_fin_pad 2 date.day)

218 | date_to_tuple : Date -> (Integer, Integer, Integer)

219 | date_to_tuple date = (date.year, natToInteger $ pred $ month_to_nat date.month, finToInteger date.day - 1)

221 | date_to_normalized_tuple : Date -> (Integer, Month, Integer)

222 | date_to_normalized_tuple date = (date.year, date.month, finToInteger date.day - 1)

224 | tuple_normalize_month : (Integer, Integer, Integer) -> (Integer, Month, Integer)

225 | tuple_normalize_month (year, month, day) =

226 |   ( if month >= 0 then year + month `div` 12 else year + ((month + 1) `div` 12) - 1

227 |   , fin_to_month $ modFinNZ (integerToNat $ month `mod'` 12) 12 SIsNonZero

228 |   , day)

230 | tuple_normalize_next_month : (Integer, Month, Integer) -> (Integer, Month, Integer)

231 | tuple_normalize_next_month (year, month, day) =

232 |   let next = next_month month

233 |       new_year = case month of { December => year + 1; _ => year; }

234 |   in (new_year, next, day - (natToInteger $ month_num_of_dates year month))

236 | tuple_normalize_prev_month : (Integer, Month, Integer) -> (Integer, Month, Integer)

237 | tuple_normalize_prev_month (year, month, day) =

238 |   let prev = prev_month month

239 |       new_year = case month of { January => year - 1; _ => year; }

240 |   in (new_year, prev, day + (natToInteger $ month_num_of_dates year prev))

242 | tuple_normalize_day : (Integer, Month, Integer) -> Date

243 | tuple_normalize_day (year, month, day) =

244 |   case integerToFin day (month_num_of_dates year month) of

245 |     Just day' => MkDate year month (FS day') FSIsNonZero

246 |     Nothing =>

247 |       if day < 0

248 |         then tuple_normalize_day $ tuple_normalize_prev_month (year, month, day)

249 |         else tuple_normalize_day $ tuple_normalize_next_month (year, month, day)

251 | tuple_normalize_date : (Integer, Integer, Integer) -> Date

252 | tuple_normalize_date = tuple_normalize_day . tuple_normalize_month

254 | days_between_dates' : (Integer, Month, Integer) -> (Integer, Month, Integer) -> Integer

255 | days_between_dates' a@(a_year, a_month, a_day) b@(b_year, b_month, b_day) =

256 |   case collapse_ordering [a_year `compare` b_year, a_month `compare` b_month] of

257 |     LT => days_between_dates' (tuple_normalize_next_month a) b

258 |     GT => days_between_dates' (tuple_normalize_prev_month a) b

259 |     EQ => a_day - b_day

262 | days_between_dates : Date -> Date -> Integer

263 | days_between_dates a b = days_between_dates' (date_to_normalized_tuple a) (date_to_normalized_tuple b)

265 | day_in_seconds : Nat

266 | day_in_seconds = 24 * 60 * 60

268 | day_in_milliseconds : Nat

269 | day_in_milliseconds = 24 * 60 * 60 * 1000

271 | day_in_seconds' : Integer

272 | day_in_seconds' = natToInteger day_in_seconds

274 | day_in_milliseconds' : Integer

275 | day_in_milliseconds' = natToInteger day_in_milliseconds

277 | public export

278 | record DateTime where

279 |   constructor MkDateTime

280 |   date : Date

281 |   hour : Fin 24

282 |   minute : Fin 60

283 |   second : Fin 60

284 |   subsecond : Fin 1000

285 |   offset_plus_or_minus : Bool

286 |   hour_offset : Nat

287 |   minute_offset : Fin 60

289 | second_of_day : Nat -> (Fin 24, Fin 60, Fin 60)

290 | second_of_day x =

291 |   let second = modFinNZ x 60 SIsNonZero

292 |       x = divNatNZ x 60 SIsNonZero

293 |       minute = modFinNZ x 60 SIsNonZero

294 |       x = divNatNZ x 60 SIsNonZero

295 |       hour = modFinNZ x 24 SIsNonZero

296 |   in (hour, minute, second)

299 | epoch_to_datetime : Integer -> DateTime

300 | epoch_to_datetime epoch =

301 |   let (hour, minute, second) = second_of_day $ integerToNat $ epoch `mod'` day_in_seconds'

302 |       dayno = if epoch >= 0 then epoch `div` day_in_seconds' else ((epoch + 1) `div` day_in_seconds') - 1

303 |       date = tuple_normalize_date (1970, 0, dayno)

304 |   in MkDateTime date hour minute second 0 True 0 0

307 | millisecond_epoch_to_datetime : Integer -> DateTime

308 | millisecond_epoch_to_datetime epoch =

309 |   let subsecond' = integerToNat $ epoch `mod'` 1000

310 |   in { subsecond := modFinNZ subsecond' 1000 SIsNonZero } (epoch_to_datetime $ epoch `div` 1000)

312 | datetime_to_epoch' : DateTime -> Integer

313 | datetime_to_epoch' datetime =

314 |   (days_between_dates datetime.date epoch_date) * day_in_seconds'

315 |   + (finToInteger datetime.hour * 60 * 60)

316 |   + (finToInteger datetime.minute * 60)

317 |   + (finToInteger datetime.second)

319 | millisecond_datetime_to_epoch' : DateTime -> Integer

320 | millisecond_datetime_to_epoch' datetime = (datetime_to_epoch' datetime) * 1000 + finToInteger datetime.subsecond

323 | gmt_datetime : DateTime -> DateTime

324 | gmt_datetime datetime =

325 |   let epoch = millisecond_datetime_to_epoch' datetime

326 |       offset = (1000 * 3600 * natToInteger datetime.hour_offset) + (1000 * 60 * finToInteger datetime.minute_offset)

327 |       epoch = if datetime.offset_plus_or_minus then epoch - offset else epoch + offset

328 |   in millisecond_epoch_to_datetime epoch

331 | datetime_to_epoch : DateTime -> Integer

332 | datetime_to_epoch = datetime_to_epoch' . gmt_datetime

335 | millisecond_datetime_to_epoch : DateTime -> Integer

336 | millisecond_datetime_to_epoch = millisecond_datetime_to_epoch' . gmt_datetime

339 | Show DateTime where

340 |   show datetime =

341 |     (show $ datetime.date)

342 |     <+> " "

343 |     <+> (show_fin_pad 2 datetime.hour)

344 |     <+> ":"

345 |     <+> (show_fin_pad 2 datetime.minute)

346 |     <+> ":"

347 |     <+> (show_fin_pad 2 datetime.second)

348 |     <+> "."

349 |     <+> (show_fin_pad 3 datetime.subsecond)

350 |     <+> " "

351 |     <+> (if datetime.offset_plus_or_minus then "+" else "-")

352 |     <+> (show_nat_pad 2 datetime.hour_offset)

353 |     <+> ":"

354 |     <+> (show_fin_pad 2 datetime.minute_offset)

356 | fromDigits : Num a => (Fin 10 -> a) -> List (Fin 10) -> a

357 | fromDigits f xs = foldl addDigit 0 xs

358 |   where

359 |     addDigit : a -> Fin 10 -> a

360 |     addDigit num d = 10*num + f d

362 | natFromDigits : List (Fin 10) -> Nat

363 | natFromDigits = fromDigits finToNat

365 | natFromNDigits : Monad m => Nat -> ParseT m Nat

366 | natFromNDigits n = natFromDigits . toList <$> ntimes n digit

368 | finNFromNDigits : Monad m => String -> (n : Nat) -> Nat -> ParseT m (Fin n)

369 | finNFromNDigits name bound n = do

370 |   number <- natFromNDigits n

371 |   case natToFin number bound of

372 |     Just fin => pure fin

373 |     Nothing => fail $ "invalid " <+> name <+> ": " <+> show number

376 | utc_time : Monad m => ParseT m DateTime

377 | utc_time = do

378 |   yy <- natFromDigits . toList <$> ntimes 2 digit

379 |   mm <- natFromDigits . toList <$> ntimes 2 digit

380 |   let year = if yy < 50 then 2000 + natToInteger yy else 1900 + natToInteger yy

381 |   let Just month = nat_to_month mm

382 |   | Nothing => fail $ "invalid month: " <+> show mm

383 |   FS fs_day <- finNFromNDigits "day" (S $ month_num_of_dates year month) 2

384 |   | FZ => fail "invalid day: 0"

385 |   hour <- finNFromNDigits "hour" 24 2

386 |   minute <- finNFromNDigits "minute" 60 2

387 |   second <- option 0 $ finNFromNDigits "second" 60 2

388 |   sign <- satisfy (const True)

389 |   let date = MkDate year month (FS fs_day) FSIsNonZero

390 |   let mk_date_time = MkDateTime date hour minute second 0

391 |   case sign of

392 |     'Z' => pure $ mk_date_time True 0 0

393 |     '+' => uncurry (mk_date_time True) <$> utc_time_offset

394 |     '-' => uncurry (mk_date_time False) <$> utc_time_offset

395 |     err => fail $ "unrecognized timezone sign: " <+> show err

396 |   where

397 |     utc_time_offset : ParseT m (Nat, Fin 60)

398 |     utc_time_offset = do

399 |       hh <- natFromDigits . toList <$> ntimes 2 digit

400 |       minute_off <- finNFromNDigits "minute offset" 60 2

401 |       pure (hh, minute_off)

404 | generalized_time : Monad m => ParseT m DateTime

405 | generalized_time = do

406 |   year <- natToInteger . natFromDigits . toList <$> ntimes 4 digit

407 |   mm <- natFromDigits . toList <$> ntimes 2 digit

408 |   let Just month = nat_to_month mm

409 |   | Nothing => fail $ "invalid month: " <+> show mm

411 |   FS fs_day <- finNFromNDigits "day" (S $ month_num_of_dates year month) 2

412 |   | FZ => fail "invalid day: 0"

414 |   hour <- finNFromNDigits "hour" 24 2

415 |   minute <- option 0 $ finNFromNDigits "minute" 60 2

416 |   second <- option 0 $ finNFromNDigits "second" 60 2

418 |   subsecond <- option 0 subsecond

420 |   sign <- satisfy (const True)

421 |   let date = MkDate year month (FS fs_day) FSIsNonZero

422 |   let mk_date_time = MkDateTime date hour minute second subsecond

423 |   case sign of

424 |     'Z' => pure $ mk_date_time True 0 0

425 |     '+' => uncurry (mk_date_time True) <$> utc_time_offset

426 |     '-' => uncurry (mk_date_time False) <$> utc_time_offset

427 |     err => fail $ "unrecognized timezone sign: " <+> show err

428 |   where

429 |     utc_time_offset : ParseT m (Nat, Fin 60)

430 |     utc_time_offset = do

431 |       hh <- natFromDigits . toList <$> ntimes 2 digit

432 |       minute_off <- finNFromNDigits "minute offset" 60 2

433 |       pure (hh, minute_off)

434 |     subsecond : ParseT m (Fin 1000)

435 |     subsecond = do

436 |       a <- char '.' *> natFromNDigits 1

437 |       b <- option 0 $ natFromNDigits 1

438 |       c <- option 0 $ natFromNDigits 1

439 |       case natToFin (a * 100 + b * 10 + c) 1000 of

440 |         Just x => pure x

441 |         Nothing => fail "how"

444 | parse_utc_time : String -> Either String DateTime

445 | parse_utc_time = map fst . parse utc_time

448 | parse_generalized_time : String -> Either String DateTime

449 | parse_generalized_time = map fst . parse generalized_time