
   0 | module IotaTime.Pattern.LocalTime
   1 | 
   2 | import Data.So
   3 | import Data.String.Parser
   4 | import IotaTime.Locale
   5 | import IotaTime.LocalTime
   6 | import IotaTime.Internal.Text
   7 | import IotaTime.Pattern
   8 | 
   9 | %default total
  10 | 
  11 | ||| Intermediate fields accumulated while parsing a local time.
  12 | export
  13 | record TimeFieldsRep where
  14 |   constructor MkTimeFields
  15 |   parsedHour : Integer
  16 |   parsedMinute : Integer
  17 |   parsedSecond : Integer
  18 |   parsedNanosecond : Integer
  19 | 
  20 | ||| Opaque intermediate state used by local-time patterns.
  21 | public export
  22 | TimeFields : Type
  23 | TimeFields = TimeFieldsRep
  24 | 
  25 | ||| Seed omitted hour, minute, second, and nanosecond fields for `parseWith`.
  26 | ||| Parsed fields replace the corresponding seed values; final local-time
  27 | ||| validation still occurs after parsing.
  28 | public export
  29 | timeFields : (hour : Integer) -> (minute : Integer) -> (second : Integer) ->
  30 |              (nanosecond : Integer) -> TimeFields
  31 | timeFields = MkTimeFields
  32 | 
  33 | initialTimeFields : TimeFields
  34 | initialTimeFields = timeFields 0 0 0 0
  35 | 
  36 | finishTime : TimeFields -> Either PatternError LocalTime
  37 | finishTime fields = case refineLocalTime
  38 |   fields.parsedHour fields.parsedMinute fields.parsedSecond fields.parsedNanosecond of
  39 |     Left _ => Left (InvalidValue "invalid local time")
  40 |     Right value => Right value
  41 | 
  42 | setHour : Integer -> TimeFields -> TimeFields
  43 | setHour value fields = { parsedHour := value } fields
  44 | 
  45 | setMinute : Integer -> TimeFields -> TimeFields
  46 | setMinute value fields = { parsedMinute := value } fields
  47 | 
  48 | setSecond : Integer -> TimeFields -> TimeFields
  49 | setSecond value fields = { parsedSecond := value } fields
  50 | 
  51 | setNanosecond : Integer -> TimeFields -> TimeFields
  52 | setNanosecond value fields = { parsedNanosecond := value } fields
  53 | 
  54 | timeHour : LocalTime -> Integer
  55 | timeHour = hourValue . hour
  56 | 
  57 | timeMinute : LocalTime -> Integer
  58 | timeMinute = minuteValue . minute
  59 | 
  60 | timeSecond : LocalTime -> Integer
  61 | timeSecond = secondValue . second
  62 | 
  63 | timeNanosecond : LocalTime -> Integer
  64 | timeNanosecond = nanosecondValue . nanosecond
  65 | 
  66 | timeField : (LocalTime -> Integer) -> (Integer -> TimeFields -> TimeFields) ->
  67 |             (width : Nat) -> (maximumWidth : Nat) ->
  68 |             (minimum : Integer) -> (maximum : Integer) ->
  69 |             Pattern TimeFields LocalTime
  70 | timeField getter setter width maximumWidth minimum maximum = MkPattern
  71 |   initialTimeFields
  72 |   finishTime
  73 |   (numberUpdatePart setter width maximumWidth minimum maximum)
  74 |   (zeroPadInteger width . getter)
  75 | 
  76 | ||| A 24-hour field with the requested output width and up to two input digits.
  77 | public export
  78 | phour : Nat -> Pattern TimeFields LocalTime
  79 | phour width = timeField timeHour setHour width 2 0 23
  80 | 
  81 | ||| A two-digit 24-hour field in the range 00 through 23.
  82 | public export
  83 | pHH : Pattern TimeFields LocalTime
  84 | pHH = phour 2
  85 | 
  86 | setTwelveHour : Integer -> TimeFields -> TimeFields
  87 | setTwelveHour value fields =
  88 |   { parsedHour := 12 * (fields.parsedHour `div` 12) + value `mod` 12 } fields
  89 | 
  90 | formatTwelveHour : LocalTime -> Integer
  91 | formatTwelveHour value =
  92 |   let folded = timeHour value `mod` 12
  93 |    in if folded == 0 then 12 else folded
  94 | 
  95 | ||| A two-digit 12-hour clock field in the range 01 through 12.
  96 | public export
  97 | phh : Pattern TimeFields LocalTime
  98 | phh = MkPattern
  99 |   initialTimeFields
 100 |   finishTime
 101 |   (numberUpdatePart setTwelveHour 2 2 1 12)
 102 |   (zeroPadInteger 2 . formatTwelveHour)
 103 | 
 104 | ||| A space-padded two-character 12-hour clock field.
 105 | public export
 106 | phhSpace : Pattern TimeFields LocalTime
 107 | phhSpace = MkPattern
 108 |   initialTimeFields
 109 |   finishTime
 110 |   (spaceNumberUpdatePart setTwelveHour 2 1 12)
 111 |   (padIntegerWith ' ' 2 . formatTwelveHour)
 112 | 
 113 | ||| A minute field with the requested output width and up to two input digits.
 114 | public export
 115 | pminute : Nat -> Pattern TimeFields LocalTime
 116 | pminute width = timeField timeMinute setMinute width 2 0 59
 117 | 
 118 | ||| A two-digit minute field in the range 00 through 59.
 119 | public export
 120 | pmm : Pattern TimeFields LocalTime
 121 | pmm = pminute 2
 122 | 
 123 | ||| A second field with the requested output width and up to two input digits.
 124 | public export
 125 | psecond : Nat -> Pattern TimeFields LocalTime
 126 | psecond width = timeField timeSecond setSecond width 2 0 59
 127 | 
 128 | ||| A two-digit second field in the range 00 through 59.
 129 | public export
 130 | pss : Pattern TimeFields LocalTime
 131 | pss = psecond 2
 132 | 
 133 | pow10 : Nat -> Integer
 134 | pow10 Z = 1
 135 | pow10 (S exponent) = 10 * pow10 exponent
 136 | 
 137 | ||| Whether a fractional-second width is representable at nanosecond precision.
 138 | public export
 139 | isValidFractionWidth : Nat -> Bool
 140 | isValidFractionWidth width = width >= 1 && width <= 9
 141 | 
 142 | ||| A fixed-width fractional-second field with one through nine digits.
 143 | |||
 144 | ||| The erased proof rejects unsupported widths at compile time.
 145 | public export
 146 | pfrac : (width : Nat) -> {auto 0 valid : So (isValidFractionWidth width)} ->
 147 |         Pattern TimeFields LocalTime
 148 | pfrac width =
 149 |   let scale = pow10 (9 `minus` width)
 150 |       maximum = pow10 width - 1
 151 |    in MkPattern
 152 |         initialTimeFields
 153 |         finishTime
 154 |         (numberUpdatePart (\value => setNanosecond (value * scale))
 155 |           width width 0 maximum)
 156 |         (zeroPadInteger width . (`div` scale) . timeNanosecond)
 157 | 
 158 | setPeriod : Bool -> TimeFields -> TimeFields
 159 | setPeriod isPm fields =
 160 |   { parsedHour := fields.parsedHour `mod` 12 + if isPm then 12 else 0 } fields
 161 | 
 162 | periodPattern : String -> String -> Pattern TimeFields LocalTime
 163 | periodPattern am pm = MkPattern
 164 |   initialTimeFields
 165 |   finishTime
 166 |   (namedUpdatePart [(pm, True), (am, False)] setPeriod)
 167 |   (\value => if timeHour value >= 12 then pm else am)
 168 | 
 169 | ||| A 12-hour period field using the supplied AM and PM labels.
 170 | public export
 171 | pPeriod : (String, String) -> Pattern TimeFields LocalTime
 172 | pPeriod (am, pm) = periodPattern am pm
 173 | 
 174 | ||| The single-letter `A` or `P` period field.
 175 | public export
 176 | pp : Pattern TimeFields LocalTime
 177 | pp = periodPattern "A" "P"
 178 | 
 179 | ||| The English `AM` or `PM` period field.
 180 | public export
 181 | ppp : Pattern TimeFields LocalTime
 182 | ppp = periodPattern "AM" "PM"
 183 | 
 184 | ||| A period field using a locale's AM and PM labels.
 185 | public export
 186 | ppp' : Locale -> Pattern TimeFields LocalTime
 187 | ppp' locale = periodPattern (amName locale) (pmName locale)
 188 | 
 189 | ||| The short `HH:mm` local-time pattern.
 190 | public export
 191 | pt : Pattern TimeFields LocalTime
 192 | pt = (pHH <% char ':') <+> pmm
 193 | 
 194 | ||| The long `HH:mm:ss` local-time pattern.
 195 | public export
 196 | pT : Pattern TimeFields LocalTime
 197 | pT = ((pHH <% char ':') <+> (pmm <% char ':')) <+> pss
 198 | 
 199 | ||| The round-trip `HH:mm:ss.fffffffff` local-time pattern.
 200 | public export
 201 | pr : Pattern TimeFields LocalTime
 202 | pr = (pT <% char '.') <+> pfrac 9
 203 |