
   0 | module IotaTime.Pattern
   1 | 
   2 | import Data.List
   3 | import Data.String.Parser
   4 | import Data.String
   5 | 
   6 | %default total
   7 | 
   8 | ||| A failure encountered while parsing or refining a patterned value.
   9 | public export
  10 | data PatternError
  11 |   = UnexpectedEnd Integer String
  12 |   | UnexpectedCharacter Integer String Char
  13 |   | InvalidNumber Integer String
  14 |   | ValueOutOfRange String Integer Integer Integer
  15 |   | TrailingInput Integer String
  16 |   | InvalidValue String
  17 | 
  18 | public export
  19 | PatternParser : Type -> Type
  20 | PatternParser = Parser.Parser
  21 | 
  22 | ||| A bidirectional textual representation of a value.
  23 | |||
  24 | ||| `state` accumulates fields during parsing. `finish` validates that state and
  25 | ||| constructs the value, while `formatPart` projects text from an existing value.
  26 | export
  27 | record PatternRep state value where
  28 |   constructor MkPattern
  29 |   initialState : state
  30 |   finish : state -> Either PatternError value
  31 |   parsePart : PatternParser (Either PatternError (state -> state))
  32 |   formatPart : value -> String
  33 | 
  34 | ||| An opaque bidirectional textual representation of a value.
  35 | public export
  36 | Pattern : Type -> Type -> Type
  37 | Pattern = PatternRep
  38 | 
  39 | export
  40 | patternInitialState : Pattern state value -> state
  41 | patternInitialState = initialState
  42 | 
  43 | export
  44 | patternFinish : Pattern state value -> state -> Either PatternError value
  45 | patternFinish = finish
  46 | 
  47 | export
  48 | patternParsePart : Pattern state value ->
  49 |                    PatternParser (Either PatternError (state -> state))
  50 | patternParsePart = parsePart
  51 | 
  52 | export
  53 | patternFormatPart : Pattern state value -> value -> String
  54 | patternFormatPart = formatPart
  55 | 
  56 | ||| Literal text that can be appended to a pattern with `<%`.
  57 | export
  58 | record LiteralPatternRep where
  59 |   constructor MkLiteralPattern
  60 |   literalText : String
  61 | 
  62 | ||| Opaque literal text that can be appended to a pattern with `<%`.
  63 | public export
  64 | LiteralPattern : Type
  65 | LiteralPattern = LiteralPatternRep
  66 | 
  67 | public export
  68 | string : String -> LiteralPattern
  69 | string = MkLiteralPattern
  70 | 
  71 | public export
  72 | char : Char -> LiteralPattern
  73 | char value = MkLiteralPattern (pack [value])
  74 | 
  75 | export
  76 | literalField : Pattern state value -> String -> Pattern state value
  77 | literalField template text = MkPattern
  78 |   template.initialState
  79 |   template.finish
  80 |   (do
  81 |     ignore (Parser.string text)
  82 |     pure (Right id))
  83 |   (const text)
  84 | 
  85 | appendLiteral : Pattern state value -> LiteralPattern -> Pattern state value
  86 | appendLiteral pattern literal = MkPattern
  87 |   pattern.initialState
  88 |   pattern.finish
  89 |   (do
  90 |     result <- pattern.parsePart
  91 |     case result of
  92 |       Left error => pure (Left error)
  93 |       Right update => do
  94 |         ignore (Parser.string literal.literalText)
  95 |         pure (Right update))
  96 |   (\value => pattern.formatPart value ++ literal.literalText)
  97 | 
  98 | export infixl 7 <%
  99 | 
 100 | public export
 101 | (<%) : Pattern state value -> LiteralPattern -> Pattern state value
 102 | (<%) = appendLiteral
 103 | 
 104 | public export
 105 | Semigroup (Pattern state value) where
 106 |   left <+> right = MkPattern
 107 |     left.initialState
 108 |     left.finish
 109 |     (do
 110 |       resultLeft <- left.parsePart
 111 |       case resultLeft of
 112 |         Left error => pure (Left error)
 113 |         Right updateLeft => do
 114 |           resultRight <- right.parsePart
 115 |           pure (map (\updateRight => updateRight . updateLeft) resultRight))
 116 |     (\value => left.formatPart value ++ right.formatPart value)
 117 | 
 118 | pairUpdate : (leftState -> leftState) -> (rightState -> rightState) ->
 119 |              (leftState, rightState) -> (leftState, rightState)
 120 | pairUpdate updateLeft updateRight (leftState, rightState) =
 121 |   (updateLeft leftState, updateRight rightState)
 122 | 
 123 | export
 124 | pairPattern : (combined -> left) -> (combined -> right) ->
 125 |               (left -> right -> combined) ->
 126 |               Pattern leftState left -> Pattern rightState right ->
 127 |               Pattern (leftState, rightState) combined
 128 | pairPattern leftOf rightOf combine left right = MkPattern
 129 |   (left.initialState, right.initialState)
 130 |   (\(leftState, rightState) => do
 131 |     leftValue <- left.finish leftState
 132 |     rightValue <- right.finish rightState
 133 |     Right (combine leftValue rightValue))
 134 |   (do
 135 |     parsedLeft <- left.parsePart
 136 |     case parsedLeft of
 137 |       Left error => pure (Left error)
 138 |       Right updateLeft => do
 139 |         parsedRight <- right.parsePart
 140 |         pure (map (pairUpdate updateLeft) parsedRight))
 141 |   (\value => left.formatPart (leftOf value) ++ right.formatPart (rightOf value))
 142 | 
 143 | ||| Format a value using the supplied pattern.
 144 | public export
 145 | format : Pattern state value -> value -> String
 146 | format pattern = pattern.formatPart
 147 | 
 148 | structuralError : String -> Int -> String -> Either PatternError value
 149 | structuralError source position expected =
 150 |   if position >= strLength source
 151 |     then Left (UnexpectedEnd (cast position) expected)
 152 |     else case unpack (strSubstr position 1 source) of
 153 |       actual :: _ => Left (UnexpectedCharacter (cast position) expected actual)
 154 |       [] => Left (UnexpectedEnd (cast position) expected)
 155 | 
 156 | ||| Parse an entire string using an explicit initial field state.
 157 | |||
 158 | ||| This is useful for partial patterns whose omitted fields should come from
 159 | ||| caller policy rather than the pattern's built-in defaults.
 160 | public export
 161 | parseWith : Pattern state value -> state -> String -> Either PatternError value
 162 | parseWith pattern start source =
 163 |   let initial = Parser.S source 0 (strLength source)
 164 |   in case runIdentity (pattern.parsePart.runParser initial) of
 165 |         Parser.Fail position expected => structuralError source position expected
 166 |         Parser.OK result final => case result of
 167 |           Left error => Left error
 168 |           Right update => if final.pos == final.maxPos
 169 |             then pattern.finish (update start)
 170 |             else Left (TrailingInput (cast final.pos)
 171 |               (strSubstr final.pos (final.maxPos - final.pos) source))
 172 | 
 173 | ||| Parse an entire string using a pattern's default initial state.
 174 | public export
 175 | parse : Pattern state value -> String -> Either PatternError value
 176 | parse pattern = parseWith pattern pattern.initialState
 177 | 
 178 | patternDigitValue : Char -> Integer
 179 | patternDigitValue value = cast value - cast '0'
 180 | 
 181 | readUnsignedInteger : Integer -> Nat -> List Char ->
 182 |                       Maybe (Integer, Nat)
 183 | readUnsignedInteger found count (value :: remaining) =
 184 |   if isDigit value
 185 |     then readUnsignedInteger
 186 |       (found * 10 + patternDigitValue value) (S count) remaining
 187 |     else if count == 0 then Nothing else Just (found, count)
 188 | readUnsignedInteger found count [] =
 189 |   if count == 0 then Nothing else Just (found, count)
 190 | 
 191 | signedIntegerParser : PatternParser (Either PatternError (Integer -> Integer))
 192 | signedIntegerParser = Parser.P (\state =>
 193 |   let remaining = unpack
 194 |         (strSubstr state.pos (state.maxPos - state.pos) state.input)
 195 |       (negative, signWidth, digits) = case remaining of
 196 |         '-' :: rest => (True, 1, rest)
 197 |         rest => (False, 0, rest)
 198 |    in case readUnsignedInteger 0 0 digits of
 199 |         Nothing => pure (Parser.Fail state.pos "signed integer")
 200 |         Just (magnitude, digitWidth) =>
 201 |           let consumed = signWidth + digitWidth
 202 |               value = if negative then negate magnitude else magnitude
 203 |            in pure (Parser.OK (Right (const value))
 204 |                 ({ pos := state.pos + cast consumed } state)))
 205 | 
 206 | ||| An arbitrary-precision signed decimal integer. Formatting is canonical;
 207 | ||| parsing also accepts leading zeroes and negative zero.
 208 | public export
 209 | pSignedInteger : Pattern Integer Integer
 210 | pSignedInteger = MkPattern 0 Right signedIntegerParser show
 211 | 
 212 | decimalDigit : PatternParser Char
 213 | decimalDigit = Parser.satisfy (\value => value >= '0' && value <= '9')
 214 |   <?> "digit"
 215 | 
 216 | fixedDigits : Nat -> PatternParser (List Char)
 217 | fixedDigits Z = pure []
 218 | fixedDigits (S width) = [| decimalDigit :: fixedDigits width |]
 219 | 
 220 | upToDigits : Nat -> PatternParser (List Char)
 221 | upToDigits Z = pure []
 222 | upToDigits (S maximum) = do
 223 |   next <- Parser.optional decimalDigit
 224 |   case next of
 225 |     Nothing => pure []
 226 |     Just digit => map (digit ::) (upToDigits maximum)
 227 | 
 228 | variableDigits : Nat -> PatternParser (List Char)
 229 | variableDigits Z = Parser.fail "digit"
 230 | variableDigits (S maximum) = [| decimalDigit :: upToDigits maximum |]
 231 | 
 232 | currentPosition : PatternParser Int
 233 | currentPosition = Parser.P (\state => pure (Parser.OK state.pos state))
 234 | 
 235 | readDigits : List Char -> Integer
 236 | readDigits = foldl (\value, digit => value * 10 + cast digit - cast '0') 0
 237 | 
 238 | numberPart : (width : Nat) -> (maximumWidth : Nat) ->
 239 |              (minimum : Integer) -> (maximum : Integer) ->
 240 |              PatternParser (Either PatternError Integer)
 241 | numberPart width maximumWidth minimum maximum = do
 242 |   position <- currentPosition
 243 |   digits <- if width <= 1
 244 |     then variableDigits maximumWidth
 245 |     else fixedDigits width
 246 |   let value = readDigits digits
 247 |   pure (if value >= minimum && value <= maximum
 248 |     then Right value
 249 |     else Left (ValueOutOfRange (pack digits) minimum maximum (cast position)))
 250 | 
 251 | export
 252 | numberUpdatePart : (Integer -> state -> state) ->
 253 |                    (width : Nat) -> (maximumWidth : Nat) ->
 254 |                    (minimum : Integer) -> (maximum : Integer) ->
 255 |                    PatternParser (Either PatternError (state -> state))
 256 | numberUpdatePart setter width maximumWidth minimum maximum =
 257 |   map (map setter) (numberPart width maximumWidth minimum maximum)
 258 | 
 259 | caseInsensitive : String -> PatternParser ()
 260 | caseInsensitive value = consume (unpack value)
 261 |   where
 262 |     consume : List Char -> PatternParser ()
 263 |     consume [] = pure ()
 264 |     consume (expected :: rest) = do
 265 |       ignore (Parser.satisfy
 266 |         (\actual => Prelude.toLower actual == Prelude.toLower expected))
 267 |       consume rest
 268 | 
 269 | namedChoice : List (String, field) -> PatternParser field
 270 | namedChoice choices = choose (sortBy longerFirst (filter nonEmpty choices))
 271 |   where
 272 |     nonEmpty : (String, field) -> Bool
 273 |     nonEmpty (name, _) = name /= ""
 274 | 
 275 |     longerFirst : (String, field) -> (String, field) -> Ordering
 276 |     longerFirst (left, _) (right, _) =
 277 |       compare (length (unpack right)) (length (unpack left))
 278 | 
 279 |     choose : List (String, field) -> PatternParser field
 280 |     choose [] = Parser.fail "named field"
 281 |     choose ((name, value) :: rest) =
 282 |       (caseInsensitive name *> pure value) <|> choose rest
 283 | 
 284 | export
 285 | namedUpdatePart : List (String, field) -> (field -> state -> state) ->
 286 |                   PatternParser (Either PatternError (state -> state))
 287 | namedUpdatePart choices setter = map (Right . setter) (namedChoice choices)
 288 | 
 289 | export
 290 | namedConsumePart : List String ->
 291 |                    PatternParser (Either PatternError (state -> state))
 292 | namedConsumePart names = map (const (Right id))
 293 |   (namedChoice (map (\name => (name, ())) names))
 294 | 
 295 | export
 296 | spaceNumberUpdatePart : (Integer -> state -> state) ->
 297 |                         (maximumWidth : Nat) ->
 298 |                         (minimum : Integer) -> (maximum : Integer) ->
 299 |                         PatternParser (Either PatternError (state -> state))
 300 | spaceNumberUpdatePart setter maximumWidth minimum maximum = do
 301 |   ignore (Parser.optional (Parser.char ' '))
 302 |   map (map setter) (numberPart 1 maximumWidth minimum maximum)
 303 |