0 | module IotaTime.Pattern.Duration
  1 |
  2 | import Data.String
  3 | import Data.String.Parser
  4 | import IotaTime.Duration
  5 | import IotaTime.Internal.Text
  6 | import IotaTime.Pattern
  7 |
  8 | %default total
  9 |
 10 | digitValue : Char -> Integer
 11 | digitValue value = cast value - cast '0'
 12 |
 13 | readDayDigits : Integer -> List Char ->
 14 |                 Maybe (Integer, Nat, List Char)
 15 | readDayDigits value (digit :: rest) = if isDigit digit
 16 |   then readMore (value * 10 + digitValue digit) 1 rest
 17 |   else Nothing
 18 |   where
 19 |     readMore : Integer -> Nat -> List Char ->
 20 |                Maybe (Integer, Nat, List Char)
 21 |     readMore value count (digit :: rest) = if isDigit digit
 22 |       then readMore (value * 10 + digitValue digit) (S count) rest
 23 |       else Just (value, count, digit :: rest)
 24 |     readMore value count [] = Just (value, count, [])
 25 | readDayDigits value [] = Nothing
 26 |
 27 | readTwoDigits : List Char -> Maybe (Integer, List Char)
 28 | readTwoDigits (tens :: units :: rest) =
 29 |   if isDigit tens && isDigit units
 30 |     then Just (digitValue tens * 10 + digitValue units, rest)
 31 |     else Nothing
 32 | readTwoDigits _ = Nothing
 33 |
 34 | readNineDigits : List Char -> Maybe (Integer, List Char)
 35 | readNineDigits = go 9 0
 36 |   where
 37 |     go : Nat -> Integer -> List Char -> Maybe (Integer, List Char)
 38 |     go Z value rest = Just (value, rest)
 39 |     go (S count) value (digit :: rest) = if isDigit digit
 40 |       then go count (value * 10 + digitValue digit) rest
 41 |       else Nothing
 42 |     go (S count) value [] = Nothing
 43 |
 44 | record DurationParts where
 45 |   constructor MkDurationParts
 46 |   consumed : Nat
 47 |   negative : Bool
 48 |   days : Integer
 49 |   hours : Integer
 50 |   minutes : Integer
 51 |   seconds : Integer
 52 |   nanoseconds : Integer
 53 |
 54 | splitSign : List Char -> (Bool, Nat, List Char)
 55 | splitSign ('-' :: rest) = (True, 1, rest)
 56 | splitSign values = (False, 0, values)
 57 |
 58 | parseDurationParts : Bool -> List Char -> Maybe DurationParts
 59 | parseDurationParts withFraction values =
 60 |   let (negative, signWidth, unsigned) = splitSign values in
 61 |   do
 62 |     (days, dayWidth, ':' :: afterDays) <- readDayDigits 0 unsigned
 63 |       | _ => Nothing
 64 |     (hours, ':' :: afterHours) <- readTwoDigits afterDays
 65 |       | _ => Nothing
 66 |     (minutes, ':' :: afterMinutes) <- readTwoDigits afterHours
 67 |       | _ => Nothing
 68 |     (seconds, afterSeconds) <- readTwoDigits afterMinutes
 69 |     if minutes > 59 || seconds > 59
 70 |       then Nothing
 71 |       else if withFraction
 72 |         then case afterSeconds of
 73 |           '.' :: fraction => do
 74 |             (nanoseconds, rest) <- readNineDigits fraction
 75 |             let used = signWidth + dayWidth + 1 + 2 + 1 + 2 + 1 + 2 + 1 + 9
 76 |             Just (MkDurationParts used negative days hours minutes seconds
 77 |               nanoseconds)
 78 |           _ => Nothing
 79 |         else
 80 |           let used = signWidth + dayWidth + 1 + 2 + 1 + 2 + 1 + 2 in
 81 |           Just (MkDurationParts used negative days hours minutes seconds 0)
 82 |
 83 | partsDuration : DurationParts -> Duration
 84 | partsDuration parts =
 85 |   let magnitude =
 86 |         ((((parts.days * 24 + parts.hours) * 60 + parts.minutes) * 60 +
 87 |           parts.seconds) * 1000000000) + parts.nanoseconds
 88 |    in fromNanoseconds (if parts.negative then negate magnitude else magnitude)
 89 |
 90 | durationParser : Bool -> PatternParser (Either PatternError (Duration -> Duration))
 91 | durationParser withFraction = Parser.P (\state =>
 92 |   let remaining = strSubstr state.pos (state.maxPos - state.pos) state.input in
 93 |   case parseDurationParts withFraction (unpack remaining) of
 94 |     Nothing => pure (Parser.Fail state.pos "duration")
 95 |     Just parts => pure (Parser.OK (Right (const (partsDuration parts)))
 96 |       ({ pos := state.pos + cast parts.consumed } state)))
 97 |
 98 | renderDuration : Bool -> Duration -> String
 99 | renderDuration withFraction value =
100 |   let totalNanoseconds = toDurationNanoseconds value
101 |       magnitude = abs totalNanoseconds
102 |       totalSeconds = magnitude `div` 1000000000
103 |       nanoseconds = magnitude `mod` 1000000000
104 |       seconds = totalSeconds `mod` 60
105 |       totalMinutes = totalSeconds `div` 60
106 |       minutes = totalMinutes `mod` 60
107 |       totalHours = totalMinutes `div` 60
108 |       hours = totalHours `mod` 24
109 |       days = totalHours `div` 24
110 |       fraction = if withFraction
111 |         then "." ++ zeroPadInteger 9 nanoseconds
112 |         else ""
113 |    in (if totalNanoseconds < 0 then "-" else "") ++ show days ++ ":" ++
114 |       zeroPadInteger 2 hours ++ ":" ++ zeroPadInteger 2 minutes ++ ":" ++
115 |       zeroPadInteger 2 seconds ++ fraction
116 |
117 | durationPattern : Bool -> Pattern Duration Duration
118 | durationPattern withFraction = MkPattern
119 |   zeroDuration
120 |   Right
121 |   (durationParser withFraction)
122 |   (renderDuration withFraction)
123 |
124 | ||| A signed duration rendered as [-]D:HH:mm:ss.
125 | public export
126 | pDuration : Pattern Duration Duration
127 | pDuration = durationPattern False
128 |
129 | ||| A signed duration rendered as [-]D:HH:mm:ss.fffffffff.
130 | public export
131 | pDurationNano : Pattern Duration Duration
132 | pDurationNano = durationPattern True