
   0 | module IotaTime.Pattern.CalendarDate
   1 | 
   2 | import Data.String.Parser
   3 | import Data.Vect
   4 | import IotaTime.Pattern
   5 | import IotaTime.Locale
   6 | import IotaTime.Calendar
   7 | import IotaTime.Calendar.Gregorian
   8 | import IotaTime.Internal.Text
   9 | import IotaTime.Pattern.Calendar
  10 | 
  11 | %default total
  12 | 
  13 | ||| Intermediate fields accumulated while parsing a calendar date.
  14 | export
  15 | record DateFieldsRep where
  16 |   constructor MkDateFields
  17 |   parsedYear : Integer
  18 |   parsedMonth : Integer
  19 |   parsedDay : Integer
  20 |   {default Nothing parsedWeekday : Maybe (Fin 7)}
  21 | 
  22 | ||| Opaque intermediate state used by calendar-date patterns.
  23 | public export
  24 | DateFields : Type
  25 | DateFields = DateFieldsRep
  26 | 
  27 | ||| Seed omitted year, month, and day fields for `parseWith`.
  28 | ||| Parsed fields replace the corresponding seed values; final calendar-date
  29 | ||| validation still occurs after parsing.
  30 | public export
  31 | dateFields : (year : Integer) -> (month : Integer) -> (day : Integer) ->
  32 |              DateFields
  33 | dateFields year month day = MkDateFields year month day
  34 | 
  35 | initialDateFields : DateFields
  36 | initialDateFields = dateFields 2000 3 1
  37 | 
  38 | monthFromInteger : Integer -> Month
  39 | monthFromInteger 1 = January
  40 | monthFromInteger 2 = February
  41 | monthFromInteger 3 = March
  42 | monthFromInteger 4 = April
  43 | monthFromInteger 5 = May
  44 | monthFromInteger 6 = June
  45 | monthFromInteger 7 = July
  46 | monthFromInteger 8 = August
  47 | monthFromInteger 9 = September
  48 | monthFromInteger 10 = October
  49 | monthFromInteger 11 = November
  50 | monthFromInteger _ = December
  51 | 
  52 | finishDate : {calendar : Type} ->
  53 |              {auto patterned : CalendarPattern calendar} ->
  54 |              DateFields -> Either PatternError (CalendarDate calendar)
  55 | finishDate {calendar} @{patterned} fields = do
  56 |   date <- refinePatternDate {calendar} @{patterned}
  57 |     fields.parsedYear fields.parsedMonth fields.parsedDay
  58 |   case fields.parsedWeekday of
  59 |     Nothing => Right date
  60 |     Just expected =>
  61 |       if patternWeekdayIndex {calendar} @{patterned} date == expected
  62 |         then Right date
  63 |         else Left (InvalidValue "weekday does not match date")
  64 | 
  65 | dateField : {calendar : Type} ->
  66 |             {auto patterned : CalendarPattern calendar} ->
  67 |             (CalendarDate calendar -> Integer) ->
  68 |             (Integer -> DateFields -> DateFields) ->
  69 |             (width : Nat) -> (maximumWidth : Nat) ->
  70 |             (minimum : Integer) -> (maximum : Integer) ->
  71 |             Pattern DateFields (CalendarDate calendar)
  72 | dateField getter setter width maximumWidth minimum maximum = MkPattern
  73 |   initialDateFields
  74 |   finishDate
  75 |   (numberUpdatePart setter width maximumWidth minimum maximum)
  76 |   (zeroPadInteger width . getter)
  77 | 
  78 | setYearField : Integer -> DateFields -> DateFields
  79 | setYearField value fields = { parsedYear := value } fields
  80 | 
  81 | setMonthField : Integer -> DateFields -> DateFields
  82 | setMonthField value fields = { parsedMonth := value } fields
  83 | 
  84 | setDayField : Integer -> DateFields -> DateFields
  85 | setDayField value fields = { parsedDay := value } fields
  86 | 
  87 | setWeekdayField : Fin 7 -> DateFields -> DateFields
  88 | setWeekdayField value fields = { parsedWeekday := Just value } fields
  89 | 
  90 | setMonth : Month -> DateFields -> DateFields
  91 | setMonth value fields = { parsedMonth := monthNumber value } fields
  92 | 
  93 | calendarYear : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
  94 |                CalendarDate calendar -> Integer
  95 | calendarYear date = yearValue (yearFor {calendar} date)
  96 | 
  97 | calendarMonthIndex : {calendar : Type} ->
  98 |                      {auto patterned : CalendarPattern calendar} ->
  99 |                      CalendarDate calendar ->
 100 |                      Fin (patternMonthCount {calendar} @{patterned})
 101 | calendarMonthIndex {calendar} @{patterned} =
 102 |   patternMonthIndex {calendar} @{patterned}
 103 | 
 104 | calendarMonth : {calendar : Type} ->
 105 |                 {auto patterned : CalendarPattern calendar} ->
 106 |                 CalendarDate calendar -> Integer
 107 | calendarMonth {calendar} @{patterned} date =
 108 |   cast (finToNat (calendarMonthIndex {calendar} @{patterned} date)) + 1
 109 | 
 110 | calendarDay : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 111 |               CalendarDate calendar -> Integer
 112 | calendarDay date = dayOfMonthValue (dayFor {calendar} date)
 113 | 
 114 | gregorianMonths : Vect 12 Month
 115 | gregorianMonths =
 116 |   [ January, February, March, April, May, June
 117 |   , July, August, September, October, November, December
 118 |   ]
 119 | 
 120 | gregorianWeekdays : Vect 7 DayOfWeek
 121 | gregorianWeekdays =
 122 |   [ Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday ]
 123 | 
 124 | abbreviate : String -> String
 125 | abbreviate = substr 0 3
 126 | 
 127 | indexedNames : Integer -> Vect size String -> List (String, Integer)
 128 | indexedNames _ [] = []
 129 | indexedNames value (name :: names) =
 130 |   (name, value) :: indexedNames (value + 1) names
 131 | 
 132 | indexedFinNames : Vect size String -> List (String, Fin size)
 133 | indexedFinNames [] = []
 134 | indexedFinNames (name :: names) =
 135 |   (name, FZ) :: map (map FS) (indexedFinNames names)
 136 | 
 137 | calendarMonthNamePattern : {calendar : Type} ->
 138 |   {auto patterned : CalendarPattern calendar} ->
 139 |   Vect (patternMonthCount {calendar} @{patterned}) String ->
 140 |   Pattern DateFields (CalendarDate calendar)
 141 | calendarMonthNamePattern {calendar} @{patterned} names = MkPattern
 142 |   initialDateFields
 143 |   finishDate
 144 |   (namedUpdatePart (indexedNames 1 names) setMonthField)
 145 |   (\date => index (calendarMonthIndex {calendar} @{patterned} date) names)
 146 | 
 147 | weekdayNames : Vect 7 String
 148 | weekdayNames =
 149 |   [ "Sunday", "Monday", "Tuesday", "Wednesday"
 150 |   , "Thursday", "Friday", "Saturday"
 151 |   ]
 152 | 
 153 | weekdayAbbreviations : Vect 7 String
 154 | weekdayAbbreviations =
 155 |   [ "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat" ]
 156 | 
 157 | calendarDayNamePattern : {calendar : Type} ->
 158 |   {auto patterned : CalendarPattern calendar} ->
 159 |   Vect 7 String -> Pattern DateFields (CalendarDate calendar)
 160 | calendarDayNamePattern {calendar} @{patterned} names = MkPattern
 161 |   initialDateFields
 162 |   finishDate
 163 |   (namedConsumePart (toList names))
 164 |   (\date => index (patternWeekdayIndex {calendar} @{patterned} date) names)
 165 | 
 166 | verifiedCalendarDayNamePattern : {calendar : Type} ->
 167 |   {auto patterned : CalendarPattern calendar} ->
 168 |   Vect 7 String -> Pattern DateFields (CalendarDate calendar)
 169 | verifiedCalendarDayNamePattern {calendar} @{patterned} names = MkPattern
 170 |   initialDateFields
 171 |   finishDate
 172 |   (namedUpdatePart (indexedFinNames names) setWeekdayField)
 173 |   (patternFormatPart (calendarDayNamePattern {calendar} @{patterned} names))
 174 | 
 175 | englishMonthNames : Vect 12 String
 176 | englishMonthNames = map show gregorianMonths
 177 | 
 178 | englishMonthAbbreviations : Vect 12 String
 179 | englishMonthAbbreviations = map abbreviate englishMonthNames
 180 | 
 181 | englishWeekdayNames : Vect 7 String
 182 | englishWeekdayNames = map show gregorianWeekdays
 183 | 
 184 | englishWeekdayAbbreviations : Vect 7 String
 185 | englishWeekdayAbbreviations = map abbreviate englishWeekdayNames
 186 | 
 187 | ||| A numeric year field with the requested output width and up to four input digits.
 188 | public export
 189 | pyear : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 190 |   Nat -> Pattern DateFields (CalendarDate calendar)
 191 | pyear width = dateField calendarYear setYearField width 4 0 9999
 192 | 
 193 | ||| A four-digit numeric year field.
 194 | public export
 195 | pyyyy : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 196 |   Pattern DateFields (CalendarDate calendar)
 197 | pyyyy = pyear 4
 198 | 
 199 | inferTwoDigitYear : Integer -> Integer -> Integer
 200 | inferTwoDigitYear template value =
 201 |   let base = (template `div` 100) * 100 + value
 202 |       adjustment = (template - base + 50) `div` 100
 203 |    in base + adjustment * 100
 204 | 
 205 | ||| A two-digit year field resolved to the century nearest the initial year.
 206 | public export
 207 | pyy : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 208 |   Pattern DateFields (CalendarDate calendar)
 209 | pyy = MkPattern
 210 |   initialDateFields
 211 |   finishDate
 212 |   (numberUpdatePart
 213 |     (\value, fields =>
 214 |       { parsedYear := inferTwoDigitYear fields.parsedYear value } fields)
 215 |     2 2 0 99)
 216 |   (zeroPadInteger 2 . (`mod` 100) . calendarYear)
 217 | 
 218 | ||| A numeric month field bounded by the selected calendar's month count.
 219 | public export
 220 | pmonthNum : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 221 |     Nat -> Pattern DateFields (CalendarDate calendar)
 222 | pmonthNum {calendar} @{patterned} width =
 223 |   dateField (calendarMonth {calendar} @{patterned}) setMonthField
 224 |     width 2 1 (cast (patternMonthCount {calendar} @{patterned}))
 225 | 
 226 | ||| A two-digit numeric month field.
 227 | public export
 228 | pMM : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 229 |   Pattern DateFields (CalendarDate calendar)
 230 | pMM = pmonthNum 2
 231 | 
 232 | ||| A calendar month field using supplied names in calendar order.
 233 | |||
 234 | ||| Parsing tries non-empty names longest-first. Equal or duplicate names retain
 235 | ||| table order and select the first matching month. Formatting uses the supplied
 236 | ||| name verbatim, including an empty name.
 237 | public export
 238 | pMonthName : {default Gregorian calendar : Type} ->
 239 |              {auto patterned : CalendarPattern calendar} ->
 240 |              {size : Nat} ->
 241 |              (names : Vect size String) ->
 242 |              {auto 0 complete : size =
 243 |                patternMonthCount {calendar} @{patterned}} ->
 244 |              Pattern DateFields (CalendarDate calendar)
 245 | pMonthName {complete = Refl} names = calendarMonthNamePattern names
 246 | 
 247 | ||| A calendar-specific full month-name field.
 248 | public export
 249 | pMMMM : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 250 |   Pattern DateFields (CalendarDate calendar)
 251 | pMMMM {calendar} @{patterned} = calendarMonthNamePattern
 252 |   (patternMonthNames {calendar} @{patterned})
 253 | 
 254 | ||| A calendar-specific abbreviated month-name field.
 255 | public export
 256 | pMMM : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 257 |   Pattern DateFields (CalendarDate calendar)
 258 | pMMM {calendar} @{patterned} = calendarMonthNamePattern
 259 |   (patternMonthAbbreviations {calendar} @{patterned})
 260 | 
 261 | ||| A numeric day-of-month field with the requested width.
 262 | public export
 263 | pday : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 264 |   Nat -> Pattern DateFields (CalendarDate calendar)
 265 | pday width = dateField calendarDay setDayField width 2 1 31
 266 | 
 267 | ||| A two-digit day-of-month field.
 268 | public export
 269 | pdd : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 270 |   Pattern DateFields (CalendarDate calendar)
 271 | pdd = pday 2
 272 | 
 273 | ||| A two-character day-of-month field padded with a leading space.
 274 | public export
 275 | pdaySpace : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 276 |             Pattern DateFields (CalendarDate calendar)
 277 | pdaySpace = MkPattern
 278 |   initialDateFields
 279 |   finishDate
 280 |   (spaceNumberUpdatePart setDayField 2 1 31)
 281 |   (\date => let shown = show (calendarDay date) in
 282 |     if length (unpack shown) < 2 then " " ++ shown else shown)
 283 | 
 284 | ||| A calendar weekday field using supplied Sunday-first names.
 285 | |||
 286 | ||| Parsing consumes and validates a name structurally; the date fields determine
 287 | ||| the resulting date. Non-empty names are tried longest-first; formatting uses
 288 | ||| the supplied name verbatim.
 289 | public export
 290 | pDayName : {default Gregorian calendar : Type} ->
 291 |            {auto patterned : CalendarPattern calendar} ->
 292 |            Vect 7 String -> Pattern DateFields (CalendarDate calendar)
 293 | pDayName = calendarDayNamePattern
 294 | 
 295 | ||| A calendar weekday field that rejects a parsed name inconsistent with the
 296 | ||| resulting date. Names are supplied in Sunday-first order.
 297 | public export
 298 | pVerifiedDayName : {default Gregorian calendar : Type} ->
 299 |                    {auto patterned : CalendarPattern calendar} ->
 300 |                    Vect 7 String -> Pattern DateFields (CalendarDate calendar)
 301 | pVerifiedDayName = verifiedCalendarDayNamePattern
 302 | 
 303 | ||| A full English weekday-name field for the selected calendar.
 304 | public export
 305 | pdddd : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 306 |   Pattern DateFields (CalendarDate calendar)
 307 | pdddd = calendarDayNamePattern weekdayNames
 308 | 
 309 | ||| An abbreviated English weekday-name field for the selected calendar.
 310 | public export
 311 | pddd : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 312 |   Pattern DateFields (CalendarDate calendar)
 313 | pddd = calendarDayNamePattern weekdayAbbreviations
 314 | 
 315 | ||| A full English weekday-name field verified against the resulting date.
 316 | public export
 317 | pddddVerified : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 318 |   Pattern DateFields (CalendarDate calendar)
 319 | pddddVerified {calendar} =
 320 |   pVerifiedDayName {calendar} englishWeekdayNames
 321 | 
 322 | ||| An abbreviated English weekday-name field verified against the resulting date.
 323 | public export
 324 | pdddVerified : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 325 |   Pattern DateFields (CalendarDate calendar)
 326 | pdddVerified {calendar} =
 327 |   pVerifiedDayName {calendar} englishWeekdayAbbreviations
 328 | 
 329 | localeMonthNames : {calendar : Type} ->
 330 |   {auto patterned : CalendarPattern calendar} ->
 331 |   Locale -> Vect (patternMonthCount {calendar} @{patterned}) String
 332 | localeMonthNames {calendar} @{patterned} locale =
 333 |   case patternMonthNameSource {calendar} @{patterned} of
 334 |     GregorianLocaleMonthNames countIsTwelve =>
 335 |       replace {p = \monthCount => Vect monthCount String}
 336 |         (sym countIsTwelve) (monthNames locale)
 337 |     CanonicalCalendarMonthNames => patternMonthNames {calendar} @{patterned}
 338 | 
 339 | localeMonthAbbreviations : {calendar : Type} ->
 340 |   {auto patterned : CalendarPattern calendar} ->
 341 |   Locale -> Vect (patternMonthCount {calendar} @{patterned}) String
 342 | localeMonthAbbreviations {calendar} @{patterned} locale =
 343 |   case patternMonthNameSource {calendar} @{patterned} of
 344 |     GregorianLocaleMonthNames countIsTwelve =>
 345 |       replace {p = \monthCount => Vect monthCount String}
 346 |         (sym countIsTwelve) (monthNamesShort locale)
 347 |     CanonicalCalendarMonthNames =>
 348 |       patternMonthAbbreviations {calendar} @{patterned}
 349 | 
 350 | ||| A full month-name field using locale names when the selected calendar
 351 | ||| shares Gregorian month identities, and canonical names otherwise.
 352 | public export
 353 | pMMMM' : {default Gregorian calendar : Type} ->
 354 |          {auto patterned : CalendarPattern calendar} ->
 355 |    Locale -> Pattern DateFields (CalendarDate calendar)
 356 | pMMMM' {calendar} @{patterned} locale = calendarMonthNamePattern
 357 |   (localeMonthNames {calendar} @{patterned} locale)
 358 | 
 359 | ||| An abbreviated month-name field using locale names when the selected
 360 | ||| calendar shares Gregorian month identities, and canonical names otherwise.
 361 | public export
 362 | pMMM' : {default Gregorian calendar : Type} ->
 363 |   {auto patterned : CalendarPattern calendar} ->
 364 |   Locale -> Pattern DateFields (CalendarDate calendar)
 365 | pMMM' {calendar} @{patterned} locale = calendarMonthNamePattern
 366 |   (localeMonthAbbreviations {calendar} @{patterned} locale)
 367 | 
 368 | ||| A full locale weekday-name field for the selected calendar.
 369 | public export
 370 | pdddd' : {default Gregorian calendar : Type} ->
 371 |          {auto patterned : CalendarPattern calendar} ->
 372 |    Locale -> Pattern DateFields (CalendarDate calendar)
 373 | pdddd' {calendar} locale = pDayName {calendar} (dayNames locale)
 374 | 
 375 | ||| An abbreviated locale weekday-name field for the selected calendar.
 376 | public export
 377 | pddd' : {default Gregorian calendar : Type} ->
 378 |   {auto patterned : CalendarPattern calendar} ->
 379 |   Locale -> Pattern DateFields (CalendarDate calendar)
 380 | pddd' {calendar} locale = pDayName {calendar} (dayNamesShort locale)
 381 | 
 382 | ||| A full locale weekday-name field verified against the resulting date.
 383 | public export
 384 | pddddVerified' : {default Gregorian calendar : Type} ->
 385 |                  {auto patterned : CalendarPattern calendar} ->
 386 |                  Locale -> Pattern DateFields (CalendarDate calendar)
 387 | pddddVerified' {calendar} locale =
 388 |   pVerifiedDayName {calendar} (dayNames locale)
 389 | 
 390 | ||| An abbreviated locale weekday-name field verified against the resulting date.
 391 | public export
 392 | pdddVerified' : {default Gregorian calendar : Type} ->
 393 |                 {auto patterned : CalendarPattern calendar} ->
 394 |                 Locale -> Pattern DateFields (CalendarDate calendar)
 395 | pdddVerified' {calendar} locale =
 396 |   pVerifiedDayName {calendar} (dayNamesShort locale)
 397 | 
 398 | ||| The numeric `dd/MM/yyyy` date pattern.
 399 | public export
 400 | pd : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 401 |   Pattern DateFields (CalendarDate calendar)
 402 | pd = ((pdd <% char '/') <+> (pMM <% char '/')) <+> pyyyy
 403 | 
 404 | ||| The long `weekday, dd month yyyy` date pattern.
 405 | public export
 406 | pD : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 407 |   Pattern DateFields (CalendarDate calendar)
 408 | pD = (((pdddd <% string ", ") <+> (pdd <% char ' ')) <+>
 409 |   (pMMMM <% char ' ')) <+> pyyyy
 410 | 
 411 | ||| The ISO-style `yyyy-MM-dd` date pattern.
 412 | public export
 413 | pR : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 414 |   Pattern DateFields (CalendarDate calendar)
 415 | pR = ((pyyyy <% char '-') <+> (pMM <% char '-')) <+> pdd
 416 | 
 417 | ||| The `month dd` pattern without a year field.
 418 | public export
 419 | pmonthDay : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 420 |   Pattern DateFields (CalendarDate calendar)
 421 | pmonthDay = (pMMMM <% char ' ') <+> pdd
 422 | 
 423 | ||| The `yyyy month` pattern without a day field.
 424 | public export
 425 | pyearMonth : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 426 |   Pattern DateFields (CalendarDate calendar)
 427 | pyearMonth = (pyyyy <% char ' ') <+> pMMMM
 428 |