0 | module IotaTime.Pattern.Scalar
  1 |
  2 | import Data.String
  3 | import Data.String.Parser
  4 | import IotaTime.Calendar
  5 | import IotaTime.Instant
  6 | import IotaTime.Pattern
  7 |
  8 | %default total
  9 |
 10 | ||| An arbitrary-precision instant encoded as nanoseconds relative to the
 11 | ||| iotaTime epoch.
 12 | public export
 13 | pInstantNanoseconds : Pattern Integer Instant
 14 | pInstantNanoseconds = MkPattern
 15 |   0
 16 |   (Right . fromNanosecondsSinceEpoch)
 17 |   (patternParsePart pSignedInteger)
 18 |   (show . toNanosecondsSinceEpoch)
 19 |
 20 | finishCalendarDays : {calendar : Type} -> {auto cal : Calendar calendar} ->
 21 |                      Integer -> Either PatternError
 22 |                        (CalendarDate calendar @{cal})
 23 | finishCalendarDays {calendar} @{cal} value =
 24 |   case choose (isValidDays {calendar} @{cal} value) of
 25 |     Left valid => Right (fromDays {calendar} @{cal} value @{valid})
 26 |     Right _ => Left (InvalidValue
 27 |       (calendarName {calendar} @{cal} ++ " day count is out of range"))
 28 |
 29 | ||| A calendar date encoded as its calendar-local day count. The expected
 30 | ||| calendar type is supplied by the pattern itself.
 31 | public export
 32 | pCalendarDays : {calendar : Type} -> {auto cal : Calendar calendar} ->
 33 |                 Pattern Integer (CalendarDate calendar @{cal})
 34 | pCalendarDays {calendar} @{cal} = MkPattern
 35 |   0
 36 |   (finishCalendarDays {calendar} @{cal})
 37 |   (patternParsePart pSignedInteger)
 38 |   (show . toDaysFor {calendar} @{cal})
 39 |
 40 | isZoneTokenCharacter : Char -> Bool
 41 | isZoneTokenCharacter value =
 42 |   value /= ' ' && value /= '\t' && value /= '\n' && value /= '\r'
 43 |
 44 | readZoneToken : List Char -> Maybe (String, Nat)
 45 | readZoneToken [] = Nothing
 46 | readZoneToken (value :: remaining) =
 47 |   if isZoneTokenCharacter value
 48 |     then go [value] 1 remaining
 49 |     else Nothing
 50 |   where
 51 |     go : List Char -> Nat -> List Char -> Maybe (String, Nat)
 52 |     go found count (value :: remaining) =
 53 |       if isZoneTokenCharacter value
 54 |         then go (value :: found) (S count) remaining
 55 |         else Just (pack (reverse found), count)
 56 |     go found count [] = Just (pack (reverse found), count)
 57 |
 58 | zoneTokenParser : PatternParser (Either PatternError (String -> String))
 59 | zoneTokenParser = Parser.P (\state =>
 60 |   let remaining = unpack
 61 |         (strSubstr state.pos (state.maxPos - state.pos) state.input)
 62 |    in case readZoneToken remaining of
 63 |         Nothing => pure (Parser.Fail state.pos "zone ID token")
 64 |         Just (value, consumed) => pure (Parser.OK (Right (const value))
 65 |           ({ pos := state.pos + cast consumed } state)))
 66 |
 67 | ||| A non-empty zone identifier containing no whitespace. This covers IANA
 68 | ||| identifiers and is directly composable with surrounding literals.
 69 | public export
 70 | pZoneIdToken : Pattern String String
 71 | pZoneIdToken = MkPattern "" Right zoneTokenParser id
 72 |
 73 | escapeZoneId : List Char -> List Char
 74 | escapeZoneId [] = []
 75 | escapeZoneId ('\\' :: remaining) = '\\' :: '\\' :: escapeZoneId remaining
 76 | escapeZoneId ('"' :: remaining) = '\\' :: '"' :: escapeZoneId remaining
 77 | escapeZoneId ('\n' :: remaining) = '\\' :: 'n' :: escapeZoneId remaining
 78 | escapeZoneId ('\r' :: remaining) = '\\' :: 'r' :: escapeZoneId remaining
 79 | escapeZoneId ('\t' :: remaining) = '\\' :: 't' :: escapeZoneId remaining
 80 | escapeZoneId (value :: remaining) = value :: escapeZoneId remaining
 81 |
 82 | readQuotedZoneId : List Char -> Maybe (String, Nat)
 83 | readQuotedZoneId ('"' :: remaining) = go [] 1 remaining
 84 |   where
 85 |     go : List Char -> Nat -> List Char -> Maybe (String, Nat)
 86 |     go [] _ ('"' :: _) = Nothing
 87 |     go found count ('"' :: _) = Just (pack (reverse found), S count)
 88 |     go found count ('\\' :: '"' :: rest) = go ('"' :: found) (count + 2) rest
 89 |     go found count ('\\' :: '\\' :: rest) = go ('\\' :: found) (count + 2) rest
 90 |     go found count ('\\' :: 'n' :: rest) = go ('\n' :: found) (count + 2) rest
 91 |     go found count ('\\' :: 'r' :: rest) = go ('\r' :: found) (count + 2) rest
 92 |     go found count ('\\' :: 't' :: rest) = go ('\t' :: found) (count + 2) rest
 93 |     go _ _ ('\\' :: _) = Nothing
 94 |     go _ _ ('\n' :: _) = Nothing
 95 |     go _ _ ('\r' :: _) = Nothing
 96 |     go _ _ ('\t' :: _) = Nothing
 97 |     go found count (value :: rest) = go (value :: found) (S count) rest
 98 |     go _ _ [] = Nothing
 99 | readQuotedZoneId _ = Nothing
100 |
101 | quotedZoneIdParser : PatternParser (Either PatternError (String -> String))
102 | quotedZoneIdParser = Parser.P (\state =>
103 |   let remaining = unpack
104 |         (strSubstr state.pos (state.maxPos - state.pos) state.input)
105 |    in case readQuotedZoneId remaining of
106 |         Nothing => pure (Parser.Fail state.pos "quoted zone ID")
107 |         Just (value, consumed) => pure (Parser.OK (Right (const value))
108 |           ({ pos := state.pos + cast consumed } state)))
109 |
110 | ||| A quoted, escaped, non-empty zone identifier. This form represents Windows
111 | ||| identifiers containing spaces as well as quote, backslash, and whitespace
112 | ||| characters when an application needs them.
113 | public export
114 | pZoneIdQuoted : Pattern String String
115 | pZoneIdQuoted = MkPattern
116 |   ""
117 |   Right
118 |   quotedZoneIdParser
119 |   (\value => "\"" ++ pack (escapeZoneId (unpack value)) ++ "\"")